证明身份类型中的对象

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

您还可以通过询问

eq

的类型来比较这个版本的

Logic.eq

与 Coq 的

Logic.eq_ind

（参见 Li-yao Xia 的回答）。另请注意，您的定义中没有

eq_rec

也没有

eq_rect

（与

Logic.eq

相反）

Answer 3

Definition equality__leibniz_equality'' (X : Type) (x y: X) (H : x == y) (P : X -> Prop)
  : P x -> P y :=
    match H with
    | eq_refl x0 => id
    end.
                                            
Lemma equality__leibniz_equality''' : forall (X : Type) (x y: X),
    x == y -> forall P:X -> Prop, P x -> P y.
Proof.
  exact equality__leibniz_equality''.
Qed.