代码之家 › 专栏 › 技术社区 › Fernando Chu

身份类型中的证明对象

coq

Fernando Chu · 技术社区 · 4 年前

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

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 迷路了,我被卡住了。有没有办法构造证明对象?

0 回复 | 直到 4 年前

Li-yao Xia 4 年前

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 用它来计算或在另一个证明中展开它。

Pierre Castéran 4 年前

看看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 与Coq Logic.eq (参见李耀霞的回答)通过询问的类型 Logic.eq_ind 。请注意,也没有 eq_rec 也没有 eq_rect 与您的定义(与 Logic.eq )

renjie sun 2 年前

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.

推荐文章

Mei Zhang · 定义“依赖类型”模函子

8 年前

Jason Hu · 参见Ltac中的Hintbase

8 年前

lllllllllllll · 通过两个实现对阶乘程序进行Coq验证

8 年前

MikkelBybjerg · 如何延迟lambda评估,以便替换lambda

8 年前

user9335697 · 实例化参数以评估函数定义

8 年前

Jian Wang · Coq中的背景目标、搁置目标和放弃目标是什么?

8 年前

Pablo Inostroza · 有没有可能表达一个定理,说明应用了哪些构造函数?

8 年前

jmite · Coq:在校样脚本编写期间查看校样术语

8 年前

ConfusedFormalizer · a是怎样的。vo文件的结构是否便于coqchk使用?

8 年前

Siddharth Bhat · 查看所有已安装的库以及如何在Coq中导入它们

8 年前