Add invert_expr

3 files changed, 101 insertions, 0 deletions

diff --git a/_CoqProject b/_CoqProject
index 513c2f7c6..4e7c793b7 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -124,6 +124,7 @@ src/Reflection/SmartMap.v
 src/Reflection/Syntax.v
 src/Reflection/TestCase.v
 src/Reflection/Tuple.v
+src/Reflection/TypeInversion.v
 src/Reflection/Wf.v
 src/Reflection/WfInversion.v
 src/Reflection/WfProofs.v
diff --git a/src/Reflection/ExprInversion.v b/src/Reflection/ExprInversion.v
index 1130570a9..3d0caa0cb 100644
--- a/src/Reflection/ExprInversion.v
+++ b/src/Reflection/ExprInversion.v
@@ -1,4 +1,5 @@
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.TypeInversion.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Tactics.DestructHead.
@@ -138,6 +139,23 @@ Global Arguments invert_Pair {_ _ _ _ _} _.
 Global Arguments invert_Abs {_ _ _ _ _} _ _.
 Global Arguments invert_Return {_ _ _ _} _.
 
+Ltac invert_one_expr e :=
+  preinvert_one_type e;
+  intros ? e;
+  destruct e;
+  try exact I.
+
+Ltac invert_expr_step :=
+  match goal with
+  | [ e : exprf _ _ (Tbase _) |- _ ] => invert_one_expr e
+  | [ e : exprf _ _ (Prod _ _) |- _ ] => invert_one_expr e
+  | [ e : exprf _ _ Unit |- _ ] => invert_one_expr e
+  | [ e : expr _ _ (Tflat _) |- _ ] => invert_one_expr e
+  | [ e : expr _ _ (Arrow _ _) |- _ ] => invert_one_expr e
+  end.
+
+Ltac invert_expr := repeat invert_expr_step.
+
 Ltac invert_expr_subst_step :=
   match goal with
   | [ H : invert_Var ?e = Some _ |- _ ] => apply invert_Var_Some in H
diff --git a/src/Reflection/TypeInversion.v b/src/Reflection/TypeInversion.v
new file mode 100644
index 000000000..964e84d36
--- /dev/null
+++ b/src/Reflection/TypeInversion.v
@@ -0,0 +1,82 @@
+Require Import Crypto.Reflection.Syntax.
+
+Section language.
+  Context {base_type_code : Type}.
+
+  Definition preinvert_Tbase (P : flat_type base_type_code -> Type) (Q : forall t, P (Tbase t) -> Type)
+    : (forall t (p : P t), match t return P t -> Type with
+                           | Tbase t' => Q t'
+                           | _ => fun _ => True
+                           end p)
+      -> forall t p, Q t p.
+  Proof.
+    intros H t p; specialize (H (Tbase t) p); assumption.
+  Defined.
+
+  Definition preinvert_Unit (P : flat_type base_type_code -> Type) (Q : P Unit -> Type)
+    : (forall t (p : P t), match t return P t -> Type with
+                           | Unit => Q
+                           | _ => fun _ => True
+                           end p)
+      -> forall p, Q p.
+  Proof.
+    intros H p; specialize (H _ p); assumption.
+  Defined.
+
+  Definition preinvert_Prod (P : flat_type base_type_code -> Type) (Q : forall A B, P (Prod A B) -> Type)
+    : (forall t (p : P t), match t return P t -> Type with
+                           | Prod A B => Q A B
+                           | _ => fun _ => True
+                           end p)
+      -> forall A B p, Q A B p.
+  Proof.
+    intros H A B p; specialize (H _ p); assumption.
+  Defined.
+
+  Definition preinvert_Arrow (P : type base_type_code -> Type) (Q : forall A B, P (Arrow A B) -> Type)
+    : (forall t (p : P t), match t return P t -> Type with
+                           | Arrow A B => Q A B
+                           | _ => fun _ => True
+                           end p)
+      -> forall A B p, Q A B p.
+  Proof.
+    intros H A B p; specialize (H _ p); assumption.
+  Defined.
+
+  Definition preinvert_Tflat (P : type base_type_code -> Type) (Q : forall T, P (Tflat T) -> Type)
+    : (forall t (p : P t), match t return P t -> Type with
+                           | Tflat T => Q T
+                           | _ => fun _ => True
+                           end p)
+      -> forall T p, Q T p.
+  Proof.
+    intros H T p; specialize (H _ p); assumption.
+  Defined.
+End language.
+
+Ltac preinvert_one_type e :=
+  lazymatch type of e with
+  | ?P (Tbase ?T)
+    => is_var T;
+       move e at top;
+       revert dependent T;
+       refine (preinvert_Tbase P _ _)
+  | ?P (Prod ?A ?B)
+    => is_var A; is_var B;
+       move e at top; revert dependent A; intros A e;
+       move e at top; revert dependent B; revert A;
+       refine (preinvert_Prod P _ _)
+  | ?P Unit
+    => revert dependent e;
+       refine (preinvert_Unit P _ _)
+  | ?P (Tflat ?T)
+    => is_var T;
+       move e at top;
+       revert dependent T;
+       refine (preinvert_Tflat P _ _)
+  | ?P (Arrow ?A ?B)
+    => is_var A; is_var B;
+       move e at top; revert dependent A; intros A e;
+       move e at top; revert dependent B; revert A;
+       refine (preinvert_Arrow P _ _)
+  end.