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/Relations.v | 79 +++++++++++++++++++++++++--- 1 file changed, 73 insertions(+), 6 deletions(-) (limited to 'src/Reflection/Z/Interpretations/Relations.v') 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