Use Fixpoint, not list_rect, for {app,lam}_forall_vars

This makes it much easier to read goals involving these combinators.

3 files changed, 134 insertions, 38 deletions

diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v
index d98fd6491..767404e01 100644
--- a/src/Experiments/NewPipeline/Rewriter.v
+++ b/src/Experiments/NewPipeline/Rewriter.v
@@ -250,6 +250,52 @@ Module Compilers.
              (List.rev (PositiveSet.elements p))
              (PositiveMap.empty _).
 
+      Fixpoint lam_forall_vars_gen {k : EvarMap -> Type}
+               (f : forall evm, k evm)
+               (ls : list PositiveMap.key)
+        : forall evm0, forall_vars_body k ls evm0
+        := match ls return forall evm0, forall_vars_body k ls evm0 with
+           | nil => f
+           | cons x xs => fun evm t => @lam_forall_vars_gen k f xs _
+           end.
+
+      Definition lam_forall_vars {p : PositiveSet.t} {k : EvarMap -> Type}
+                 (f : forall evm, k evm)
+        : forall_vars p k
+        := @lam_forall_vars_gen k f _ _.
+
+      Fixpoint app_forall_vars_gen {k : EvarMap -> Type}
+                 (evm : EvarMap)
+                 (ls : list PositiveMap.key)
+        : forall evm0, forall_vars_body k ls evm0
+                       -> option (k (fold_right (fun i k evm'
+                                                 => k (match PositiveMap.find i evm with Some v => PositiveMap.add i v evm' | None => evm' end))
+                                                (fun evm => evm)
+                                                ls
+                                                evm0))
+        := match ls return forall evm0, forall_vars_body k ls evm0
+                                        -> option (k (fold_right (fun i k evm'
+                                                                  => k (match PositiveMap.find i evm with Some v => PositiveMap.add i v evm' | None => evm' end))
+                                                                 (fun evm => evm)
+                                                                 ls
+                                                                 evm0)) with
+           | nil => fun evm0 val => Some val
+           | cons x xs
+             => match PositiveMap.find x evm as xt
+                      return (forall evm0,
+                                 (forall t, fold_right _ k xs (PositiveMap.add x t evm0))
+                                 -> option (k (fold_right
+                                                 _ _ xs
+                                                 match xt with
+                                                 | Some v => PositiveMap.add x v evm0
+                                                 | None => evm0
+                                                 end)))
+                with
+                | Some v => fun evm0 val => @app_forall_vars_gen k evm xs _ (val v)
+                | None => fun evm0 val => None
+                end
+           end.
+
       Definition app_forall_vars {p : PositiveSet.t} {k : EvarMap -> Type}
                  (f : forall_vars p k)
                  (evm : EvarMap)
@@ -258,42 +304,11 @@ Module Compilers.
                                 (fun evm => evm)
                                 (List.rev (PositiveSet.elements p))
                                 (PositiveMap.empty _)))
-        := list_rect
-             (fun ls
-              => forall evm0, forall_vars_body k ls evm0
-                  -> option (k (fold_right (fun i k evm'
-                                            => k (match PositiveMap.find i evm with Some v => PositiveMap.add i v evm' | None => evm' end))
-                                           (fun evm => evm)
-                                           ls
-                                           evm0)))
-             (fun evm0 val => Some val)
-             (fun x xs rec
-              => match PositiveMap.find x evm as xt
-                       return (forall evm0,
-                                  (forall t, fold_right _ k xs (PositiveMap.add x t evm0))
-                                  -> option (k (fold_right
-                                                  _ _ xs
-                                                  match xt with
-                                                  | Some v => PositiveMap.add x v evm0
-                                                  | None => evm0
-                                                  end)))
-                 with
-                 | Some v => fun evm0 val => rec _ (val v)
-                 | None => fun evm0 val => None
-                 end)
+        := @app_forall_vars_gen
+             k evm
              (List.rev (PositiveSet.elements p))
              (PositiveMap.empty _)
              f.
