平等感性类型

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.