Generalize InlineWf

1 files changed, 158 insertions, 31 deletions

diff --git a/src/Reflection/InlineWf.v b/src/Reflection/InlineWf.v
index defd5b23e..46f4824b3 100644
--- a/src/Reflection/InlineWf.v
+++ b/src/Reflection/InlineWf.v
@@ -1,9 +1,16 @@
 (** * Inline: Remove some [Let] expressions *)
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Wf.
+Require Import Crypto.Reflection.TypeInversion.
+Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.WfProofs.
+Require Import Crypto.Reflection.WfInversion.
 Require Import Crypto.Reflection.Inline.
 Require Import Crypto.Util.Tactics.SpecializeBy Crypto.Util.Tactics.DestructHead Crypto.Util.Sigma Crypto.Util.Prod.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.UniquePose.
+Require Import Crypto.Util.Tactics.SplitInContext.
 
 Local Open Scope ctype_scope.
 Section language.
@@ -19,6 +26,21 @@ Section language.
   Local Notation wff := (@wff base_type_code op).
   Local Notation wf := (@wf base_type_code op).
 
+  Local Notation wff_inline_directive G x y :=
+    (wff G (exprf_of_inline_directive x) (exprf_of_inline_directive y)
+     /\ (fun x' y'
+         => match x', y' with
+            | default_inline _ _, default_inline _ _
+            | no_inline _ _, no_inline _ _
+            | inline _ _, inline _ _
+              => True
+            | default_inline _ _, _
+            | no_inline _ _, _
+            | inline _ _, _
+              => False
+            end) x y).
+
+
   Section with_var.
     Context {var1 var2 : base_type_code -> Type}.
 
@@ -45,59 +67,164 @@ Section language.
                    | constructor
                    | solve [ eauto ] ].
 
-    Lemma wff_inline_constf is_const {t} e1 e2 G G'
+    Local Ltac invert_inline_directive' i :=
+      preinvert_one_type i;
+      intros ? i;
+      destruct i;
+      try exact I.
+    Local Ltac invert_inline_directive :=
+      match goal with
+      | [ i : inline_directive _ |- _ ] => invert_inline_directive' i
+      end.
+
+    (** XXX TODO: Clean up this proof *)
+    Lemma wff_inline_const_genf postprocess1 postprocess2 {t} e1 e2 G G'
              (H : forall t x x', List.In (existT (fun t : base_type_code => (exprf (Tbase t) * exprf (Tbase t))%type) t (x, x')) G'
