エラー：現在の環境でリファレンスfstが見つかりませんでした

Question

私はHoTTブック（et。al。）のタイプ導入/除外ルールを使ってdeMorgansの法則のいくつかの証明を行うことができるように小さなプログラムを作成しています。私のモデル/サンプルコードはすべてhttps://mdnahas.github.io/doc/Reading_HoTT_in_Coq.pdfです。これまでのところ私は、

Definition idmap {A:Type} (x:A) : A := x. 

Inductive prod (A B:Type) : Type := pair : A -> B -> @prod A B. 

Notation "x * y" := (prod x y) : type_scope. 

Notation "x , y" := (pair _ _ x y) (at level 10). 

Section projections. 
    Context {A : Type} {B : Type}. 
    Definition fst (p: A * B) := 
    match p with 
     | (x , y) => x 
    end. 

    Definition snd (p:A * B) := 
    match p with 
     | (x , y) => y 
    end. 
End projections. 

Inductive sum (A B : Type) : Type := 
    | inl : A -> sum A B 
    | inr : B -> sum A B. 

Arguments inl {A B} _ , [A] B _. 
Arguments inr {A B} _ , A [B]. 

Notation "x + y" := (sum x y) : type_scope. 

Inductive Empty_set:Set :=. 

Inductive unit:Set := tt:unit. 

Definition Empty := Empty_set. 
Definition Unit := unit. 

Definition not (A:Type) : Type := A -> Empty. 
Notation "~ x" := (not x) : type_scope. 

Variables X:Type. 
Variables Y:Type. 

Goal (X * Y) -> (not X + not Y). 
intro h. fst h. 

私は本当に問題が何かを知りません。私は定義を使っている人々の例を持っていますが、それらは常に "Compute"コマンドを含んでいます。そして、x：Xを得るためにルールfstをhに適用したいので役に立ちません。

「apply fst」を試しました。これは私に証明文脈では

Error: Cannot infer the implicit parameter B of fst whose type is 
"Type" in environment: 
h : A * B 

Answer 1

を得た、コックは戦術実行する、ない評価する式を取得する予定です。 fstが戦術として定義されていないので、それはError: The reference fst was not found in the current environment.

を与えるあなたがやろうとしているように見えるものの線に沿って実行するための一つの可能​​な戦術がset次のとおりです。

set (x := fst h). 

Answer 2

I want to apply the rule fst to h to get x:X

私はあなたと考えていますあなただけのapply fstを記述する場合、コックではなく、ゴールへfstルールを適用します

apply fst in h. 

を行うことができますhより。答えがfst hと書かれている場合、ダニエルは答えとして、fstの戦術を実行しようとしますが、それは存在しません。 fst hがそれに表示されます（これは、またはあなたが望むものであってもなくてもよい）場合、目標を変更しますダニエルのsetソリューションに加えて、次のようにも働く：

pose (fst h) as x. (* adds x := fst h to the context *) 
pose proof (fst h) as x. (* adds opaque x : X to the context, justified by the term fst h *) 
destruct h as [x y]. (* adds x : X and y : Y to the context, and replaces h with pair x y everywhere *)