Что является case_eq эквивалентом тактики индукции? - PullRequest
Новая
       9

Что является case_eq эквивалентом тактики индукции?

0 голосов
/ 14 апреля 2019

Я хочу сделать индукцию по индуктивной переменной, но я хочу, чтобы дело было в гипотезе, как это было бы с case_eq. Например, если бы я сделал induction n, в базовом случае я бы хотел иметь n = 0 в своих гипотезах. Есть ли тактика, которая может сделать это для меня?

1 Ответ

0 голосов
/ 14 апреля 2019

Как правило, это немного больно, Основы программного обеспечения предоставляет некоторые тактики для этого, но наиболее поучительным является сделать это самостоятельно, добавив равенство к гипотезе индукции: 

Lemma foo P (n : nat) : P n.
Proof.
generalize (eq_refl n); generalize n at 1.
induction n.

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

edit : Это решение работает в примере, указанном @yves: 

Require Import List.
Import ListNotations.

Section EqList.

Variables (A : Type) (eqb : A -> A -> bool).
Variables (eqbP : forall a1 a2, eqb a1 a2 = true <-> a1 = a2).
Implicit Types (l : list A).

Fixpoint eqb_list l1 l2 {struct l1} : bool :=
  match l1,l2 with
  | [], [] => false
  | (x1::l1), (x2::l2) => eqb x1 x2 && eqb_list l1 l2
  | _,_ => false
  end.

Lemma eqb_list_true_iff_left_to_right l1 l2 :
  eqb_list l1 l2 = true -> l1 = l2.
Proof.
revert l2; generalize (eq_refl l1); generalize l1 at 1.
induction l1 as [|x1 l1 IHl1]; intros l1'.
- now destruct l1'; destruct l2; auto.
- destruct l1' as [|x1' l1']; [congruence|intros hl].
  destruct l2 as [|x2 l2]; [simpl; congruence|]; simpl; intros heq.
  pose proof (andb_prop _ _ heq) as [h1 h2].
  pose proof (eqbP x1 x2) as [rl rr].
  rewrite rl; auto.
  pose proof (IHl1 l1 (eq_refl _) l2 h2).
  now rewrite H.
Qed.

edit 2 : я должен был сделать доказательство на языке, с которым я более знаком: 

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section EqList.

Variables (A : eqType).
Implicit Types (l : seq A).

Fixpoint eqb_list l1 l2 {struct l1} : bool :=
  match l1,l2 with
  | [::], [::] => false
  | (x1::l1), (x2::l2) => [&& x1 == x2 & eqb_list l1 l2]
  | _, _ => false
  end.

Lemma eqb_list_true_iff_left_to_right l1 l2 :
  eqb_list l1 l2 = true -> l1 = l2.
Proof.
move E: l1 l2 => l1'; elim: l1' l1 E => [|x1 l1 ihl1] [|? ?] // ? [|x2 l2] //=.
by case/andP=> /eqP-> /(ihl1 l1 erefl)->.
Qed.
...