coq - 在 Coq 中证明共归纳惰性列表上的相等性

Question

我正在尝试 Coq 共感类型。我使用 Coq'Art 书中的惰性列表类型(第 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.

为了匹配保护条件，我还使用了本书中的以下分解函数:

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 是左中性的引理很容易证明:

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 也是右中性时陷入了困境:

Lemma LAppend_v_LNil : forall (A:Set) (v:LList A), LAppend v LNil = v.

在亚瑟回答之后，我尝试了新的等式:

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 的答案是:

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 的回答之后，我想通过引入外延性公理来对其进行最后的修饰:

Axiom LList_ext: forall (A:Set)(l1 l2: LList A), (LListEq l1 l2 ) -> l1 = l2.

有了这个公理，我得到了引理的最终剪切:

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.

现在，这是我对此主题的最后一个问题:

• 某些 Coq 库中是否已经存在这样的公理？
• 该公理与 Coq 一致吗？
• 该公理与 Coq 的哪些标准公理(例如 classic、UIP、fun ext、Streicher K)不一致？

Answer 1

您猜对了:就像函数一样，Coq 的通用相等概念太弱，无法用于大多数共归纳类型。如果你想证明你的结果，你需要将 eq 替换为列表的共归纳相等概念；例如:

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).

操作无限对象是 Coq 中的一个广泛主题。如果您想了解更多信息，Adam Chlipala 的 CPDT 有完整的 chapter关于共感应。