Minor improvements to wf framework

2 files changed, 113 insertions, 90 deletions

diff --git a/src/Experiments/NewPipeline/LanguageInversion.v b/src/Experiments/NewPipeline/LanguageInversion.v
index 9b4dd8ff1..e65630e43 100644
--- a/src/Experiments/NewPipeline/LanguageInversion.v
+++ b/src/Experiments/NewPipeline/LanguageInversion.v
@@ -12,6 +12,76 @@ Require Import Crypto.Util.FixCoqMistakes.
 Import EqNotations.
 Module Compilers.
   Import Language.Compilers.
+
+  Module base.
+    Module type.
+      Section encode_decode.
+          Definition code (t1 t2 : base.type) : Prop
+            := match t1, t2 with
+               | base.type.type_base t1, base.type.type_base t2 => t1 = t2
+               | base.type.prod A1 B1, base.type.prod A2 B2 => A1 = A2 /\ B1 = B2
+               | base.type.list A1, base.type.list A2 => A1 = A2
+               | base.type.type_base _, _
+               | base.type.prod _ _, _
+               | base.type.list _, _
+                 => False
+               end.
+
+          Definition encode (x y : base.type) : x = y -> code x y.
+          Proof. intro p; destruct p, x; repeat constructor. Defined.
+          Definition decode (x y : base.type) : code x y -> x = y.
+          Proof. destruct x, y; intro p; try assumption; destruct p; (apply f_equal || apply f_equal2); (assumption || reflexivity). Defined.
+
+          Definition path_rect {x y : base.type} (Q : x = y -> Type)
+                     (f : forall p, Q (decode x y p))
+            : forall p, Q p.
+          Proof. intro p; specialize (f (encode x y p)); destruct x, p; exact f. Defined.
+      End encode_decode.
+
+      Global Instance base_eq_Decidable : DecidableRel (@eq base.type.base) := base.type.base_eq_dec.
+      Global Instance base_type_eq_Decidable : DecidableRel (@eq base.type.type) := base.type.type_eq_dec.
+      Global Instance base_eq_HProp : IsHPropRel (@eq base.type.base) := _.
+      Global Instance base_type_eq_HProp : IsHPropRel (@eq base.type.type) := _.
+
+      Ltac induction_type_in_using H rect :=
+        induction H as [H] using (rect _ _);
+        cbv [code] in H;
+        let H1 := fresh H in
+        let H2 := fresh H in
+        try lazymatch type of H with
+            | False => exfalso; exact H
+            | True => destruct H
+            | ?x = ?x => clear H
+            | _ = _ :> base.type.base => try solve [ exfalso; inversion H ]
+            | _ /\ _ => destruct H as [H1 H2]
+            end.
+
+      Ltac inversion_type_step :=
+        cbv [defaults.type_base] in *;
+        first [ lazymatch goal with
+                | [ H : ?x = ?x :> base.type.type |- _ ] => clear H || eliminate_hprop_eq_helper H base_type_eq_HProp
+                | [ H : ?x = ?x :> base.type.base |- _ ] => clear H || eliminate_hprop_eq_helper H base_eq_HProp
+                | [ H : ?x = ?y :> base.type.type |- _ ] => subst x || subst y
+                | [ H : ?x = ?y :> base.type.base |- _ ] => subst x || subst y
+                end
+              | lazymatch goal with
+                | [ H : _ = base.type.type_base _ |- _ ]
+                  => induction_type_in_using H @path_rect
+                | [ H : base.type.type_base _ = _ |- _ ]
+                  => induction_type_in_using H @path_rect
+                | [ H : _ = base.type.prod _ _ |- _ ]
+                  => induction_type_in_using H @path_rect
+                | [ H : base.type.prod _ _ = _ |- _ ]
+                  => induction_type_in_using H @path_rect
+                | [ H : _ = base.type.list _ |- _ ]
+                  => induction_type_in_using H @path_rect
+                | [ H : base.type.list _ = _ |- _ ]
+                  => induction_type_in_using H @path_rect
+                end ].
+      Ltac inversion_type := repeat inversion_type_step.
+    End type.
+  End base.
+
   Module type.
     Section with_base.
       Context {base_type : Type}.
