「natへの注入から型への決定可能な総順序の取得」

Question

自然数が決定的な総順序をサポートしているので、ascii型に決定可能な合計順序が誘導されます。 Coqでこれを表現する簡潔で慣用的な方法は何でしょうか？ （タイプクラス、モジュールなどの有無にかかわらず）

Answer 1

このようなプロセスは、あなたが選択したライブラリに依存します。数学-COMPに基づいてorder.vについては、プロセスが完全に機械的である[実際には、我々は後の記事で総受注への注射でのタイプの一般的な構造を開発します]：提供すること

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であり、順序、および満たすtotal場合、あなたが行われています。

より一般的に、あなたは注射を使用して、このようなタイプを構築するために、一般的な原則を定義することができます。

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. 

を