Converting an existance proof of an infinite series to a function that gives that infinite series

user_2872678 0
Viewed 53

I'm trying to reason on a TRS, and I have ran into the following proof obligation:

  infinite_sequence : forall t' : Term,
                      transitive_closure R t t' ->
                      exists t'' : Term, R t' t''
  ============================
   exists f : nat -> Term, forall n : nat, R (f n) (f (n + 1))

With transitive_closure defined as follows:

Definition transitive_closure (trs : TRS) (x y : Term) := 
    exists f: nat -> Term, 
            f 0 = x 
        /\ 
            exists l: nat, 
                    f l = y 
                /\ 
                    forall n: nat, 
                            n < l 
                        -> 
                            trs (f n) (f (n + 1))
.

So when I unfold:

  infinite_sequence : forall t' : Term,
                      (exists f : nat -> Term,
                         f 0 = t /\
                         (exists l : nat,
                            f l = t' /\
                            (forall n : nat, n < l -> R (f n) (f (n + 1))))) ->
                      exists t'' : Term, R t' t''
  ============================
   exists f : nat -> Term, forall n : nat, R (f n) (f (n + 1))

Is this proof obligation possible to fulfill? I am not married this exact definition of transitive_closure, so if it becomes much easier by choosing a different definition for that, I'm open to that.

coq
1 Answers

Since your goal starts with exists f : nat -> Term, you have to explicitly build such a function. The easiest way to do so is to first build a function with a slightly richer return type ({ u: Term | transitive_closure R t u } instead of Term) and then to project pointwise its first component to finish the proof. This would give the following script:

simple refine (let f : nat -> { u: Term | transitive_closure R t u } := _ in _).
- fix f 1.
  intros [|n].
  { exists t. exists (fun _ => t). admit. }
  destruct (f n) as [t' H].
  destruct (infinite_sequence t' H) as [t'' H']. (* ISSUE *)
  exists t''.
  destruct H as [f' [H1 [l [H2 H3]]]].
  exists (fun m => if Nat.ltb m l then f' m else t'').
  admit.
- exists (fun n => proj1_sig (f n)).
  intros n.
  rewrite Nat.add_1_r.
  simpl.
  destruct (f n) as [fn Hn].
  now destruct infinite_sequence as [t'' H'].

The two admit are just there to keep the code simple; there is nothing difficult about them. The real issue comes from the line destruct (infinite_sequence t' H), since Coq will complain that "Case analysis on sort Set is not allowed for inductive definition ex." Indeed, infinite_sequence states that there exists t'' such that R t' t'', but it does so in a non-informative way (i.e., in Prop), while you need it to build a function that lives in the concrete world (i.e., in Set).

There are only two axiom-free solutions, but both might be incompatible with the remaining of your development. The easiest one is to put infinite_sequence in Set, which means its type is changed to forall t', transitive_closure R t t' -> { t'' | R t' t'' }.

The second solution requires R to be a decidable relation and Term to be an enumerable set. That way, you can still build a concrete t'' by enumerating all the terms until you find one that satisfies R t' t''. In that case, infinite_sequence is only used to prove that this process terminates, so it can be non-informative.

user_134991210
Related