Можно ли форсировать тактику индукции, чтобы получить больше уравнений? - PullRequest
Новая
       6

Можно ли форсировать тактику индукции, чтобы получить больше уравнений?

0 голосов
/ 25 августа 2018

Я играю с индуктивными предложениями. У меня есть следующее индуктивное определение: 

Inductive subseq {X : Type} : list X -> list X -> Prop :=
| empty_subseq : subseq [ ] [ ]
| subseq_left_elim : forall (l1 l2 : list X) (x : X),
              subseq (x :: l1) l2 -> subseq l1 l2
| subseq_intro : forall (l1 l2 : list X) (x : X),
              subseq l1 l2 -> subseq (x :: l1) (x :: l2).

Notation "l <<< k" := (subseq l k) (at level 10).

И я пытаюсь доказать такую ​​лемму: 

Lemma subseq_right_elim : forall (X : Type) (l1 l2 : list X) (x y : X),  
  (x :: l1) <<< (y :: l2) -> x = y \/ (x :: l1) <<< l2.
Proof.
  intros X l1 l2 x y H.
  induction H as [| l1' l2' z E IH | l1' l2' z E IH ].
  + right. apply empty_subseq_l. 
    (* empty_subseq_l : forall (X : Type) (l : list X), [ ] <<< l. *)
  + destruct IH as [IH | IH].
    * left. apply IH.
    * right. apply subseq_left_elim with z.
      apply IH.
  + (* stuck *)
Abort.

Понятия не имею, как доказать дело subseq_intro. Кажется, это правда, потому что, неофициально, если subseq_intro был применен для получения (x :: l1) <<< (y :: l2), то x и y должны быть равны, и это просто влечет за собой цель. Но Coq не дает таких утверждений в третьем случае. Как заставить это сделать это, как если бы применялась тактика инверсии?

1 Ответ

0 голосов
/ 25 августа 2018

Как получить решение для исходной задачи

Вы можете использовать тактику remember, потому что induction (и destruct) "забывает" точную форму индексы .А в типе arg1 <<< arg2 оба arg1 и arg2 являются индексами.Кстати, в этом блоге Джеймса Уилкокса подробно объясняется, как это работает.В любом случае, если вы хотите сделать индукцию для семейства индуктивных типов, вы часто хотите, чтобы индексы были переменными (с дополнительными уравнениями, хранящими всю необходимую информацию).

Итак, если вы начнете так: 

remember (x :: l1) as xl1 eqn: E1.
remember (y :: l2) as xl2 eqn: E2.

Вы получите свои уравнения, но в конечном итоге у вас возникнут проблемы, потому что гипотезы индукции не будут использоваться.Чтобы сделать их пригодными для использования, просто обобщите гипотезы индукции, выполнив 

revert x y l1 l2 E1 E2.

Более явно, вы начинаете так: 

Lemma subseq_right_elim (X : Type) (l1 l2 : list X) (x y : X) :
  (x :: l1) <<< (y :: l2) -> (x = y) \/ (x :: l1) <<< l2.
Proof.
  intros H.
  remember (x :: l1) as xl1 eqn: E1; remember (y :: l2) as xl2 eqn: E2.
  revert x y l1 l2 E1 E2.
  induction H as [| l1' l2' z S IH | l1' l2' z S IH ]; intros x y l1 l2 E1 E2.

Для чего стоит утверждение вашей леммы не является общимдостаточно, чтобы индукция не помогла - на этот раз вы сможете решить третью подцель, но не вторую.Чтобы преодолеть эту трудность, сделайте утверждение леммы более похожим на subseq_left_elim.

ПРЕДУПРЕЖДЕНИЕ СПОЙЛЕРА : этот гист имеет полное доказательство.

A лучшеспособ переопределить индуктивный предикат

Теперь трудности, с которыми вы сталкиваетесь, связаны с окольным путем определения понятия субпоследовательности.Вы можете увидеть это более ясно из доказательства очень простого примера: 

Goal [1; 3; 5] <<< [0; 1; 2; 3; 4; 5; 6].
Proof.
apply subseq_left_elim with 0. apply subseq_intro.
apply subseq_intro.
apply subseq_left_elim with 2. apply subseq_intro.
apply subseq_intro.
apply subseq_left_elim with 4. apply subseq_intro.
apply subseq_intro.
apply subseq_left_elim with 6. apply subseq_intro.
apply empty_subseq.
Qed.

По сути, вам нужно увеличить размер вашей цели, чтобы уменьшить ее позже.

Если бы вы выбралиболее простое кодирование, например 

Reserved Notation "l <<< k" (at level 10).
Inductive subseq {X : Type} : list X -> list X -> Prop :=
| empty_subseq : [ ] <<< [ ]
| subseq_drop_right l1 l2 x : l1 <<< l2 ->       l1  <<< (x :: l2)
| subseq_drop_both l1 l2 x  : l1 <<< l2 -> (x :: l1) <<< (x :: l2)
where "l <<< k" := (subseq l k).

ваша жизнь была бы намного проще!Например, вот новое доказательство вышеупомянутого простого факта: 

Goal [1; 3; 5] <<< [0; 1; 2; 3; 4; 5; 6].
apply subseq_drop_right.
apply subseq_drop_both.
apply subseq_drop_right.
apply subseq_drop_both.
apply subseq_drop_right.
apply subseq_drop_both.
apply subseq_drop_right.
apply empty_subseq.
Qed.

На этот раз вы просто уменьшаете цель с каждым вашим шагом.

...