Add Wf_InterpToPHOAS

4 files changed, 226 insertions, 51 deletions

diff --git a/src/Reflection/Named/ContextProperties.v b/src/Reflection/Named/ContextProperties.v
index d9bca2683..f8e9df198 100644
--- a/src/Reflection/Named/ContextProperties.v
+++ b/src/Reflection/Named/ContextProperties.v
@@ -14,6 +14,7 @@ Require Import Crypto.Util.Tactics.SplitInContext.
 Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.RewriteHyp.
+Require Import Crypto.Util.Tactics.SpecializeBy.
 
 Section with_context.
   Context {base_type_code Name var} (Context : @Context base_type_code Name var)
@@ -66,6 +67,7 @@ Section with_context.
           | rewrite lookupb_extendb_wrong_type by assumption ].
   Local Ltac misc_t_step :=
     first [ progress intros
+          | progress specialize_by_assumption
           | match goal with
             | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl)
             end
@@ -215,6 +217,20 @@ Section with_context.
     end.
   Local Ltac find_Name_and_val_default_to_None := repeat find_Name_and_val_default_to_None_step.
 
+  Lemma find_Name_and_val_flatten_binding_list
+        {var' var'' t n T N V1 V2 v1 v2}
+        (H1 : @find_Name_and_val var' t n T N V1 None = Some v1)
+        (H2 : @find_Name_and_val var'' t n T N V2 None = Some v2)
+    : List.In (existT (fun t => (var' t * var'' t)%type) t (v1, v2)) (Wf.flatten_binding_list V1 V2).
+  Proof.
+    induction T;
+      [ | | specialize (IHT1 (fst N) (fst V1) (fst V2));
+            specialize (IHT2 (snd N) (snd V1) (snd V2)) ];
+      repeat first [ find_Name_and_val_default_to_None_step
+                   | rewrite List.in_app_iff
+                   | t_step ].
+  Qed.
+
   Lemma find_Name_SmartFlatTypeMapInterp2_None_iff {var' n f T V N}
     : @find_Name n (SmartFlatTypeMap f (t:=T) V)
                  (SmartFlatTypeMapInterp2 (var':=var') (fun _ _ (n' : Name) => n') V N) = None
diff --git a/src/Reflection/Named/InterpretToPHOAS.v b/src/Reflection/Named/InterpretToPHOAS.v
index 4b3ef1b84..978d263d4 100644
--- a/src/Reflection/Named/InterpretToPHOAS.v
+++ b/src/Reflection/Named/InterpretToPHOAS.v
@@ -7,42 +7,57 @@ Module Export Named.
   Section language.
     Context {base_type_code : Type}
             {op : flat_type base_type_code -> flat_type base_type_code -> Type}
-            {var : base_type_code -> Type}
-            {Name}
-            {Context : Context Name var}.
+            {Name : Type}.
+    Section with_var.
+      Context {var : base_type_code -> Type}
+              {Context : Context Name var}.
 
-    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
-         | 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
-              end
-         | Named.TT => fun _ => TT
-         | Named.Pair tx ex ty ey
-           => fun Hwf : prop_of_option (Named.wff _ _ /\ Named.wff _ _)%option_pointed_prop
-              => let Hwf' := proj1 (prop_of_option_and _ _) Hwf in
-                 Pair (@interpf_to_phoas ctx tx ex (proj1 Hwf')) (@interpf_to_phoas ctx ty ey (proj2 Hwf'))
-         | Named.Op _ _ opc args
-           => fun Hwf
-              => Op opc (@interpf_to_phoas ctx _ args Hwf)
-         | 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' := proj1 (prop_of_option_and _ _) Hwf in
-                 LetIn (@interpf_to_phoas ctx _ ex (proj1 Hwf'))
-                       (fun v
-                        => @interpf_to_phoas (extend ctx n v) _ eC (proj2 Hwf' _))
-         end.
+      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
+           | 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
+                end
+           | Named.TT => fun _ => TT
+           | Named.Pair tx ex ty ey
+             => fun Hwf : prop_of_option (Named.wff _ _ /\ Named.wff _ _)%option_pointed_prop
+                => let Hwf' := proj1 (prop_of_option_and _ _) Hwf in
+                   Pair (@interpf_to_phoas ctx tx ex (proj1 Hwf')) (@interpf_to_phoas ctx ty ey (proj2 Hwf'))
+           | Named.Op _ _ opc args
+             => fun Hwf
+                => Op opc (@interpf_to_phoas ctx _ args Hwf)
+           | 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' := proj1 (prop_of_option_and _ _) Hwf in
+                   LetIn (@interpf_to_phoas ctx _ ex (proj1 Hwf'))
+                         (fun v
+                          => @interpf_to_phoas (extend ctx n v) _ eC (proj2 Hwf' _))
+           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)).
+      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)).
+    End with_var.
+
+    Section all.
+      Context {Context : forall var, @Context base_type_code Name var}.
+      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).
+
+      Definition InterpToPHOAS {t} e (Hwf : forall var, wf empty e)
+        := @InterpToPHOAS_gen (fun var => empty) t e Hwf.
+    End all.
   End language.
 End Named.
diff --git a/src/Reflection/Named/InterpretToPHOASWf.v b/src/Reflection/Named/InterpretToPHOASWf.v
new file mode 100644
index 000000000..b3c10a8c4
--- /dev/null
+++ b/src/Reflection/Named/InterpretToPHOASWf.v
@@ -0,0 +1,137 @@
+Require Import Crypto.Reflection.Named.Syntax.
+Require Import Crypto.Reflection.Named.Wf.
+Require Import Crypto.Reflection.Named.ContextDefinitions.
+Require Import Crypto.Reflection.Named.ContextProperties.
+Require Import Crypto.Reflection.Named.InterpretToPHOAS.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Wf.
+Require Import Crypto.Util.PointedProp.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.Tactics.BreakMatch.
+
+Section language.
+  Context {base_type_code : Type}
+          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
+          {Name : Type}
+          {base_type_code_dec : DecidableRel (@eq base_type_code)}
+          {Name_dec : DecidableRel (@eq Name)}.
+  Section with_var.
+    Context {var1 var2 : base_type_code -> Type}
+            {Context1 : Context Name var2}
+            {Context2 : Context Name var1}
+            {Context1Ok : ContextOk Context1}
+            {Context2Ok : ContextOk Context2}.
+
+    Local Ltac t_step :=
+      first [ progress intros
+            | progress unfold dec in *
+            | reflexivity
+            | progress subst
+            | progress inversion_option
+            | erewrite lookupb_extend by assumption
+            | rewrite <- !find_Name_and_val_None_iff
+            | progress break_innermost_match_step
+            | progress break_match_hyps
+            | solve [ eauto using find_Name_and_val_flatten_binding_list ]
+            | congruence
+            | tauto
+            | match goal with
+              | [ H : lookupb (extend _ _ _) _ = _ |- _ ]
+                => erewrite (lookupb_extend _ _ _) in H by assumption
+              | [ H : context[List.In _ (_ ++ _)] |- _ ]
+                => setoid_rewrite List.in_app_iff in H
+              | [ |- context[List.In _ (_ ++ _)] ]
+                => rewrite List.in_app_iff
+              | [ |- context[find_Name_and_val ?tdec ?ndec ?a ?b ?c ?d ?default] ]
+                => lazymatch default with None => fail | _ => idtac end;
+                   rewrite (find_Name_and_val_split tdec ndec (default:=default))
+              | [ H : context[find_Name_and_val ?tdec ?ndec ?a ?b ?c ?d ?default] |- _ ]
+                => lazymatch default with None => fail | _ => idtac end;
+                   rewrite (find_Name_and_val_split tdec ndec (default:=default)) in H
+              | [ H : forall n t, lookupb _ n t = None <-> lookupb _ n t = None |- context[lookupb _ _ = None] ]
+                => rewrite H
+              | [ H : forall n t, lookupb _ n t = None |- context[lookupb _ _ = None] ]
+                => rewrite H
+              end ].
+    Local Ltac t := repeat t_step.
+
+    Lemma wff_interpf_to_phoas
+          (ctx1 : Context1) (ctx2 : Context2)
+          {t} (e : @Named.exprf base_type_code op Name t)
+          (Hwf1 : prop_of_option (Named.wff ctx1 e))
+          (Hwf2 : prop_of_option (Named.wff ctx2 e))
+          G
+          (HG : forall n t v1 v2,
+              lookupb ctx1 n t = Some v1
+              -> lookupb ctx2 n t = Some v2
+              -> 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).
+    Proof.
+      revert dependent G; revert dependent ctx1; revert dependent ctx2; induction e;
+        repeat first [ progress intros
+                     | progress break_innermost_match_step
+                     | progress simpl in *
+                     | solve [ eauto ]
+                     | 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.
+    Qed.
+
+    Lemma wf_interp_to_phoas_gen
+          (ctx1 : Context1) (ctx2 : Context2)
+          {t} (e : @Named.expr base_type_code op Name t)
+          (Hwf1 : Named.wf ctx1 e)
+          (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).
+    Proof.
+      constructor; intros.
+      apply wff_interpf_to_phoas; t.
+    Qed.
+
+    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).
+    Proof.
+      apply wf_interp_to_phoas_gen; apply lookupb_empty; assumption.
+    Qed.
+  End with_var.
+
+  Section all.
+    Context {Context : forall var, @Context base_type_code Name var}
+            {ContextOk : forall var, ContextOk (Context var)}.
+
+    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).
+    Proof.
+      intros ??; apply wf_interp_to_phoas_gen; auto.
+    Qed.
+
+    Lemma Wf_InterpToPHOAS
+          {t} (e : @Named.expr base_type_code op Name t)
+          (Hwf : Named.Wf Context e)
+      : Wf (InterpToPHOAS e Hwf).
+    Proof.
+      intros ??; apply wf_interp_to_phoas; auto.
+    Qed.
+  End all.
+End language.
+
+Hint Resolve Wf_InterpToPHOAS : wf.
diff --git a/src/Reflection/Named/Wf.v b/src/Reflection/Named/Wf.v
index 07e08f27a..6b1e68e65 100644
--- a/src/Reflection/Named/Wf.v
+++ b/src/Reflection/Named/Wf.v
@@ -4,26 +4,33 @@ Require Import Crypto.Util.PointedProp.
 
 Module Export Named.
   Section language.
-    Context {base_type_code Name var}
-            {op : flat_type base_type_code -> flat_type base_type_code -> Type}
-            (Context : @Context base_type_code Name var).
+    Context {base_type_code Name : Type}
+            {op : flat_type base_type_code -> flat_type base_type_code -> Type}.
+    Section with_var.
+      Context {var}
+              (Context : @Context base_type_code Name var).
 
-    Fixpoint wff (ctx : Context) {t} (e : @exprf base_type_code op Name t) : option pointed_Prop
-      := match e with
-         | TT => Some trivial
-         | Var t n => match lookupb ctx n t return bool with
-                      | Some _ => true
-                      | None => false
-                      end
-         | Op _ _ op args => @wff ctx _ args
-         | LetIn _ n ex _ eC => @wff ctx _ ex /\ inject (forall v, prop_of_option (@wff (extend ctx n v) _ eC))
-         | Pair _ ex _ ey => @wff ctx _ ex /\ @wff ctx _ ey
-         end%option_pointed_prop.
+      Fixpoint wff (ctx : Context) {t} (e : @exprf base_type_code op Name t) : option pointed_Prop
+        := match e with
+           | TT => Some trivial
+           | Var t n => match lookupb ctx n t return bool with
+                        | Some _ => true
+                        | None => false
+                        end
+           | Op _ _ op args => @wff ctx _ args
+           | LetIn _ n ex _ eC => @wff ctx _ ex /\ inject (forall v, prop_of_option (@wff (extend ctx n v) _ eC))
+           | Pair _ ex _ ey => @wff ctx _ ex /\ @wff ctx _ ey
+           end%option_pointed_prop.
 
-    Definition wf (ctx : Context) {t} (e : @expr base_type_code op Name t) : Prop
-      := forall v, prop_of_option (@wff (extend ctx (Abs_name e) v) _ (invert_Abs e)).
+      Definition wf (ctx : Context) {t} (e : @expr base_type_code op Name t) : Prop
+        := forall v, prop_of_option (@wff (extend ctx (Abs_name e) v) _ (invert_Abs e)).
+    End with_var.
+
+    Definition Wf (Context : forall var, @Context base_type_code Name var) {t} (e : @expr base_type_code op Name t)
+      := forall var, wf (Context var) empty e.
   End language.
 End Named.
 
 Global Arguments wff {_ _ _ _ _} ctx {t} _.
 Global Arguments wf {_ _ _ _ _} ctx {t} _.
+Global Arguments Wf {_ _ _} Context {t} _.