身份类型中的证明对象

Question

我正在阅读software foundation他们将等式定义为

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在我的第一个证明中起作用，因为该策略立即用x代替了y，但是模式匹配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(参见夏丽瑶的回答)。还请注意，在您的定义中没有eq_rec或eq_rect(与Logic.eq形成对比)