平等感性類型

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.