prove an admit in ArithmeticSynthesisTest

3 files changed, 145 insertions, 144 deletions

diff --git a/src/Specific/ArithmeticSynthesisTest.v b/src/Specific/ArithmeticSynthesisTest.v
index a2e1442a4..71100cdcf 100644
--- a/src/Specific/ArithmeticSynthesisTest.v
+++ b/src/Specific/ArithmeticSynthesisTest.v
@@ -6,6 +6,7 @@ Require Import Crypto.Arithmetic.Saturated.Freeze.
 Require Import (*Crypto.Util.Tactics*) Crypto.Util.Decidable.
 Require Import Crypto.Util.LetIn Crypto.Util.ZUtil Crypto.Util.Tactics.
 Require Crypto.Util.Tuple.
+Require Import Crypto.Util.QUtil.
 Local Notation tuple := Tuple.tuple.
 Local Open Scope list_scope.
 Local Open Scope Z_scope.
@@ -24,16 +25,18 @@ Section Ops51.
   Definition bitwidth := 64.
   Definition s : Z := 2^255.
   Definition c : list B.limb := [(1, 19)].
-  Definition coef_div_modulus : nat := 2. (* add 2*modulus before subtracting *)
   Definition carry_chain1 := Eval vm_compute in (seq 0 (pred sz)).
-  Definition carry_chain2 := ([0;1])%nat.
-  Definition a24 := 121665%Z.
+  Definition carry_chain2 := [0;1]%nat.
 
+  Definition a24 := 121665%Z.
+  Definition coef_div_modulus : nat := 2. (* add 2*modulus before subtracting *)
   (* These definitions are inferred from those above *)
   Definition m := Eval vm_compute in Z.to_pos (s - Associational.eval c). (* modulus *)
-  Definition wt := fun i : nat =>
-                     let si := Z.log2 s * i in
-                     2 ^ ((si/sz) + (if dec ((si/sz)*sz=si) then 0 else 1)).
+  Section wt.
+    Import QArith Qround.
+    Local Coercion QArith_base.inject_Z : Z >-> Q.
+    Definition wt (i:nat) : Z := 2^Qceiling((Z.log2_up m/sz)*i).
+  End wt.
   Definition sz2 := Eval vm_compute in ((sz * 2) - 1)%nat.
   Definition m_enc :=
     Eval vm_compute in (Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (s-Associational.eval c)).
@@ -45,44 +48,15 @@ Section Ops51.
          | S n => addm (Positional.add_cps wt acc m_enc id) n
         end) (Positional.zeros sz) coef_div_modulus).
   Definition coef_mod : mod_eq m (Positional.eval (n:=sz) wt coef) 0 := eq_refl.
-
   Lemma sz_nonzero : sz <> 0%nat. Proof. vm_decide. Qed.
   Lemma wt_nonzero i : wt i <> 0.
-  Proof.
-    apply Z.pow_nonzero; zero_bounds; try break_match; vm_decide.
-  Qed.
-
-  Lemma wt_divides_chain1 i (H:In i carry_chain1) : wt (S i) / wt i <> 0.
-  Proof.
-    cbv [In carry_chain1] in H.
-    repeat match goal with H : _ \/ _ |- _ => destruct H end;
-      try (exfalso; assumption); subst; try vm_decide.
-  Qed.
-  Lemma wt_divides_chain2 i (H:In i carry_chain2) : wt (S i) / wt i <> 0.
-  Proof.
-    cbv [In carry_chain2] in H.
-    repeat match goal with H : _ \/ _ |- _ => destruct H end;
-      try (exfalso; assumption); subst; try vm_decide.
-  Qed.
-  Lemma wt_divides_full i : wt (S i) / wt i <> 0.
-  Proof.
-    cbv [wt].
-    match goal with |- _ ^ ?x / _ ^ ?y <> _ => assert (0 <= y <= x) end.
-    { rewrite Nat2Z.inj_succ.
-      split; try break_match; ring_simplify;
-      repeat match goal with
-             | _ => apply Z.div_le_mono; try vm_decide; [ ]
-             | _ => apply Z.mul_le_mono_nonneg_l; try vm_decide; [ ]
-             | _ => apply Z.add_le_mono; try vm_decide; [ ]
-             | |- ?x <= ?y + 1 => assert (x <= y); [|omega]
-             | |- ?x + 1 <= ?y => rewrite <- Z.div_add by vm_decide
-             | _ => progress zero_bounds
-             | _ => progress ring_simplify
-             | _ => vm_decide
-             end. }
-    break_match; rewrite <-Z.pow_sub_r by omega;
-      apply Z.pow_nonzero; omega.
-  Qed.
+  Proof. eapply pow_ceil_mul_nat_nonzero; vm_decide. Qed.
+  Lemma wt_divides i : wt (S i) / wt i > 0.
+  Proof. apply pow_ceil_mul_nat_divide; vm_decide. Qed.
+  Lemma wt_divides' i : wt (S i) / wt i <> 0.
+  Proof. symmetry; apply Z.lt_neq, Z.gt_lt_iff, wt_divides. Qed.
+  Definition wt_divides_chain1 i (H:In i carry_chain1) : wt (S i) / wt i <> 0 := wt_divides' i.
+  Definition wt_divides_chain2 i (H:In i carry_chain2) : wt (S i) / wt i <> 0 := wt_divides' i.
 
   Local Ltac solve_constant_sig :=
     lazymatch goal with
