Closed under the global context

2 files changed, 49 insertions, 12 deletions

diff --git a/src/Arithmetic/Saturated/AddSub.v b/src/Arithmetic/Saturated/AddSub.v
index 06836b90c..b8b6ee31a 100644
--- a/src/Arithmetic/Saturated/AddSub.v
+++ b/src/Arithmetic/Saturated/AddSub.v
@@ -207,8 +207,26 @@ Module B.
         Proof. exact (proj2 (sat_sub_divmod n p q)). Qed.
 
         Lemma small_sat_sub n p q : small (snd (@sat_sub n p q)).
-        Admitted.
-
+        Proof.
+          cbv [small UniformWeight.small sat_sub sat_sub_cps chain_op_cps].
+          remember None as c. destruct Heqc. revert c.
+          induction n; intros;
+            repeat match goal with
+                   | p: Z^0 |- _ => destruct p
+                   | _ => progress (cbv [Let_In] in * )
+                   | _ => progress (simpl chain_op'_cps in * )
+                   | _ => progress autorewrite with uncps push_id cancel_pair in H
+                   | H : _ |- _ => rewrite to_list_append in H;
+                                     simpl In in H 
+                   | H : _ \/ _ |- _ => destruct H 
+                   | _ => contradiction
+                   end.
+          { subst x.
+            destruct c; rewrite ?Z.sub_with_get_borrow_full_mod,
+                        ?Z.sub_get_borrow_full_mod;
+            apply Z.mod_pos_bound; omega. }
+          {  apply IHn in H. assumption. }
+        Qed.
       End AddSub.
     End Positional.
   End Positional.
diff --git a/src/Arithmetic/Saturated/MontgomeryAPI.v b/src/Arithmetic/Saturated/MontgomeryAPI.v
index 7e755e64d..092630eab 100644
--- a/src/Arithmetic/Saturated/MontgomeryAPI.v
+++ b/src/Arithmetic/Saturated/MontgomeryAPI.v
@@ -345,30 +345,43 @@ Section API.
         apply Z.mod_pos_bound, Z.gt_lt, bound_pos. }
     Qed.
 
+    Lemma small_left_append {n} b x :
+      0 <= x < bound -> small b -> small (@left_append _ n x b).
+    Proof.
+      intros.
+      cbv [small].
+      setoid_rewrite Tuple.to_list_left_append.
+      setoid_rewrite in_app_iff.
+      intros y HIn; destruct HIn as [HIn|[]]; (contradiction||omega||eauto).
+    Qed.
+
     Lemma small_add n a b :
       (2 <= bound) ->
       small a -> small b -> small (@add n a b).
     Proof.
       intros.
-      cbv [add add_cps small]; autorewrite with uncps push_id in *.
+      cbv [add add_cps]; autorewrite with uncps push_id in *.
       pose proof @B.Positional.small_sat_add bound ltac:(omega) _ a b.
-      setoid_rewrite Tuple.to_list_left_append.
-      setoid_rewrite in_app_iff.
-      intros x HIn; destruct HIn as [HIn|[]]; (contradiction||omega||eauto); [].
-      subst x.
+      eapply small_left_append; eauto.
       rewrite @B.Positional.sat_add_div by omega.
       repeat match goal with H:_|-_=> unique pose proof (eval_small _ _ H) end.
       cbv [eval] in *; Z.div_mod_to_quot_rem; nia.
     Qed.
 
+    Lemma small_join0 {n} b : small b -> small (@join0 n b).
+    Proof.
+      cbv [join0 join0_cps]; autorewrite with uncps push_id in *.
+      eapply small_left_append; omega.
+    Qed.
+
     Lemma small_add_S1 n a b :
       (2 <= bound) ->
       small a -> small b -> small (@add_S1 n a b).
     Proof.
-      intros. pose_all.
-      cbv [add_cps add add_S1 Let_In].
-      (*apply Positional.small_sat_add.*)
-    Admitted.
+      intros.
+      cbv [add_S1 add_S1_cps Let_In]; autorewrite with uncps push_id in *.
+      eauto using small_add, small_join0.
+    Qed.
 
     Lemma small_add_S2 n a b :
       (2 <= bound) ->
@@ -556,7 +569,13 @@ Section API.
            (psmall : small p) (qsmall : small q) :
       0 <= eval p < eval q + uweight bound n ->
       small (conditional_sub p q).
-    Admitted.
+    Proof.
+      intros.
+      cbv [conditional_sub conditional_sub_cps]; autorewrite with uncps push_id.
+      eapply small_drop_high.
+      rewrite map2_zselect; break_match; [|assumption].
+      eauto using @B.Positional.small_sat_sub with omega.
+    Qed.
 
     Lemma eval_scmul n a v : small v -> 0 <= a < bound ->
       eval (@scmul n a v) = a * eval v.