Prove pattern.ident.type_vars_enough

4 files changed, 111 insertions, 14 deletions

diff --git a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v
index c991c3454..37db3be83 100644
--- a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v
+++ b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v
@@ -1,5 +1,6 @@
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.FSets.FMapPositive.
+Require Import Coq.MSets.MSetPositive.
 Require Import Coq.Lists.List.
 Require Import Crypto.Util.CPSNotations.
 Require Import Crypto.Util.Option.
@@ -45,6 +46,14 @@ Module Compilers.
            | type.list A => Compilers.base.type.list (subst_default A evar_map)
            end.
 
+      Fixpoint collect_vars (t : type) : PositiveSet.t
+        := match t with
+           | type.var p => PositiveSet.add p PositiveSet.empty
+           | type.type_base t => PositiveSet.empty
+           | type.prod A B => PositiveSet.union (collect_vars A) (collect_vars B)
+           | type.list A => collect_vars A
+           end.
+
       Module Notations.
         Global Coercion type.type_base : Compilers.base.type.base >-> type.type.
         Bind Scope pbtype_scope with type.type.
@@ -85,6 +94,12 @@ Module Compilers.
            | type.base t => type.base (base.subst_default t evar_map)
            | type.arrow A B => type.arrow (subst_default A evar_map) (subst_default B evar_map)
            end.
