Ponieważ liczby naturalne obsługują rozstrzygające całkowite zamówienie, wstrzyknięcie nat_of_ascii (a : ascii) : nat
indukuje decydującą całkowitą kolejność na typie ascii
. Jaki byłby zwięzły, idiomatyczny sposób wyrażania tego w Coq? (Z lub bez klas, modułów itp.)Uzyskaj decydującą całkowitą kolejność na typie z iniekcji do `nat`
Odpowiedz
Takie postępowanie jest dość rutynowe i zależy od wybranej biblioteki. Dla order.v, na podstawie matematyki-comp, proces jest całkowicie mechaniczny [w rzeczywistości, będziemy rozwijać ogólną konstrukcję typów zastrzykiem do łącznych zamówień później w post]:
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.
Należy pamiętać, że zapewnienie instancji postanowienie ascii
daje nam dostęp do dużej teorii całkowitej zamówień, plus operatorów, itp ..., jednak definicja samej sumie jest dość prosta:
"<= is total" == x <= y || y <= x
< = gdzie jest „rozstrzygalne relacja” i zakładamy, oczywiście, rozstrzygalność równości dla danego typu. Konkretnie, na dowolnym stosunku:
Definition total (T: Type) (r : T -> T -> bool) := forall x y, r x y || r y x.
więc jeśli T
jest i porządek, i spełnia total
, gotowe.
Bardziej ogólnie można zdefiniować zasadę ogólną budować takie typy za pomocą zastrzyków:
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.
Następnie instancja ascii
zostanie przepisana następująco:
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.
- 1. QByteArray na liczbę całkowitą
- 2. Uzyskaj całkowitą liczbę wierszy podczas przeglądania
- 3. RabbitMQ - Uzyskaj całkowitą liczbę wiadomości zaksięgowanych
- 4. Uzyskaj całkowitą liczbę węzłów i węzłów zliczających
- 5. Android: NAT Traversal?
- 6. Przejdź do definicji na typie betonu
- 7. Java nat traversal do aplikacji czatu
- 8. Uzyskaj całkowitą wartość wyliczenia, która jest generyczna
- 9. Uzyskaj całkowitą liczbę wierszy w strukturze jednostki
- 10. Jak utworzyć dynamiczne powiązania w Guice, które wymagają iniekcji iniekcji?
- 11. Mechanizm wiązania iniekcji automatycznej
- 12. Wiosna 3.0 pliki do iniekcji jako zasoby
- 13. Zrób tekst Zaniknij na typie
- 14. Używanie czytnika Reader do iniekcji zależności
- 15. Jak uniknąć zderzeń z cechami PHP używanymi do iniekcji zależności
- 16. Konwersja Java na liczbę całkowitą do szesnastkowej
- 17. Synchronizacja na wartość całkowitą
- 18. Literały Idris Nat w typach
- 19. Jak korzystać z iniekcji zależności w serwletu?
- 20. Wiele właściwości indeksu na typie?
- 21. Uzyskaj całkowitą sumę rozmiaru wszystkich baz danych w serwerze SQL
- 22. Port Forwarding (NAT UPNP) BŁĄD
- 23. Kolejność kolumn na OpenJPA
- 24. Uzyskaj różnicę między dwoma datami w MySQL jako liczbą całkowitą
- 25. Uzyskaj 2 cyfry na miesiąc
- 26. Biblioteki iniekcji zależnej od Rubiego
- 27. Uzyskaj całkowitą liczbę przepracowanych godzin w ciągu dnia mysql
- 28. Zapobieganie iniekcji SQL w hibernacji
- 29. Pułapka unsigned char i IA64 NaT
- 30. Listy o stałej długości i typie literowym