From f8eab3da78edd44864e12e50962e5c1e382759fc Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 7 Nov 2016 17:55:34 -0500 Subject: Finish related_bounds_t_map1_tuple2 --- src/Reflection/Z/Interpretations.v | 64 ++++++++++++++-------- src/Reflection/Z/Interpretations/Relations.v | 79 +++++++++++++++++++++++++--- 2 files changed, 114 insertions(+), 29 deletions(-) (limited to 'src') 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. -- cgit v1.2.3