+
+      Fixpoint collect_vars (t : type) : PositiveSet.t
+        := match t with
+           | type.base t => base.collect_vars t
+           | type.arrow s d => PositiveSet.union (collect_vars s) (collect_vars d)
+           end.
     End type.
 
     (*
@@ -816,6 +831,7 @@ rettypes = [i.replace(prefix + 'ident.ident', 'ident').replace(prefix, '').repla
 
 retcode = r"""Require Import Coq.ZArith.ZArith.
 Require Import Coq.FSets.FMapPositive.
+Require Import Coq.MSets.MSetPositive.
 Require Import Coq.Lists.List.
 Require Import Crypto.Util.CPSNotations.
 Require Import Crypto.Util.Option.
@@ -861,6 +877,14 @@ Module Compilers.
            | type.list A => Compilers.base.type.list (subst_default A evar_map)
            end.
 
+      Fixpoint collect_vars (t : type) : PositiveSet.t
+        := match t with
+           | type.var p => PositiveSet.add p PositiveSet.empty
+           | type.type_base t => PositiveSet.empty
+           | type.prod A B => PositiveSet.union (collect_vars A) (collect_vars B)
+           | type.list A => collect_vars A
+           end.
+
       Module Notations.
         Global Coercion type.type_base : Compilers.base.type.base >-> type.type.
         Bind Scope pbtype_scope with type.type.
@@ -901,6 +925,12 @@ Module Compilers.
            | type.base t => type.base (base.subst_default t evar_map)
            | type.arrow A B => type.arrow (subst_default A evar_map) (subst_default B evar_map)
            end.
+
+      Fixpoint collect_vars (t : type) : PositiveSet.t
+        := match t with
+           | type.base t => base.collect_vars t
+           | type.arrow s d => PositiveSet.union (collect_vars s) (collect_vars d)
+           end.
     End type.
 
     (""" + """*
diff --git a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v
index bd8c8f341..c877c3898 100644
--- a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v
+++ b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v
@@ -1,7 +1,11 @@
 Require Import Coq.ZArith.ZArith.
+Require Import Coq.MSets.MSetPositive.
+Require Import Coq.FSets.FMapPositive.
+Require Import Crypto.Util.MSetPositive.Facts.
 Require Import Crypto.Util.CPSNotations.
 Require Import Crypto.Util.ZRange.
 Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.HProp.
@@ -195,6 +199,33 @@ Module Compilers.
                             end
                           | progress Compilers.type.inversion_type ].
       Qed.
+
+      Local Ltac solve_ex_or_eq :=
+        lazymatch goal with
+        | [ |- ex _ ] => eexists; solve_ex_or_eq
+        | [ |- _ /\ _ ] => split; solve_ex_or_eq
+        | [ |- _ \/ _ ] => (left + right); solve_ex_or_eq
+        | [ |- _ = _ ] => reflexivity || eassumption
+        end.
+      Lemma type_vars_enough
+        : forall t idc k,
+          PositiveSet.mem k (pattern.type.collect_vars t) = true
+          -> exists v, List.In v (@pattern.ident.type_vars t idc) /\ PositiveSet.mem k (pattern.type.collect_vars v) = true.
+      Proof using Type.
+        destruct idc; cbn [type.collect_vars ident.type_vars List.In base.collect_vars PositiveSet.mem PositiveSet.empty PositiveSet.union] in *.
+        all: repeat first [ match goal with
+                            | [ H : true = false |- _ ] => exfalso; apply Bool.diff_true_false, H
+                            | [ H : false = true |- _ ] => exfalso; apply Bool.diff_false_true, H
+                            | [ H : context[PositiveSet.mem _ (PositiveSet.union _ _)] |- _ ]
+                              => rewrite PositiveSetFacts.union_b in H
+                            | [ H : context[orb _ _ = true] |- _ ]
+                              => rewrite Bool.orb_true_iff in H
+                            end
+                          | progress cbn [PositiveSet.mem PositiveSet.empty] in *
+                          | progress intros
+                          | progress destruct_head'_or
+                          | solve_ex_or_eq ].
+      Qed.
     End ident.
   End pattern.
 End Compilers.
diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v
index d4746687e..d98fd6491 100644
--- a/src/Experiments/NewPipeline/Rewriter.v
+++ b/src/Experiments/NewPipeline/Rewriter.v
@@ -129,14 +129,6 @@ Module Compilers.
                    | _ => k None
                    end
            end%cps.
-
-      Fixpoint collect_vars (t : type) : PositiveSet.t
-        := match t with
-           | type.var p => PositiveSet.add p PositiveSet.empty
-           | type.type_base t => PositiveSet.empty
-           | type.prod A B => PositiveSet.union (collect_vars A) (collect_vars B)
-           | type.list A => collect_vars A
-           end.
     End base.
 
     Module type.
@@ -215,12 +207,6 @@ Module Compilers.
 
       Notation unify_extracted ptype etype := (unify_extracted_cps ptype etype _ id).
 
-      Fixpoint collect_vars (t : type) : PositiveSet.t
-        := match t with
-           | type.base t => base.collect_vars t
-           | type.arrow s d => PositiveSet.union (collect_vars s) (collect_vars d)
-           end.
-
       Local Notation forall_vars_body K LS EVM0
         := (fold_right
               (fun i k evm => forall t : Compilers.base.type, k (PositiveMap.add i t evm))
diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v
index a1244dd74..8169fc38a 100644
--- a/src/Experiments/NewPipeline/RewriterWf1.v
+++ b/src/Experiments/NewPipeline/RewriterWf1.v
@@ -385,6 +385,56 @@ Module Compilers.
         Ltac unify_extracted_cps_id :=
           cps_id_with_option (@unify_extracted_cps_id _ _ _ _).
 
+        Local Ltac t_subst_eq_iff :=
+          repeat first [ progress apply conj
+                       | progress cbv [option_map Option.bind] in *
+                       | progress intros
+                       | progress inversion_option
+                       | progress subst
+                       | progress destruct_head'_and
+                       | progress destruct_head'_or
+                       | progress destruct_head' iff
+                       | match goal with
+                         | [ |- context[PositiveSet.mem _ (PositiveSet.union _ _)] ]
+                           => setoid_rewrite PositiveSetFacts.union_b
+                         | [ |- context[orb _ _ = true] ]
+                           => setoid_rewrite Bool.orb_true_iff
+                         | [ H : context[PositiveSet.mem _ (PositiveSet.union _ _)] |- _ ]
+                           => setoid_rewrite PositiveSetFacts.union_b in H
+                         | [ H : context[orb _ _ = true] |- _ ]
+                           => setoid_rewrite Bool.orb_true_iff in H
+                         | [ H : type.base _ = type.base _ |- _ ] => inversion H; clear H
+                         | [ H : type.arrow _ _ = type.arrow _ _ |- _ ] => inversion H; clear H
+                         | [ H : ?x = ?x |- _ ] => clear H
+                         | [ H : (Some _ = None /\ _) \/ _ -> _ |- _ ]
+                           => specialize (fun pf => H (or_intror pf))
+                         | [ H : (_ /\ Some _ = None) \/ _ -> _ |- _ ]
+                           => specialize (fun pf => H (or_intror pf))
+                         | [ |- (Some _ = None /\ _) \/ _ ] => right
+                         end
+                       | progress specialize_by (exact eq_refl)
+                       | progress specialize_by_assumption
+                       | progress split_contravariant_or
+                       | solve [ eauto ]
+                       | break_innermost_match_hyps_step
+                       | break_innermost_match_step ].
+
+        Lemma subst_eq_iff {t evm1 evm2}
+          : pattern.type.subst t evm1 = pattern.type.subst t evm2
+            <-> ((pattern.type.subst t evm1 = None
+                  /\ pattern.type.subst t evm2 = None)
+                 \/ (forall t', PositiveSet.mem t' (pattern.type.collect_vars t) = true -> PositiveMap.find t' evm1 = PositiveMap.find t' evm2)).
+        Proof using Type.
+          induction t as [t|s IHs d IHd]; cbn [pattern.type.collect_vars pattern.type.subst];
+            [ pose proof (@pattern.base.subst_eq_iff t evm1 evm2) | ].
+          all: t_subst_eq_iff.
+        Qed.
+
+        Lemma subst_eq_if_mem {t evm1 evm2}
+          : (forall t', PositiveSet.mem t' (pattern.type.collect_vars t) = true -> PositiveMap.find t' evm1 = PositiveMap.find t' evm2)
+            -> pattern.type.subst t evm1 = pattern.type.subst t evm2.
+        Proof using Type. rewrite subst_eq_iff; eauto. Qed.
+
         Lemma app_forall_vars_under_forall_vars_relation
               {p k1 k2 F v1 v2 evm}
           : @pattern.type.under_forall_vars_relation p k1 k2 F v1 v2