-
-      Definition lam_forall_vars {p : PositiveSet.t} {k : EvarMap -> Type}
-                 (f : forall evm, k evm)
-        : forall_vars p k
-        := list_rect
-             (fun ls => forall evm0, forall_vars_body k ls evm0)
-             f
-             (fun x xs rec evm t => rec _)
-             _
-             _.
     End type.
 
     Inductive pattern {ident : type -> Type} : type -> Type :=
diff --git a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
index 684c027a1..88a4f6670 100644
--- a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
+++ b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
@@ -104,7 +104,7 @@ Module Compilers.
       Local Ltac do_cbv0 :=
         cbv [id
                Compile.rewrite_rules_interp_goodT_curried
-               Compile.rewrite_rule_data_interp_goodT_curried 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 Compile.under_type_of_list_relation1_cps pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.rew_replacement 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.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.rewrite_rule_data_interp_goodT_curried 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 Compile.under_type_of_list_relation1_cps pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.rew_replacement 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 Compilers.pattern.type.lam_forall_vars_gen 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.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].
       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 8169fc38a..967921da5 100644
--- a/src/Experiments/NewPipeline/RewriterWf1.v
+++ b/src/Experiments/NewPipeline/RewriterWf1.v
@@ -305,6 +305,29 @@ Module Compilers.
 
         Ltac unify_extracted_cps_id :=
           cps_id_with_option (@unify_extracted_cps_id _ _ _ _).
