身份类型中的证明对象

Question

我正在阅读软件基金会，他们将平等定义为

Inductive eq {X:Type} : X -> X -> Prop :=
  | eq_refl : forall x, eq x x.

Notation "x == y" := (eq x y)
                       (at level 70, no associativity)
                     : type_scope.

我已经能够使用策略

证明equality__leibniz_equality

Lemma equality__leibniz_equality : forall (X : Type) (x y: X),
  x == y -> forall P:X->Prop, P x -> P y.
Proof.
  intros X x y H P evP. destruct H. apply evP.
Qed.

不过我也想构造证明对象。这是我试过的：

Definition equality__leibniz_equality' : forall (X : Type) (x y: X),
  x == y -> forall P:X->Prop, P x -> P y :=
  fun (X:Type) (x y: X) (H: x==y) (P:X->Prop) (evP: P x) =>
  match H with
  | eq_refl a => evP
  end.

虽然 destruct H 在我的第一个证明中起作用，因为该策略立即将 y 替换为 x，但是模式匹配 eq_refl a 似乎没有类似的效果，以至于 x=y=a 的信息好像丢失了，卡住了。有没有办法构造证明对象？

Answer 1

Definition equality__leibniz_equality' : forall (X : Type) (x y: X),
  x == y -> forall P:X->Prop, P x -> P y :=
  fun (X:Type) (x y: X) (H: x==y) (P:X->Prop) =>
  match H with
  | eq_refl a => fun evP => evP
  end.

使您的定义通过的 eq 更好的定义是：

Inductive eq {X:Type} (x : X) : X -> Prop :=
  | eq_refl : eq x x.

您可以使用Print查看任何标识符的定义。或者用 Defined 而不是 Qed 结束证明来计算它或在另一个证明中展开它。

Answer 2

看看Coq生成的消元原理，玩玩Check可能也很有趣。根据您的定义：

Check eq_ind.
(*
eq_ind
     : forall (X : Type) (P : X -> X -> Prop),
       (forall x : X, P x x) -> forall y y0 : X, eq y y0 -> P y y0
*) 

Check fun (X: Type)(Q: X -> Prop) =>
        eq_ind _ (fun x y  => Q x -> Q y) (fun x Hx => Hx). 

fun (X : Type) (Q : X -> Prop) =>
eq_ind X (fun x y : X => Q x -> Q y) (fun (x : X) (Hx : Q x) => Hx)
     : forall (X : Type) (Q : X -> Prop) (y y0 : X), eq y y0 -> Q y -> Q y0

你也可以通过询问 Logic.eq_ind 的类型来比较这个版本的 eq 和 Coq 的 Logic.eq（参见 Li-yao Xia 的回答）。另请注意，您的定义中没有 eq_rec 或 eq_rect（与 Logic.eq 形成对比）

身份类型中的证明对象

Proof objects in the identity type

coq