From d2b87ee92202a55e764da1a220e118a7282b3b93 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 8 Nov 2016 16:00:56 -0500 Subject: More progress on src/Reflection/Z/Interpretations/Relations.v --- src/Reflection/Z/Interpretations.v | 95 ++++++++++++++++++++++++++-- src/Reflection/Z/Interpretations/Relations.v | 30 ++++++--- 2 files changed, 112 insertions(+), 13 deletions(-) diff --git a/src/Reflection/Z/Interpretations.v b/src/Reflection/Z/Interpretations.v index 7b323cd2b..88009d48d 100644 --- a/src/Reflection/Z/Interpretations.v +++ b/src/Reflection/Z/Interpretations.v @@ -406,9 +406,9 @@ Module ZBounds. : 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' - => if check_conditional_subtract_bounds pred_n int_width modulus value' - then Some (conditional_subtract' pred_n int_width modulus value') + | Some int_width, Some modulus, Some 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. @@ -671,6 +671,31 @@ Module BoundedWord64. (H : ZBounds.check_conditional_subtract_bounds pred_n (BoundedWordToBounds x) (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z) = true) + : HList.hlist + (fun vlu : Z * ZBounds.bounds => + (0 <= ZBounds.lower (snd vlu))%Z /\ + (ZBounds.lower (snd vlu) <= fst vlu <= ZBounds.upper (snd vlu))%Z /\ + (Z.log2 (ZBounds.upper (snd vlu)) < Word64.bit_width)%Z) + (Tuple.map2 (fun v lu => (v, lu)) + (ModularBaseSystemListZOperations.conditional_subtract_modulus + (S pred_n) + (Word64.word64ToZ (value x)) + (Tuple.map Word64.word64ToZ (Tuple.map value y)) + (Tuple.map Word64.word64ToZ (Tuple.map value z))) + (ZBounds.conditional_subtract' + pred_n (BoundedWordToBounds x) + (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z))). + Proof. Admitted. + + Local Hint Resolve Word64.bit_width_pos : zarith. + Local Hint Extern 1 (Z.log2 _ < _)%Z => eapply Z.le_lt_trans; [ eapply Z.log2_le_mono; eassumption | eassumption ] : zarith. + (* Local *) Hint Resolve <- Z.log2_lt_pow2_alt : zarith. + Lemma conditional_subtract_bounded_word + (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.hlist (fun vlu : Word64.word64 * ZBounds.bounds => (0 <= ZBounds.lower (snd vlu))%Z /\ @@ -682,8 +707,68 @@ Module BoundedWord64. (ZBounds.conditional_subtract' pred_n (BoundedWordToBounds x) (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z))). - Proof. Admitted. + Proof. + generalize (conditional_subtract_bounded pred_n x y z H). + unfold Word64.conditional_subtract; rewrite Tuple.map2_map_fst. + rewrite <- (Tuple.map_map2 (fun a b => (a, b)) (fun ab => (Word64.ZToWord64 (fst ab), snd ab))). + rewrite HList.hlist_map; simpl @fst; simpl @snd. + apply HList.hlist_impl, HList.const. + intros; destruct_head' and; repeat split; + autorewrite with push_word64ToZ; omega. + Qed. + + Lemma conditional_subtract_bounded_lite_helper + (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.hlist + (fun v : Z => + (0 <= v)%Z /\ + (Z.log2 v < Word64.bit_width)%Z) + (Tuple.map + (@fst _ _) + (Tuple.map2 (fun v lu => (v, lu)) + (ModularBaseSystemListZOperations.conditional_subtract_modulus + (S pred_n) + (Word64.word64ToZ (value x)) + (Tuple.map Word64.word64ToZ (Tuple.map value y)) + (Tuple.map Word64.word64ToZ (Tuple.map value z))) + (ZBounds.conditional_subtract' + pred_n (BoundedWordToBounds x) + (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z)))). + Proof. + generalize (conditional_subtract_bounded pred_n x y z H). + rewrite HList.hlist_map. + apply HList.hlist_impl, HList.const; intros. + destruct_head' and. + split; try omega; []. + eapply Z.le_lt_trans; [ eapply Z.log2_le_mono | eassumption ]; omega. + Qed. + Lemma conditional_subtract_bounded_lite + (pred_n : nat) + (xbw : BoundedWord) (ybw zbw : Tuple.tuple BoundedWord (S pred_n)) + (x : Word64.word64) (y z : Tuple.tuple Word64.word64 (S pred_n)) + (xb : ZBounds.bounds) (yb zb : Tuple.tuple ZBounds.bounds (S pred_n)) + (Hx : value xbw = x) (Hy : Tuple.map value ybw = y) (Hz : Tuple.map value zbw = z) + (Hxb : BoundedWordToBounds xbw = xb) + (Hyb : Tuple.map BoundedWordToBounds ybw = yb) (Hzb : Tuple.map BoundedWordToBounds zbw = zb) + (Hc : ZBounds.check_conditional_subtract_bounds pred_n xb yb zb = true) + : HList.hlist (fun v : Z => (0 <= v)%Z /\ (Z.log2 v < Z.of_nat Word64.bit_width)%Z) + (ModularBaseSystemListZOperations.conditional_subtract_modulus + (S pred_n) + (Word64.word64ToZ x) + (Tuple.map Word64.word64ToZ y) + (Tuple.map Word64.word64ToZ z)). + Proof. + subst. + generalize (conditional_subtract_bounded_lite_helper pred_n xbw ybw zbw Hc). + rewrite Tuple.map_map2; simpl @fst. + rewrite Tuple.map2_fst, Tuple.map_id. + trivial. + Qed. Definition add : t -> t -> t. Proof. @@ -748,7 +833,7 @@ Module BoundedWord64. | progress subst | progress inversion_option | intro - | solve [ auto using conditional_subtract_bounded ] ] + | solve [ auto using conditional_subtract_bounded_word ] ] ). Defined. diff --git a/src/Reflection/Z/Interpretations/Relations.v b/src/Reflection/Z/Interpretations/Relations.v index 457d0d5ad..f59abad12 100644 --- a/src/Reflection/Z/Interpretations/Relations.v +++ b/src/Reflection/Z/Interpretations/Relations.v @@ -556,10 +556,15 @@ Tactic Notation "admit" := abstract case proof_admitted. Local Arguments related'_Z _ _ _ / . Lemma related_Z_t_map1_tuple2 n opZ opW opB pf (H : forall x y z bxs bys bzs brs, - Tuple.push_option (Some brs) = opB (Some bxs) (Tuple.push_option (Some bys)) (Tuple.push_option (Some bzs)) + Some brs = Tuple.lift_option (opB (Some bxs) (Tuple.push_option (Some bys)) (Tuple.push_option (Some bzs))) -> is_in_bounds x bxs - (*-> is_in_bounds y bys - -> is_in_bounds z bzs + -> { ybw : Tuple.tuple BoundedWord64.BoundedWord _ + | Tuple.map BoundedWord64.value ybw = y + /\ Tuple.map BoundedWord64.BoundedWordToBounds ybw = bys } + -> { zbw : Tuple.tuple BoundedWord64.BoundedWord _ + | Tuple.map BoundedWord64.value zbw = z + /\ Tuple.map BoundedWord64.BoundedWordToBounds zbw = bzs } + (* -> is_in_bounds (opW x y z) brs*) -> Tuple.map Word64.word64ToZ (opW x y z) = (opZ (Word64.word64ToZ x) (Tuple.map Word64.word64ToZ y) (Tuple.map Word64.word64ToZ z))) sv1 sv2 @@ -594,8 +599,13 @@ Local Ltac related_Z_op_fin_t_step := | progress inversion_option | intro | progress autorewrite with push_word64ToZ - | match goal with H : andb _ _ = true |- _ => rewrite Bool.andb_true_iff in H end - | progress Z.ltb_to_lt ]. + | match goal with + | [ H : andb _ _ = true |- _ ] => rewrite Bool.andb_true_iff in H + | [ H : context[Tuple.lift_option (Tuple.push_option _)] |- _ ] + => rewrite Tuple.lift_push_option in H + end + | progress Z.ltb_to_lt + | (progress unfold ZBounds.conditional_subtract in * ); break_match_hyps ]. Local Ltac related_Z_op_fin_t := repeat related_Z_op_fin_t_step. Local Opaque Word64.bit_width. @@ -614,9 +624,13 @@ Proof. { apply related_Z_t_map4; related_Z_op_fin_t. } { apply related_Z_t_map4; related_Z_op_fin_t. } { apply related_Z_t_map1_tuple2; related_Z_op_fin_t; - rewrite Word64.word64ToZ_conditional_subtract; try Word64.Rewrites.word64_util_arith. - pose proof BoundedWord64.conditional_subtract_bounded. - admit. (** TODO(jadep or jgross): Fill me in *) } + rewrite Word64.word64ToZ_conditional_subtract; try Word64.Rewrites.word64_util_arith; []. + destruct_head' sig; destruct_head' and; subst. + eapply BoundedWord64.conditional_subtract_bounded_lite + with (xbw := {| BoundedWord64.value := _ |}); + [ .. | eassumption ]; reflexivity. + Grab Existential Variables. + omega. } Qed. Create HintDb interp_related discriminated. -- cgit v1.2.3