@@ -235,20 +209,10 @@ Section Ops51.
 
   Section PreFreeze.
     Lemma wt_pos i : wt i > 0.
-    Proof.
-        apply Z.lt_gt.
-        apply Z.pow_pos_nonneg; zero_bounds; try break_match; vm_decide.
-    Qed.
+    Proof. eapply pow_ceil_mul_nat_pos; vm_decide. Qed.
 
     Lemma wt_multiples i : wt (S i) mod (wt i) = 0.
-    Admitted.
-
-    Lemma wt_divides_full_pos i : wt (S i) / wt i > 0.
-    Proof.
-        pose proof (wt_divides_full i).
-        apply Z.div_positive_gt_0; auto using wt_pos.
-        apply wt_multiples.
-    Qed.
+    Proof. apply pow_ceil_mul_nat_multiples; vm_decide. Qed.
   End PreFreeze.
 
   Hint Opaque freeze : uncps.
@@ -263,7 +227,7 @@ Section Ops51.
   Proof.
     eexists; cbv beta zeta; intros a ?.
     pose proof wt_nonzero. pose proof wt_pos.
-    pose proof div_mod. pose proof wt_divides_full_pos.
+    pose proof div_mod. pose proof wt_divides.
     pose proof wt_multiples.
     pose proof div_correct. pose proof modulo_correct.
     let x := constr:(freeze (n:=sz) wt (Z.ones bitwidth) m_enc a) in
@@ -299,7 +263,7 @@ Section Ops51.
          (Positional.Fdecode_Fencode_id
             (sz_nonzero := sz_nonzero)
             (div_mod := div_mod)
-            wt eq_refl wt_nonzero wt_divides_full)
+            wt eq_refl wt_nonzero wt_divides')
          (Positional.eq_Feq_iff wt)
          (proj2_sig add_sig)
          (proj2_sig sub_sig)
diff --git a/src/Specific/Karatsuba.v b/src/Specific/Karatsuba.v
index 09e014667..7d329a613 100644
--- a/src/Specific/Karatsuba.v
+++ b/src/Specific/Karatsuba.v
@@ -9,6 +9,7 @@ Require Import Crypto.Util.LetIn Crypto.Util.ZUtil Crypto.Util.Tactics.
 Require Import Crypto.Arithmetic.Karatsuba.
 Require Crypto.Util.Tuple.
 Require Import Crypto.Util.IdfunWithAlt.
+Require Import Crypto.Util.QUtil.
 Local Notation tuple := Tuple.tuple.
 Local Open Scope list_scope.
 Local Open Scope Z_scope.
@@ -27,17 +28,18 @@ Section Ops51.
   Definition bitwidth := 64.
   Definition s : Z := 2^448.
   Definition c : list B.limb := [(1, 1); (2^224, 1)].
-  Definition coef_div_modulus : nat := 2. (* add 2*modulus before subtracting *)
   Definition carry_chain1 := [3;7]%nat.
   Definition carry_chain2 := [0;4;1;5;2;6;3;7]%nat.
   Definition carry_chain3 := [4;0]%nat.
-  Definition a24 := 121665%Z.
 
+  Definition coef_div_modulus : nat := 2. (* add 2*modulus before subtracting *)
   (* These definitions are inferred from those above *)
   Definition m := Eval vm_compute in Z.to_pos (s - Associational.eval c). (* modulus *)
