Some proofs for the Int63 glue

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.