Don't pass a wf proof into InterpToPHOAS

Use a fail-value instead.  This makes it easier to compose with other
transformations.

3 files changed, 59 insertions, 53 deletions

diff --git a/src/Reflection/Named/InterpretToPHOAS.v b/src/Reflection/Named/InterpretToPHOAS.v
index 3972dbdad..a9a44a93f 100644
--- a/src/Reflection/Named/InterpretToPHOAS.v
+++ b/src/Reflection/Named/InterpretToPHOAS.v
@@ -1,5 +1,6 @@
 Require Import Crypto.Reflection.Named.Syntax.
 Require Import Crypto.Reflection.Named.Wf.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Util.PointedProp.
 
@@ -12,54 +13,52 @@ Module Export Named.
             {Name : Type}.
     Section with_var.
       Context {var : base_type_code -> Type}
-              {Context : Context Name var}.
+              {Context : Context Name var}
+              (failb : forall t, @Syntax.exprf base_type_code op var (Tbase t)).
+
+      Local Notation failf t (* : @Syntax.exprf base_type_code op var t*)
+        := (SmartPairf (SmartValf _ failb t)).
 
       Fixpoint interpf_to_phoas
                (ctx : Context)
                {t} (e : @Named.exprf base_type_code op Name t)
                {struct e}
-        : prop_of_option (wff ctx e) -> @Syntax.exprf base_type_code op var t
-        := match e in Named.exprf _ _ _ t return prop_of_option (wff ctx e) -> @Syntax.exprf base_type_code op var t with
+        : @Syntax.exprf base_type_code op var t
+        := match e in Named.exprf _ _ _ t return @Syntax.exprf base_type_code op var t with
            | Named.Var t' x
-             => match lookupb ctx x t' as v return prop_of_option (if v return bool then true else false) -> _ with
-                | Some v => fun _ => Var v
-                | None => fun b => match b : False with end
+             => match lookupb ctx x t' with
+                | Some v => Var v
+                | None => failf _
                 end
-           | Named.TT => fun _ => TT
+           | Named.TT => TT
            | Named.Pair tx ex ty ey
-             => fun Hwf : prop_of_option (Named.wff _ _ /\ Named.wff _ _)%option_pointed_prop
-                => let (Hwf'1, Hwf'2) := eta_and (proj1 (prop_of_option_and _ _) Hwf) in
-                   Pair (@interpf_to_phoas ctx tx ex Hwf'1) (@interpf_to_phoas ctx ty ey Hwf'2)
+             => Pair (@interpf_to_phoas ctx tx ex) (@interpf_to_phoas ctx ty ey)
            | Named.Op _ _ opc args
-             => fun Hwf
-                => Op opc (@interpf_to_phoas ctx _ args Hwf)
+             => Op opc (@interpf_to_phoas ctx _ args)
            | Named.LetIn _ n ex _ eC
