From 8d4037118be3ffb7259ed03a5ba4ae09d9b51f4a Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Mon, 10 Oct 2016 16:54:37 +0200 Subject: Some proofs for the Int63 glue --- src/Misc.v | 8 +- src/versions/standard/Array/PArray_standard.v | 11 +- src/versions/standard/Int63/Int63Axioms_standard.v | 85 ++++++++++--- src/versions/standard/Int63/Int63Native_standard.v | 35 +++--- src/versions/standard/Int63/Int63Op_standard.v | 40 +++--- .../standard/Int63/Int63Properties_standard.v | 139 +++++++++++---------- src/versions/standard/Int63/Int63_standard.v | 7 +- 7 files changed, 199 insertions(+), 126 deletions(-) diff --git a/src/Misc.v b/src/Misc.v index a7ba19d..2aa6b0e 100644 --- a/src/Misc.v +++ b/src/Misc.v @@ -387,7 +387,7 @@ Proof. intros;ring_simplify ([|i|] - 1 + 1)%Z;rewrite of_to_Z;auto. assert (i < length t - 1 = true). rewrite ltb_spec. rewrite leb_spec in H0. replace (length t - 2) with (length t - 1 - 1) in H0 by ring. rewrite to_Z_sub_1_diff in H0; [omega| ]. intro H4. assert (H5: [|length t - 1|] = 0%Z) by (rewrite H4; auto). assert (H6: 1 < length t = true) by (rewrite ltb_negb_geb, Heq; auto). rewrite ltb_spec in H6. change ([|1|]) with (1%Z) in H6. rewrite to_Z_sub_1_diff in H5; [omega| ]. intro H7. assert (H8: [|length t|] = 0%Z) by (rewrite H7; auto). omega. - apply H1;trivial. + apply H1; [trivial| ]. rewrite <-(to_Z_add_1 _ _ H4), of_to_Z in H3;auto. symmetry. rewrite eqb_false_spec. intro H. rewrite H in Heq. discriminate. Qed. @@ -1002,3 +1002,9 @@ End Forall2. Implicit Arguments forallb2 [A B]. + +(* + Local Variables: + coq-load-path: ((rec "." "SMTCoq")) + End: +*) diff --git a/src/versions/standard/Array/PArray_standard.v b/src/versions/standard/Array/PArray_standard.v index 373e8af..2cc8366 100644 --- a/src/versions/standard/Array/PArray_standard.v +++ b/src/versions/standard/Array/PArray_standard.v @@ -21,9 +21,6 @@ Require Import Int31. Require Export Int63. -(* Require Export Int63. *) -(* Require Import Ring63. *) -(* Require Int63Lib. *) Require FMapAVL. Local Open Scope int63_scope. @@ -270,7 +267,6 @@ Proof. assert (i < length t = true). rewrite ltb_leb_sub1;auto. apply H;trivial. - rewrite <-(to_Z_add_1 _ _ H4), of_to_Z in H3;auto. exact H1. Qed. @@ -394,3 +390,10 @@ Proof. intros i _; rewrite <- (reflect_iff _ _ (HA _ _));trivial. rewrite <- not_true_iff_false, <- (reflect_iff _ _ (HA _ _)) in H0;apply H0;trivial. Qed. + + +(* + Local Variables: + coq-load-path: ((rec "../../.." "SMTCoq")) + End: +*) 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: +*) diff --git a/src/versions/standard/Int63/Int63Native_standard.v b/src/versions/standard/Int63/Int63Native_standard.v index c833a41..9e5058a 100644 --- a/src/versions/standard/Int63/Int63Native_standard.v +++ b/src/versions/standard/Int63/Int63Native_standard.v @@ -36,13 +36,29 @@ Notation "1" := 1%int31 : int63_scope. Notation "2" := 2%int31 : int63_scope. Notation "3" := 3%int31 : int63_scope. +(* Comparisons *) +Definition eqb := eqb31. +Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope. + +Definition ltb : int -> int -> bool := + fun i j => match compare31 i j with | Lt => true | _ => false end. +Notation "m < n" := (ltb m n) : int63_scope. + +Definition leb : int -> int -> bool := + fun i j => match compare31 i j with | Gt => false | _ => true end. +Notation "m <= n" := (leb m n) : int63_scope. + + +Lemma eqb_correct : forall i j, (i==j)%int = true -> i = j. +Proof. exact eqb31_correct. Qed. + (* Logical operations *) Definition lsl : int -> int -> int := fun i j => addmuldiv31 j i 0. Infix "<<" := lsl (at level 30, no associativity) : int63_scope. Definition lsr : int -> int -> int := - fun i j => addmuldiv31 (31-j)%int31 0 i. + fun i j => if (j < 31%int31)%int then addmuldiv31 (31-j)%int31 0 i else 0%int31. Infix ">>" := lsr (at level 30, no associativity) : int63_scope. Definition land : int -> int -> int := land31. @@ -79,23 +95,6 @@ Definition modulo : int -> int -> int := fun i j => let (_,r) := div31 i j in r. Notation "n '\%' m" := (modulo n m) (at level 40, left associativity) : int63_scope. -(* Comparisons *) -Definition eqb := eqb31. -Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope. - -Definition ltb : int -> int -> bool := - fun i j => match compare31 i j with | Lt => true | _ => false end. -Notation "m < n" := (ltb m n) : int63_scope. - -Definition leb : int -> int -> bool := - fun i j => match compare31 i j with | Gt => false | _ => true end. -Notation "m <= n" := (leb m n) : int63_scope. - - -(* TODO: fill this proof (should be in the stdlib) *) -Lemma eqb_correct : forall i j, (i==j)%int = true -> i = j. -Admitted. - (* Iterators *) diff --git a/src/versions/standard/Int63/Int63Op_standard.v b/src/versions/standard/Int63/Int63Op_standard.v index f34260c..d0df921 100644 --- a/src/versions/standard/Int63/Int63Op_standard.v +++ b/src/versions/standard/Int63/Int63Op_standard.v @@ -154,23 +154,24 @@ Definition existsb (f:int -> bool) from to := (* Definition to_Z := to_Z_rec size. *) Definition to_Z := phi. +Definition of_Z := phi_inv. + +(* Fixpoint of_pos_rec (n:nat) (p:positive) := *) +(* match n, p with *) +(* | O, _ => 0 *) +(* | S n, xH => 1 *) +(* | S n, xO p => (of_pos_rec n p) << 1 *) +(* | S n, xI p => (of_pos_rec n p) << 1 lor 1 *) +(* end. *) -Fixpoint of_pos_rec (n:nat) (p:positive) := - match n, p with - | O, _ => 0 - | S n, xH => 1 - | S n, xO p => (of_pos_rec n p) << 1 - | S n, xI p => (of_pos_rec n p) << 1 lor 1 - end. - -Definition of_pos := of_pos_rec size. +(* Definition of_pos := of_pos_rec size. *) -Definition of_Z z := - match z with - | Zpos p => of_pos p - | Z0 => 0 - | Zneg p => - (of_pos p) - end. +(* Definition of_Z z := *) +(* match z with *) +(* | Zpos p => of_pos p *) +(* | Z0 => 0 *) +(* | Zneg p => - (of_pos p) *) +(* end. *) (** Gcd **) Fixpoint gcd_rec (guard:nat) (i j:int) {struct guard} := @@ -250,7 +251,7 @@ Definition cast_digit d1 d2 : | _, _ => None end. -(* TODO: improve this definition... *) +(* May need to improve this definition, but no reported efficiency problem for the moment *) Definition cast i j : option (forall P : int -> Type, P i -> P j) := match i, j return option (forall P : int -> Type, P i -> P j) with @@ -331,3 +332,10 @@ Definition eqo i j : option (i = j) := | Some k => Some (k (fun j => i = j) (refl_equal i)) | None => None end. + + +(* + Local Variables: + coq-load-path: ((rec "../../.." "SMTCoq")) + End: +*) diff --git a/src/versions/standard/Int63/Int63Properties_standard.v b/src/versions/standard/Int63/Int63Properties_standard.v index f6557fa..9b9649f 100644 --- a/src/versions/standard/Int63/Int63Properties_standard.v +++ b/src/versions/standard/Int63/Int63Properties_standard.v @@ -1955,77 +1955,78 @@ Proof. Qed. -Lemma of_pos_spec : forall p, [|of_pos p|] = Zpos p mod wB. -Proof. - unfold of_pos. - unfold wB. - assert (forall k, (k <= size)%nat -> - forall p : positive, [|of_pos_rec k p|] = Zpos p mod 2 ^ Z_of_nat k). - induction k. - simpl;intros;rewrite to_Z_0,Zmod_1_r;trivial. -Opaque Z_of_nat. - destruct p;simpl. - destruct (bit_add_or (of_pos_rec k p << 1) 1) as (H1, _). - rewrite <- H1;clear H1. - change (Zpos p~1) with (2*(Zpos p) + 1)%Z. - rewrite add_spec,lsl_spec, IHk, to_Z_1. - rewrite Zmult_comm, Zplus_mod_idemp_l, Zmod_small. - change 2%Z with (2^1)%Z. - rewrite Zmod_distr. - rewrite inj_S, Zpower_Zsucc;[ | apply Zle_0_nat]. - repeat change (2^1)%Z with 2%Z. - rewrite Zmult_mod_distr_l;trivial. -Transparent Z_of_nat. - rewrite inj_S;omega. - discriminate. - split;[discriminate | trivial]. - compute;trivial. - assert (W:0 <= Zpos p mod 2 ^ Z_of_nat k < 2 ^ Z_of_nat k). - apply Z.mod_pos_bound;auto with zarith. - change (2^1)%Z with 2%Z;split;try omega. - apply Zlt_le_trans with (2 ^ Z_of_nat (S k)). - rewrite inj_S, Zpower_Zsucc;omega. - unfold wB;apply Zpower_le_monotone;auto with zarith. - split;auto using inj_le with zarith. - auto with zarith. - intros n H1 H2. - rewrite bit_1, eqb_spec in H2;subst. - rewrite bit_lsl in H1;discriminate H1. - - change (Zpos p~0) with (2*(Zpos p))%Z. - rewrite lsl_spec, IHk, to_Z_1. - rewrite Zmult_comm, Zmod_small. - rewrite inj_S, Zpower_Zsucc;[ | apply Zle_0_nat]. - rewrite Zmult_mod_distr_l;trivial. - assert (W:0 <= Zpos p mod 2 ^ Z_of_nat k < 2 ^ Z_of_nat k). - apply Z.mod_pos_bound;auto with zarith. - change (2^1)%Z with 2%Z;split;try omega. - apply Zlt_le_trans with (2 ^ Z_of_nat (S k)). - rewrite inj_S, Zpower_Zsucc;omega. - unfold wB;apply Zpower_le_monotone;auto with zarith. - split;auto using inj_le with zarith. - auto with zarith. - - rewrite to_Z_1, Zmod_small;trivial. - split;auto with zarith. - apply Zpower_gt_1;auto with zarith. - rewrite inj_S;auto with zarith. - - apply H;auto with zarith. -Qed. +(* Lemma of_pos_spec : forall p, [|of_pos p|] = Zpos p mod wB. *) +(* Proof. *) +(* unfold of_pos. *) +(* unfold wB. *) +(* assert (forall k, (k <= size)%nat -> *) +(* forall p : positive, [|of_pos_rec k p|] = Zpos p mod 2 ^ Z_of_nat k). *) +(* induction k. *) +(* simpl;intros;rewrite to_Z_0,Zmod_1_r;trivial. *) +(* Opaque Z_of_nat. *) +(* destruct p;simpl. *) +(* destruct (bit_add_or (of_pos_rec k p << 1) 1) as (H1, _). *) +(* rewrite <- H1;clear H1. *) +(* change (Zpos p~1) with (2*(Zpos p) + 1)%Z. *) +(* rewrite add_spec,lsl_spec, IHk, to_Z_1. *) +(* rewrite Zmult_comm, Zplus_mod_idemp_l, Zmod_small. *) +(* change 2%Z with (2^1)%Z. *) +(* rewrite Zmod_distr. *) +(* rewrite inj_S, Zpower_Zsucc;[ | apply Zle_0_nat]. *) +(* repeat change (2^1)%Z with 2%Z. *) +(* rewrite Zmult_mod_distr_l;trivial. *) +(* Transparent Z_of_nat. *) +(* rewrite inj_S;omega. *) +(* discriminate. *) +(* split;[discriminate | trivial]. *) +(* compute;trivial. *) +(* assert (W:0 <= Zpos p mod 2 ^ Z_of_nat k < 2 ^ Z_of_nat k). *) +(* apply Z.mod_pos_bound;auto with zarith. *) +(* change (2^1)%Z with 2%Z;split;try omega. *) +(* apply Zlt_le_trans with (2 ^ Z_of_nat (S k)). *) +(* rewrite inj_S, Zpower_Zsucc;omega. *) +(* unfold wB;apply Zpower_le_monotone;auto with zarith. *) +(* split;auto using inj_le with zarith. *) +(* auto with zarith. *) +(* intros n H1 H2. *) +(* rewrite bit_1, eqb_spec in H2;subst. *) +(* rewrite bit_lsl in H1;discriminate H1. *) + +(* change (Zpos p~0) with (2*(Zpos p))%Z. *) +(* rewrite lsl_spec, IHk, to_Z_1. *) +(* rewrite Zmult_comm, Zmod_small. *) +(* rewrite inj_S, Zpower_Zsucc;[ | apply Zle_0_nat]. *) +(* rewrite Zmult_mod_distr_l;trivial. *) +(* assert (W:0 <= Zpos p mod 2 ^ Z_of_nat k < 2 ^ Z_of_nat k). *) +(* apply Z.mod_pos_bound;auto with zarith. *) +(* change (2^1)%Z with 2%Z;split;try omega. *) +(* apply Zlt_le_trans with (2 ^ Z_of_nat (S k)). *) +(* rewrite inj_S, Zpower_Zsucc;omega. *) +(* unfold wB;apply Zpower_le_monotone;auto with zarith. *) +(* split;auto using inj_le with zarith. *) +(* auto with zarith. *) + +(* rewrite to_Z_1, Zmod_small;trivial. *) +(* split;auto with zarith. *) +(* apply Zpower_gt_1;auto with zarith. *) +(* rewrite inj_S;auto with zarith. *) + +(* apply H;auto with zarith. *) +(* Qed. *) Lemma of_Z_spec : forall z, [|of_Z z|] = z mod wB. -Proof. - unfold of_Z;destruct z. - assert (W:= to_Z_bounded 0);rewrite Zmod_small;trivial. - apply of_pos_spec. - rewrite opp_spec, of_pos_spec. - rewrite <- Zmod_opp_opp. - change (- Zpos p)%Z with (Zneg p). - destruct (Z_eq_dec (Zneg p mod wB) 0). - rewrite e, Z_mod_zero_opp_r;trivial. - rewrite Z_mod_nz_opp_r, Zminus_mod, Z_mod_same_full, Zmod_mod, Zminus_0_r, Zmod_mod;trivial. -Qed. +Admitted. (* no more of_pos *) +(* Proof. *) +(* unfold of_Z;destruct z. *) +(* assert (W:= to_Z_bounded 0);rewrite Zmod_small;trivial. *) +(* apply of_pos_spec. *) +(* rewrite opp_spec, of_pos_spec. *) +(* rewrite <- Zmod_opp_opp. *) +(* change (- Zpos p)%Z with (Zneg p). *) +(* destruct (Z_eq_dec (Zneg p mod wB) 0). *) +(* rewrite e, Z_mod_zero_opp_r;trivial. *) +(* rewrite Z_mod_nz_opp_r, Zminus_mod, Z_mod_same_full, Zmod_mod, Zminus_0_r, Zmod_mod;trivial. *) +(* Qed. *) Lemma foldi_cont_Ind : forall A B (P: int -> (A -> B) -> Prop) (f:int -> (A -> B) -> (A -> B)) min max cont, max < max_int = true -> diff --git a/src/versions/standard/Int63/Int63_standard.v b/src/versions/standard/Int63/Int63_standard.v index 865c238..85ee8b7 100644 --- a/src/versions/standard/Int63/Int63_standard.v +++ b/src/versions/standard/Int63/Int63_standard.v @@ -17,8 +17,11 @@ (**************************************************************************) -(** Naive software representation of Int63. To improve. Anyway, if you - want efficiency, rather use native-coq. **) +(** Glue with the Int31 library of standard coq, which is linked to + native integers during VM computations. + + CAUTION: The name "Int63" is given for compatibility reasons, but + int31 is used. **) Require Export Ring31. Require Export Int63Native. -- cgit