More powerful preinvert_one_type

It's be nice if we could find a uniform way to do this for all flat_types which resolve to constructors...

1 files changed, 57 insertions, 27 deletions

diff --git a/src/Reflection/TypeInversion.v b/src/Reflection/TypeInversion.v
index 964e84d36..f7f3e9929 100644
--- a/src/Reflection/TypeInversion.v
+++ b/src/Reflection/TypeInversion.v
@@ -3,35 +3,47 @@ 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.
+  Section flat.
+    Context (P : flat_type base_type_code -> Type).
 
-  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.
+    Local Ltac t :=
+      let H := fresh in
+      intro H; intros;
+      match goal with
+      | [ p : _ |- _ ] => specialize (H _ p)
+      end;
+      assumption.
 
-  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_Tbase (Q : forall t, P (Tbase t) -> Type)
+      : (forall t (p : P t), match t return P t -> Type with Tbase _ => Q _ | _ => fun _ => True end p)
+        -> forall t p, Q t p.
+    Proof. t. Defined.
+
+    Definition preinvert_Unit (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. t. Defined.
+
+    Definition preinvert_Prod (Q : forall A B, P (Prod A B) -> Type)
+      : (forall t (p : P t), match t return P t -> Type with Prod _ _ => Q _ _ | _ => fun _ => True end p)
+        -> forall A B p, Q A B p.
+    Proof. t. Defined.
+
+    Definition preinvert_Prod2 (Q : forall A B, P (Prod (Tbase A) (Tbase B)) -> Type)
+      : (forall t (p : P t), match t return P t -> Type with Prod (Tbase _) (Tbase _) => Q _ _ | _ => fun _ => True end p)
+        -> forall A B p, Q A B p.
+    Proof. t. Defined.
+
+    Definition preinvert_Prod3 (Q : forall A B C, P (Tbase A * Tbase B * Tbase C)%ctype -> Type)
+      : (forall t (p : P t), match t return P t -> Type with Prod (Prod (Tbase _) (Tbase _)) (Tbase _) => Q _ _ _ | _ => fun _ => True end p)
+        -> forall A B C p, Q A B C p.
+    Proof. t. Defined.
+
+    Definition preinvert_Prod4 (Q : forall A B C D, P (Tbase A * Tbase B * Tbase C * Tbase D)%ctype -> Type)
+      : (forall t (p : P t), match t return P t -> Type with Prod (Prod (Prod (Tbase _) (Tbase _)) (Tbase _)) (Tbase _) => Q _ _ _ _ | _ => fun _ => True end p)
+        -> forall A B C D p, Q A B C D p.
+    Proof. t. Defined.
+  End flat.
 
   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
@@ -66,6 +78,24 @@ Ltac preinvert_one_type e :=
        move e at top; revert dependent A; intros A e;
        move e at top; revert dependent B; revert A;
        refine (preinvert_Prod P _ _)
+  | ?P (Prod (Tbase ?A) (Tbase ?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_Prod2 P _ _)
+  | ?P (Prod (Prod (Tbase ?A) (Tbase ?B)) (Tbase ?C))
+    => is_var A; is_var B; is_var C;
+       move e at top; revert dependent A; intros A e;
+       move e at top; revert dependent B; intros B e;
+       move e at top; revert dependent C; revert A B;
+       refine (preinvert_Prod3 P _ _)
+  | ?P (Prod (Prod (Prod (Tbase ?A) (Tbase ?B)) (Tbase ?C)) (Tbase ?D))
+    => is_var A; is_var B; is_var C; is_var D;
+       move e at top; revert dependent A; intros A e;
+       move e at top; revert dependent B; intros B e;
+       move e at top; revert dependent C; intros C e;
+       move e at top; revert dependent D; revert A B C;
+       refine (preinvert_Prod4 P _ _)
   | ?P Unit
     => revert dependent e;
        refine (preinvert_Unit P _ _)