Update rewriter correctness condition

Now we don't need any relation on values when going under binders to get
the cps-id condition.  This seems essential to getting the rewriter
interp correctness proofs to work.

3 files changed, 87 insertions, 20 deletions

diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v
index 6c0572ea4..4882b9b1e 100644
--- a/src/Experiments/NewPipeline/Rewriter.v
+++ b/src/Experiments/NewPipeline/Rewriter.v
@@ -240,6 +240,17 @@ Module Compilers.
              (List.rev (PositiveSet.elements p))
              (PositiveMap.empty _).
 
+      Definition under_forall_vars_relation1 {p k1}
+                 (F : forall evm, k1 evm -> Prop)
+        : forall_vars p k1 -> Prop
+        := list_rect
+             (fun ls
+              => forall evm0, forall_vars_body k1 ls evm0 -> Prop)
+             F
+             (fun x xs rec evm0 K1 => forall t, rec _ (K1 t))
+             (List.rev (PositiveSet.elements p))
+             (PositiveMap.empty _).
+
       Definition under_forall_vars_relation {p k1 k2}
                  (F : forall evm, k1 evm -> k2 evm -> Prop)
         : forall_vars p k1 -> forall_vars p k2 -> Prop
@@ -483,6 +494,16 @@ Module Compilers.
                (fun T Ts rec f x => rec (f x))
                ls.
 
+        Definition under_type_of_list_relation1_cps {A1 ls}
+                   (F : A1 -> Prop)
+          : type_of_list_cps A1 ls -> Prop
+          := list_rect
+               (fun ls
+                => type_of_list_cps A1 ls -> Prop)
+               F
+               (fun T Ts rec f1 => forall x, rec (f1 x))
+               ls.
+
         Definition under_type_of_list_relation_cps {A1 A2 ls}
                    (F : A1 -> A2 -> Prop)
           : type_of_list_cps A1 ls -> type_of_list_cps A2 ls -> Prop
