Доказательство равенства на коиндуктивных ленивых списках в Coq

Question

Я экспериментирую с Coq Coinductive типами 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:

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 (например, классическими, UIP, fun ext, Streicher K) является то, что аксиома непоследовательна?

Answer 1

Простым правилом является использование cofix как можно скорее в ваших доказательствах.

Фактически, в вашем доказательстве LAppend_v_LNil охранное состояние уже нарушено на destruct v. Вы можете проверить этот факт, используя команду Guarded, которая помогает тестировать до конца доказательства, если все применения гипотез о coinduction являются законными.

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

Вы должны фактически поменять intros и cofix. Оттуда это не сложно.

EDIT: вот полное решение.

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. 

Answer 2

Вы догадались, что это правильно: точно так же, как и для функций, общее понятие равенства 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. Если вы хотите узнать больше, CPDT Адама Хлипалы имеет целое число chapter на монументации.