归纳类型的相等

Question

我如何证明以下微不足道的引理：

Require Import Vector.

Lemma t0_nil: forall A (x:t A 0), x = nil A.
Proof.
Qed.

FAQ 推荐 decide equality 和 discriminate 策略，但我找不到应用其中任何一个的方法。作为参考，这里是归纳定义：

Inductive t A : nat -> Type :=
  |nil : t A 0
  |cons : forall (h:A) (n:nat), t A n -> t A (S n).

Answer 1

您要做的是反转x。不幸的是，事实证明依赖类型假设的一般反转是不可判定的，请参阅 Adam Chlipala 的 CPDT。您可以手动在结构上进行模式匹配，例如与：

Lemma t0_nil: forall A (x:t A 0), x = nil A.
  intros.
  refine (match x with 
  | nil => _
  | cons _ _ _ => _
  end).
  - reflexivity.
  - exact @id.
Qed.

在许多情况下，您还可以使用 the tactic dep_destruct provided by CPDT 。在这种情况下，您的证明就变成了：

Require Import CpdtTactics.

Lemma t0_nil: forall A (x:t A 0), x = nil A.
  intros.
  dep_destruct x.
  reflexivity.
Qed.