@@ -623,6 +644,26 @@ Module Compilers.
                     (@under_with_unification_resultT' _ x evm _ _ F)
              end.
 
+        Fixpoint under_with_unification_resultT'_relation1_gen {t p evm K1}
+                 (FH : forall t, value t -> Prop)
+                 (F : K1 -> Prop)
+                 {struct p}
+          : @with_unification_resultT' t p evm K1 -> Prop
+          := match p return with_unification_resultT' p evm K1 -> Prop with
+             | pattern.Wildcard t => fun f1 => forall v1, FH _ v1 -> F (f1 v1)
+             | pattern.Ident t idc => under_type_of_list_relation1_cps F
+             | pattern.App s d f x
+               => @under_with_unification_resultT'_relation1_gen
+                    _ f evm _
+                    FH
+                    (@under_with_unification_resultT'_relation1_gen _ x evm _ FH F)
+             end.
+
+        Definition under_with_unification_resultT'_relation1 {t p evm K1}
+                 (F : K1 -> Prop)
+          : @with_unification_resultT' t p evm K1 -> Prop
+          := @under_with_unification_resultT'_relation1_gen t p evm K1 (fun _ _ => True) F.
+
         Fixpoint under_with_unification_resultT'_relation_hetero {t p evm K1 K2}
                  (FH : forall t, value t -> value t -> Prop)
                  (F : K1 -> K2 -> Prop)
@@ -658,6 +699,19 @@ Module Compilers.
           := pattern.type.under_forall_vars
                (fun evm => under_with_unification_resultT' (F evm)).
 
+        Definition under_with_unification_resultT_relation1_gen {t p K1}
+                   (FH : forall t, value t -> Prop)
+                   (F : forall evm, K1 (pattern.type.subst_default t evm) -> Prop)
+          : @with_unification_resultT t p K1 -> Prop
+          := pattern.type.under_forall_vars_relation1
+               (fun evm => under_with_unification_resultT'_relation1_gen FH (F evm)).
+
+        Definition under_with_unification_resultT_relation1 {t p K1}
+                   (F : forall evm, K1 (pattern.type.subst_default t evm) -> Prop)
+          : @with_unification_resultT t p K1 -> Prop
+          := pattern.type.under_forall_vars_relation1
+               (fun evm => under_with_unification_resultT'_relation1 (F evm)).
+
         Definition under_with_unification_resultT_relation_hetero {t p K1 K2}
                    (FH : forall t, value t -> value t -> Prop)
                    (F : forall evm, K1 (pattern.type.subst_default t evm) -> K2 (pattern.type.subst_default t evm) -> Prop)
diff --git a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
index 3a7bef3e7..5b95e56c6 100644
--- a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
+++ b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
@@ -101,7 +101,7 @@ Module Compilers.
       Local Ltac do_cbv0 :=
         cbv [id
                Compile.rewrite_rules_interp_goodT
-               Compile.rewrite_rule_data_interp_goodT Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT'_relation_hetero Compile.wf_with_unification_resultT Compile.under_type_of_list_relation_cps pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.rew_replacement Compile.rew_is_cps Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unification_resultT' Compile.pattern_default_interp pattern.type.under_forall_vars_relation Compile.deep_rewrite_ruleTP_gen Compile.with_unification_resultT' pattern.ident.arg_types pattern.type.lam_forall_vars Compile.pattern_default_interp' pattern.collect_vars PositiveMap.empty Compile.ident_collect_vars pattern.ident.type_vars pattern.type.collect_vars PositiveSet.elements PositiveSet.union pattern.base.collect_vars PositiveSet.empty PositiveSet.xelements Compile.lam_type_of_list id pattern.ident.to_typed Compile.forall2_type_of_list_cps Compile.deep_rewrite_ruleTP_gen_good_relation Compile.normalize_deep_rewrite_rule_cps_id_hypsT Compile.normalize_deep_rewrite_rule pattern.type.subst_default PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add Compile.option_bind' Compile.wf_value Compile.value pattern.base.subst_default PositiveMap.find Compile.rewrite_ruleTP ident.smart_Literal Compile.value_interp_related Compile.value'_interp_related].
+               Compile.rewrite_rule_data_interp_goodT Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT_relation1_gen Compile.under_with_unification_resultT_relation1 Compile.under_with_unification_resultT'_relation_hetero Compile.wf_with_unification_resultT Compile.under_with_unification_resultT'_relation1 Compile.under_with_unification_resultT'_relation1_gen Compile.under_type_of_list_relation_cps Compile.under_type_of_list_relation1_cps pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.rew_replacement Compile.rew_is_cps Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unification_resultT' Compile.pattern_default_interp pattern.type.under_forall_vars_relation pattern.type.under_forall_vars_relation1 Compile.deep_rewrite_ruleTP_gen Compile.with_unification_resultT' pattern.ident.arg_types pattern.type.lam_forall_vars Compile.pattern_default_interp' pattern.collect_vars PositiveMap.empty Compile.ident_collect_vars pattern.ident.type_vars pattern.type.collect_vars PositiveSet.elements PositiveSet.union pattern.base.collect_vars PositiveSet.empty PositiveSet.xelements Compile.lam_type_of_list id pattern.ident.to_typed Compile.forall2_type_of_list_cps Compile.deep_rewrite_ruleTP_gen_good_relation Compile.deep_rewrite_ruleTP_gen_ok_relation Compile.normalize_deep_rewrite_rule_cps_id_hypsT Compile.normalize_deep_rewrite_rule pattern.type.subst_default PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add Compile.option_bind' Compile.wf_value Compile.value pattern.base.subst_default PositiveMap.find Compile.rewrite_ruleTP ident.smart_Literal Compile.value_interp_related Compile.value'_interp_related].
       Local Ltac do_cbv :=
         do_cbv0;
         cbv [List.map List.fold_right List.rev list_rect orb List.app].
@@ -121,6 +121,7 @@ Module Compilers.
                      | match goal with
                        | [ |- { pf : ?x = ?x | _ } ] => (exists eq_refl)
                        | [ |- True /\ _ ] => split; [ exact I | ]
+                       | [ |- _ /\ _ ] => split; [ intros; exact I | ]
                        end
                      | progress cbn [eq_rect] in * ];
         cbn [fst snd base.interp base.base_interp type.interp projT1 projT2 UnderLets.interp expr.interp type.related ident.gen_interp] in *.
diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v
index 2537523a4..8ae987eec 100644
--- a/src/Experiments/NewPipeline/RewriterWf1.v
+++ b/src/Experiments/NewPipeline/RewriterWf1.v
@@ -1128,6 +1128,9 @@ Module Compilers.
           Local Notation normalize_deep_rewrite_rule := (@normalize_deep_rewrite_rule ident var).
           Local Notation under_with_unification_resultT_relation := (@under_with_unification_resultT_relation ident var pident pident_arg_types type_vars_of_pident).
           Local Notation under_with_unification_resultT_relation_hetero := (@under_with_unification_resultT_relation_hetero ident var pident pident_arg_types type_vars_of_pident).
+          Local Notation under_with_unification_resultT_relation1 := (@under_with_unification_resultT_relation1 ident var pident pident_arg_types type_vars_of_pident).
+          Local Notation under_with_unification_resultT_relation1_gen := (@under_with_unification_resultT_relation1_gen ident var pident pident_arg_types type_vars_of_pident).
+
           Local Notation deep_rewrite_ruleTP_gen := (@deep_rewrite_ruleTP_gen ident var).
 
           Local Notation UnderLets_maybe_interp with_lets
@@ -1209,35 +1212,44 @@ Module Compilers.
                  (fun evm
                   => pattern_default_interp' p evm id).
 
+          Definition deep_rewrite_ruleTP_gen_ok_relation
+                     {should_do_again with_opt under_lets is_cps : bool} {t}
+                     (v1 : @deep_rewrite_ruleTP_gen should_do_again with_opt under_lets is_cps t)
+            : Prop
+            := @normalize_deep_rewrite_rule_cps_id_hypsT var _ _ _ _ _ v1.
+
           Definition deep_rewrite_ruleTP_gen_good_relation
                      {should_do_again with_opt under_lets is_cps : bool} {t}
                      (v1 : @deep_rewrite_ruleTP_gen should_do_again with_opt under_lets is_cps t)
                      (v2 : expr t)
             : Prop
-            := @normalize_deep_rewrite_rule_cps_id_hypsT var _ _ _ _ _ v1
-               /\ (let v1 := normalize_deep_rewrite_rule v1 _ id in
-                   match v1 with
-                   | None => True
-                   | Some v1 => let v1 := UnderLets.interp ident_interp v1 in
-                                (if should_do_again
-                                    return (@expr.expr base.type ident (if should_do_again then @value var else var) t) -> Prop
-                                 then
-                                   (fun v1
-                                    => expr.interp ident_interp (reify_expr v1) == expr.interp ident_interp v2)
-                                 else
-                                   (fun v1 => expr.interp ident_interp v1 == expr.interp ident_interp v2))
-                                  v1
-                   end).
+            := (let v1 := normalize_deep_rewrite_rule v1 _ id in
+                match v1 with
+                | None => True
+                | Some v1 => let v1 := UnderLets.interp ident_interp v1 in
+                             (if should_do_again
+                                 return (@expr.expr base.type ident (if should_do_again then @value var else var) t) -> Prop
+                              then
+                                (fun v1
+                                 => expr.interp ident_interp (reify_expr v1) == expr.interp ident_interp v2)
+                              else
+                                (fun v1 => expr.interp ident_interp v1 == expr.interp ident_interp v2))
+                               v1
+                end).
 
           Definition rewrite_rule_data_interp_goodT
                      {t} {p : pattern t} (r : @rewrite_rule_data t p)
             : Prop
-            := @under_with_unification_resultT_relation_hetero
-                 _ _ _ _
-                 (fun _ => value_interp_related)
-                 (fun evm => deep_rewrite_ruleTP_gen_good_relation)
+            := @under_with_unification_resultT_relation1
+                 _ _ _
+                 (fun evm => deep_rewrite_ruleTP_gen_ok_relation)
                  (rew_replacement _ _ r)
-                 (pattern_default_interp p).
+               /\ @under_with_unification_resultT_relation_hetero
+                    _ _ _ _
+                    (fun _ => value_interp_related)
+                    (fun evm => deep_rewrite_ruleTP_gen_good_relation)
+                    (rew_replacement _ _ r)
+                    (pattern_default_interp p).
 
           Definition rewrite_rules_interp_goodT
                      (rews : rewrite_rulesT)