Add under_forall_vars_relation1_lam_forall_vars, remove forall2_type_of_list_cps alias of under_type_of_list_relation_cps

4 files changed, 29 insertions, 14 deletions

diff --git a/src/Experiments/NewPipeline/RewriterRulesGood.v b/src/Experiments/NewPipeline/RewriterRulesGood.v
index 04e65dee3..a9953e056 100644
--- a/src/Experiments/NewPipeline/RewriterRulesGood.v
+++ b/src/Experiments/NewPipeline/RewriterRulesGood.v
@@ -213,7 +213,7 @@ Module Compilers.
         end;
         (exists eq_refl);
         cbn [eq_rect];
-        cbv [Compile.wf_deep_rewrite_ruleTP_gen Compile.wf_rewrite_rule_data Compile.rew_replacement Compile.rew_is_cps Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unif_rewrite_ruleTP_gen Compile.wf_with_unification_resultT pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.wf_maybe_under_lets_expr Compile.wf_maybe_do_again_expr Compile.wf_with_unification_resultT' pattern.type.under_forall_vars_relation Compile.with_unification_resultT' pattern.collect_vars Compile.ident_collect_vars pattern.ident.type_vars pattern.type.collect_vars pattern.base.collect_vars PositiveSet.empty PositiveSet.elements Compile.forall2_type_of_list_cps pattern.ident.arg_types pattern.type.subst_default pattern.base.subst_default PositiveSet.rev PositiveMap.empty];
+        cbv [Compile.wf_deep_rewrite_ruleTP_gen Compile.wf_rewrite_rule_data Compile.rew_replacement Compile.rew_is_cps Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unif_rewrite_ruleTP_gen Compile.wf_with_unification_resultT pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.wf_maybe_under_lets_expr Compile.wf_maybe_do_again_expr Compile.wf_with_unification_resultT' pattern.type.under_forall_vars_relation Compile.with_unification_resultT' pattern.collect_vars Compile.ident_collect_vars pattern.ident.type_vars pattern.type.collect_vars pattern.base.collect_vars PositiveSet.empty PositiveSet.elements Compile.under_type_of_list_relation_cps pattern.ident.arg_types pattern.type.subst_default pattern.base.subst_default PositiveSet.rev PositiveMap.empty];
         cbn [List.map List.fold_right PositiveSet.union PositiveSet.xelements List.rev List.app projT1 projT2 list_rect PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add PositiveMap.find orb];
         repeat first [ progress intros
                      | match goal with
diff --git a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
index 5b95e56c6..2bad756c9 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_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].
+               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.under_type_of_list_relation_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].
diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v
index a05fd7b04..ef0e9aaab 100644
--- a/src/Experiments/NewPipeline/RewriterWf1.v
+++ b/src/Experiments/NewPipeline/RewriterWf1.v
@@ -233,6 +233,29 @@ Module Compilers.
                                     | [ H : _ |- _ ] => apply H; rewrite PositiveMap.gso by congruence; assumption
                                     end ]. } } }
         Qed.
+
+        Lemma under_forall_vars_relation1_lam_forall_vars
+              {p k1 F f}
+          : @pattern.type.under_forall_vars_relation1 p k1 F (@pattern.type.lam_forall_vars p k1 f)
+            <-> forall ls',
+              List.length ls' = List.length (List.rev (PositiveSet.elements p))
+              -> let evm := fold_left (fun m '(k, v) => PositiveMap.add k v m) (List.combine (List.rev (PositiveSet.elements p)) ls') (PositiveMap.empty _) in
+                 F evm (f evm).
+        Proof using Type.
+          cbv [pattern.type.under_forall_vars_relation1 pattern.type.lam_forall_vars].
+          generalize (PositiveMap.empty base.type).
+          generalize (rev (PositiveSet.elements p)).
+          clear p.
+          intros ls m.
+          revert k1 F f m.
+          induction ls as [|l ls IHls]; cbn [list_rect fold_right fold_left List.length] in *; intros.
+          { split; intro H; [ intros [|] | specialize (H nil eq_refl) ]; cbn [List.length List.combine fold_right] in *; intros; try discriminate; assumption. }
+          { setoid_rewrite IHls; clear IHls.
+            split; intro H; [ intros [|l' ls'] Hls'; [ | specialize (H l' ls') ]
+                            | intros t ls' Hls'; specialize (H (cons t ls')) ];
+            cbn [List.length List.combine fold_left] in *;
+            try discriminate; inversion Hls'; eauto. }
+        Qed.
       End type.
     End pattern.
 
@@ -1089,18 +1112,10 @@ Module Compilers.
                            | progress expr.inversion_wf_constr ].
           Qed.
 
-          Definition forall2_type_of_list_cps {ls K1 K2} (P : K1 -> K2 -> Prop)
-            : type_of_list_cps K1 ls -> type_of_list_cps K2 ls -> Prop
-            := list_rect
-                 (fun ls => type_of_list_cps K1 ls -> type_of_list_cps K2 ls -> Prop)
-                 P
-                 (fun T Ts rec f1 f2 => forall x : T, rec (f1 x) (f2 x))
-                 ls.
-
-          Lemma related_app_type_of_list_of_forall2_type_of_list_cps {K1 K2 ls args}
+          Lemma related_app_type_of_list_of_under_type_of_list_relation_cps {K1 K2 ls args}
                 {v1 v2}
                 (P : _ -> _ -> Prop)
-            : @forall2_type_of_list_cps ls K1 K2 P v1 v2
+            : @under_type_of_list_relation_cps K1 K2 ls P v1 v2
               -> P (app_type_of_list v1 args) (app_type_of_list v2 args).
           Proof using Type.
             induction ls as [|x ls IHls]; [ now (cbn; eauto) | ].
@@ -1156,7 +1171,7 @@ Module Compilers.
                | pattern.Ident t1 idc1, pattern.Ident t2 idc2
                  => fun v1 v2
                     => { pf : existT pident t1 idc1 = existT pident t2 idc2
-                       | forall2_type_of_list_cps
+                       | under_type_of_list_relation_cps
                            P
                            (rew [fun tidc => type_of_list_cps K1 (pident_arg_types (projT1 tidc) (projT2 tidc))] pf in (v1 : type_of_list_cps _ (pident_arg_types _ (projT2 (existT pident _ _)))))
                            v2 }
diff --git a/src/Experiments/NewPipeline/RewriterWf2.v b/src/Experiments/NewPipeline/RewriterWf2.v
index feb5b98f9..e7b1f179b 100644
--- a/src/Experiments/NewPipeline/RewriterWf2.v
+++ b/src/Experiments/NewPipeline/RewriterWf2.v
@@ -200,7 +200,7 @@ Module Compilers.
                                 end
                               | solve [ eauto ]
                               | progress cbv [Option.bind] in *
-                              | apply related_app_type_of_list_of_forall2_type_of_list_cps ].
+                              | apply related_app_type_of_list_of_under_type_of_list_relation_cps ].
           Qed.
 
           Lemma wf_unify_pattern'_id