错误:在当前环境中找不到引用fst。

Question

我正在编写一个小程序，这样我就可以使用deMorgans书(et )中的类型介绍/消除规则对HoTT定律进行一些证明。(A.)我的模型/示例代码都在这里，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.

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

我试过“申请fst”这让我

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

Answer 1

在证明上下文中，Coq希望得到执行的策略，而不是要评估的表达式。因为fst没有被定义为一种策略，所以它将给Error: The reference fst was not found in the current environment.

按照你似乎想要做的方式执行的一个可能的策略是set。

set (x := fst h).

Answer 2

我想把第f条规则应用到h上，得到x:X。

我相信你能做到

apply fst in h.

如果只编写apply fst，Coq将将fst规则应用于目标，而不是h。如果你写fst h，正如丹尼尔在他的回答中所说，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 *)