From a2f5cc26baca0db087a677196f186ac2f75aa484 Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Thu, 14 May 2020 15:58:23 +0200 Subject: [zify] Add support for Int63.int Update doc/sphinx/addendum/micromega.rst Co-authored-by: Jason Gross Update theories/micromega/ZifyInt63.v Co-authored-by: Jason Gross --- theories/micromega/ZifyInt63.v | 179 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 179 insertions(+) create mode 100644 theories/micromega/ZifyInt63.v (limited to 'theories') diff --git a/theories/micromega/ZifyInt63.v b/theories/micromega/ZifyInt63.v new file mode 100644 index 0000000000..69f3502d8c --- /dev/null +++ b/theories/micromega/ZifyInt63.v @@ -0,0 +1,179 @@ +Require Import ZArith. +Require Import Int63. +Require Import ZifyBool. +Import ZifyClasses. + +Lemma to_Z_bounded : forall x, (0 <= to_Z x < 9223372036854775808)%Z. +Proof. apply to_Z_bounded. Qed. + +Instance Inj_int_Z : InjTyp int Z := + mkinj _ _ to_Z (fun x => 0 <= x < 9223372036854775808)%Z to_Z_bounded. +Add Zify InjTyp Inj_int_Z. + +Instance Op_max_int : CstOp max_int := + { TCst := 9223372036854775807 ; TCstInj := eq_refl }. +Add Zify CstOp Op_max_int. + +Instance Op_digits : CstOp digits := + { TCst := 63 ; TCstInj := eq_refl }. +Add Zify CstOp Op_digits. + +Instance Op_size : CstOp size := + { TCst := 63 ; TCstInj := eq_refl }. +Add Zify CstOp Op_size. + +Instance Op_wB : CstOp wB := + { TCst := 2^63 ; TCstInj := eq_refl }. +Add Zify CstOp Op_wB. + +Lemma ltb_lt : forall n m, + (n (φ n = φ m)%int63. +Proof. + split; intro H. + rewrite H ; reflexivity. + apply to_Z_inj; auto. +Qed. + +Instance Op_eq : BinRel (@eq int) := + {| TR := @eq Z; TRInj := eq_int_inj |}. +Add Zify BinRel Op_eq. + +Instance Op_add : BinOp add := + {| TBOp := fun x y => (x + y) mod 9223372036854775808%Z; TBOpInj := add_spec |}%Z. +Add Zify BinOp Op_add. + +Instance Op_sub : BinOp sub := + {| TBOp := fun x y => (x - y) mod 9223372036854775808%Z; TBOpInj := sub_spec |}%Z. +Add Zify BinOp Op_sub. + +Instance Op_opp : UnOp Int63.opp := + {| TUOp := (fun x => (- x) mod 9223372036854775808)%Z; TUOpInj := (sub_spec 0) |}%Z. +Add Zify UnOp Op_opp. + +Instance Op_oppcarry : UnOp oppcarry := + {| TUOp := (fun x => 2^63 - x - 1)%Z; TUOpInj := oppcarry_spec |}%Z. +Add Zify UnOp Op_oppcarry. + +Instance Op_succ : UnOp succ := + {| TUOp := (fun x => (x + 1) mod 2^63)%Z; TUOpInj := succ_spec |}%Z. +Add Zify UnOp Op_succ. + +Instance Op_pred : UnOp Int63.pred := + {| TUOp := (fun x => (x - 1) mod 2^63)%Z; TUOpInj := pred_spec |}%Z. +Add Zify UnOp Op_pred. + +Instance Op_mul : BinOp mul := + {| TBOp := fun x y => (x * y) mod 9223372036854775808%Z; TBOpInj := mul_spec |}%Z. +Add Zify BinOp Op_mul. + +Instance Op_gcd : BinOp gcd:= + {| TBOp := (fun x y => Zgcd_alt.Zgcdn (2 * 63)%nat y x) ; TBOpInj := to_Z_gcd |}. +Add Zify BinOp Op_gcd. + +Instance Op_mod : BinOp Int63.mod := + {| TBOp := Z.modulo ; TBOpInj := mod_spec |}. +Add Zify BinOp Op_mod. + +Instance Op_subcarry : BinOp subcarry := + {| TBOp := (fun x y => (x - y - 1) mod 2^63)%Z ; TBOpInj := subcarry_spec |}. +Add Zify BinOp Op_subcarry. + +Instance Op_addcarry : BinOp addcarry := + {| TBOp := (fun x y => (x + y + 1) mod 2^63)%Z ; TBOpInj := addcarry_spec |}. +Add Zify BinOp Op_addcarry. + +Instance Op_lsr : BinOp lsr := + {| TBOp := (fun x y => x / 2^ y)%Z ; TBOpInj := lsr_spec |}. +Add Zify BinOp Op_lsr. + +Instance Op_lsl : BinOp lsl := + {| TBOp := (fun x y => (x * 2^ y) mod 2^ 63)%Z ; TBOpInj := lsl_spec |}. +Add Zify BinOp Op_lsl. + +Instance Op_lor : BinOp Int63.lor := + {| TBOp := Z.lor ; TBOpInj := lor_spec' |}. +Add Zify BinOp Op_lor. + +Instance Op_land : BinOp Int63.land := + {| TBOp := Z.land ; TBOpInj := land_spec' |}. +Add Zify BinOp Op_land. + +Instance Op_lxor : BinOp Int63.lxor := + {| TBOp := Z.lxor ; TBOpInj := lxor_spec' |}. +Add Zify BinOp Op_lxor. + +Instance Op_div : BinOp div := + {| TBOp := Z.div ; TBOpInj := div_spec |}. +Add Zify BinOp Op_div. + +Instance Op_bit : BinOp bit := + {| TBOp := Z.testbit ; TBOpInj := bitE |}. +Add Zify BinOp Op_bit. + +Instance Op_of_Z : UnOp of_Z := + { TUOp := (fun x => x mod 9223372036854775808)%Z; TUOpInj := of_Z_spec }. +Add Zify UnOp Op_of_Z. + +Instance Op_to_Z : UnOp to_Z := + { TUOp := fun x => x ; TUOpInj := fun x : int => eq_refl }. +Add Zify UnOp Op_to_Z. + +Instance Op_is_zero : UnOp is_zero := + { TUOp := (Z.eqb 0) ; TUOpInj := is_zeroE }. +Add Zify UnOp Op_is_zero. + +Lemma is_evenE : forall x, + is_even x = Z.even φ (x)%int63. +Proof. + intros. + generalize (is_even_spec x). + rewrite Z_evenE. + destruct (is_even x). + symmetry. apply Z.eqb_eq. auto. + symmetry. apply Z.eqb_neq. congruence. +Qed. + +Instance Op_is_even : UnOp is_even := + { TUOp := Z.even ; TUOpInj := is_evenE }. +Add Zify UnOp Op_is_even. + + + +Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations. -- cgit v1.2.3 From 031af730ae12601127d71b18adfc54d1a94eaaac Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Tue, 7 Jul 2020 10:14:44 +0200 Subject: [zify] Use flag for Z.to_euclidean_division_equations. Update doc/sphinx/addendum/micromega.rst Co-authored-by: Jason Gross Co-authored-by: Jim Fehrle --- theories/micromega/Zify.v | 15 +++++++++++++-- theories/micromega/ZifyInt63.v | 3 +-- theories/omega/PreOmega.v | 2 ++ 3 files changed, 16 insertions(+), 4 deletions(-) (limited to 'theories') diff --git a/theories/micromega/Zify.v b/theories/micromega/Zify.v index 183fd6a914..01cc9ad810 100644 --- a/theories/micromega/Zify.v +++ b/theories/micromega/Zify.v @@ -16,11 +16,22 @@ Ltac zify_pre_hook := idtac. Ltac zify_post_hook := idtac. -Ltac iter_specs := zify_iter_specs. +Ltac zify_convert_to_euclidean_division_equations_flag := constr:(false). + +(** [zify_internal_to_euclidean_division_equations] is bound in [PreOmega] *) +Ltac zify_internal_to_euclidean_division_equations := idtac. + +Ltac zify_to_euclidean_division_equations := + lazymatch zify_convert_to_euclidean_division_equations_flag with + | true => zify_internal_to_euclidean_division_equations + | false => idtac + end. + Ltac zify := intros; zify_pre_hook ; zify_elim_let ; zify_op ; (zify_iter_specs) ; - zify_saturate ; zify_post_hook. + zify_saturate ; + zify_to_euclidean_division_equations ; zify_post_hook. diff --git a/theories/micromega/ZifyInt63.v b/theories/micromega/ZifyInt63.v index 69f3502d8c..27845898aa 100644 --- a/theories/micromega/ZifyInt63.v +++ b/theories/micromega/ZifyInt63.v @@ -175,5 +175,4 @@ Instance Op_is_even : UnOp is_even := Add Zify UnOp Op_is_even. - -Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations. +Ltac Zify.zify_convert_to_euclidean_division_equations_flag ::= constr:(true). diff --git a/theories/omega/PreOmega.v b/theories/omega/PreOmega.v index 506a4108ee..70f25e7243 100644 --- a/theories/omega/PreOmega.v +++ b/theories/omega/PreOmega.v @@ -573,4 +573,6 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *. Require Import ZifyClasses ZifyInst. Require Zify. +Ltac Zify.zify_internal_to_euclidean_division_equations ::= Z.to_euclidean_division_equations. + Ltac zify := Zify.zify. -- cgit v1.2.3