+
+        Lemma mem_collect_vars_subst_Some_find {x t evm t'}
+              (Hmem : PositiveSet.mem x (pattern.base.collect_vars t) = true)
+              (H : pattern.base.subst t evm = Some t')
+          : PositiveMap.find x evm <> None.
+        Proof using Type.
+          revert t' H; induction t; intros.
+          all: repeat first [ progress cbn [pattern.base.collect_vars pattern.base.subst] in *
+                            | progress cbv [PositiveSetFacts.eqb Option.bind option_map] in *
+                            | progress subst
+                            | progress inversion_option
+                            | progress specialize_by_assumption
+                            | rewrite PositiveSetFacts.add_b in *
+                            | rewrite PositiveSetFacts.empty_b in *
+                            | rewrite PositiveSetFacts.union_b in *
+                            | rewrite Bool.orb_true_iff in *
+                            | congruence
+                            | break_innermost_match_hyps_step
+                            | progress destruct_head'_or
+                            | match goal with
+                              | [ H : forall x, Some _ = Some x -> _ |- _ ] => specialize (H _ eq_refl)
+                              end ].
+        Qed.
       End base.
 
       Module type.
@@ -560,7 +583,7 @@ Module Compilers.
               rewrite <- H''.
               clear -H_NoDup.
               match goal with
-              | [ |- context[list_rect _ _ _ _ _ (?f ?t)] ]
+              | [ |- context[pattern.type.app_forall_vars_gen _ _ _ (?f ?t)] ]
                 => generalize (f t); clear f
               end.
               intro f.
@@ -571,7 +594,7 @@ Module Compilers.
                      generalize dependent (PositiveMap.add x v evm); clear evm
               end.
               revert dependent evm.
-              induction xs as [|x' xs IHxs]; cbn [list_rect fold_right] in *.
+              induction xs as [|x' xs IHxs]; cbn [pattern.type.app_forall_vars_gen fold_right] in *.
               { intros; eliminate_hprop_eq; reflexivity. }
               { repeat first [ progress subst
                              | progress destruct_head'_and
@@ -613,7 +636,7 @@ Module Compilers.
           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.
+          induction ls as [|l ls IHls]; cbn [pattern.type.lam_forall_vars_gen 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') ]
@@ -629,12 +652,37 @@ Module Compilers.
           revert v; cbv [pattern.type.app_forall_vars pattern.type.lam_forall_vars].
           generalize (rev (PositiveSet.elements p)); clear p; intro ls.
           generalize (PositiveMap.empty base.type).
-          induction ls as [|x xs IHxs]; cbn [list_rect fold_right]; [ congruence | ].
+          induction ls as [|x xs IHxs]; cbn [pattern.type.app_forall_vars_gen pattern.type.lam_forall_vars_gen fold_right]; [ congruence | ].
           intros t v H; eapply IHxs; clear IHxs.
           rewrite <- H.
           break_innermost_match; [ | now discriminate ].
           reflexivity.
         Qed.
+
+        Lemma mem_collect_vars_subst_Some_find {x t evm t'}
+              (Hmem : PositiveSet.mem x (pattern.type.collect_vars t) = true)
+              (H : pattern.type.subst t evm = Some t')
+          : PositiveMap.find x evm <> None.
+        Proof using Type.
+          (* Coq's dependency tracking is broken and erroneously claims that [base.mem_collect_vars_subst_Some_find] depends on [type_base] if we wait too long to use it *)
+          pose proof (@base.mem_collect_vars_subst_Some_find).
+          revert t' H; induction t as [|s IHs d IHd]; intros.
+          all: repeat first [ progress cbn [pattern.type.collect_vars pattern.type.subst] in *
+                            | progress cbv [option_map Option.bind] in *
+                            | rewrite PositiveSetFacts.union_b in *
+                            | rewrite Bool.orb_true_iff in *
+                            | progress specialize_by_assumption
+                            | progress inversion_option
+                            | progress subst
+                            | break_innermost_match_hyps_step
+                            | progress destruct_head'_or
+                            | eassumption
+                            | reflexivity
+                            | solve [ eauto ]
+                            | match goal with
+                              | [ H : forall x, Some _ = Some x -> _ |- _ ] => specialize (H _ eq_refl)
+                              end ].
+        Qed.
       End type.
     End pattern.
 
@@ -2140,6 +2188,39 @@ Module Compilers.
                  (fun evm
                   => pattern_default_interp' p evm id).
 
+          Lemma app_lam_forall_vars_not_None_iff {k f p} {args}
+            : (@pattern.type.app_forall_vars p k (pattern.type.lam_forall_vars f) args <> None)
+              <-> (forall x, PositiveSet.mem x p = true -> PositiveMap.find x args <> None).
+          Proof.
+            setoid_rewrite <- PositiveSetFacts.In_elements_mem_iff; setoid_rewrite List.in_rev.
+            cbv [pattern.type.app_forall_vars pattern.type.lam_forall_vars].
+            generalize (PositiveMap.empty base.type).
+            induction (List.rev (PositiveSet.elements p)) as [|x xs IHxs];
+              cbn [pattern.type.app_forall_vars_gen pattern.type.lam_forall_vars_gen List.In].
+            { intuition congruence. }
+            { repeat first [ progress cbn [List.In] in *
+                           | progress specialize_by_assumption
+                           | progress split_contravariant_or
+                           | progress destruct_head'_ex
+                           | progress inversion_option
+                           | progress subst
+                           | progress intros
+                           | progress destruct_head'_or
+                           | solve [ eauto ]
+                           | match goal with
+                             | [ H : forall x, _ = x -> _ |- _ ] => specialize (H _ eq_refl)
+                             | [ H : ?x <> None |- _ ]
+                               => assert (exists v, x = Some v) by (destruct x; [ eexists; reflexivity | congruence ]); clear H
+                             | [ |- ?x <> None <-> ?RHS ]
+                               => let v := match x with context[match ?v with None => _ | _ => _ end] => v end in
+                                  let f := match (eval pattern v in x) with ?f _ => f end in
+                                  change (f v <> None <-> RHS); destruct v eqn:?
+                             | [ H : forall t, _ <-> _ |- _ ] => setoid_rewrite H; clear H
+                             end
+                           | apply conj
+                           | congruence ]. }
+          Qed.
+
           Definition deep_rewrite_ruleTP_gen_good_relation
                      {should_do_again with_opt under_lets : bool} {t}
                      (v1 : @deep_rewrite_ruleTP_gen should_do_again with_opt under_lets t)