-             => fun Hwf : prop_of_option (Named.wff _ _ /\ inject (forall k, prop_of_option (Named.wff _ _)))%option_pointed_prop
-                => let (Hwf'1, Hwf'2) := eta_and (proj1 (prop_of_option_and _ _) Hwf) in
-                   LetIn (@interpf_to_phoas ctx _ ex Hwf'1)
-                         (fun v
-                          => @interpf_to_phoas (extend ctx n v) _ eC (Hwf'2 _))
+             => LetIn (@interpf_to_phoas ctx _ ex)
+                      (fun v
+                       => @interpf_to_phoas (extend ctx n v) _ eC)
            end.
 
       Definition interp_to_phoas
                  (ctx : Context)
                  {t} (e : @Named.expr base_type_code op Name t)
-                 (Hwf : wf ctx e)
         : @Syntax.expr base_type_code op var (domain t -> codomain t)
-        := Abs (fun v => interpf_to_phoas (extend ctx (Abs_name e) v) (invert_Abs e) (Hwf v)).
+        := Abs (fun v => interpf_to_phoas (extend ctx (Abs_name e) v) (invert_Abs e)).
     End with_var.
 
     Section all.
-      Context {Context : forall var, @Context base_type_code Name var}.
+      Context {Context : forall var, @Context base_type_code Name var}
+              (failb : forall var t, @Syntax.exprf base_type_code op var (Tbase t)).
       Definition InterpToPHOAS_gen
                  (ctx : forall var, Context var)
                  {t} (e : @Named.expr base_type_code op Name t)
-                 (Hwf : forall var, wf (ctx var) e)
         : @Syntax.Expr base_type_code op (domain t -> codomain t)
-        := fun var => interp_to_phoas (ctx var) e (Hwf var).
+        := fun var => interp_to_phoas (failb var) (ctx var) e.
 
-      Definition InterpToPHOAS {t} e (Hwf : forall var, wf empty e)
-        := @InterpToPHOAS_gen (fun var => empty) t e Hwf.
+      Definition InterpToPHOAS {t} e
+        := @InterpToPHOAS_gen (fun var => empty) t e.
     End all.
   End language.
 End Named.
diff --git a/src/Reflection/Named/InterpretToPHOASInterp.v b/src/Reflection/Named/InterpretToPHOASInterp.v
index 1cd0c5494..7dcdc198b 100644
--- a/src/Reflection/Named/InterpretToPHOASInterp.v
+++ b/src/Reflection/Named/InterpretToPHOASInterp.v
@@ -9,6 +9,7 @@ Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.DestructHead.
 
 Section language.
   Context {base_type_code : Type}
@@ -20,28 +21,33 @@ Section language.
           {interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst}.
   Section with_context.
     Context {Context : Context Name interp_base_type}
-            {ContextOk : ContextOk Context}.
+            {ContextOk : ContextOk Context}
+            (failb : forall t, @Syntax.exprf base_type_code op interp_base_type (Tbase t)).
 
     Lemma interpf_interpf_to_phoas
           (ctx : Context)
           {t} (e : @Named.exprf base_type_code op Name t)
           (Hwf : prop_of_option (Named.wff ctx e))
       : Named.interpf (interp_op:=interp_op) (ctx:=ctx) e
-        = Some (Syntax.interpf interp_op (interpf_to_phoas ctx e Hwf)).
+        = Some (Syntax.interpf interp_op (interpf_to_phoas failb ctx e)).
     Proof.
       revert dependent ctx; induction e;
         repeat first [ progress intros
                      | progress subst
                      | progress inversion_option
+                     | progress destruct_head' and
                      | progress break_innermost_match_step
                      | progress unfold option_map, LetIn.Let_In in *
                      | apply (f_equal (@Some _))
                      | apply (f_equal (@interp_op _ _ _))
                      | progress simpl in *
-                     | solve [ eauto | congruence ]
+                     | progress autorewrite with push_prop_of_option in *
+                     | solve [ eauto | congruence | tauto ]
                      | match goal with
                        | [ H : forall ctx Hwf', Named.interpf ?e = Some _, Hwf : prop_of_option (Named.wff _ ?e) |- _ ]
                          => specialize (H _ Hwf)
+                       | [ H : forall ctx Hwf, Named.interpf ?e = Some _ |- Named.interpf ?e = Some _ ]
+                         => rewrite H by auto
                        end ].
     Qed.
 
@@ -51,15 +57,16 @@ Section language.
           (Hwf : Named.wf ctx e)
           v
       : Named.interp (interp_op:=interp_op) (ctx:=ctx) e v
-        = Some (Syntax.interp interp_op (interp_to_phoas ctx e Hwf) v).
+        = Some (Syntax.interp interp_op (interp_to_phoas failb ctx e) v).
     Proof.
-      unfold interp, interp_to_phoas, Named.interp; apply interpf_interpf_to_phoas.
+      unfold interp, interp_to_phoas, Named.interp; apply interpf_interpf_to_phoas; auto.
     Qed.
   End with_context.
 
   Section all.
     Context {Context : forall var, @Context base_type_code Name var}
-            {ContextOk : forall var, ContextOk (Context var)}.
+            {ContextOk : forall var, ContextOk (Context var)}
+            (failb : forall var t, @Syntax.exprf base_type_code op var (Tbase t)).
 
     Lemma Interp_InterpToPHOAS_gen
           {ctx : forall var, Context var}
@@ -67,15 +74,15 @@ Section language.
           (Hwf : forall var, Named.wf (ctx var) e)
           v
       : Named.interp (interp_op:=interp_op) (ctx:=ctx _) e v
-        = Some (Interp interp_op (InterpToPHOAS_gen ctx e Hwf) v).
-    Proof. apply interp_interp_to_phoas. Qed.
+        = Some (Interp interp_op (InterpToPHOAS_gen failb ctx e) v).
+    Proof. apply interp_interp_to_phoas; auto. Qed.
 
     Lemma Interp_InterpToPHOAS
           {t} (e : @Named.expr base_type_code op Name t)
           (Hwf : Named.Wf Context e)
           v
       : Named.interp (Context:=Context _) (interp_op:=interp_op) (ctx:=empty) e v
-        = Some (Interp interp_op (InterpToPHOAS e Hwf) v).
-    Proof. apply interp_interp_to_phoas. Qed.
+        = Some (Interp interp_op (InterpToPHOAS (Context:=Context) failb e) v).
+    Proof. apply interp_interp_to_phoas; auto. Qed.
   End all.
 End language.
diff --git a/src/Reflection/Named/InterpretToPHOASWf.v b/src/Reflection/Named/InterpretToPHOASWf.v
index b3c10a8c4..e265dd0dc 100644
--- a/src/Reflection/Named/InterpretToPHOASWf.v
+++ b/src/Reflection/Named/InterpretToPHOASWf.v
@@ -9,6 +9,7 @@ Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.DestructHead.
 
 Section language.
   Context {base_type_code : Type}
@@ -18,10 +19,12 @@ Section language.
           {Name_dec : DecidableRel (@eq Name)}.
   Section with_var.
     Context {var1 var2 : base_type_code -> Type}
-            {Context1 : Context Name var2}
-            {Context2 : Context Name var1}
+            {Context1 : Context Name var1}
+            {Context2 : Context Name var2}
             {Context1Ok : ContextOk Context1}
-            {Context2Ok : ContextOk Context2}.
+            {Context2Ok : ContextOk Context2}
+            (failb1 : forall t, @Syntax.exprf base_type_code op var1 (Tbase t))
+            (failb2 : forall t, @Syntax.exprf base_type_code op var2 (Tbase t)).
 
     Local Ltac t_step :=
       first [ progress intros
@@ -68,20 +71,16 @@ Section language.
               -> List.In (existT _ t (v1, v2)%core) G)
           (Hctx1_ctx2 : forall n t,
               lookupb ctx1 n t = None <-> lookupb ctx2 n t = None)
-      : wff G (interpf_to_phoas ctx1 e Hwf1) (interpf_to_phoas ctx2 e Hwf2).
+      : wff G (interpf_to_phoas failb1 ctx1 e) (interpf_to_phoas failb2 ctx2 e).
     Proof.
       revert dependent G; revert dependent ctx1; revert dependent ctx2; induction e;
         repeat first [ progress intros
+                     | progress destruct_head' and
                      | progress break_innermost_match_step
                      | progress simpl in *
-                     | solve [ eauto ]
+                     | progress autorewrite with push_prop_of_option in *
+                     | solve [ eauto | tauto ]
                      | match goal with
-                       | [ |- context[@proj1 ?A ?B (prop_of_option_and ?a ?b) ?H] ]
-                         => destruct (@proj1 A B (prop_of_option_and a b) H); clear H
-                       | [ |- context[@proj1 ?A ?B (@conj ?A' ?B' ?x ?y)] ]
-                         => generalize (@proj1 A B (@conj A' B' x y));
-                            generalize (@proj2 A B (@conj A' B' x y));
-                            clear x y
                        | [ |- wff _ _ _ ] => constructor
                        end ].
       match goal with H : _ |- _ => eapply H end; t.
@@ -94,7 +93,7 @@ Section language.
           (Hwf2 : Named.wf ctx2 e)
           (Hctx1 : forall n t, lookupb ctx1 n t = None)
           (Hctx2 : forall n t, lookupb ctx2 n t = None)
-      : wf (interp_to_phoas ctx1 e Hwf1) (interp_to_phoas ctx2 e Hwf2).
+      : wf (interp_to_phoas failb1 ctx1 e) (interp_to_phoas failb2 ctx2 e).
     Proof.
       constructor; intros.
       apply wff_interpf_to_phoas; t.
@@ -102,24 +101,25 @@ Section language.
 
     Lemma wf_interp_to_phoas
           {t} (e : @Named.expr base_type_code op Name t)
-          (Hwf1 : Named.wf empty e)
-          (Hwf2 : Named.wf empty e)
-      : wf (interp_to_phoas (Context:=Context1) empty e Hwf1) (interp_to_phoas (Context:=Context2) empty e Hwf2).
+          (Hwf1 : Named.wf (Context:=Context1) empty e)
+          (Hwf2 : Named.wf (Context:=Context2) empty e)
+      : wf (interp_to_phoas (Context:=Context1) failb1 empty e) (interp_to_phoas (Context:=Context2) failb2 empty e).
     Proof.
-      apply wf_interp_to_phoas_gen; apply lookupb_empty; assumption.
+      apply wf_interp_to_phoas_gen; auto using lookupb_empty.
     Qed.
   End with_var.
 
   Section all.
     Context {Context : forall var, @Context base_type_code Name var}
-            {ContextOk : forall var, ContextOk (Context var)}.
+            {ContextOk : forall var, ContextOk (Context var)}
+            (failb : forall var t, @Syntax.exprf base_type_code op var (Tbase t)).
 
     Lemma Wf_InterpToPHOAS_gen
           {ctx : forall var, Context var}
           {t} (e : @Named.expr base_type_code op Name t)
           (Hctx : forall var n t, lookupb (ctx var) n t = None)
           (Hwf : forall var, Named.wf (ctx var) e)
-      : Wf (InterpToPHOAS_gen ctx e Hwf).
+      : Wf (InterpToPHOAS_gen failb ctx e).
     Proof.
       intros ??; apply wf_interp_to_phoas_gen; auto.
     Qed.
@@ -127,7 +127,7 @@ Section language.
     Lemma Wf_InterpToPHOAS
           {t} (e : @Named.expr base_type_code op Name t)
           (Hwf : Named.Wf Context e)
-      : Wf (InterpToPHOAS e Hwf).
+      : Wf (InterpToPHOAS (Context:=Context) failb e).
     Proof.
       intros ??; apply wf_interp_to_phoas; auto.
     Qed.