@@ -81,76 +151,15 @@ Module Compilers.
         => refine (@preinvert_one_type _ P t Q _)
       end;
       intros ? e ?; intros; cbv [mark].
-  End type.
 
-  Module base.
-    Module type.
-      Section encode_decode.
-          Definition code (t1 t2 : base.type) : Prop
-            := match t1, t2 with
-               | base.type.type_base t1, base.type.type_base t2 => t1 = t2
-               | base.type.prod A1 B1, base.type.prod A2 B2 => A1 = A2 /\ B1 = B2
-               | base.type.list A1, base.type.list A2 => A1 = A2
-               | base.type.type_base _, _
-               | base.type.prod _ _, _
-               | base.type.list _, _
-                 => False
-               end.
-
-          Definition encode (x y : base.type) : x = y -> code x y.
-          Proof. intro p; destruct p, x; repeat constructor. Defined.
-          Definition decode (x y : base.type) : code x y -> x = y.
-          Proof. destruct x, y; intro p; try assumption; destruct p; (apply f_equal || apply f_equal2); (assumption || reflexivity). Defined.
-
-          Definition path_rect {x y : base.type} (Q : x = y -> Type)
-                     (f : forall p, Q (decode x y p))
-            : forall p, Q p.
-          Proof. intro p; specialize (f (encode x y p)); destruct x, p; exact f. Defined.
-      End encode_decode.
-
-      Global Instance base_eq_Decidable : DecidableRel (@eq base.type.base) := base.type.base_eq_dec.
-      Global Instance base_type_eq_Decidable : DecidableRel (@eq base.type.type) := base.type.type_eq_dec.
-      Global Instance base_eq_HProp : IsHPropRel (@eq base.type.base) := _.
-      Global Instance base_type_eq_HProp : IsHPropRel (@eq base.type.type) := _.
-
-      Ltac induction_type_in_using H rect :=
-        induction H as [H] using (rect _ _);
-        cbv [code] in H;
-        let H1 := fresh H in
-        let H2 := fresh H in
-        try lazymatch type of H with
-            | False => exfalso; exact H
-            | True => destruct H
-            | ?x = ?x => clear H
-            | _ = _ :> base.type.base => try solve [ exfalso; inversion H ]
-            | _ /\ _ => destruct H as [H1 H2]
-            end.
-
-      Ltac inversion_type_step :=
-        cbv [defaults.type_base] in *;
-        first [ lazymatch goal with
-                | [ H : ?x = ?x :> base.type.type |- _ ] => clear H || eliminate_hprop_eq_helper H base_type_eq_HProp
-                | [ H : ?x = ?x :> base.type.base |- _ ] => clear H || eliminate_hprop_eq_helper H base_eq_HProp
-                | [ H : ?x = ?y :> base.type.type |- _ ] => subst x || subst y
-                | [ H : ?x = ?y :> base.type.base |- _ ] => subst x || subst y
-                end
-              | lazymatch goal with
-                | [ H : _ = base.type.type_base _ |- _ ]
-                  => induction_type_in_using H @path_rect
-                | [ H : base.type.type_base _ = _ |- _ ]
-                  => induction_type_in_using H @path_rect
-                | [ H : _ = base.type.prod _ _ |- _ ]
-                  => induction_type_in_using H @path_rect
-                | [ H : base.type.prod _ _ = _ |- _ ]
-                  => induction_type_in_using H @path_rect
-                | [ H : _ = base.type.list _ |- _ ]
-                  => induction_type_in_using H @path_rect
-                | [ H : base.type.list _ = _ |- _ ]
-                  => induction_type_in_using H @path_rect
-                end ].
-      Ltac inversion_type := repeat inversion_type_step.
-    End type.
-  End base.
+    Ltac invert_one e :=
+      generalize_one_eq_var e;
+      destruct e;
+      try discriminate;
+      type.inversion_type;
+      base.type.inversion_type;
+      cbn [type.decode base.type.decode f_equal f_equal2 eq_rect] in *.
+  End type.
 
   Module expr.
     Section with_var.
