I'm trying to prove the first example in "Practical Coinduction" in Coq. The first example is to prove that lexicographical ordering on infinite streams of integers is transitive.
I haven't been able to formulate the proof to get around the Guardedness condition
Here is my development so far. First just the usual definition of infinite streams. Then definition of lexicographical order called lex. And in the end the failed proof of the transitivity theorem.
Require Import Omega.
Section stream.
Variable A:Set.
CoInductive Stream : Set :=
| Cons : A -> Stream -> Stream.
Definition head (s : Stream) :=
match s with Cons a s' => a end.
Definition tail (s : Stream) :=
match s with Cons a s' => s' end.
Lemma cons_ht: forall s, Cons (head s) (tail s) = s.
intros. destruct s. reflexivity. Qed.
End stream.
Implicit Arguments Cons [A].
Implicit Arguments head [A].
Implicit Arguments tail [A].
Implicit Arguments cons_ht [A].
CoInductive lex s1 s2 : Prop :=
is_le : head s1 <= head s2 ->
(head s1 = head s2 -> lex (tail s1) (tail s2)) ->
lex s1 s2.
Lemma lex_helper: forall s1 s2,
head s1 = head s2 ->
lex (Cons (head s1) (tail s1)) (Cons (head s2) (tail s2)) ->
lex (tail s1) (tail s2).
Proof. intros; inversion H0; auto. Qed.
Here is the lemma I want to prove. I start by preparing the goal so I can apply a constructor, hoping to eventually be able to use the "hypothesis" from cofix.
Lemma lex_lemma : forall s1 s2 s3, lex s1 s2 -> lex s2 s3 -> lex s1 s3.
intros s1 s2 s3 lex12 lex23.
cofix.
rewrite <- (cons_ht s1).
rewrite <- (cons_ht s3).
assert (head s1 <= head s3) by (inversion lex12; inversion lex23; omega).
apply is_le; auto.
simpl; intros. inversion lex12; inversion lex23.
assert (head s2 = head s1) by omega.
rewrite <- H0, H5 in *.
assert (lex (tail s1) (tail s2)) by (auto).
assert (lex (tail s2) (tail s3)) by (auto).
apply lex_helper.
auto.
repeat rewrite cons_ht.
Guarded.
How do I proceed from here? Thanks for any hints!
Thanks to Arthur's (as always!) helpful and enlightening answer I too could complete the proof. I give my version below for reference.
Lemma lex_lemma : forall s1 s2 s3, lex s1 s2 -> lex s2 s3 -> lex s1 s3.
cofix.
intros s1 s2 s3 lex12 lex23.
inversion lex12; inversion lex23.
rewrite <- (cons_ht s1).
rewrite <- (cons_ht s3).
constructor; simpl.
inversion lex12; inversion lex23; omega.
intros; eapply lex_lemma; [apply H0 | apply H2]; omega.
Qed.
I use the cons_ht lemma to "expand" the value of s1 and s3. The definition of lex here (with head and tail) is more close to the verbatim formulation in Practical Coinduction. Arthur uses a more elegant technique which makes Coq expand the values automatically - much nicer!
One problem with your proof is that you made the call to cofix too late, after s1 s2 s3 had been introduced. As a consequence, the coinductive hypothesis that you get, lex s1 s2, is not very useful: in order to apply it while staying guarded, as you mentioned, we need to do it after having applied the constructor of lex. However, after doing that, we would need to show at some point that lex (tail s1) (tail s3) holds, where the hypothesis introduced by cofix can't do any good.
In order to solve this problem, we need to perform the call to cofix before introducing the variables, so that the hypothesis it produces is sufficiently general. I took the liberty of reformulating your definition of lex, so that it becomes easier to manipulate in such a proof:
CoInductive lex : Stream nat -> Stream nat -> Prop :=
| le_head n1 n2 s1 s2 : n1 < n2 -> lex (Cons n1 s1) (Cons n2 s2)
| le_tail n s1 s2 : lex s1 s2 -> lex (Cons n s1) (Cons n s2).
Lemma lex_trans : forall s1 s2 s3, lex s1 s2 -> lex s2 s3 -> lex s1 s3.
Proof.
cofix.
intros s1 s2 s3 lex12 lex23.
inversion lex12; subst; clear lex12;
inversion lex23; subst; clear lex23;
try (apply le_head; omega).
apply le_tail; eauto.
Qed.
Now, the hypothesis has the form
forall s1 s2 s3, lex s1 s2 -> lex s2 s3 -> lex s1 s3
which can easily be applied to the tail of our streams, as long as the resulting application is guarded.