равенства индуктивных типов

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. К сожалению, оказывается, что общая инверсия зависимых типовых гипотез неразрешима, см. 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.