@@ -222,34 +231,21 @@ Module Compilers.
       End encode_decode.
     End with_var.
 
-    Ltac invert_one e :=
-      type.generalize_one_eq_var e;
-      destruct e;
-      try discriminate;
-      type.inversion_type;
-      base.type.inversion_type;
-      cbn [type.decode base.type.decode f_equal f_equal2 eq_rect] in *.
-
     Ltac invert_step :=
       match goal with
-      | [ e : expr (type.base _) |- _ ] => invert_one e
-      | [ e : expr (type.arrow _ _) |- _ ] => invert_one e
+      | [ e : expr.expr (type.base _) |- _ ] => type.invert_one e
+      | [ e : expr.expr (defaults.type_base _) |- _ ] => type.invert_one e
+      | [ e : expr.expr (type.arrow _ _) |- _ ] => type.invert_one e
       end.
 
     Ltac invert := repeat invert_step.
 
     Ltac invert_match_step :=
       match goal with
-      | [ |- context[match ?e with expr.Ident _ _ => _ | _ => _ end] ]
-        => invert_one e
-      | [ |- context[match ?e with expr.Var _ _ => _ end] ]
-        => invert_one e
-      | [ |- context[match ?e with expr.App _ _ _ _ => _ end] ]
-        => invert_one e
-      | [ |- context[match ?e with expr.LetIn _ _ _ _ => _ end] ]
-        => invert_one e
-      | [ |- context[match ?e with expr.Abs _ _ _ => _ end] ]
-        => invert_one e
+      | [ H : context[match ?e with expr.Var _ _ => _ | _ => _ end] |- _ ]
+        => type.invert_one e
+      | [ |- context[match ?e with expr.Var _ _ => _ | _ => _ end] ]
+        => type.invert_one e
       end.
 
     Ltac invert_match := repeat invert_match_step.
@@ -308,4 +304,24 @@ Module Compilers.
       end.
     Ltac inversion_expr := repeat inversion_expr_step.
   End expr.
+
+  Module ident.
+    Ltac invert_step :=
+      match goal with
+      | [ e : ident (type.base _) |- _ ] => type.invert_one e
+      | [ e : ident (type.arrow _ _) |- _ ] => type.invert_one e
+      end.
+
+    Ltac invert := repeat invert_step.
+
+    Ltac invert_match_step :=
+      match goal with
+      | [ H : context[match ?e with ident.Literal _ _ => _ | _ => _ end] |- _ ]
+        => type.invert_one e
+      | [ |- context[match ?e with ident.Literal _ _ => _ | _ => _ end] ]
+        => type.invert_one e
+      end.
+
+    Ltac invert_match := repeat invert_match_step.
+  End ident.
 End Compilers.
diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v
index 5e9696d77..2aac184ec 100644
--- a/src/Experiments/NewPipeline/LanguageWf.v
+++ b/src/Experiments/NewPipeline/LanguageWf.v
@@ -585,8 +585,15 @@ Module Compilers.
             | [ H : context[expr.interp _ _ == expr.interp _ _] |- expr.interp _ _ == expr.interp _ _ ]
               => eapply H; eauto with nocore; solve [ repeat interp_safe_t_step ]
             end ].
+  Ltac interp_unsafe_t_step :=
+    first [ solve [ eauto with nocore ]
+          | match goal with
+            | [ H : context[expr.interp _ _ == expr.interp _ _] |- expr.interp _ _ == expr.interp _ _ ]
+              => eapply H; eauto with nocore; match goal with |- ?G => tryif has_evar G then fail else idtac end
+            end ].
   Ltac interp_safe_t := repeat interp_safe_t_step.
-  Ltac interp_t_step := first [ interp_safe_t_step ].
+  Ltac interp_unsafe_t := repeat interp_unsafe_t_step.
+  Ltac interp_t_step := first [ interp_safe_t_step | interp_unsafe_t_step ].
   Ltac interp_t := repeat interp_t_step.