Add Wf_from_unit

This one is much easier to compute with, and it means we can get rid of
a lot of pesky Named.wff proofs.

2 files changed, 112 insertions, 11 deletions

diff --git a/src/Compilers/Named/Wf.v b/src/Compilers/Named/Wf.v
index fec1de5ed..736d0bd81 100644
--- a/src/Compilers/Named/Wf.v
+++ b/src/Compilers/Named/Wf.v
@@ -1,3 +1,4 @@
+Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.Syntax.
@@ -11,27 +12,45 @@ Module Export Named.
       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.
+      Section gen.
+        Context (quantify : forall tx, (interp_flat_type var tx -> option pointed_Prop) -> option pointed_Prop).
 
+        Fixpoint wff_gen (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_gen ctx _ args
+             | LetIn _ n ex _ eC => @wff_gen ctx _ ex
+                                    /\ quantify _ (fun v => @wff_gen (extend ctx n v) _ eC)
+             | Pair _ ex _ ey => @wff_gen ctx _ ex /\ @wff_gen ctx _ ey
+             end%option_pointed_prop.
+      End gen.
+
+      Definition wff := wff_gen (fun tx f => inject (forall v, prop_of_option (f v))).
       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.
 
+    Section unit.
+      Context (Context : @Context base_type_code Name (fun _ => unit)).
+
+      Local Notation TT := (SmartValf _ (fun _ => tt) _).
+      Definition wff_unit := wff_gen Context (fun tx f => f TT).
+      Definition wf_unit ctx {t} (e : @expr base_type_code op Name t) : option pointed_Prop
+        := @wff_unit (extend ctx (Abs_name e) TT) _ (invert_Abs e).
+    End unit.
+
     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_gen {_ _ _ _ _} quantify ctx {t} _.
+Global Arguments wff_unit {_ _ _ _} ctx {t} _.
+Global Arguments wf_unit {_ _ _ _} ctx {t} _.
 Global Arguments wff {_ _ _ _ _} ctx {t} _.
 Global Arguments wf {_ _ _ _ _} ctx {t} _.
 Global Arguments Wf {_ _ _} Context {t} _.
diff --git a/src/Compilers/Named/WfFromUnit.v b/src/Compilers/Named/WfFromUnit.v
new file mode 100644
index 000000000..c6b28f824
--- /dev/null
+++ b/src/Compilers/Named/WfFromUnit.v
@@ -0,0 +1,82 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Context.
+Require Import Crypto.Compilers.Named.ContextProperties.
+Require Import Crypto.Compilers.Named.ContextDefinitions.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.Wf.
+Require Import Crypto.Util.PointedProp.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.SplitInContext.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.Option.
+
+Section language.
+  Context {base_type_code Name : Type}
+          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
+          {base_type_code_dec : DecidableRel (@eq base_type_code)}
+          {Name_dec : DecidableRel (@eq Name)}.
+
+  Section with_var.
+    Context {var}
+            (uContext : @Context base_type_code Name (fun _ => unit))
+            (uContextOk : ContextOk uContext)
+            (vContext : @Context base_type_code Name var)
+            (vContextOk : ContextOk vContext).
+
+    Local Ltac t :=
+      repeat first [ progress simpl in *
+                   | progress intros
+                   | progress subst
+                   | progress inversion_option
+                   | congruence
+                   | tauto
+                   | solve [ eauto ]
+                   | break_innermost_match_step
+                   | break_innermost_match_hyps_step
+                   | progress destruct_head'_and
+                   | progress autorewrite with push_prop_of_option push_eq_Some_trivial in *
+                   | rewrite !(@lookupb_extend base_type_code _ Name _) by auto
+                   | rewrite (@find_Name_and_val_split base_type_code _ Name _) with (default := lookupb _ _)
+                   | match goal with
+                     | [ H : ?x = Some _ |- _ ]
+                       => assert (x = None) by (split_iff; eauto); congruence
+                     | [ |- _ /\ _ ] => split
+                     | [ H : _ |- prop_of_option _ ] => eapply H; [ | eassumption ]; clear H
+                     | [ |- context[find_Name_and_val ?tdec ?ndec ?b _ _ _ _ = None] ]
+                       => rewrite <- !(@find_Name_and_val_None_iff _ tdec _ ndec _ b)
+                     end ].
+
+    Lemma wff_from_unit
+          (vctx : vContext)
+          (uctx : uContext)
+          (Hctx : forall t n, lookupb vctx n t = None <-> lookupb uctx n t = None)
+          {t} (e : @exprf base_type_code op Name t)
+      : wff_unit uctx e = Some trivial -> prop_of_option (wff vctx e).
+    Proof using Name_dec base_type_code_dec uContextOk vContextOk.
+      revert uctx vctx Hctx; induction e; t.
+    Qed.
+
+    Lemma wf_from_unit
+          (vctx : vContext)
+          (uctx : uContext)
+          (Hctx : forall t n, lookupb vctx n t = None <-> lookupb uctx n t = None)
+          {t} (e : @expr base_type_code op Name t)
+      : wf_unit uctx e = Some trivial -> wf vctx e.
+    Proof using Name_dec base_type_code_dec uContextOk vContextOk.
+      intros H ?; revert H; apply wff_from_unit; t.
+    Qed.
+  End with_var.
+
+  Lemma Wf_from_unit
+        (Context : forall var, @Context base_type_code Name var)
+        (ContextOk : forall var, ContextOk (Context var))
+        {t} (e : @expr base_type_code op Name t)
+    : wf_unit (Context:=Context _) empty e = Some trivial -> Wf Context e.
+  Proof using Name_dec base_type_code_dec.
+    intros H ?; revert H; apply wf_from_unit; auto; intros.
+    rewrite !lookupb_empty by auto; tauto.
+  Qed.
+End language.
+
+Hint Resolve wf_from_unit Wf_from_unit wff_from_unit : wf.