-  Definition wt := fun i : nat =>
-                     let si := Z.log2 s * i in
-                     2 ^ ((si/sz) + (if dec ((si/sz)*sz=si) then 0 else 1)).
+  Section wt.
+    Import QArith Qround.
+    Local Coercion QArith_base.inject_Z : Z >-> Q.
+    Definition wt (i:nat) : Z := 2^Qceiling((Z.log2_up m/sz)*i).
+  End wt.
   Definition sz2 := Eval vm_compute in ((sz * 2) - 1)%nat.
   Definition m_enc :=
     Eval vm_compute in (Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (s-Associational.eval c)).
@@ -49,50 +51,16 @@ Section Ops51.
          | S n => addm (Positional.add_cps wt acc m_enc id) n
         end) (Positional.zeros sz) coef_div_modulus).
   Definition coef_mod : mod_eq m (Positional.eval (n:=sz) wt coef) 0 := eq_refl.
-
   Lemma sz_nonzero : sz <> 0%nat. Proof. vm_decide. Qed.
   Lemma wt_nonzero i : wt i <> 0.
-  Proof.
-    apply Z.pow_nonzero; zero_bounds; try break_match; vm_decide.
-  Qed.
-
-  Lemma wt_divides_chain1 i (H:In i carry_chain1) : wt (S i) / wt i <> 0.
-  Proof.
-    cbv [In carry_chain1] in H.
-    repeat match goal with H : _ \/ _ |- _ => destruct H end;
-      try (exfalso; assumption); subst; try vm_decide.
-  Qed.
-  Lemma wt_divides_chain2 i (H:In i carry_chain2) : wt (S i) / wt i <> 0.
-  Proof.
-    cbv [In carry_chain2] in H.
-    repeat match goal with H : _ \/ _ |- _ => destruct H end;
-      try (exfalso; assumption); subst; try vm_decide.
-  Qed.
-  Lemma wt_divides_chain3 i (H:In i carry_chain3) : wt (S i) / wt i <> 0.
-  Proof.
-    cbv [In carry_chain3] in H.
-    repeat match goal with H : _ \/ _ |- _ => destruct H end;
-      try (exfalso; assumption); subst; try vm_decide.
-  Qed.
-  Lemma wt_divides_full i : wt (S i) / wt i <> 0.
-  Proof.
-    cbv [wt].
-    match goal with |- _ ^ ?x / _ ^ ?y <> _ => assert (0 <= y <= x) end.
-    { rewrite Nat2Z.inj_succ.
-      split; try break_match; ring_simplify;
-      repeat match goal with
-             | _ => apply Z.div_le_mono; try vm_decide; [ ]
-             | _ => apply Z.mul_le_mono_nonneg_l; try vm_decide; [ ]
-             | _ => apply Z.add_le_mono; try vm_decide; [ ]
-             | |- ?x <= ?y + 1 => assert (x <= y); [|omega]
-             | |- ?x + 1 <= ?y => rewrite <- Z.div_add by vm_decide
-             | _ => progress zero_bounds
-             | _ => progress ring_simplify
-             | _ => vm_decide
-             end. }
-    break_match; rewrite <-Z.pow_sub_r by omega;
-      apply Z.pow_nonzero; omega.
-  Qed.
+  Proof. eapply pow_ceil_mul_nat_nonzero; vm_decide. Qed.
+  Lemma wt_divides i : wt (S i) / wt i > 0.
+  Proof. apply pow_ceil_mul_nat_divide; vm_decide. Qed.
+  Lemma wt_divides' i : wt (S i) / wt i <> 0.
+  Proof. symmetry; apply Z.lt_neq, Z.gt_lt_iff, wt_divides. Qed.
+  Definition wt_divides_chain1 i (H:In i carry_chain1) : wt (S i) / wt i <> 0 := wt_divides' i.
+  Definition wt_divides_chain2 i (H:In i carry_chain2) : wt (S i) / wt i <> 0 := wt_divides' i.
+  Definition wt_divides_chain3 i (H:In i carry_chain3) : wt (S i) / wt i <> 0 := wt_divides' i.
 
   Local Ltac solve_constant_sig :=
     lazymatch goal with
@@ -114,12 +82,6 @@ Section Ops51.
     solve_constant_sig.
   Defined.
 
