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

Я экспериментирую с типами Coq Coinductive. Я использую ленивый тип списка из книги 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.

Здесь я застрял. Кок ответ:

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)

После ответа Эпонье я хочу дать ему последний штрих, введя аксиому экстенсиональности:

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) эта аксиома несовместима?
Источник

2 ответа

Решение

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

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

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

Вы должны на самом деле поменяться intros а также cofix, Оттуда доказательство не сложно.

РЕДАКТИРОВАТЬ: вот полное решение.

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

Источник
Другие вопросы по тегам