-                            -> wff G x x')
+                                 -> wff G x x')
              (wf : wff G' e1 e2)
-      : @wff var1 var2 G t (inline_constf is_const e1) (inline_constf is_const e2).
+             (wf_postprocess : forall G t e1 e2,
+                 wff G e1 e2
+                 -> wff_inline_directive G (postprocess1 t e1) (postprocess2 t e2))
+      : @wff var1 var2 G t (inline_const_genf postprocess1 e1) (inline_const_genf postprocess2 e2).
     Proof.
-      revert dependent G; induction wf; simpl in *; intros; auto;
-        specialize_by auto; unfold postprocess_for_const.
+      revert dependent G; induction wf; simpl in *; auto; intros; [].
       repeat match goal with
              | [ H : context[List.In _ (_ ++ _)] |- _ ]
                => setoid_rewrite List.in_app_iff in H
+             | [ |- context[postprocess1 ?t ?e1] ]
+               => match goal with
+                  | [ |- context[postprocess2 t ?e2] ]
+                    => specialize (fun G => wf_postprocess G t e1 e2);
+                         generalize dependent (postprocess1 t e1);
+                         generalize dependent (postprocess2 t e2)
+                  end
+             | _ => intro
              end.
-      match goal with
-      | [ H : _ |- _ ]
-        => pose proof (IHwf _ H) as IHwf'
-      end.
-      generalize dependent (inline_constf is_const e1); generalize dependent (inline_constf is_const e1'); intros.
-      destruct IHwf'; simpl in *;
-        try match goal with |- context[@is_const ?x ?y ?z] => is_var y; destruct (@is_const x y z), y end;
-        repeat constructor; auto; intros;
-          match goal with
-          | [ H : _ |- _ ]
-            => apply H; intros; progress destruct_head_hnf' or
-          end;
-          t_fin.
+      repeat match goal with
+             | [ H : forall G : list _, _ |- wff ?G' _ _ ]
+               => unique pose proof (H G')
+             | [ H : forall x y (G : list _), _ |- wff ?G' _ _ ]
+               => unique pose proof (fun x y => H x y G')
+             | [ H : forall x1 x2, (forall t x x', _ \/ List.In _ ?G -> wff ?G0 x x') -> _,
+                   H' : forall t1 x1 x1', List.In _ ?G -> wff ?G0 x1 x1' |- _ ]
+               => unique pose proof (fun x1 x2 f => H x1 x2 (fun t x x' pf => match pf with or_introl pf => f t x x' pf | or_intror pf => H' t x x' pf end))
+             end.
+      repeat match goal with
+             | _ => exact I
+             | [ H : forall x1 : unit, _ |- _ ] => specialize (H tt)
+             | [ H : False |- _ ] => exfalso; assumption
+             | _ => progress subst
+             | _ => progress inversion_sigma
+             | _ => progress inversion_prod
+             | _ => progress destruct_head' and
+             | _ => inversion_wff_step; progress subst
+             | _ => progress specialize_by_assumption
+             | _ => progress break_match
+             | _ => progress invert_inline_directive
+             | [ |- context[match ?e with _ => _ end] ]
+               => invert_one_expr e
+             | _ => progress destruct_head' or
+             | _ => progress simpl in *
+             | _ => intro
+             | _ => progress split_and
+             | [ H : wff _ TT _ |- _ ] => solve [ inversion H ]
+             | [ H : wff _ (Var _ _) _ |- _ ] => solve [ inversion H ]
+             | [ H : wff _ (Op _ _) _ |- _ ] => solve [ inversion H ]
+             | [ H : wff _ (LetIn _ _) _ |- _ ] => solve [ inversion H ]
+             | [ H : wff _ (Pair _ _) _ |- _ ] => solve [ inversion H ]
+             end;
+        repeat first [ progress specialize_by tauto
+                     | progress specialize_by auto
+                     | solve [ auto ] ];
+        try (constructor; auto; intros).
+      { match goal with H : _ |- _ => apply H end.
+        intros; destruct_head or; t_fin. }
+      { match goal with H : _ |- _ => apply H end.
+        intros; destruct_head or; t_fin. }
+      { match goal with H : _ |- _ => apply H end.
+        intros; destruct_head or; t_fin. }
+      { match goal with H : _ |- _ => apply H end.
+        intros; destruct_head' or; t_fin. }
+      { match goal with H : _ |- _ => apply H end.
+        intros; destruct_head or; t_fin. }
+      { match goal with H : _ |- _ => apply H end.
+        intros; destruct_head or; t_fin. }
     Qed.
 
-    Lemma wf_inline_const is_const {t} e1 e2 G G'
+    Lemma wff_postprocess_for_const is_const G t
+          (e1 : @exprf var1 t)
+          (e2 : @exprf var2 t)
+          (Hwf : wff G e1 e2)
+      : wff_inline_directive G (postprocess_for_const is_const t e1) (postprocess_for_const is_const t e2).
+    Proof.
+      destruct e1; unfold postprocess_for_const;
+        repeat first [ progress subst
+                     | intro
+                     | progress destruct_head' sig
+                     | progress destruct_head' and
+                     | progress inversion_sigma
+                     | progress inversion_option
+                     | progress inversion_prod
+                     | progress destruct_head' False
+                     | progress simpl in *
+                     | progress invert_expr
+                     | progress inversion_wff
+                     | progress break_innermost_match_step
+                     | congruence
+                     | solve [ auto ] ].
+    Qed.
+
+    Local Hint Resolve wff_postprocess_for_const.
+
+    Lemma wff_inline_constf is_const {t} e1 e2 G G'
+             (H : forall t x x', List.In (existT (fun t : base_type_code => (exprf (Tbase t) * exprf (Tbase t))%type) t (x, x')) G'
+                            -> wff G x x')
+             (wf : wff G' e1 e2)
+      : @wff var1 var2 G t (inline_constf is_const e1) (inline_constf is_const e2).
+    Proof. eapply wff_inline_const_genf; eauto. Qed.
+
+    Lemma wf_inline_const_gen postprocess1 postprocess2 {t} e1 e2 G G'
           (H : forall t x x', List.In (existT (fun t : base_type_code => (exprf (Tbase t) * exprf (Tbase t))%type) t (x, x')) G'
                               -> wff G x x')
           (Hwf : wf G' e1 e2)
-      : @wf var1 var2 G t (inline_const is_const e1) (inline_const is_const e2).
+          (wf_postprocess : forall G t e1 e2,
+              wff G e1 e2
+              -> wff_inline_directive G (postprocess1 t e1) (postprocess2 t e2))
+      : @wf var1 var2 G t (inline_const_gen postprocess1 e1) (inline_const_gen postprocess2 e2).
     Proof.
-      revert dependent G; induction Hwf; simpl; constructor; intros;
-        [ eapply (wff_inline_constf is_const); [ | solve [ eauto ] ] | ];
-        match goal with
-        | [ H : _ |- _ ]
-          => apply H; simpl; intros; progress destruct_head' or
-        end;
-        inversion_sigma; inversion_prod; repeat subst; simpl.
-      { constructor; left; reflexivity. }
-      { eauto. }
+      revert dependent G; induction Hwf; simpl; constructor; intros.
+      { eapply wff_inline_const_genf; eauto using wff_SmartVarVarf_nil. }
+      { match goal with H : _ |- _ => apply H end.
+        intros; destruct_head_hnf' or; t_fin. }
     Qed.
+
+    Lemma wf_inline_const is_const {t} e1 e2 G G'
+          (H : forall t x x', List.In (existT (fun t : base_type_code => (exprf (Tbase t) * exprf (Tbase t))%type) t (x, x')) G'
+                              -> wff G x x')
+          (Hwf : wf G' e1 e2)
+      : @wf var1 var2 G t (inline_const is_const e1) (inline_const is_const e2).
+    Proof. eapply wf_inline_const_gen; eauto. Qed.
   End with_var.
 
+  Lemma Wf_InlineConstGen postprocess {t} (e : Expr t)
+        (Hwf : Wf e)
+        (Hpostprocess : forall var1 var2 G t e1 e2,
+            wff G e1 e2
+            -> wff_inline_directive G (postprocess var1 t e1) (postprocess var2 t e2))
+    : Wf (InlineConstGen postprocess e).
+  Proof.
+    intros var1 var2.
+    apply (@wf_inline_const_gen var1 var2 (postprocess _) (postprocess _) t (e _) (e _) nil nil); simpl; auto; tauto.
+  Qed.
+
   Lemma Wf_InlineConst is_const {t} (e : Expr t)
         (Hwf : Wf e)
     : Wf (InlineConst is_const e).
   Proof.
     intros var1 var2.
-    apply (@wf_inline_const var1 var2 is_const t (e _) (e _) nil nil); simpl; [ tauto | ].
+    apply (@wf_inline_const var1 var2 is_const t (e _) (e _) nil nil); simpl; try tauto.
     apply Hwf.
   Qed.
 End language.
 
-Hint Resolve Wf_InlineConst : wf.
+Hint Resolve Wf_InlineConstGen Wf_InlineConst : wf.