-  Definition a24_sig :
-    { a24t : Z^sz | Positional.Fdecode (m:=m) wt a24t = F.of_Z m a24 }.
-  Proof.
-    solve_constant_sig.
-  Defined.
-
   Definition add_sig :
     { add : (Z^sz -> Z^sz -> Z^sz)%type |
                forall a b : Z^sz,
@@ -293,24 +255,11 @@ Ltac basesystem_partial_evaluation_RHS :=
     solve_op_F wt x. reflexivity.
   Defined.
 
-  Section PreFreeze.
-    Lemma wt_pos i : wt i > 0.
-    Proof.
-        apply Z.lt_gt.
-        apply Z.pow_pos_nonneg; zero_bounds; try break_match; vm_decide.
-    Qed.
-
-    Lemma wt_multiples i : wt (S i) mod (wt i) = 0.
-    Admitted.
-
-    Lemma wt_divides_full_pos i : wt (S i) / wt i > 0.
-    Proof.
-        pose proof (wt_divides_full i).
-        apply Z.div_positive_gt_0; auto using wt_pos.
-        apply wt_multiples.
-    Qed.
-  End PreFreeze.
-
+  (* [freeze] preconditions *)
+  Lemma wt_pos i : wt i > 0.
+  Proof. eapply pow_ceil_mul_nat_pos; vm_decide. Qed.
+  Lemma wt_multiples i : wt (S i) mod (wt i) = 0.
+  Proof. apply pow_ceil_mul_nat_multiples; vm_decide. Qed.
   Hint Opaque freeze : uncps.
   Hint Rewrite freeze_id : uncps.
 
@@ -323,7 +272,7 @@ Ltac basesystem_partial_evaluation_RHS :=
   Proof.
     eexists; cbv beta zeta; intros.
     pose proof wt_nonzero. pose proof wt_pos.
-    pose proof div_mod. pose proof wt_divides_full_pos.
+    pose proof div_mod. pose proof wt_divides.
     pose proof wt_multiples.
     pose proof div_correct. pose proof modulo_correct.
     let x := constr:(freeze (n:=sz) wt (Z.ones bitwidth) m_enc a) in
@@ -359,7 +308,7 @@ Ltac basesystem_partial_evaluation_RHS :=
          (Positional.Fdecode_Fencode_id
             (sz_nonzero := sz_nonzero)
             (div_mod := div_mod)
-            wt eq_refl wt_nonzero wt_divides_full)
+            wt eq_refl wt_nonzero wt_divides')
          (Positional.eq_Feq_iff wt)
          (proj2_sig add_sig)
          (proj2_sig sub_sig)
diff --git a/src/Util/QUtil.v b/src/Util/QUtil.v
index 453cad308..96bf34c3b 100644
--- a/src/Util/QUtil.v
+++ b/src/Util/QUtil.v
@@ -1,19 +1,107 @@
 Require Import Coq.ZArith.ZArith Coq.QArith.QArith QArith.Qround.
+Require Import Crypto.Util.Decidable.
+Require Import ZUtil Lia.
 
 Local Open Scope Z_scope.
 
-Lemma pow_ceil_mul_nat_nonzero b f
-      (b_nz:b <> 0)
-      (f_pos:(0 <= f)%Q)
-  : forall i, b^Qceiling (f * inject_Z (Z.of_nat i)) <> 0.
-Proof.
-  intros.
-  eapply Z.pow_nonzero; try omega.
-  rewrite Zle_Qle.
-  eapply Qle_trans; [|eapply Qle_ceiling].
-  eapply Qle_trans; [|eapply (Qmult_le_compat_r 0)]; trivial.
-  cbv; discriminate.
-  apply (Qle_trans _ (inject_Z 0)); [eapply Qle_refl|].
-  rewrite <-Zle_Qle.
-  eapply Zle_0_nat.
-Qed.
\ No newline at end of file
+Lemma Qfloor_le_add a b :  Qfloor a + Qfloor b <= Qfloor (a + b).
+  destruct a as [x y], b as [a b]; cbv [Qceiling Qfloor Qplus Qopp QArith_base.Qden QArith_base.Qnum].
+  Z.div_mod_to_quot_rem; nia.
+Qed.
+
+Lemma Qceiling_le_add a b : Qceiling (a + b) <= Qceiling a + Qceiling b.
+  destruct a as [x y], b as [a b]; cbv [Qceiling Qfloor Qplus Qopp QArith_base.Qden QArith_base.Qnum].
+  Z.div_mod_to_quot_rem. nia.
+Qed.
+
+Lemma add_floor_l_le_ceiling a b : Qfloor a + Qceiling b <= Qceiling (a + b).
+  destruct a as [x y], b as [a b]; cbv [Qceiling Qfloor Qplus Qopp QArith_base.Qden QArith_base.Qnum].
+  Z.div_mod_to_quot_rem; nia.
+Qed.
+
+Lemma Zle_floor_ceiling  a : Z.le (Qfloor a) (Qceiling a).
+  pose proof Qle_floor_ceiling.
+  destruct a as [x y]; cbv [Qceiling Qfloor Qplus Qopp QArith_base.Qden QArith_base.Qnum].
+  Z.div_mod_to_quot_rem; nia.
+Qed.
+
+Section pow_ceil_mul_nat.
+  Context b f (b_nz:0 <> b) (f_pos:(0 <= f)%Q).
+  Local Notation wt i := (b^Qceiling (f * inject_Z (Z.of_nat i))) (only parsing).
+
+  Lemma zero_le_ceil_mul_nat i :
+    0 <= Qceiling (f * inject_Z (Z.of_nat i))%Q.
+  Proof.
+    rewrite Zle_Qle.
+    eapply Qle_trans; [|eapply Qle_ceiling].
+    eapply Qle_trans; [|eapply (Qmult_le_compat_r 0)]; trivial.
+    cbv; discriminate.
+    apply (Qle_trans _ (inject_Z 0)); [vm_decide|].
+    change 0%Q with (inject_Z 0).
+    rewrite <-Zle_Qle.
+    eapply Zle_0_nat.
+  Qed.
+
+  Lemma pow_ceil_mul_nat_nonzero
+    : forall i, wt i <> 0.
+  Proof.
+    intros.
+    eapply Z.pow_nonzero; try omega.
+    eapply zero_le_ceil_mul_nat.
+  Qed.
+
+  Lemma pow_ceil_mul_S i :
+    wt (S i) = 
+    (b ^ (Qceiling (f + f * inject_Z (Z.of_nat i)) - Qceiling (f * inject_Z (Z.of_nat i))) * wt i).
+  Proof.
+    rewrite Nat2Z.inj_succ.
+    rewrite <-Z.add_1_l.
+    rewrite inject_Z_plus.
+    change (inject_Z 1) with 1%Q.
+    rewrite Qmult_plus_distr_r, Qmult_1_r.
+    let g := constr:((f * inject_Z (Z.of_nat i))%Q) in
+    replace (Qceiling (f+g)) with ((Qceiling (f+g)-Qceiling g)+Qceiling g) at 1 by omega.
+    rewrite Z.pow_add_r; [reflexivity|eapply Zle_minus_le_0|apply zero_le_ceil_mul_nat].
+    eapply Qceiling_resp_le.
+    rewrite <-Qplus_0_l at 1.
+    eapply Qplus_le_compat;
+      auto with qarith.
+  Qed.
+
+  Lemma pow_ceil_mul_nat_multiples i :
+    wt (S i) mod (wt i) = 0.
+  Proof.
+    rewrite pow_ceil_mul_S, Z_mod_mult; reflexivity.
+  Qed.
+End pow_ceil_mul_nat.
+
+Section pow_ceil_mul_nat2.
+  Context b f (b_pos:0 < b) (f_ge_1:(1 <= f)%Q).
+  Local Notation wt i := (b^Qceiling (f * inject_Z (Z.of_nat i))) (only parsing).
+
+  Lemma pow_ceil_mul_nat_pos
+    : forall i, wt i > 0.
+  Proof.
+    intros.
+    eapply Z.gt_lt_iff.
+    eapply Z.pow_pos_nonneg; [assumption|].
+    eapply zero_le_ceil_mul_nat.
+    eapply (Qle_trans _ 1 _); [vm_decide|assumption].
+  Qed.
+
+  Lemma pow_ceil_mul_nat_divide i :
+    wt (S i) / (wt i) > 0.
+  Proof.
+    rewrite pow_ceil_mul_S.
+    rewrite Z_div_mult_full; [|apply pow_ceil_mul_nat_nonzero].
+    rewrite Z.gt_lt_iff.
+    eapply Z.pow_pos_nonneg; [assumption|].
+    etransitivity; [|eapply Z.sub_le_ge_Proper].
+    2:eapply add_floor_l_le_ceiling.
+    2:eapply Z.ge_le_iff; reflexivity.
+    assert (1 <= Qfloor f); [|omega].
+    change 1%Z with (Qfloor 1).
+    eapply Qfloor_resp_le.
+    all: trivial; try omega; (eapply (Qle_trans _ 1 _); [vm_decide|assumption]).
+  Qed.
+End pow_ceil_mul_nat2.
\ No newline at end of file