Move ContextOk to ContextDefinitions

5 files changed, 85 insertions, 38 deletions

diff --git a/src/Reflection/Named/ContextDefinitions.v b/src/Reflection/Named/ContextDefinitions.v
new file mode 100644
index 000000000..90c220e70
--- /dev/null
+++ b/src/Reflection/Named/ContextDefinitions.v
@@ -0,0 +1,80 @@
+Require Import Coq.Logic.Eqdep_dec.
+Require Import Crypto.Util.FixCoqMistakes.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Relations.
+Require Import Crypto.Reflection.SmartMap.
+Require Import Crypto.Reflection.Named.Syntax.
+Require Import Crypto.Util.PointedProp.
+Require Import Crypto.Util.Logic.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.Sigma.
+Require Import Crypto.Util.Tactics.SplitInContext.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.RewriteHyp.
+
+Section with_context.
+  Context {base_type_code Name var} (Context : @Context base_type_code Name var)
+          (base_type_code_dec : forall x y : base_type_code, {x = y} + {x <> y})
+          (Name_dec : forall x y : Name, {x = y} + {x <> y}).
+
+  Fixpoint find_Name n
+           {T : flat_type base_type_code}
+    : interp_flat_type (fun _ => Name) T -> option base_type_code
+    := match T with
+       | Tbase t' => fun n' : Name => if Name_dec n n' then Some t' else None
+       | Unit => fun _ => None
+       | Prod A B
+         => fun ab : interp_flat_type _ A * interp_flat_type _ B
+            => match @find_Name n B (snd ab), @find_Name n A (fst ab) with
+               | Some tb, _ => Some tb
+               | None, Some ta => Some ta
+               | None, None => None
+               end
+       end.
+
+  Definition cast_if_eq {var'} t t' (v : var' t) : option (var' t')
+    := match base_type_code_dec t t', base_type_code_dec t' t' with
+       | left pf, left pf' => Some (eq_rect _ var' v _ (eq_trans pf (eq_sym pf')))
+       | _, right pf' => match pf' eq_refl with end
+       | right pf, _ => None
+       end.
+
+  Lemma cast_if_eq_refl {var'} t v : @cast_if_eq var' t t v = Some v.
+  Proof.
+    compute; clear; break_match; reflexivity.
+  Qed.
+
+  Fixpoint find_Name_and_val {var'} t n
+           {T : flat_type base_type_code}
+    : interp_flat_type (fun _ => Name) T -> interp_flat_type var' T -> option (var' t) -> option (var' t)
+    := match T with
+       | Tbase t' => fun n' v default => if Name_dec n n'
+                                         then cast_if_eq t' t v
+                                         else default
+       | Unit => fun _ _ default => default
+       | Prod A B
+         => fun (ab : interp_flat_type _ A * interp_flat_type _ B)
+                (a'b' : interp_flat_type _ A * interp_flat_type _ B)
+                default
+            => @find_Name_and_val
+                 var' t n B (snd ab) (snd a'b')
+                 (@find_Name_and_val
+                    var' t n A (fst ab) (fst a'b')
+                    default)
+       end.
+
+  Class ContextOk :=
+    { lookupb_extendb_same
+      : forall (ctx : Context) n t v, lookupb (extendb ctx n (t:=t) v) n t = Some v;
+      lookupb_extendb_different
+      : forall (ctx : Context) n n' t t' v, n <> n' -> lookupb (extendb ctx n (t:=t) v) n' t'
+                                                                                 = lookupb ctx n' t';
+      lookupb_extendb_wrong_type
+      : forall (ctx : Context) n t t' v, t <> t' -> lookupb (extendb ctx n (t:=t) v) n t' = None;
+      lookupb_removeb
+      : forall (ctx : Context) n n' t t', n <> n' -> lookupb (removeb ctx n t) n' t'
+                                                                     = lookupb ctx n' t';
+      lookupb_empty
+      : forall n t, lookupb (@empty _ _ _ Context) n t = None }.
+End with_context.
diff --git a/src/Reflection/Named/FMapContext.v b/src/Reflection/Named/FMapContext.v
index d3d94235d..b838c1b4f 100644
--- a/src/Reflection/Named/FMapContext.v
+++ b/src/Reflection/Named/FMapContext.v
@@ -2,7 +2,7 @@ Require Import Coq.Bool.Sumbool.
 Require Import Coq.FSets.FMapInterface.
 Require Import Coq.FSets.FMapFacts.
 Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.Wf.
+Require Import Crypto.Reflection.Named.ContextDefinitions.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Equality.
 
diff --git a/src/Reflection/Named/Syntax.v b/src/Reflection/Named/Syntax.v
index 5971e2bf9..28e7256fc 100644
--- a/src/Reflection/Named/Syntax.v
+++ b/src/Reflection/Named/Syntax.v
@@ -131,6 +131,8 @@ Global Arguments Op {_ _ _ _ _} _ _.
 Global Arguments LetIn {_ _ _} _ _ _ {_} _.
 Global Arguments Pair {_ _ _ _} _ {_} _.
 Global Arguments Abs {_ _ _ _ _} _ _.
+Global Arguments invert_Abs {_ _ _ _} _.
+Global Arguments Abs_name {_ _ _ _} _.
 Global Arguments extend {_ _ _ _} ctx {_} _ _.
 Global Arguments remove {_ _ _ _} ctx {_} _.
 Global Arguments lookup {_ _ _ _} ctx {_} _, {_ _ _ _} ctx _ _.
diff --git a/src/Reflection/Named/Wf.v b/src/Reflection/Named/Wf.v
index 87d84a07f..9ae8fb596 100644
--- a/src/Reflection/Named/Wf.v
+++ b/src/Reflection/Named/Wf.v
@@ -2,45 +2,11 @@ Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Named.Syntax.
 Require Import Crypto.Util.PointedProp.
 
-Section with_context.
-  Context {base_type_code Name var} (Context : @Context base_type_code Name var).
-
-  Class ContextOk :=
-    { lookupb_extendb_same
-      : forall (ctx : Context) n t v, lookupb (extendb ctx n (t:=t) v) n t = Some v;
-      lookupb_extendb_different
-      : forall (ctx : Context) n n' t t' v, n <> n' -> lookupb (extendb ctx n (t:=t) v) n' t'
-                                                                                 = lookupb ctx n' t';
-      lookupb_extendb_wrong_type
-      : forall (ctx : Context) n t t' v, t <> t' -> lookupb (extendb ctx n (t:=t) v) n t' = None;
-      lookupb_removeb
-      : forall (ctx : Context) n n' t t', n <> n' -> lookupb (removeb ctx n t) n' t'
-                                                                     = lookupb ctx n' t';
-      lookupb_empty
-      : forall n t, lookupb (@empty _ _ _ Context) n t = None }.
-
-  Context (ContextOk : ContextOk).
-
-  Lemma lookupb_eq_cast
-    : forall (ctx : Context) n t t' (pf : t = t'),
-      lookupb ctx n t' = option_map (fun v => eq_rect _ var v _ pf) (lookupb ctx n t).
-  Proof.
-    intros; subst; edestruct lookupb; reflexivity.
-  Defined.
-  Lemma lookupb_extendb_eq
-    : forall (ctx : Context) n t t' (pf : t = t') v,
-      lookupb (extendb ctx n (t:=t) v) n t' = Some (eq_rect _ var v _ pf).
-  Proof.
-    intros; subst; apply lookupb_extendb_same; assumption.
-  Defined.
-End with_context.
-
 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)
-            (ContextOk : @ContextOk base_type_code Name var Context).
+            (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
diff --git a/src/Reflection/Named/WfInterp.v b/src/Reflection/Named/WfInterp.v
index b8cfb7fbe..17fc43ca5 100644
--- a/src/Reflection/Named/WfInterp.v
+++ b/src/Reflection/Named/WfInterp.v
@@ -10,8 +10,7 @@ Section language.
   Context {base_type_code Name interp_base_type}
           {op : flat_type base_type_code -> flat_type base_type_code -> Type}
           {interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst}
-          {Context : @Context base_type_code Name interp_base_type}
-          {ContextOk : ContextOk Context}.
+          {Context : @Context base_type_code Name interp_base_type}.
 
   Lemma wff_interpf_not_None {ctx : Context} {t} {e : @exprf base_type_code op Name t}
         (Hwf : prop_of_option (wff ctx e))