Finish related_bounds_t_map1_tuple2

2 files changed, 114 insertions, 29 deletions

diff --git a/src/Reflection/Z/Interpretations.v b/src/Reflection/Z/Interpretations.v
index 068c33a24..06727225e 100644
--- a/src/Reflection/Z/Interpretations.v
+++ b/src/Reflection/Z/Interpretations.v
@@ -349,19 +349,19 @@ Module ZBounds.
          modulus value.
   (** TODO(jadep): Fill me in.  This should check that the modulus and
       value fit within int_width, that the modulus is of the right
-      form, and that the value is small enough.  If not, it should
-      [None]; otherwise, it should delegate to
-      [conditional_subtract']. *)
-  Axiom conditional_subtract_o
+      form, and that the value is small enough. *)
+  Axiom check_conditional_subtract_bounds
     : forall (pred_n : nat) (int_width : bounds)
-             (modulus value : Tuple.tuple bounds (S pred_n)), option (Tuple.tuple bounds (S pred_n)).
+             (modulus value : Tuple.tuple bounds (S pred_n)), bool.
   Definition conditional_subtract (pred_n : nat) (int_width : t)
              (modulus value : Tuple.tuple t (S pred_n))
     : Tuple.tuple t (S pred_n)
     := Tuple.push_option
          match int_width, Tuple.lift_option modulus, Tuple.lift_option value with
          | Some int_width, Some modulus, Some value
-           => conditional_subtract_o pred_n int_width modulus value
+           => if check_conditional_subtract_bounds pred_n int_width modulus value
+              then Some (conditional_subtract' pred_n int_width modulus value)
+              else None
          | _, _, _ => None
          end.
 
@@ -612,6 +612,31 @@ Module BoundedWord64.
 
   Tactic Notation "admit" := abstract case proof_admitted.
 
+
+  (** TODO(jadep): Use the bounds lemma here to prove that if each
+      component of [ret_val] is [Some (l, v, u)], then we can fill in
+      [pf] and return the tuple of [{| lower := l ; value := v ; upper
+      := u ; in_bounds := pf |}]. *)
+  Lemma conditional_subtract_bounded
+        (pred_n : nat) (x : BoundedWord)
+        (y z : Tuple.tuple BoundedWord (S pred_n))
+        (H : ZBounds.check_conditional_subtract_bounds
+               pred_n (BoundedWordToBounds x)
+               (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z) = true)
+    : hlist
+        (fun vlu : Word64.word64 * ZBounds.bounds =>
+           (0 <= ZBounds.lower (snd vlu))%Z /\
+           (ZBounds.lower (snd vlu) <= Word64.word64ToZ (fst vlu) <= ZBounds.upper (snd vlu))%Z /\
+           (Z.log2 (ZBounds.upper (snd vlu)) < Word64.bit_width)%Z)
+        (Tuple.map2 (fun v lu => (v, lu))
+                    (Word64.conditional_subtract
+                       pred_n (value x) (Tuple.map value y) (Tuple.map value z))
+                    (ZBounds.conditional_subtract'
+                       pred_n (BoundedWordToBounds x)
+                       (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z))).
+  Proof. Admitted.
+
+
   Definition add : t -> t -> t.
   Proof.
     refine (t_map2 Word64.add ZBounds.add _); t_start; admit.
@@ -667,25 +692,18 @@ Module BoundedWord64.
       Tuple.tuple t (S pred_n).
   Proof.
     refine (@t_map1_tuple2 pred_n (@Word64.conditional_subtract _) (@ZBounds.conditional_subtract _) _).
-    (** TODO(jadep): Use the bounds lemma here to prove that if each
-        component of [ret_val] is [Some (l, v, u)], then we can fill
-        in [pf] and return the tuple of [{| lower := l ; value := v ;
-        upper := u ; in_bounds := pf |}]. *)
-    admit.
+    abstract (
+        repeat first [ progress unfold ZBounds.conditional_subtract
+                     | rewrite !Tuple.lift_push_option
+                     | progress break_match
+                     | congruence
+                     | progress subst
+                     | progress inversion_option
+                     | intro
+                     | solve [ auto using conditional_subtract_bounded ] ]
+      ).
   Defined.
 
-  Local Ltac convoy_destruct_in H :=
-    match type of H with
-    | context G[match ?e with Some x => @?S x | None => ?N end eq_refl]
-      => let e' := fresh in
-         let H' := fresh in
-         pose e as e';
-         pose (eq_refl : e = e') as H';
-         let G' := context G[match e' with Some x => S x | None => N end H'] in
-         change G' in H;
-         clearbody H' e'; destruct e'
-    end.
-
   Local Notation binop_correct op opW opB :=
     (forall x y v, op (Some x) (Some y) = Some v
                    -> value v = opW (value x) (value y)
diff --git a/src/Reflection/Z/Interpretations/Relations.v b/src/Reflection/Z/Interpretations/Relations.v
index 36a3a054a..affd671e0 100644
--- a/src/Reflection/Z/Interpretations/Relations.v
+++ b/src/Reflection/Z/Interpretations/Relations.v
@@ -285,15 +285,50 @@ Proof.
                                  | progress break_match ] ]. }
 Qed.
 
+Lemma lift_option_flat_interp_tuple'
+      {n T x y}
+  : (Tuple.lift_option (n:=S n) (A:=T) (flat_interp_tuple' (interp_base_type:=LiftOption.interp_base_type' _) (T:=Tbase TZ) x) = Some y)
+    <-> (x = flat_interp_untuple' (T:=Tbase TZ) (n:=n) (Tuple.push_option (n:=S n) (Some y))).
+Proof.
+  rewrite Tuple.push_lift_option; generalize (Tuple.push_option (Some y)); intro.
+  split; intro; subst;
+    rewrite ?flat_interp_tuple'_untuple', ?flat_interp_untuple'_tuple';
+    reflexivity.
+Qed.
+
+Lemma lift_option_None_interp_flat_type_rel_pointwise2_1
+      T U n R x y
+      (H : interp_flat_type_rel_pointwise2 (LiftOption.lift_relation2 R) x y)
+      (HNone : Tuple.lift_option (A:=T) (n:=S n) (flat_interp_tuple' (T:=Tbase TZ) (n:=n) x) = None)
+  : Tuple.lift_option (A:=U) (n:=S n) (flat_interp_tuple' (T:=Tbase TZ) (n:=n) y) = None.
+Proof.
+  induction n; [ | specialize (IHn (fst x) (fst y) (proj1 H)) ];
+    repeat first [ progress destruct_head_hnf' False
+                 | reflexivity
+                 | progress inversion_option
+                 | progress simpl in *
+                 | progress subst
+                 | progress specialize_by congruence
+                 | progress destruct_head_hnf' prod
+                 | progress destruct_head_hnf' and
+                 | progress destruct_head_hnf' option
+                 | progress break_match
+                 | progress break_match_hyps ].
+Qed.
+
 Local Arguments LiftOption.lift_relation _ _ _ _ !_ _ / .
+Local Arguments LiftOption.of' _ _ !_ / .
+Local Arguments BoundedWord64.BoundedWordToBounds !_ / .
 
 Local Ltac t_map1_tuple2_t_step :=
   first [ exact I
+        | reflexivity
         | progress destruct_head_hnf' False
         | progress subst
         | progress destruct_head_hnf' prod
         | progress destruct_head_hnf' and
         | progress destruct_head_hnf' option
+        | progress inversion_option
         | intro
         | apply @related_tuples_None_left; constructor
         | apply -> @related_tuples_Some_left
@@ -309,24 +344,36 @@ Local Ltac t_map1_tuple2_t_step :=
                [ | first [ left; eexists; eassumption | right eexists; eassumption ] ]
           | [ H : Tuple.lift_option ?x = Some _, H' : context[?x] |- _ ]
             => setoid_rewrite H in H'
+          | [ H : proj_eq_rel _ _ _ |- _ ] => hnf in H
+          | [ H : Tuple.lift_option (flat_interp_tuple' ?x) = Some _ |- _ ]
+            => is_var x; apply lift_option_flat_interp_tuple' in H
           end
         | progress rewrite ?HList.map'_mapt', <- ?HList.map_is_mapt'
         | progress rewrite ?Tuple.map_map2, ?Tuple.map2_fst, ?Tuple.map2_snd, ?Tuple.map_id
-        | progress rewrite ?flat_interp_tuple_untuple' in *
+        | progress rewrite Tuple.map_id_ext by repeat (reflexivity || intros [] || intro)
+        | progress rewrite ?flat_interp_tuple_untuple', ?flat_interp_tuple'_untuple' in *
         | progress unfold BoundedWord64.t_map1_tuple2, HList.mapt
         | progress unfold related_word64, related'_word64, related_bounds in *
         | progress simpl @BoundedWord64.to_word64' in *
         | progress simpl @fst in *
         | progress simpl @snd in *
         | progress simpl @option_map in *
+        | progress simpl @BoundedWord64.BoundedWordToBounds in *
         | progress break_match
         | progress convoy_destruct
         | progress simpl @interp_flat_type_rel_pointwise2 in *
         | progress simpl @LiftOption.lift_relation in *
         | progress simpl @LiftOption.lift_relation2 in *
         | progress simpl @flat_interp_tuple in *
+        | progress simpl @LiftOption.of' in *
+        | progress simpl @smart_interp_flat_map in *
         | rewrite_hyp <- !*; reflexivity
-        | progress unfold proj_eq_rel in * ].
+        | solve [ eauto using lift_option_None_interp_flat_type_rel_pointwise2_1 ]
+        | match goal with
+          | [ H : LiftOption.lift_relation2 _ _ _ _ |- _ ] => unfold LiftOption.lift_relation2 in H
+          | [ H : LiftOption.of' _ = _ |- _ ] => unfold LiftOption.of' in H
+          | [ H : option_map _ _ = _ |- _ ] => unfold option_map in H
+          end ].
 Local Ltac t_map1_tuple2_t := repeat t_map1_tuple2_t_step.
 
 Lemma related_word64_t_map1_tuple2 {n} opW opB pf
@@ -377,10 +424,16 @@ Proof.
   related_word64_op_t.
 Qed.
 
+Local Arguments Tuple.lift_option : simpl never.
+Local Arguments Tuple.push_option : simpl never.
+Local Arguments Tuple.map : simpl never.
+Local Arguments Tuple.map2 : simpl never.
+
 Lemma related_bounds_t_map1_tuple2 {n} opW opB pf
       (HN0 : forall x y, opB None x y = Tuple.push_option None)
       (HN1 : forall x y z, Tuple.lift_option y = None -> opB x y z = Tuple.push_option None)
       (HN2 : forall x y z, Tuple.lift_option z = None -> opB x y z = Tuple.push_option None)
+      (HN3 : forall x y z, Tuple.lift_option (opB x y z) = None -> opB x y z = Tuple.push_option None)
       sv1 sv2
   : interp_flat_type_rel_pointwise2 (t:=Prod (Prod (Tbase TZ) (Syntax.tuple (Tbase TZ) (S n))) (Syntax.tuple (Tbase TZ) (S n))) related_bounds sv1 sv2
     -> interp_flat_type_rel_pointwise2
@@ -389,9 +442,21 @@ Lemma related_bounds_t_map1_tuple2 {n} opW opB pf
          (Syntax.flat_interp_untuple' (n:=n) (T:=Tbase TZ) (opB (fst (fst sv2)) (Syntax.flat_interp_tuple (snd (fst sv2))) (Syntax.flat_interp_tuple (snd sv2)))).
 Proof.
   t_map1_tuple2_t;
-    rewrite ?HN0, ?HN1, ?HN2 by assumption;
-    t_map1_tuple2_t;
-    admit.
+    try first [ rewrite HN0 by (assumption || t_map1_tuple2_t)
+              | rewrite HN1 by (assumption || t_map1_tuple2_t)
+              | rewrite HN2 by (assumption || t_map1_tuple2_t)
+              | rewrite HN3 by (assumption || t_map1_tuple2_t) ];
+    t_map1_tuple2_t.
+  { repeat match goal with
+           | [ |- context[HList.mapt' _ ?ls] ]
+             => not is_var ls; generalize ls; intro
+           | [ H : Tuple.lift_option _ = Some _ |- _ ]
+             => apply Tuple.push_lift_option in H; setoid_rewrite H
+           | _ => progress (break_match_hyps; t_map1_tuple2_t)
+           end. }
+  { repeat (break_match_hyps; t_map1_tuple2_t).
+    rewrite HN3 by (assumption || t_map1_tuple2_t).
+    t_map1_tuple2_t. }
 Qed.
 
 Local Arguments ZBounds.SmartBuildBounds _ _ / .
@@ -409,7 +474,9 @@ Proof.
   { apply related_bounds_t_map4; intros; destruct_head' option; reflexivity. }
   { apply related_bounds_t_map4; intros; destruct_head' option; reflexivity. }
   { apply related_bounds_t_map1_tuple2; intros; destruct_head' option; try reflexivity;
-      unfold ZBounds.conditional_subtract; rewrite ?Tuple.lift_push_option; try reflexivity;
+      unfold ZBounds.conditional_subtract in *; rewrite ?Tuple.lift_push_option in *;
+        repeat match goal with H : _ |- _ => rewrite !Tuple.lift_push_option in H end;
+        try reflexivity;
         (rewrite_hyp ?* );
         break_match; try reflexivity. }
 Qed.