diff options
Diffstat (limited to 'src/versions/standard/Int63/Int63Axioms_standard.v')
| -rw-r--r-- | src/versions/standard/Int63/Int63Axioms_standard.v | 85 |
1 files changed, 69 insertions, 16 deletions
diff --git a/src/versions/standard/Int63/Int63Axioms_standard.v b/src/versions/standard/Int63/Int63Axioms_standard.v index 83969ba..7e89ef6 100644 --- a/src/versions/standard/Int63/Int63Axioms_standard.v +++ b/src/versions/standard/Int63/Int63Axioms_standard.v @@ -17,15 +17,12 @@ (**************************************************************************) -(* Add LoadPath "." as SMTCoq.versions.standard.Int63. *) Require Import Bvector. Require Export BigNumPrelude. -(* Require Import Int63Lib. *) -Require Import Int31. +Require Import Int31 Cyclic31. Require Export Int63Native. -(* Require Export SMTCoq.versions.standard.Int63.Int63Native. *) Require Export Int63Op. -(* Require Export SMTCoq.versions.standard.Int63.Int63Op. *) +Require Import Psatz. Definition wB := (2^(Z_of_nat size)). @@ -45,14 +42,70 @@ Local Open Scope Z_scope. (* Bijection : int63 <-> Bvector size *) -Axiom to_Z_inj : forall x y, [|x|] = [|y|] -> x = y. +Lemma to_Z_inj : forall x y, [|x|] = [|y|] -> x = y. +Proof Ring31.Int31_canonic. -Axiom of_to_Z : forall x, of_Z ([|x|]) = x. +Lemma of_to_Z : forall x, of_Z ([|x|]) = x. +Proof. exact phi_inv_phi. Qed. + +(* Comparisons *) +Axiom eqb_refl : forall x, (x == x)%int = true. + +Axiom ltb_spec : forall x y, (x < y)%int = true <-> [|x|] < [|y|]. + +Axiom leb_spec : forall x y, (x <= y)%int = true <-> [|x|] <= [|y|]. (** Specification of logical operations *) -Axiom lsl_spec : forall x p, [| x << p |] = [|x|] * 2^[|p|] mod wB. +Lemma lsl_spec_alt p : + forall x, [| addmuldiv31_alt p x 0 |] = ([|x|] * 2^(Z.of_nat p)) mod wB. +Proof. + induction p as [ |p IHp]; simpl; intro x. + - rewrite Z.mul_1_r. symmetry. apply Zmod_small. apply phi_bounded. + - rewrite IHp, phi_twice, Zmult_mod_idemp_l, Z.double_spec, + Z.mul_comm, Z.mul_assoc, Z.mul_comm, + Z.pow_pos_fold, Zpos_P_of_succ_nat, <- Z.add_1_r, Z.pow_add_r. + * reflexivity. + * apply Zle_0_nat. + * exact Z.le_0_1. +Qed. + +Lemma lsl_spec x p : [| x << p |] = ([|x|] * 2^[|p|]) mod wB. +Proof. + unfold lsl. + rewrite addmuldiv31_equiv, lsl_spec_alt, Nat2Z.inj_abs_nat, Z.abs_eq. + - reflexivity. + - now destruct (phi_bounded p). +Qed. + +Lemma div_greater (p x:int) (H:Z.of_nat Int31.size <= [|p|]) : [|x|] / 2 ^ [|p|] = 0. +Proof. + apply Z.div_small. destruct (phi_bounded x) as [H1 H2]. split; auto. + apply (Z.lt_le_trans _ _ _ H2). apply Z.pow_le_mono_r; auto. + exact Z.lt_0_2. +Qed. + +Lemma lsr_spec x p : [|x >> p|] = [|x|] / 2 ^ [|p|]. +Proof. + unfold lsr. case_eq (p < 31%int31)%int; intro Heq. + - assert (H : [|31%int31 - p|] = 31 - [|p|]). + * rewrite spec_sub. rewrite Zmod_small; auto. + split. + + rewrite ltb_spec in Heq. assert (forall x y, x < y -> 0 <= y - x) by (intros;lia); auto. + + assert (H:forall x y z, 0 <= y /\ x < z -> x - y < z) by (intros;lia). + apply H. destruct (phi_bounded p). destruct (phi_bounded (31%int31)). split; auto. + * rewrite spec_add_mul_div. + + rewrite Z.add_0_l. change (phi (31%int31 - p)) with [|31%int31 - p|]. rewrite H. replace (31 - (31 - [|p|])) with [|p|] by ring. apply Zmod_small. split. + ++ apply div_le_0. now destruct (phi_bounded x). + ++ apply div_lt. apply phi_bounded. + + change (phi (31%int31 - p)) with [|31%int31 - p|]. rewrite H. assert (forall x y, 0 <= y -> x - y <= x) by (intros;lia). apply H0. now destruct (phi_bounded p). + - rewrite div_greater; auto. + destruct (Z.le_gt_cases [|31%int31|] [|p|]); auto. + rewrite <- ltb_spec in H. rewrite H in Heq. discriminate. +Qed. + + + -Axiom lsr_spec : forall x p, [|x >> p|] = [|x|] / 2 ^ [|p|]. Axiom land_spec: forall x y i , bit (x land y) i = bit x i && bit y i. @@ -79,13 +132,6 @@ Axiom div_spec : forall x y, [|x / y|] = [|x|] / [|y|]. Axiom mod_spec : forall x y, [|x \% y|] = [|x|] mod [|y|]. -(* Comparisons *) -Axiom eqb_refl : forall x, (x == x)%int = true. - -Axiom ltb_spec : forall x y, (x < y)%int = true <-> [|x|] < [|y|]. - -Axiom leb_spec : forall x y, (x <= y)%int = true <-> [|x|] <= [|y|]. - (** Iterators *) Axiom foldi_cont_gt : forall A B f from to cont, @@ -140,3 +186,10 @@ Axiom diveucl_21_spec : forall a1 a2 b, Axiom addmuldiv_def_spec : forall p x y, addmuldiv p x y = addmuldiv_def p x y. + + +(* + Local Variables: + coq-load-path: ((rec "../../.." "SMTCoq")) + End: +*) |