如何证明fin 1类型的元素必等于First 0？（禁用dependent destruction）

你定义的依赖归纳类型：

Inductive fin : nat -> Set :=
| First : forall n, fin (S n)
| Next : forall n, fin n -> fin (S n).

要证明的引理：

Lemma fin_1_first : forall (i : fin 1), i = First 0.

下面是几种不用dependent destruction的证明方法：

方法1：使用inversion策略 #

inversion是处理依赖类型归纳结构的常用策略，它会自动分析构造子的可能性，并生成必要的等式和矛盾假设：

Proof.
  intros i.
  inversion i.
  - reflexivity. (* 匹配到First 0的情况，直接得证 *)
  - discriminate. (* Next构造子会导出fin 0类型的元素，而fin 0是空类型，矛盾 *)
Qed.

方法2：手动构造递归证明项 #

直接利用fin类型的递归原理fin_rect编写证明项，完全不依赖策略：

Lemma fin_1_first : forall (i : fin 1), i = First 0.
Proof.
  exact (fun i => fin_rect
    (fun n _ => n = 1 -> i = First 0)
    (fun n H => match n return (S n = 1 -> First n = First 0) with
                | 0 => fun _ => eq_refl
                | S _ => fun _ => False_rect _
                end)
    (fun n f _ H => False_rect _)
    i eq_refl).
Qed.

方法3：destruct配合等式约束 #

先对i做解构，再用等式约束排除不可能的情况：

Proof.
  intros i.
  destruct i as [n | n f].
  - (* 情况1：i = First n，此时S n = 1，故n=0 *)
    assert (n = 0) by omega.
    rewrite H. reflexivity.
  - (* 情况2：i = Next n f，此时S n = 1即n=0，但f:fin 0无元素 *)
    assert (n = 0) by omega.
    rewrite H in f. inversion f.
Qed.

内容的提问来源于stack exchange，提问作者Wiktor