coq - 归纳类型的相等

Question

我如何证明以下琐碎的引理：

Require Import Vector.

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

常见问题解答建议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.

在许多情况下，您还可以使用CPDT 提供的策略dep_destruct。在这种情况下，您的证明就变成了：

Require Import CpdtTactics.

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