错误：在当前环境中找不到参考fst

我正在编写一个小程序，以便我可以使用HoTT书（等）中的类型导入/消除规则来对deMorgans定律进行一些证明。我的模型/示例代码都在这里，https://mdnahas.github.io/doc/Reading_HoTT_in_Coq.pdf。到目前为止，我有，错误：在当前环境中找不到参考fst

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.

现在我真的不知道问题是什么。我有人使用定义的例子，但他们总是涉及“计算”命令，我想将规则fst应用到h以获得x：X，所以它们没有帮助。

我试过“apply fst”。这让我

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

来源

2017-10-08 bkbowser

在证据方面，勒柯克期望得到战术执行，不表达来评价。由于fst没有被定义为一种战术，它会给Error: The reference fst was not found in the current environment.

一个可能的策略，以沿线的执行你仿佛是试图做的是set：

set (x := fst h).

来源

2017-10-08 20:59:53

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

我相信你可以做

apply fst in h.

如果你只写apply fst，勒柯克将应用fst规则的目标，而比到h。如果你写下fst h，正如Daniel在他的回答中所说的那样，Coq将尝试运行不存在的fst策略。除了丹尼尔的set解决办法，如果fst h出现在它（这可能是也可能不是你想要的），这将改变目标，下面还工作：

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 *)

来源

2017-10-08 22:11:53

错误：在当前环境中找不到参考fst

回答

相关问题