Minor changes to rewriter

These changes make it easier to prove things about the interpretation of
the rewriter.

1 files changed, 0 insertions, 73 deletions

diff --git a/src/Experiments/NewPipeline/RewriterWf2.v b/src/Experiments/NewPipeline/RewriterWf2.v
index de17f2896..feb5b98f9 100644
--- a/src/Experiments/NewPipeline/RewriterWf2.v
+++ b/src/Experiments/NewPipeline/RewriterWf2.v
@@ -378,79 +378,6 @@ Module Compilers.
                    end;
             fin_handle_list.
 
-          Fixpoint eval_decision_tree_cont_None_ext
-                {var} {T ctx d cont}
-                (Hcont : forall x y, cont x y = None)
-                {struct d}
-            : @eval_decision_tree var T ctx d cont = None.
-          Proof using Type.
-            clear -Hcont eval_decision_tree_cont_None_ext.
-            specialize (fun d ctx => @eval_decision_tree_cont_None_ext var T ctx d).
-            destruct d; cbn [eval_decision_tree]; intros; try (clear eval_decision_tree_cont_None_ext; tauto).
-            { let d := match goal with d : decision_tree |- _ => d end in
-              specialize (eval_decision_tree_cont_None_ext d).
-              rewrite !Hcont, !eval_decision_tree_cont_None_ext by assumption.
-              break_innermost_match; reflexivity. }
-            { let d := match goal with d : decision_tree |- _ => d end in
-              pose proof (eval_decision_tree_cont_None_ext d) as IHd.
-              let d := match goal with d : option decision_tree |- _ => d end in
-              pose proof (match d as d' return match d' with Some _ => _ | None => True end with
-                          | Some d => eval_decision_tree_cont_None_ext d
-                          | None => I
-                          end) as IHapp_case.
-              all: destruct ctx; try (clear eval_decision_tree_cont_None_ext; (tauto || congruence)); [].
-              all: lazymatch goal with
-                   | [ |- match ?d with
-                          | TryLeaf _ _ => (?res ;; ?ev)%option
-                          | _ => _
-                          end = None ]
-                     => cut (res = None /\ ev = None);
-                          [ clear eval_decision_tree_cont_None_ext;
-                            let H1 := fresh in
-                            let H2 := fresh in
-                            intros [H1 H2]; rewrite H1, H2; destruct d; reflexivity
-                          | ]
-                   end.
-              all: split; [ | clear eval_decision_tree_cont_None_ext; eapply IHd; eassumption ].
-              (** We use the trick that [induction] inside [Fixpoint]
-                  gives us nested [fix]es that pass the guarded
-                  checker, as long as we're careful about how we do
-                  things *)
-              let icases := match goal with d : list (_ * decision_tree) |- _ => d end in
-              induction icases as [|icase icases IHicases];
-                [ | pose proof (eval_decision_tree_cont_None_ext (snd icase)) as IHicase ];
-                clear eval_decision_tree_cont_None_ext.
-              (** now we can stop being super-careful about [destruct]
-                  ordering because, if we're [Guarded] here (which we
-                  are), then we cannot break guardedness from this
-                  point on, because we've cleared the bare fixpoint
-                  after specializing it to valid arguments *)
-              2: revert IHicases.
-              all: repeat (rewrite reveal_rawexpr_cps_id; set (reveal_rawexpr _)).
-              all: repeat match goal with H := reveal_rawexpr _ |- _ => subst H end.
-              all: repeat first [ progress cbn [fold_right Option.sequence Option.sequence_return fst snd] in *
-                                | progress subst
-                                | reflexivity
-                                | rewrite IHd
-                                | rewrite IHapp_case
-                                | rewrite IHicase
-                                | break_innermost_match_step
-                                | progress intros
-                                | solve [ auto ]
-                                | progress break_match
-                                | progress cbv [Option.bind option_bind'] in * ]. }
-            { let d := match goal with d : decision_tree |- _ => d end in
-              specialize (eval_decision_tree_cont_None_ext d); rename eval_decision_tree_cont_None_ext into IHd.
-              repeat first [ break_innermost_match_step
-                           | rewrite IHd
-                           | solve [ auto ]
-                           | progress intros ]. }
-          Qed.
-
-          Lemma eval_decision_tree_cont_None {var} {T ctx d}
-            : @eval_decision_tree var T ctx d (fun _ _ => None) = None.
-          Proof using Type. apply eval_decision_tree_cont_None_ext; reflexivity. Qed.
-
           Fixpoint wf_eval_decision_tree' {T1 T2} G d (P : option T1 -> option T2 -> Prop) (HPNone : P None None) {struct d}
             : forall (ctx1 : list (@rawexpr var1))
                      (ctx2 : list (@rawexpr var2))