diff options
| -rw-r--r-- | src/Reflection/Z/Interpretations/Relations.v | 61 |
1 files changed, 57 insertions, 4 deletions
diff --git a/src/Reflection/Z/Interpretations/Relations.v b/src/Reflection/Z/Interpretations/Relations.v index 2fdcd22ab..4f0ea7b3b 100644 --- a/src/Reflection/Z/Interpretations/Relations.v +++ b/src/Reflection/Z/Interpretations/Relations.v @@ -149,6 +149,25 @@ Proof. related_word64_op_t. Qed. +Lemma related_tuples_None_left : forall n + (i2 : interp_flat_type Word64.interp_base_type (tuple' (Tbase TZ) n)), + @interp_flat_type_rel_pointwise2 base_type + BoundedWord64.interp_base_type Word64.interp_base_type related_word64 + (@tuple' base_type (@Tbase base_type TZ) n) + (@flat_interp_untuple' base_type BoundedWord64.interp_base_type + (@Tbase base_type TZ) n + (@Tuple.push_option (S n) BoundedWord64.BoundedWord + (@None (Tuple.tuple BoundedWord64.BoundedWord (S n))))) i2. +Proof. + induction n; simpl; intuition; simpl; constructor. +Qed. + +Definition tuple_tl {T n} : Tuple.tuple T (S n) -> Tuple.tuple T n := + match n with + | O => fun _ => tt + | S _ => fun p => fst p + end. + Lemma related_word64_t_map1_tuple2 {n} opW opB pf 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_word64 sv1 sv2 @@ -162,11 +181,45 @@ Proof. destruct_head_hnf' option; destruct_head_hnf' False. Focus 2. { destruct_head_hnf' True. - unfold BoundedWord64.t_map1_tuple2. - admit. (* TODO(jadep (or jgross)): Fill me in *) } + apply related_tuples_None_left. } Unfocus. - admit. (* TODO(jadep (or jgross)): Fill me in *) -Admitted. + unfold BoundedWord64.t_map1_tuple2. + case_eq (@Tuple.lift_option (S n) BoundedWord64.BoundedWord + (@flat_interp_tuple' base_type + BoundedWord64.interp_base_type (@Tbase base_type TZ) n i4)); + intros; try apply related_tuples_None_left. + case_eq (@Tuple.lift_option (S n) BoundedWord64.BoundedWord + (@flat_interp_tuple' base_type + BoundedWord64.interp_base_type (@Tbase base_type TZ) n i3)); + intros; try apply related_tuples_None_left. + generalize (pf b t t0); clear pf. + generalize (eq_refl (Tuple.lift_option (opB (Some (BoundedWord64.BoundedWordToBounds b)) + (Tuple.push_option + (Some (Tuple.map BoundedWord64.BoundedWordToBounds t))) + (Tuple.push_option + (Some + (Tuple.map BoundedWord64.BoundedWordToBounds t0)))))). + case_eq (Tuple.lift_option + (opB (Some (BoundedWord64.BoundedWordToBounds b)) + (Tuple.push_option + (Some (Tuple.map BoundedWord64.BoundedWordToBounds t))) + (Tuple.push_option + (Some + (Tuple.map BoundedWord64.BoundedWordToBounds t0))))); + intros; try apply related_tuples_None_left. + generalize (h t1 e); clear h e; intro. + induction n. + unfold related_word64 in *; simpl in *; subst. + hnf. + simpl in *. + hnf in H0; subst. + hnf in H1; subst. + hnf in H; subst. + reflexivity. + split. + admit. + admit. +Qed. Lemma related_word64_op : related_op related_word64 (@BoundedWord64.interp_op) (@Word64.interp_op). Proof. |