Proving equality on coinductive lazy lists in Coq

问题:

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?

回答1:

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 at destruct v. You can check this fact using the command Guarded, which helps testing before the end of the proof if all the uses of coinduction hypotheses are legit.

Lemma LAppend_v_LNil : forall (A:Set) (v:LList A), LListEq  (LAppend v LNil)  v.
  intros.
  cofix.
  destruct v. Fail Guarded.
Abort.

You should actually swap intros and cofix. From there, the proof is not difficult.

EDIT: here is the complete solution.

Lemma LAppend_v_LNil : forall (A:Set) (v:LList A), LListEq (LAppend v LNil)  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.

回答2:

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:

CoInductive LListEq (A:Set) : LList A -> LList A -> Prop :=
| LNilEq : LListEq A LNil LNil
| LConsEq x lst1 lst2 : LListEq A lst1 lst2 -> 
  LListEq A (LCons x lst1) (LCons x lst2).

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.