diff options
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 53 | ||||
| -rw-r--r-- | plugins/micromega/g_zify.mlg | 50 | ||||
| -rw-r--r-- | plugins/micromega/zify.ml | 13 | ||||
| -rw-r--r-- | theories/micromega/ZifyBool.v | 42 | ||||
| -rw-r--r-- | theories/micromega/ZifyComparison.v | 14 | ||||
| -rw-r--r-- | theories/micromega/ZifyInst.v | 210 |
6 files changed, 212 insertions, 170 deletions
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 717b0deb43..c4947e6b3a 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -284,37 +284,54 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. + To support :g:`Z.quot` and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.quot_rem_to_equations``. + To support :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations``. + The :tacn:`zify` tactic can be extended with new types and operators by declaring and registering new typeclass instances using the following commands. + The typeclass declarations can be found in the module ``ZifyClasses`` and the default instances can be found in the module ``ZifyInst``. -.. cmd:: Show Zify InjTyp - :name: Show Zify InjTyp +.. cmd:: Add Zify {| InjTyp | BinOp | UnOp |CstOp | BinRel | UnOpSpec | BinOpSpec } @qualid - This command shows the list of types that can be injected into :g:`Z`. + This command registers an instance of one of the typeclasses among ``InjTyp``, ``BinOp``, ``UnOp``, ``CstOp``, ``BinRel``, + ``UnOpSpec``, ``BinOpSpec``. -.. cmd:: Show Zify BinOp - :name: Show Zify BinOp +.. cmd:: Show Zify {| InjTyp | BinOp | UnOp |CstOp | BinRel | UnOpSpec | BinOpSpec } - This command shows the list of binary operators processed by :tacn:`zify`. + The command prints the typeclass instances of one the typeclasses + among ``InjTyp``, ``BinOp``, ``UnOp``, ``CstOp``, ``BinRel``, + ``UnOpSpec``, ``BinOpSpec``. For instance, :cmd:`Show Zify` ``InjTyp`` + prints the list of types that supported by :tacn:`zify` i.e., + :g:`Z`, :g:`nat`, :g:`positive` and :g:`N`. -.. cmd:: Show Zify BinRel - :name: Show Zify BinRel +.. cmd:: Show Zify Spec - This command shows the list of binary relations processed by :tacn:`zify`. + .. deprecated:: 8.13 + Use instead either :cmd:`Show Zify` ``UnOpSpec`` or :cmd:`Show Zify` ``BinOpSpec``. +.. cmd:: Add InjTyp -.. cmd:: Show Zify UnOp - :name: Show Zify UnOp + .. deprecated:: 8.13 + Use instead either :cmd:`Add Zify` ``InjTyp``. - This command shows the list of unary operators processed by :tacn:`zify`. +.. cmd:: Add BinOp -.. cmd:: Show Zify CstOp - :name: Show Zify CstOp + .. deprecated:: 8.13 + Use instead either :cmd:`Add Zify` ``BinOp``. + +.. cmd:: Add UnOp + + .. deprecated:: 8.13 + Use instead either :cmd:`Add Zify` ``UnOp``. + +.. cmd:: Add CstOp + + .. deprecated:: 8.13 + Use instead either :cmd:`Add Zify` ``CstOp``. + +.. cmd:: Add BinRel + + .. deprecated:: 8.13 + Use instead either :cmd:`Add Zify` ``BinRel``. - This command shows the list of constants processed by :tacn:`zify`. -.. cmd:: Show Zify Spec - :name: Show Zify Spec - This command shows the list of operators over :g:`Z` that are compiled using their specification e.g., :g:`Z.min`. .. [#csdp] Sources and binaries can be found at https://projects.coin-or.org/Csdp .. [#fnpsatz] Variants deal with equalities and strict inequalities. diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg index 80a40c4315..0e5cac2d4a 100644 --- a/plugins/micromega/g_zify.mlg +++ b/plugins/micromega/g_zify.mlg @@ -14,23 +14,44 @@ open Ltac_plugin open Stdarg open Tacarg +let warn_deprecated_Spec = + CWarnings.create ~name:"deprecated-Zify-Spec" ~category:"deprecated" + (fun () -> + Pp.strbrk ("Show Zify Spec is deprecated. Use either \"Show Zify BinOpSpec\" or \"Show Zify UnOpSpec\".")) + +let warn_deprecated_Add = + CWarnings.create ~name:"deprecated-Zify-Add" ~category:"deprecated" + (fun () -> + Pp.strbrk ("Add <X> is deprecated. Use instead Add Zify <X>.")) + } DECLARE PLUGIN "zify_plugin" VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF -| ["Add" "InjTyp" constr(t) ] -> { Zify.InjTable.register t } -| ["Add" "BinOp" constr(t) ] -> { Zify.BinOp.register t } -| ["Add" "UnOp" constr(t) ] -> { Zify.UnOp.register t } -| ["Add" "CstOp" constr(t) ] -> { Zify.CstOp.register t } -| ["Add" "BinRel" constr(t) ] -> { Zify.BinRel.register t } -| ["Add" "PropOp" constr(t) ] -> { Zify.PropBinOp.register t } -| ["Add" "PropBinOp" constr(t) ] -> { Zify.PropBinOp.register t } -| ["Add" "PropUOp" constr(t) ] -> { Zify.PropUnOp.register t } -| ["Add" "BinOpSpec" constr(t) ] -> { Zify.BinOpSpec.register t } -| ["Add" "UnOpSpec" constr(t) ] -> { Zify.UnOpSpec.register t } -| ["Add" "Saturate" constr(t) ] -> { Zify.Saturate.register t } +| ["Add" "Zify" "InjTyp" constr(t) ] -> { Zify.InjTable.register t } +| ["Add" "Zify" "BinOp" constr(t) ] -> { Zify.BinOp.register t } +| ["Add" "Zify" "UnOp" constr(t) ] -> { Zify.UnOp.register t } +| ["Add" "Zify" "CstOp" constr(t) ] -> { Zify.CstOp.register t } +| ["Add" "Zify" "BinRel" constr(t) ] -> { Zify.BinRel.register t } +| ["Add" "Zify" "PropOp" constr(t) ] -> { Zify.PropBinOp.register t } +| ["Add" "Zify" "PropBinOp" constr(t) ] -> { Zify.PropBinOp.register t } +| ["Add" "Zify" "PropUOp" constr(t) ] -> { Zify.PropUnOp.register t } +| ["Add" "Zify" "BinOpSpec" constr(t) ] -> { Zify.BinOpSpec.register t } +| ["Add" "Zify" "UnOpSpec" constr(t) ] -> { Zify.UnOpSpec.register t } +| ["Add" "Zify" "Saturate" constr(t) ] -> { Zify.Saturate.register t } +| ["Add" "InjTyp" constr(t) ] -> { warn_deprecated_Add (); Zify.InjTable.register t } +| ["Add" "BinOp" constr(t) ] -> { warn_deprecated_Add (); Zify.BinOp.register t } +| ["Add" "UnOp" constr(t) ] -> { warn_deprecated_Add (); Zify.UnOp.register t } +| ["Add" "CstOp" constr(t) ] -> { warn_deprecated_Add (); Zify.CstOp.register t } +| ["Add" "BinRel" constr(t) ] -> { warn_deprecated_Add (); Zify.BinRel.register t } +| ["Add" "PropOp" constr(t) ] -> { warn_deprecated_Add (); Zify.PropBinOp.register t } +| ["Add" "PropBinOp" constr(t) ] -> { warn_deprecated_Add (); Zify.PropBinOp.register t } +| ["Add" "PropUOp" constr(t) ] -> { warn_deprecated_Add (); Zify.PropUnOp.register t } +| ["Add" "BinOpSpec" constr(t) ] -> { warn_deprecated_Add (); Zify.BinOpSpec.register t } +| ["Add" "UnOpSpec" constr(t) ] -> { warn_deprecated_Add (); Zify.UnOpSpec.register t } +| ["Add" "Saturate" constr(t) ] -> { warn_deprecated_Add (); Zify.Saturate.register t } END TACTIC EXTEND ITER @@ -50,6 +71,9 @@ VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF |[ "Show" "Zify" "UnOp" ] -> { Zify.UnOp.print () } |[ "Show" "Zify" "CstOp"] -> { Zify.CstOp.print () } |[ "Show" "Zify" "BinRel"] -> { Zify.BinRel.print () } -|[ "Show" "Zify" "Spec"] -> { (* This prints both UnOpSpec and BinOpSpec *) - Zify.UnOpSpec.print() } +|[ "Show" "Zify" "UnOpSpec"] -> { Zify.UnOpSpec.print() } +|[ "Show" "Zify" "BinOpSpec"] -> { Zify.BinOpSpec.print() } +|[ "Show" "Zify" "Spec"] -> { + warn_deprecated_Spec () ; + Zify.UnOpSpec.print() ; Zify.BinOpSpec.print ()} END diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index ec0f278326..4e1f9a66ac 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -320,7 +320,8 @@ type decl_kind = | UnOp of EUnOpT.t decl | CstOp of ECstOpT.t decl | Saturate of ESatT.t decl - | Spec of ESpecT.t decl + | UnOpSpec of ESpecT.t decl + | BinOpSpec of ESpecT.t decl type term_kind = Application of EConstr.constr | OtherTerm of EConstr.constr @@ -664,8 +665,8 @@ module EUnopSpec = struct let name = "UnopSpec" let table = specs - let cast x = Spec x - let dest = function Spec x -> Some x | _ -> None + let cast x = UnOpSpec x + let dest = function UnOpSpec x -> Some x | _ -> None let mk_elt evd i a = {spec = a.(4)} let get_key = 2 end @@ -677,8 +678,8 @@ module EBinOpSpec = struct let name = "BinOpSpec" let table = specs - let cast x = Spec x - let dest = function Spec x -> Some x | _ -> None + let cast x = BinOpSpec x + let dest = function BinOpSpec x -> Some x | _ -> None let mk_elt evd i a = {spec = a.(5)} let get_key = 3 end @@ -1419,7 +1420,7 @@ let rec spec_of_term env evd (senv : spec_env) t = with Not_found -> ( try match snd (HConstr.find c !specs_cache) with - | Spec s -> + | UnOpSpec s | BinOpSpec s -> let thm = EConstr.mkApp (s.deriv.ESpecT.spec, a') in register_constr senv' t' thm | _ -> (get_name t' senv', senv') diff --git a/theories/micromega/ZifyBool.v b/theories/micromega/ZifyBool.v index 6c34040155..fa3f123b18 100644 --- a/theories/micromega/ZifyBool.v +++ b/theories/micromega/ZifyBool.v @@ -16,21 +16,21 @@ Local Open Scope Z_scope. Instance Inj_bool_bool : InjTyp bool bool := { inj := (fun x => x) ; pred := (fun b => b = true \/ b = false) ; cstr := (ltac:(intro b; destruct b; tauto))}. -Add InjTyp Inj_bool_bool. +Add Zify InjTyp Inj_bool_bool. (** Boolean operators *) Instance Op_andb : BinOp andb := { TBOp := andb ; TBOpInj := fun _ _ => eq_refl}. -Add BinOp Op_andb. +Add Zify BinOp Op_andb. Instance Op_orb : BinOp orb := { TBOp := orb ; TBOpInj := fun _ _ => eq_refl}. -Add BinOp Op_orb. +Add Zify BinOp Op_orb. Instance Op_implb : BinOp implb := { TBOp := implb; TBOpInj := fun _ _ => eq_refl }. -Add BinOp Op_implb. +Add Zify BinOp Op_implb. Definition xorb_eq : forall b1 b2, xorb b1 b2 = andb (orb b1 b2) (negb (eqb b1 b2)). @@ -40,49 +40,49 @@ Qed. Instance Op_xorb : BinOp xorb := { TBOp := fun x y => andb (orb x y) (negb (eqb x y)); TBOpInj := xorb_eq }. -Add BinOp Op_xorb. +Add Zify BinOp Op_xorb. Instance Op_eqb : BinOp eqb := { TBOp := eqb; TBOpInj := fun _ _ => eq_refl }. -Add BinOp Op_eqb. +Add Zify BinOp Op_eqb. Instance Op_negb : UnOp negb := { TUOp := negb ; TUOpInj := fun _ => eq_refl}. -Add UnOp Op_negb. +Add Zify UnOp Op_negb. Instance Op_eq_bool : BinRel (@eq bool) := {TR := @eq bool ; TRInj := ltac:(reflexivity) }. -Add BinRel Op_eq_bool. +Add Zify BinRel Op_eq_bool. Instance Op_true : CstOp true := { TCst := true ; TCstInj := eq_refl }. -Add CstOp Op_true. +Add Zify CstOp Op_true. Instance Op_false : CstOp false := { TCst := false ; TCstInj := eq_refl }. -Add CstOp Op_false. +Add Zify CstOp Op_false. (** Comparison over Z *) Instance Op_Zeqb : BinOp Z.eqb := { TBOp := Z.eqb ; TBOpInj := fun _ _ => eq_refl }. -Add BinOp Op_Zeqb. +Add Zify BinOp Op_Zeqb. Instance Op_Zleb : BinOp Z.leb := { TBOp := Z.leb; TBOpInj := fun _ _ => eq_refl }. -Add BinOp Op_Zleb. +Add Zify BinOp Op_Zleb. Instance Op_Zgeb : BinOp Z.geb := { TBOp := Z.geb; TBOpInj := fun _ _ => eq_refl }. -Add BinOp Op_Zgeb. +Add Zify BinOp Op_Zgeb. Instance Op_Zltb : BinOp Z.ltb := { TBOp := Z.ltb ; TBOpInj := fun _ _ => eq_refl }. -Add BinOp Op_Zltb. +Add Zify BinOp Op_Zltb. Instance Op_Zgtb : BinOp Z.gtb := { TBOp := Z.gtb; TBOpInj := fun _ _ => eq_refl }. -Add BinOp Op_Zgtb. +Add Zify BinOp Op_Zgtb. (** Comparison over nat *) @@ -118,15 +118,15 @@ Qed. Instance Op_nat_eqb : BinOp Nat.eqb := { TBOp := Z.eqb; TBOpInj := Z_of_nat_eqb_iff }. -Add BinOp Op_nat_eqb. +Add Zify BinOp Op_nat_eqb. Instance Op_nat_leb : BinOp Nat.leb := { TBOp := Z.leb; TBOpInj := Z_of_nat_leb_iff }. -Add BinOp Op_nat_leb. +Add Zify BinOp Op_nat_leb. Instance Op_nat_ltb : BinOp Nat.ltb := { TBOp := Z.ltb; TBOpInj := Z_of_nat_ltb_iff }. -Add BinOp Op_nat_ltb. +Add Zify BinOp Op_nat_ltb. Lemma b2n_b2z : forall x, Z.of_nat (Nat.b2n x) = Z.b2z x. Proof. @@ -135,11 +135,11 @@ Qed. Instance Op_b2n : UnOp Nat.b2n := { TUOp := Z.b2z; TUOpInj := b2n_b2z }. -Add UnOp Op_b2n. +Add Zify UnOp Op_b2n. Instance Op_b2z : UnOp Z.b2z := { TUOp := Z.b2z; TUOpInj := fun _ => eq_refl }. -Add UnOp Op_b2z. +Add Zify UnOp Op_b2z. Lemma b2z_spec : forall b, (b = true /\ Z.b2z b = 1) \/ (b = false /\ Z.b2z b = 0). Proof. @@ -150,7 +150,7 @@ Instance b2zSpec : UnOpSpec Z.b2z := { UPred := fun b r => (b = true /\ r = 1) \/ (b = false /\ r = 0); USpec := b2z_spec }. -Add UnOpSpec b2zSpec. +Add Zify UnOpSpec b2zSpec. Ltac elim_bool_cstr := repeat match goal with diff --git a/theories/micromega/ZifyComparison.v b/theories/micromega/ZifyComparison.v index b8d38adcc5..a4ada571f1 100644 --- a/theories/micromega/ZifyComparison.v +++ b/theories/micromega/ZifyComparison.v @@ -28,30 +28,30 @@ Qed. Instance Inj_comparison_Z : InjTyp comparison Z := { inj := Z_of_comparison ; pred :=(fun x => -1 <= x <= 1) ; cstr := Z_of_comparison_bound}. -Add InjTyp Inj_comparison_Z. +Add Zify InjTyp Inj_comparison_Z. Definition ZcompareZ (x y : Z) := Z_of_comparison (Z.compare x y). Program Instance BinOp_Zcompare : BinOp Z.compare := { TBOp := ZcompareZ }. -Add BinOp BinOp_Zcompare. +Add Zify BinOp BinOp_Zcompare. Instance Op_eq_comparison : BinRel (@eq comparison) := {TR := @eq Z ; TRInj := ltac:(destruct n,m; simpl ; intuition congruence) }. -Add BinRel Op_eq_comparison. +Add Zify BinRel Op_eq_comparison. Instance Op_Eq : CstOp Eq := { TCst := 0 ; TCstInj := eq_refl }. -Add CstOp Op_Eq. +Add Zify CstOp Op_Eq. Instance Op_Lt : CstOp Lt := { TCst := -1 ; TCstInj := eq_refl }. -Add CstOp Op_Lt. +Add Zify CstOp Op_Lt. Instance Op_Gt : CstOp Gt := { TCst := 1 ; TCstInj := eq_refl }. -Add CstOp Op_Gt. +Add Zify CstOp Op_Gt. Lemma Zcompare_spec : forall x y, @@ -79,4 +79,4 @@ Instance ZcompareSpec : BinOpSpec ZcompareZ := /\ (x < y -> r = -1) ; BSpec := Zcompare_spec|}. -Add BinOpSpec ZcompareSpec. +Add Zify BinOpSpec ZcompareSpec. diff --git a/theories/micromega/ZifyInst.v b/theories/micromega/ZifyInst.v index e5d0312f3d..0e135ba793 100644 --- a/theories/micromega/ZifyInst.v +++ b/theories/micromega/ZifyInst.v @@ -25,117 +25,117 @@ Ltac refl := Instance Inj_Z_Z : InjTyp Z Z := mkinj _ _ (fun x => x) (fun x => True ) (fun _ => I). -Add InjTyp Inj_Z_Z. +Add Zify InjTyp Inj_Z_Z. (** Support for nat *) Instance Inj_nat_Z : InjTyp nat Z := mkinj _ _ Z.of_nat (fun x => 0 <= x ) Nat2Z.is_nonneg. -Add InjTyp Inj_nat_Z. +Add Zify InjTyp Inj_nat_Z. (* zify_nat_rel *) Instance Op_ge : BinRel ge := {| TR := Z.ge; TRInj := Nat2Z.inj_ge |}. -Add BinRel Op_ge. +Add Zify BinRel Op_ge. Instance Op_lt : BinRel lt := {| TR := Z.lt; TRInj := Nat2Z.inj_lt |}. -Add BinRel Op_lt. +Add Zify BinRel Op_lt. Instance Op_Nat_lt : BinRel Nat.lt := Op_lt. -Add BinRel Op_Nat_lt. +Add Zify BinRel Op_Nat_lt. Instance Op_gt : BinRel gt := {| TR := Z.gt; TRInj := Nat2Z.inj_gt |}. -Add BinRel Op_gt. +Add Zify BinRel Op_gt. Instance Op_le : BinRel le := {| TR := Z.le; TRInj := Nat2Z.inj_le |}. -Add BinRel Op_le. +Add Zify BinRel Op_le. Instance Op_Nat_le : BinRel Nat.le := Op_le. -Add BinRel Op_Nat_le. +Add Zify BinRel Op_Nat_le. Instance Op_eq_nat : BinRel (@eq nat) := {| TR := @eq Z ; TRInj := fun x y : nat => iff_sym (Nat2Z.inj_iff x y) |}. -Add BinRel Op_eq_nat. +Add Zify BinRel Op_eq_nat. Instance Op_Nat_eq : BinRel (Nat.eq) := Op_eq_nat. -Add BinRel Op_Nat_eq. +Add Zify BinRel Op_Nat_eq. (* zify_nat_op *) Instance Op_plus : BinOp Nat.add := {| TBOp := Z.add; TBOpInj := Nat2Z.inj_add |}. -Add BinOp Op_plus. +Add Zify BinOp Op_plus. Instance Op_sub : BinOp Nat.sub := {| TBOp := fun n m => Z.max 0 (n - m) ; TBOpInj := Nat2Z.inj_sub_max |}. -Add BinOp Op_sub. +Add Zify BinOp Op_sub. Instance Op_mul : BinOp Nat.mul := {| TBOp := Z.mul ; TBOpInj := Nat2Z.inj_mul |}. -Add BinOp Op_mul. +Add Zify BinOp Op_mul. Instance Op_min : BinOp Nat.min := {| TBOp := Z.min ; TBOpInj := Nat2Z.inj_min |}. -Add BinOp Op_min. +Add Zify BinOp Op_min. Instance Op_max : BinOp Nat.max := {| TBOp := Z.max ; TBOpInj := Nat2Z.inj_max |}. -Add BinOp Op_max. +Add Zify BinOp Op_max. Instance Op_pred : UnOp Nat.pred := {| TUOp := fun n => Z.max 0 (n - 1) ; TUOpInj := Nat2Z.inj_pred_max |}. -Add UnOp Op_pred. +Add Zify UnOp Op_pred. Instance Op_S : UnOp S := {| TUOp := fun x => Z.add x 1 ; TUOpInj := Nat2Z.inj_succ |}. -Add UnOp Op_S. +Add Zify UnOp Op_S. Instance Op_O : CstOp O := {| TCst := Z0 ; TCstInj := eq_refl (Z.of_nat 0) |}. -Add CstOp Op_O. +Add Zify CstOp Op_O. Instance Op_Z_abs_nat : UnOp Z.abs_nat := { TUOp := Z.abs ; TUOpInj := Zabs2Nat.id_abs }. -Add UnOp Op_Z_abs_nat. +Add Zify UnOp Op_Z_abs_nat. (** Support for positive *) Instance Inj_pos_Z : InjTyp positive Z := {| inj := Zpos ; pred := (fun x => 0 < x ) ; cstr := Pos2Z.pos_is_pos |}. -Add InjTyp Inj_pos_Z. +Add Zify InjTyp Inj_pos_Z. Instance Op_pos_to_nat : UnOp Pos.to_nat := {TUOp := (fun x => x); TUOpInj := positive_nat_Z}. -Add UnOp Op_pos_to_nat. +Add Zify UnOp Op_pos_to_nat. Instance Inj_N_Z : InjTyp N Z := mkinj _ _ Z.of_N (fun x => 0 <= x ) N2Z.is_nonneg. -Add InjTyp Inj_N_Z. +Add Zify InjTyp Inj_N_Z. Instance Op_N_to_nat : UnOp N.to_nat := { TUOp := fun x => x ; TUOpInj := N_nat_Z }. -Add UnOp Op_N_to_nat. +Add Zify UnOp Op_N_to_nat. (* zify_positive_rel *) Instance Op_pos_ge : BinRel Pos.ge := {| TR := Z.ge; TRInj := fun x y => iff_refl (Z.pos x >= Z.pos y) |}. -Add BinRel Op_pos_ge. +Add Zify BinRel Op_pos_ge. Instance Op_pos_lt : BinRel Pos.lt := {| TR := Z.lt; TRInj := fun x y => iff_refl (Z.pos x < Z.pos y) |}. -Add BinRel Op_pos_lt. +Add Zify BinRel Op_pos_lt. Instance Op_pos_gt : BinRel Pos.gt := {| TR := Z.gt; TRInj := fun x y => iff_refl (Z.pos x > Z.pos y) |}. -Add BinRel Op_pos_gt. +Add Zify BinRel Op_pos_gt. Instance Op_pos_le : BinRel Pos.le := {| TR := Z.le; TRInj := fun x y => iff_refl (Z.pos x <= Z.pos y) |}. -Add BinRel Op_pos_le. +Add Zify BinRel Op_pos_le. Lemma eq_pos_inj : forall (x y:positive), x = y <-> Z.pos x = Z.pos y. Proof. @@ -145,36 +145,36 @@ Qed. Instance Op_eq_pos : BinRel (@eq positive) := { TR := @eq Z ; TRInj := eq_pos_inj }. -Add BinRel Op_eq_pos. +Add Zify BinRel Op_eq_pos. (* zify_positive_op *) Instance Op_Z_of_N : UnOp Z.of_N := { TUOp := (fun x => x) ; TUOpInj := fun x => eq_refl (Z.of_N x) }. -Add UnOp Op_Z_of_N. +Add Zify UnOp Op_Z_of_N. Instance Op_Z_to_N : UnOp Z.to_N := { TUOp := fun x => Z.max 0 x ; TUOpInj := ltac:(now intro x; destruct x) }. -Add UnOp Op_Z_to_N. +Add Zify UnOp Op_Z_to_N. Instance Op_Z_neg : UnOp Z.neg := { TUOp := Z.opp ; TUOpInj := (fun x => eq_refl (Zneg x))}. -Add UnOp Op_Z_neg. +Add Zify UnOp Op_Z_neg. Instance Op_Z_pos : UnOp Z.pos := { TUOp := (fun x => x) ; TUOpInj := (fun x => eq_refl (Z.pos x))}. -Add UnOp Op_Z_pos. +Add Zify UnOp Op_Z_pos. Instance Op_pos_succ : UnOp Pos.succ := { TUOp := fun x => x + 1; TUOpInj := Pos2Z.inj_succ }. -Add UnOp Op_pos_succ. +Add Zify UnOp Op_pos_succ. Instance Op_pos_pred_double : UnOp Pos.pred_double := { TUOp := fun x => 2 * x - 1; TUOpInj := ltac:(refl) }. -Add UnOp Op_pos_pred_double. +Add Zify UnOp Op_pos_pred_double. Instance Op_pos_pred : UnOp Pos.pred := { TUOp := fun x => Z.max 1 (x - 1) ; @@ -182,266 +182,266 @@ Instance Op_pos_pred : UnOp Pos.pred := (intros; rewrite <- Pos.sub_1_r; apply Pos2Z.inj_sub_max) }. -Add UnOp Op_pos_pred. +Add Zify UnOp Op_pos_pred. Instance Op_pos_predN : UnOp Pos.pred_N := { TUOp := fun x => x - 1 ; TUOpInj := ltac: (now destruct x; rewrite N.pos_pred_spec) }. -Add UnOp Op_pos_predN. +Add Zify UnOp Op_pos_predN. Instance Op_pos_of_succ_nat : UnOp Pos.of_succ_nat := { TUOp := fun x => x + 1 ; TUOpInj := Zpos_P_of_succ_nat }. -Add UnOp Op_pos_of_succ_nat. +Add Zify UnOp Op_pos_of_succ_nat. Instance Op_pos_of_nat : UnOp Pos.of_nat := { TUOp := fun x => Z.max 1 x ; TUOpInj := ltac: (now destruct x; [|rewrite <- Pos.of_nat_succ, <- (Nat2Z.inj_max 1)]) }. -Add UnOp Op_pos_of_nat. +Add Zify UnOp Op_pos_of_nat. Instance Op_pos_add : BinOp Pos.add := { TBOp := Z.add ; TBOpInj := ltac: (refl) }. -Add BinOp Op_pos_add. +Add Zify BinOp Op_pos_add. Instance Op_pos_add_carry : BinOp Pos.add_carry := { TBOp := fun x y => x + y + 1 ; TBOpInj := ltac:(now intros; rewrite Pos.add_carry_spec, Pos2Z.inj_succ) }. -Add BinOp Op_pos_add_carry. +Add Zify BinOp Op_pos_add_carry. Instance Op_pos_sub : BinOp Pos.sub := { TBOp := fun n m => Z.max 1 (n - m) ;TBOpInj := Pos2Z.inj_sub_max }. -Add BinOp Op_pos_sub. +Add Zify BinOp Op_pos_sub. Instance Op_pos_mul : BinOp Pos.mul := { TBOp := Z.mul ; TBOpInj := ltac: (refl) }. -Add BinOp Op_pos_mul. +Add Zify BinOp Op_pos_mul. Instance Op_pos_min : BinOp Pos.min := { TBOp := Z.min ; TBOpInj := Pos2Z.inj_min }. -Add BinOp Op_pos_min. +Add Zify BinOp Op_pos_min. Instance Op_pos_max : BinOp Pos.max := { TBOp := Z.max ; TBOpInj := Pos2Z.inj_max }. -Add BinOp Op_pos_max. +Add Zify BinOp Op_pos_max. Instance Op_pos_pow : BinOp Pos.pow := { TBOp := Z.pow ; TBOpInj := Pos2Z.inj_pow }. -Add BinOp Op_pos_pow. +Add Zify BinOp Op_pos_pow. Instance Op_pos_square : UnOp Pos.square := { TUOp := Z.square ; TUOpInj := Pos2Z.inj_square }. -Add UnOp Op_pos_square. +Add Zify UnOp Op_pos_square. Instance Op_xO : UnOp xO := { TUOp := fun x => 2 * x ; TUOpInj := ltac: (refl) }. -Add UnOp Op_xO. +Add Zify UnOp Op_xO. Instance Op_xI : UnOp xI := { TUOp := fun x => 2 * x + 1 ; TUOpInj := ltac: (refl) }. -Add UnOp Op_xI. +Add Zify UnOp Op_xI. Instance Op_xH : CstOp xH := { TCst := 1%Z ; TCstInj := ltac:(refl)}. -Add CstOp Op_xH. +Add Zify CstOp Op_xH. Instance Op_Z_of_nat : UnOp Z.of_nat:= { TUOp := fun x => x ; TUOpInj := (fun x : nat => @eq_refl Z (Z.of_nat x)) }. -Add UnOp Op_Z_of_nat. +Add Zify UnOp Op_Z_of_nat. (* zify_N_rel *) Instance Op_N_ge : BinRel N.ge := {| TR := Z.ge ; TRInj := N2Z.inj_ge |}. -Add BinRel Op_N_ge. +Add Zify BinRel Op_N_ge. Instance Op_N_lt : BinRel N.lt := {| TR := Z.lt ; TRInj := N2Z.inj_lt |}. -Add BinRel Op_N_lt. +Add Zify BinRel Op_N_lt. Instance Op_N_gt : BinRel N.gt := {| TR := Z.gt ; TRInj := N2Z.inj_gt |}. -Add BinRel Op_N_gt. +Add Zify BinRel Op_N_gt. Instance Op_N_le : BinRel N.le := {| TR := Z.le ; TRInj := N2Z.inj_le |}. -Add BinRel Op_N_le. +Add Zify BinRel Op_N_le. Instance Op_eq_N : BinRel (@eq N) := {| TR := @eq Z ; TRInj := fun x y : N => iff_sym (N2Z.inj_iff x y) |}. -Add BinRel Op_eq_N. +Add Zify BinRel Op_eq_N. (* zify_N_op *) Instance Op_N_N0 : CstOp N0 := { TCst := Z0 ; TCstInj := eq_refl }. -Add CstOp Op_N_N0. +Add Zify CstOp Op_N_N0. Instance Op_N_Npos : UnOp Npos := { TUOp := (fun x => x) ; TUOpInj := ltac:(refl) }. -Add UnOp Op_N_Npos. +Add Zify UnOp Op_N_Npos. Instance Op_N_of_nat : UnOp N.of_nat := { TUOp := fun x => x ; TUOpInj := nat_N_Z }. -Add UnOp Op_N_of_nat. +Add Zify UnOp Op_N_of_nat. Instance Op_Z_abs_N : UnOp Z.abs_N := { TUOp := Z.abs ; TUOpInj := N2Z.inj_abs_N }. -Add UnOp Op_Z_abs_N. +Add Zify UnOp Op_Z_abs_N. Instance Op_N_pos : UnOp N.pos := { TUOp := fun x => x ; TUOpInj := ltac:(refl)}. -Add UnOp Op_N_pos. +Add Zify UnOp Op_N_pos. Instance Op_N_add : BinOp N.add := {| TBOp := Z.add ; TBOpInj := N2Z.inj_add |}. -Add BinOp Op_N_add. +Add Zify BinOp Op_N_add. Instance Op_N_min : BinOp N.min := {| TBOp := Z.min ; TBOpInj := N2Z.inj_min |}. -Add BinOp Op_N_min. +Add Zify BinOp Op_N_min. Instance Op_N_max : BinOp N.max := {| TBOp := Z.max ; TBOpInj := N2Z.inj_max |}. -Add BinOp Op_N_max. +Add Zify BinOp Op_N_max. Instance Op_N_mul : BinOp N.mul := {| TBOp := Z.mul ; TBOpInj := N2Z.inj_mul |}. -Add BinOp Op_N_mul. +Add Zify BinOp Op_N_mul. Instance Op_N_sub : BinOp N.sub := {| TBOp := fun x y => Z.max 0 (x - y) ; TBOpInj := N2Z.inj_sub_max|}. -Add BinOp Op_N_sub. +Add Zify BinOp Op_N_sub. Instance Op_N_div : BinOp N.div := {| TBOp := Z.div ; TBOpInj := N2Z.inj_div|}. -Add BinOp Op_N_div. +Add Zify BinOp Op_N_div. Instance Op_N_mod : BinOp N.modulo := {| TBOp := Z.rem ; TBOpInj := N2Z.inj_rem|}. -Add BinOp Op_N_mod. +Add Zify BinOp Op_N_mod. Instance Op_N_pred : UnOp N.pred := { TUOp := fun x => Z.max 0 (x - 1) ; TUOpInj := ltac:(intros; rewrite N.pred_sub; apply N2Z.inj_sub_max) }. -Add UnOp Op_N_pred. +Add Zify UnOp Op_N_pred. Instance Op_N_succ : UnOp N.succ := {| TUOp := fun x => x + 1 ; TUOpInj := N2Z.inj_succ |}. -Add UnOp Op_N_succ. +Add Zify UnOp Op_N_succ. (** Support for Z - injected to itself *) (* zify_Z_rel *) Instance Op_Z_ge : BinRel Z.ge := {| TR := Z.ge ; TRInj := fun x y => iff_refl (x>= y)|}. -Add BinRel Op_Z_ge. +Add Zify BinRel Op_Z_ge. Instance Op_Z_lt : BinRel Z.lt := {| TR := Z.lt ; TRInj := fun x y => iff_refl (x < y)|}. -Add BinRel Op_Z_lt. +Add Zify BinRel Op_Z_lt. Instance Op_Z_gt : BinRel Z.gt := {| TR := Z.gt ;TRInj := fun x y => iff_refl (x > y)|}. -Add BinRel Op_Z_gt. +Add Zify BinRel Op_Z_gt. Instance Op_Z_le : BinRel Z.le := {| TR := Z.le ;TRInj := fun x y => iff_refl (x <= y)|}. -Add BinRel Op_Z_le. +Add Zify BinRel Op_Z_le. Instance Op_eqZ : BinRel (@eq Z) := { TR := @eq Z ; TRInj := fun x y => iff_refl (x = y) }. -Add BinRel Op_eqZ. +Add Zify BinRel Op_eqZ. Instance Op_Z_Z0 : CstOp Z0 := { TCst := Z0 ; TCstInj := eq_refl }. -Add CstOp Op_Z_Z0. +Add Zify CstOp Op_Z_Z0. Instance Op_Z_add : BinOp Z.add := { TBOp := Z.add ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_add. +Add Zify BinOp Op_Z_add. Instance Op_Z_min : BinOp Z.min := { TBOp := Z.min ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_min. +Add Zify BinOp Op_Z_min. Instance Op_Z_max : BinOp Z.max := { TBOp := Z.max ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_max. +Add Zify BinOp Op_Z_max. Instance Op_Z_mul : BinOp Z.mul := { TBOp := Z.mul ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_mul. +Add Zify BinOp Op_Z_mul. Instance Op_Z_sub : BinOp Z.sub := { TBOp := Z.sub ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_sub. +Add Zify BinOp Op_Z_sub. Instance Op_Z_div : BinOp Z.div := { TBOp := Z.div ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_div. +Add Zify BinOp Op_Z_div. Instance Op_Z_mod : BinOp Z.modulo := { TBOp := Z.modulo ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_mod. +Add Zify BinOp Op_Z_mod. Instance Op_Z_rem : BinOp Z.rem := { TBOp := Z.rem ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_rem. +Add Zify BinOp Op_Z_rem. Instance Op_Z_quot : BinOp Z.quot := { TBOp := Z.quot ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_quot. +Add Zify BinOp Op_Z_quot. Instance Op_Z_succ : UnOp Z.succ := { TUOp := fun x => x + 1 ; TUOpInj := ltac:(refl) }. -Add UnOp Op_Z_succ. +Add Zify UnOp Op_Z_succ. Instance Op_Z_pred : UnOp Z.pred := { TUOp := fun x => x - 1 ; TUOpInj := ltac:(refl) }. -Add UnOp Op_Z_pred. +Add Zify UnOp Op_Z_pred. Instance Op_Z_opp : UnOp Z.opp := { TUOp := Z.opp ; TUOpInj := ltac:(refl) }. -Add UnOp Op_Z_opp. +Add Zify UnOp Op_Z_opp. Instance Op_Z_abs : UnOp Z.abs := { TUOp := Z.abs ; TUOpInj := ltac:(refl) }. -Add UnOp Op_Z_abs. +Add Zify UnOp Op_Z_abs. Instance Op_Z_sgn : UnOp Z.sgn := { TUOp := Z.sgn ; TUOpInj := ltac:(refl) }. -Add UnOp Op_Z_sgn. +Add Zify UnOp Op_Z_sgn. Instance Op_Z_pow : BinOp Z.pow := { TBOp := Z.pow ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_pow. +Add Zify BinOp Op_Z_pow. Instance Op_Z_pow_pos : BinOp Z.pow_pos := { TBOp := Z.pow ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_pow_pos. +Add Zify BinOp Op_Z_pow_pos. Instance Op_Z_double : UnOp Z.double := { TUOp := Z.mul 2 ; TUOpInj := Z.double_spec }. -Add UnOp Op_Z_double. +Add Zify UnOp Op_Z_double. Instance Op_Z_pred_double : UnOp Z.pred_double := { TUOp := fun x => 2 * x - 1 ; TUOpInj := Z.pred_double_spec }. -Add UnOp Op_Z_pred_double. +Add Zify UnOp Op_Z_pred_double. Instance Op_Z_succ_double : UnOp Z.succ_double := { TUOp := fun x => 2 * x + 1 ; TUOpInj := Z.succ_double_spec }. -Add UnOp Op_Z_succ_double. +Add Zify UnOp Op_Z_succ_double. Instance Op_Z_square : UnOp Z.square := { TUOp := fun x => x * x ; TUOpInj := Z.square_spec }. -Add UnOp Op_Z_square. +Add Zify UnOp Op_Z_square. Instance Op_Z_div2 : UnOp Z.div2 := { TUOp := fun x => x / 2 ; TUOpInj := Z.div2_div }. -Add UnOp Op_Z_div2. +Add Zify UnOp Op_Z_div2. Instance Op_Z_quot2 : UnOp Z.quot2 := { TUOp := fun x => Z.quot x 2 ; TUOpInj := Zeven.Zquot2_quot }. -Add UnOp Op_Z_quot2. +Add Zify UnOp Op_Z_quot2. Lemma of_nat_to_nat_eq : forall x, Z.of_nat (Z.to_nat x) = Z.max 0 x. Proof. @@ -455,28 +455,28 @@ Qed. Instance Op_Z_to_nat : UnOp Z.to_nat := { TUOp := fun x => Z.max 0 x ; TUOpInj := of_nat_to_nat_eq }. -Add UnOp Op_Z_to_nat. +Add Zify UnOp Op_Z_to_nat. (** Specification of derived operators over Z *) Instance ZmaxSpec : BinOpSpec Z.max := {| BPred := fun n m r => n < m /\ r = m \/ m <= n /\ r = n ; BSpec := Z.max_spec|}. -Add BinOpSpec ZmaxSpec. +Add Zify BinOpSpec ZmaxSpec. Instance ZminSpec : BinOpSpec Z.min := {| BPred := fun n m r => n < m /\ r = n \/ m <= n /\ r = m ; BSpec := Z.min_spec |}. -Add BinOpSpec ZminSpec. +Add Zify BinOpSpec ZminSpec. Instance ZsgnSpec : UnOpSpec Z.sgn := {| UPred := fun n r : Z => 0 < n /\ r = 1 \/ 0 = n /\ r = 0 \/ n < 0 /\ r = - (1) ; USpec := Z.sgn_spec|}. -Add UnOpSpec ZsgnSpec. +Add Zify UnOpSpec ZsgnSpec. Instance ZabsSpec : UnOpSpec Z.abs := {| UPred := fun n r: Z => 0 <= n /\ r = n \/ n < 0 /\ r = - n ; USpec := Z.abs_spec|}. -Add UnOpSpec ZabsSpec. +Add Zify UnOpSpec ZabsSpec. (** Saturate positivity constraints *) @@ -487,7 +487,7 @@ Instance SatProd : Saturate Z.mul := PRes := fun r => 0 <= r; SatOk := Z.mul_nonneg_nonneg |}. -Add Saturate SatProd. +Add Zify Saturate SatProd. Instance SatProdPos : Saturate Z.mul := {| @@ -496,7 +496,7 @@ Instance SatProdPos : Saturate Z.mul := PRes := fun r => 0 < r; SatOk := Z.mul_pos_pos |}. -Add Saturate SatProdPos. +Add Zify Saturate SatProdPos. Lemma pow_pos_strict : forall a b, @@ -515,4 +515,4 @@ Instance SatPowPos : Saturate Z.pow := PRes := fun r => 0 < r; SatOk := pow_pos_strict |}. -Add Saturate SatPowPos. +Add Zify Saturate SatPowPos. |