More WIP on PullCast

1 files changed, 41 insertions, 35 deletions

diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v b/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v
index 8df34b903..1220665d5 100644
--- a/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v
+++ b/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v
@@ -37,6 +37,27 @@ Section with_round_up.
   Local Notation pick_typeb := (@Bounds.bounds_to_base_type round_up) (only parsing).
   Local Notation pick_type v := (SmartFlatTypeMap pick_typeb v).
 
+  Local Ltac t_small :=
+    repeat first [ progress cbv [Bounds.bounds_to_base_type Bounds.smallest_logsz Bounds.actual_logsz] in *
+                 | progress simpl in *
+                 | progress autorewrite with push_Zof_nat zsimplify_const
+                 | solve [ trivial ]
+                 | progress change (@interpToZ) with (fun t1 => cast_const (t1:=t1) (t2:=TZ)) in *
+                 | progress change (@cast_const TZ TZ) with (fun x : Z => x) in *
+                 | progress Z.ltb_to_lt
+                 | rewrite Z2Nat.id in * by auto with zarith
+                 | rewrite <- Z.log2_up_le_pow2_full in * by auto with zarith
+                 | break_innermost_match_step
+                 | apply conj
+                 | omega
+                 | rewrite <- Z.log2_up_le_full
+                 | match goal with
+                   | [ |- ?x < ?y ] => cut (x + 1 <= y); [ omega | ]
+                   | [ H : (_ <=? _)%nat = true |- _ ] => apply Nat.leb_le in H
+                   | [ H : (_ <= _)%nat |- _ ] => apply inj_le in H
+                   end ].
+
+  Local Arguments cast_const : simpl never.
   Lemma pull_cast_genericize_op
         t tR (opc : op t tR)
         (bs : interp_flat_type Bounds.interp_base_type t)
@@ -53,40 +74,25 @@ Section with_round_up.
     generalize dependent (Zinterp_op t tR opc).
     generalize dependent (Bounds.interp_op opc bs); simpl; intros.
     repeat (destruct_one_head flat_type; try solve [ inversion opc ]).
-    all:simpl in *; destruct_head unit; destruct_head True; simpl in *.
-    all:unfold unzify_op, cast_back_flat_const, lift_op in *; simpl in *.
-    all:unfold Bounds.is_bounded_by', ZRange.is_bounded_by' in *.
-    all:change (@interpToZ) with (fun t1 => cast_const (t1:=t1) (t2:=TZ)) in *.
-    all:cbv beta in *.
-    { specialize (H0 (cast_const v)).
-      specialize_by_assumption.
-      (*{ simpl in *.
-      specialize (H0 tt I).
-      simpl in *.
-      hnf in H0.
-      unfold cast_back_flat_const, lift_op, unzify_op in *; simpl in *.
-      unfold interpToZ in *.
-      unfold Bounds.bounds_to_base_type in *.
-      destruct_head base_type; simpl in *.
-      split_andb.
-      Z.ltb_to_lt.
-      all:destruct_head' and.
-      all:simpl in *.
-      all:break_innermost_match; break_match_hyps; split_andb; Z.ltb_to_lt; try reflexivity.
-      all:try (simpl in *;
-               rewrite wordToZ_ZToWord
-                 by (autorewrite with push_Zof_nat zsimplify_const;
-                     rewrite Z2Nat.id by auto with zarith;
-                     split; try omega;
-                     match goal with
-                     | [ |- (?x < ?y)%Z ]
-                       => apply (Z.lt_le_trans x (x + 1) y); [ omega | ]
-                     end;
-                     rewrite <- !Z.log2_up_le_full;
-                     omega)).
-      all:try reflexivity.
-      unfold interpToZ, cast_const.
-      simpl.
-*)
+    all:repeat first [ progress simpl in *
+                     | progress destruct_head unit
+                     | progress destruct_head True
+                     | progress cbv [unzify_op cast_back_flat_const lift_op Bounds.is_bounded_by' ZRange.is_bounded_by'] in *
+                     | progress change (@interpToZ) with (fun t1 => cast_const (t1:=t1) (t2:=TZ)) in *
+                     | progress change (@cast_const TZ TZ) with (fun x : Z => x) in *
+                     | progress specialize_by auto
+                     | progress specialize_by constructor
+                     | match goal with
+                       | [ H : forall v, _ <= ?f v <= _ /\ _ -> _ |- context[?f ?v'] ]
+                         => specialize (H v')
+                       | _ => progress specialize_by auto
+                       | [ H : forall v : _ * _, _ /\ _ -> _ |- _ ]
+                         => specialize (fun v1 v2 p1 p2 => H (v1, v2) (conj p1 p2));
+                            cbn [fst snd] in H;
+                            specialize (fun v1 p1 v2 p2 => H v1 v2 p1 p2)
+                       end
+                     | progress destruct_head'_and ].
+    2:rewrite cast_const_idempotent_small by t_small; reflexivity.
+
   Admitted.
 End with_round_up.