case_eq相当于感应策略是什么？

Question

我想对归纳变量进行归纳，但我希望案例与case_eq一样在假设中。例如，如果我做induction n，在基本情况下，我想在我的假设中有n = 0。是否有一种策略可以为我做到这一点？

Answer 1

一般来说这有点痛苦，Software Foundations确实提供了一些策略来做到这一点，但最有启发性的是通过在归纳假设中加入相等来自己做：

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

请注意，这很痛苦，因为您需要构建正确的相等以使用归纳假设。

编辑：此解决方案适用于@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.

编辑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.