I am experimenting with Coq Coinductive types. I use the lazy list type form the Coq'Art book (sect. 13.1.4):
Set Implicit Arguments.
CoInductive LList (A:Set) : Set :=
| LNil : LList A
| LCons : A -> LList A -> LList A.
Implicit Arguments LNil [A].
CoFixpoint LAppend (A:Set) (u v:LList A) : LList A :=
match u with
| LNil => v
| LCons a u' => LCons a (LAppend u' v)
end.
In order to match the guard condition I also use the following decomposition functions form this book:
Definition LList_decomp (A:Set) (l:LList A) : LList A :=
match l with
| LNil => LNil
| LCons a l' => LCons a l'
end.
Lemma LList_decompose : forall (A:Set) (l:LList A), l = LList_decomp l.
Proof.
intros.
case l.
simpl.
reflexivity.
intros.
simpl.
reflexivity.
Qed.
The Lemma that LNil
is left-neutral is easy to prove:
Lemma LAppend_LNil : forall (A:Set) (v:LList A), LAppend LNil v = v.
Proof.
intros A v.
rewrite LList_decompose with (l:= LAppend LNil v).
case v.
simpl.
reflexivity.
intros.
simpl.
reflexivity.
Qed.
But I got stuck by proving that LNil
is also right-neutral:
Lemma LAppend_v_LNil : forall (A:Set) (v:LList A), LAppend v LNil = v.
After Arthur's answer, I tried with the new equality:
Lemma LAppend_v_LNil : forall (A:Set) (v:LList A), LListEq (LAppend v LNil) v.
Proof.
intros.
cofix.
destruct v.
rewrite LAppend_LNil.
apply LNilEq.
Here I'm stuck. Coq's answer is:
1 subgoal
A : Set
a : A
v : LList A
LAppend_v_LNil : LListEq (LAppend (LCons a v) LNil) (LCons a v)
______________________________________(1/1)
LListEq (LAppend (LCons a v) LNil) (LCons a v)
After Eponier's answer I want to give it the final touch by introducing an Extensionality Axiom:
Axiom LList_ext: forall (A:Set)(l1 l2: LList A), (LListEq l1 l2 ) -> l1 = l2.
With that axiom I get the final cut of the Lemma:
Lemma LAppend_v_LNil : forall (A:Set) (v:LList A), (LAppend v LNil) = v.
Proof.
intros.
apply LList_ext.
revert v.
cofix.
intros.
destruct v. Guarded. (* now we can safely destruct v *)
- rewrite LAppend_LNil.
constructor.
- rewrite (LList_decompose (LAppend _ _)).
simpl. constructor. apply LAppend_v_LNil.
Qed.
Now, here are my final questions for this thread:
- Does such an axiom already exist in some Coq library?
- Is that axiom consistent with Coq?
- With what standard axioms of Coq (e.g. classic, UIP, fun ext, Streicher K) is that axiom inconsistent?
A simple rule is to use
cofix
as soon as possible in your proofs.Actually, in your proof of
LAppend_v_LNil
, the guarded condition is already violated atdestruct v
. You can check this fact using the commandGuarded
, which helps testing before the end of the proof if all the uses of coinduction hypotheses are legit.You should actually swap
intros
andcofix
. From there, the proof is not difficult.EDIT: here is the complete solution.
You guessed it right: just like for functions, Coq's generic notion of equality is too weak to be useful for most coinductive types. If you want to prove your result, you need to replace
eq
by a coinductive notion of equality for lists; for instance:Manipulating infinite objects is a vast topic in Coq. If you want to learn more, Adam Chlipala's CPDT has an entire chapter on coinduction.