Абстрактные структуры в правиле индукции для индуктивных предикатов для Coq - PullRequest
Новая
       3

Абстрактные структуры в правиле индукции для индуктивных предикатов для Coq

1 голос
/ 02 февраля 2020

Рассмотрим следующее предложение в Coq: 

Inductive subseq : list nat -> list nat -> Prop :=
 | nil_s : forall (l: list nat), subseq nil l 
 | cons_in l1 l2 x (H: subseq l1 l2) : subseq (x :: l1) (x :: l2)
 | cons_nin l1 l2 x (H: subseq l1 l2) : subseq l1 (x :: l2)
.

Lemma subseq_remove_rewritten: forall (x:nat) (l1' l1 l2 : list nat),
  subseq l1' l2 ->
  l1' = (x :: l1) ->
  subseq l1 l2.
Proof. 
  intros x l1' l1 l2 H1 H2.
  induction H1.
  - discriminate.
  - injection H2 as H3 H4.
    rewrite H4 in H1.
    apply cons_nin. apply H1.
  - apply IHsubseq in H2.
    apply cons_nin. apply H2.
Qed.

Lemma subseq_remove: forall (x:nat) (l1 l2 : list nat),
  subseq (x :: l1) l2 ->
  subseq l1 l2.
Proof. 
  intros x l1 l2 H. 
  apply subseq_remove_rewritten with (x:=x) (l1':=x :: l1).
  apply H.
  reflexivity.
Qed.

Я работал в Изабель до Coq. Первоначально индуктивные тактики c не могли напрямую решить эту задачу, и хитрость заключалась в том, чтобы придумать лемму, подобную subseq_remove_rewritten, а затем доказать исходную цель. Это ситуация в руководстве Изабель / HOL: помощник по проверке логики высшего порядка c. Позже, tacti c стал умнее, и можно писать шаблоны, в которых можно абстрагироваться. Итак, доказательство написано так: 

lemma 
  assumes "subseq (x # l1) l2"
  shows "subseq l1 l2"
  using assms
  apply(induction "x # l1" "l2" rule: subseq.induct)
    apply simp
   apply(intro subseq.intros(3),simp)
  by (intro subseq.intros(3))

Мне было интересно, есть ли у Coq похожий способ избежать доказательства леммы типа subseq_remove_rewritten и go непосредственно для доказательства subseq_remove.

1 Ответ

1 голос
/ 02 февраля 2020

Вы можете использовать dependent induction tacti c (задокументировано здесь ). Например: 

Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.Program.Equality. (* Needed to use the tactic *)

Inductive subseq : list nat -> list nat -> Prop :=
 | nil_s : forall (l: list nat), subseq nil l
 | cons_in l1 l2 x (H: subseq l1 l2) : subseq (x :: l1) (x :: l2)
 | cons_nin l1 l2 x (H: subseq l1 l2) : subseq l1 (x :: l2)
.

Lemma subseq_remove: forall (x:nat) (l1 l2 : list nat),
  subseq (x :: l1) l2 ->
  subseq l1 l2.
Proof.
  intros x l1 l2 H.
  dependent induction H generalizing x.
  - now apply cons_nin.
  - eauto using cons_nin.
Qed.

К сожалению, хотя эта тактика c существует уже некоторое время, в справочном руководстве она все еще описывается как экспериментальная, и я не знаю, есть ли у разработчиков Coq какие-либо планы по его улучшению в будущем. У этого есть несколько недостатков, таких как не позволение пользователю называть переменные и гипотезы, используемые в доказательстве индукции. Лично я предпочитаю добавить предположения о равенстве к доказательству самостоятельно, как в вашей первой попытке, или переформулировать определение subseq как Fixpoint, чтобы вы могли перевернуть гипотезу путем упрощения. Например: 

Require Import Coq.Lists.List.
Import ListNotations.

Fixpoint subseq (l1 l2 : list nat) : Prop :=
  match l1, l2 with
  | [], _ => True
  | x1 :: l1, [] => False
  | x1 :: l1, x2 :: l2 => x1 = x2 /\ subseq l1 l2 \/ subseq (x1 :: l1) l2
  end.

Lemma subseq_nin x2 l1 l2 : subseq l1 l2 -> subseq l1 (x2 :: l2).
Proof. destruct l1 as [|x1 l1]; simpl; eauto. Qed.

Lemma subseq_remove: forall (x:nat) (l1 l2 : list nat),
  subseq (x :: l1) l2 ->
  subseq l1 l2.
Proof.
  intros x l1 l2 H.
  induction l2 as [|x2 l2 IH]; try easy.
  destruct H as [[<- H]|H]; eauto using subseq_nin.
Qed.
...