coq - 错误 : The reference fst was not found in the current environment

Question

我正在编写一个小程序，以便我可以使用 HoTT 书籍(等)中的类型引入/消除规则来证明 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.

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

我试过“先申请”。这让我着迷

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