Vì các số tự nhiên hỗ trợ một tổng số có thể giải quyết được, việc tiêm nat_of_ascii (a : ascii) : nat gây ra một tổng số có thể quyết định trên loại ascii. Điều gì sẽ là một cách ngắn gọn, thành ngữ để thể hiện điều này trong Coq? (Có hoặc không có lớp học, mô-đun, vv)Nhận tổng số thứ tự có thể quyết định trên một loại từ một lần tiêm vào `nat`
Quy trình này khá thường xuyên và sẽ tùy thuộc vào thư viện bạn đã chọn. Đối với order.v, dựa trên toán học-comp, quá trình này là hoàn toàn cơ khí [trên thực tế, chúng tôi sẽ phát triển một cấu trúc chung của các loại với một tiêm để tổng đơn đặt hàng sau này trong bài]:
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.
Lưu ý rằng việc cung cấp một để ví dụ cho ascii cho chúng ta truy cập vào một lý thuyết lớn trong tổng số đơn đặt hàng, cộng với các nhà khai thác, vv ..., tuy nhiên định nghĩa của tổng chính nó là khá đơn giản:
"<= is total" == x <= y || y <= x
nơi < = là một "mối quan hệ decidable" và chúng tôi giả định, tất nhiên, tính khả thi của sự bình đẳng đối với loại hình cụ thể. Cụ thể, đối với một mối quan hệ tùy ý:
Definition total (T: Type) (r : T -> T -> bool) := forall x y, r x y || r y x.
vì vậy nếu T là trật tự, đáp ứng total, bạn đang thực hiện.
Tổng quát hơn, bạn có thể xác định một nguyên tắc chung để xây dựng các loại như sử dụng thuốc tiêm:
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.
Sau đó, các trường hợp ascii được viết lại như sau:
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.