身份类型中的证明对象答案

【问题标题】：Proof objects in the identity type身份类型中的证明对象
【发布时间】：2022-05-06 14:57:14
【问题描述】：

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

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 的信息似乎是迷路了，我被卡住了。有没有办法构造证明对象？

【问题讨论】：

标签： coq

【解决方案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 以使用它进行计算或在另一个证明中展开它。

【讨论】：

【解决方案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（参见夏立耀的回答）。另请注意，您的定义中没有eq_rec 或eq_rect（与Logic.eq 相比）

【讨论】：