在Coq中证明共导惰性列表的相等性 [英] Proving equality on coinductive lazy lists in Coq

问题描述

我正在尝试Coq归纳类型.我使用Coq'Art书(第13.1.4节)中的惰性列表类型:

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.

LNil左中性的引理很容易证明:

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.

但是我被证明LNil也是中立的而被困住了:

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.

在这里我被卡住了. Coq的答案是:

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)

在Eponier回答之后，我想通过引入扩展性公理给它做最后的润饰:

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:

• 这样的公理在某些Coq库中已经存在吗?
• 公理与Coq一致吗?
• 该公理与Coq有哪些标准公理(例如经典，UIP，趣味扩展，Streicher K)不一致?

推荐答案

一个简单的规则是在证明中尽快使用cofix.

A simple rule is to use cofix as soon as possible in your proofs.

实际上，在您的LAppend_v_LNil证明中，destruct v处的保护条件已经违反.您可以使用命令Guarded来检查这一事实，该命令有助于在证明结束之前进行测试，如果所有共归假设的使用都是合法的.

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.

您实际上应该交换intros和cofix.从那里开始，证明并不困难.

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

这是完整的解决方案.

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.

这篇关于在Coq中证明共导惰性列表的相等性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！