gpt4 book ai didi

module - 从注入(inject) `nat` 中获取类型的可判定总顺序

转载 作者:行者123 更新时间:2023-12-04 14:39:18 25 4
gpt4 key购买 nike

由于自然数支持可判定的全序,注入(inject) nat_of_ascii (a : ascii) : nat 在类型 ascii 上产生一个可判定的总顺序.在 Coq 中表达这一点的简洁、惯用的方式是什么? (有或没有类型类、模块等)

最佳答案

这样的过程是相当常规的,将取决于您选择的库。对于order.v ,基于 math-comp,这个过程完全是机械的 [事实上,我们将在后面的帖子中为总订单注入(inject)的类型开发一个通用构造]:

From Coq Require Import Ascii String ssreflect ssrfun ssrbool.
From mathcomp Require Import eqtype choice ssrnat.
Require Import order.

Import Order.Syntax.
Import Order.Theory.

Lemma ascii_of_natK : cancel nat_of_ascii ascii_of_nat.
Proof. exact: ascii_nat_embedding. Qed.

(* Declares ascii to be a member of the eq class *)
Definition ascii_eqMixin := CanEqMixin ascii_of_natK.
Canonical ascii_eqType := EqType _ ascii_eqMixin.

(* Declares ascii to be a member of the choice class *)
Definition ascii_choiceMixin := CanChoiceMixin ascii_of_natK.
Canonical ascii_choiceType := ChoiceType _ ascii_choiceMixin.

(* Specific stuff for the order library *)
Definition ascii_display : unit. Proof. exact: tt. Qed.

Open Scope order_scope.

(* We use the order from nat *)
Definition lea x y := nat_of_ascii x <= nat_of_ascii y.
Definition lta x y := ~~ (lea y x).

Lemma lea_ltNeq x y : lta x y = (x != y) && (lea x y).
Proof.
rewrite /lta /lea leNgt negbK lt_neqAle.
by rewrite (inj_eq (can_inj ascii_of_natK)).
Qed.
Lemma lea_refl : reflexive lea.
Proof. by move=> x; apply: le_refl. Qed.
Lemma lea_trans : transitive lea.
Proof. by move=> x y z; apply: le_trans. Qed.
Lemma lea_anti : antisymmetric lea.
Proof. by move=> x y /le_anti /(can_inj ascii_of_natK). Qed.
Lemma lea_total : total lea.
Proof. by move=> x y; apply: le_total. Qed.

(* We can now declare ascii to belong to the order class. We must declare its
subclasses first. *)
Definition asciiPOrderMixin :=
POrderMixin lea_ltNeq lea_refl lea_anti lea_trans.

Canonical asciiPOrderType := POrderType ascii_display ascii asciiPOrderMixin.

Definition asciiLatticeMixin := Order.TotalLattice.Mixin lea_total.
Canonical asciiLatticeType := LatticeType ascii asciiLatticeMixin.
Canonical asciiOrderType := OrderType ascii lea_total.

请注意,为 ascii 提供订单实例使我们可以访问总订单的大理论,加上运算符等......,但是总本身的定义相当简单:
"<= is total" == x <= y || y <= x

其中 <= 是一个“可判定的关系”,我们当然假设特定类型的相等性的可判定性。具体来说,对于任意关系:
Definition total (T: Type) (r : T -> T -> bool) := forall x y, r x y || r y x.

所以如果 T is and order, 满足 total ,你完成了。

更一般地说,您可以定义一个通用原则来使用注入(inject)构建此类类型:
Section InjOrder.

Context {display : unit}.
Local Notation orderType := (orderType display).
Variable (T : orderType) (U : eqType) (f : U -> T) (f_inj : injective f).

Open Scope order_scope.

Let le x y := f x <= f y.
Let lt x y := ~~ (f y <= f x).
Lemma CO_le_ltNeq x y: lt x y = (x != y) && (le x y).
Proof. by rewrite /lt /le leNgt negbK lt_neqAle (inj_eq f_inj). Qed.
Lemma CO_le_refl : reflexive le. Proof. by move=> x; apply: le_refl. Qed.
Lemma CO_le_trans : transitive le. Proof. by move=> x y z; apply: le_trans. Qed.
Lemma CO_le_anti : antisymmetric le. Proof. by move=> x y /le_anti /f_inj. Qed.

Definition InjOrderMixin : porderMixin U :=
POrderMixin CO_le_ltNeq CO_le_refl CO_le_anti CO_le_trans.
End InjOrder.

然后, ascii实例被重写如下:
Definition ascii_display : unit. Proof. exact: tt. Qed.
Definition ascii_porderMixin := InjOrderMixin (can_inj ascii_of_natK).
Canonical asciiPOrderType := POrderType ascii_display ascii ascii_porderMixin.

Lemma lea_total : @total ascii (<=%O)%O.
Proof. by move=> x y; apply: le_total. Qed.

Definition asciiLatticeMixin := Order.TotalLattice.Mixin lea_total.
Canonical asciiLatticeType := LatticeType ascii asciiLatticeMixin.
Canonical asciiOrderType := OrderType ascii lea_total.

关于module - 从注入(inject) `nat` 中获取类型的可判定总顺序,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/47128936/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com