Merge pull request #60 from JasonGross/common-phoas

Common PHOAS syntax

8 files changed, 1350 insertions, 0 deletions

diff --git a/_CoqProject b/_CoqProject
index 897d82a6c..8921587d1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -63,6 +63,13 @@ src/ModularArithmetic/BarrettReduction/ZHandbook.v
 src/ModularArithmetic/Montgomery/Z.v
 src/ModularArithmetic/Montgomery/ZBounded.v
 src/ModularArithmetic/Montgomery/ZProofs.v
+src/Reflection/InputSyntax.v
+src/Reflection/InterpProofs.v
+src/Reflection/Linearize.v
+src/Reflection/Reify.v
+src/Reflection/Syntax.v
+src/Reflection/TestCase.v
+src/Reflection/WfReflective.v
 src/Spec/CompleteEdwardsCurve.v
 src/Spec/EdDSA.v
 src/Spec/Encoding.v
diff --git a/src/Reflection/InputSyntax.v b/src/Reflection/InputSyntax.v
new file mode 100644
index 000000000..c3c796d75
--- /dev/null
+++ b/src/Reflection/InputSyntax.v
@@ -0,0 +1,130 @@
+(** * PHOAS Representation of Gallina which allows exact denotation *)
+Require Import Coq.Strings.String.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.InterpProofs.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Notations.
+
+(** We parameterize the language over a type of basic type codes (for
+    things like [Z], [word], [bool]), as well as a type of n-ary
+    operations returning one value, and n-ary operations returning two
+    values. *)
+Local Open Scope ctype_scope.
+Section language.
+  Context (base_type_code : Type).
+
+  Local Notation flat_type := (flat_type base_type_code).
+  Local Notation type := (type base_type_code).
+  Local Notation Tbase := (@Tbase base_type_code).
+
+  Section expr_param.
+    Context (interp_base_type : base_type_code -> Type).
+    Context (op : flat_type (* input tuple *) -> flat_type (* output type *) -> Type).
+    Local Notation interp_type := (interp_type interp_base_type).
+    Local Notation interp_flat_type := (interp_flat_type_gen interp_base_type).
+    Section expr.
+      Context {var : flat_type -> Type}.
+
+      (** N.B. [Let] destructures pairs *)
+      Inductive exprf : flat_type -> Type :=
+      | Const {t : flat_type} : interp_type t -> exprf t
+      | Var {t} : var t -> exprf t
+      | Op {t1 tR} : op t1 tR -> exprf t1 -> exprf tR
+      | Let : forall {tx}, exprf tx -> forall {tC}, (var tx -> exprf tC) -> exprf tC
+      | Pair : forall {t1}, exprf t1 -> forall {t2}, exprf t2 -> exprf (Prod t1 t2)
+      | MatchPair : forall {t1 t2}, exprf (Prod t1 t2) -> forall {tC}, (var t1 -> var t2 -> exprf tC) -> exprf tC.
+      Inductive expr : type -> Type :=
+      | Return {t} : exprf t -> expr t
+      | Abs {src dst} : (var (Tbase src) -> expr dst) -> expr (Arrow src dst).
+      Global Coercion Return : exprf >-> expr.
+    End expr.
+
+    Definition Expr (t : type) := forall var, @expr var t.
+
+    Section interp.
+      Context (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst).
+
+      Fixpoint interpf {t} (e : @exprf interp_flat_type t) : interp_flat_type t
+        := match e in exprf t return interp_flat_type t with
+           | Const _ x => x
+           | Var _ x => x
+           | Op _ _ op args => @interp_op _ _ op (@interpf _ args)
+           | Let _ ex _ eC => let x := @interpf _ ex in @interpf _ (eC x)
+           | Pair _ ex _ ey => (@interpf _ ex, @interpf _ ey)
+           | MatchPair _ _ ex _ eC => match @interpf _ ex with pair x y => @interpf _ (eC x y) end
+           end.
+      Fixpoint interp {t} (e : @expr interp_type t) : interp_type t
+        := match e in expr t return interp_type t with
+           | Return _ x => interpf x
+           | Abs _ _ f => fun x => @interp _ (f x)
+           end.
+
+      Definition Interp {t} (E : Expr t) : interp_type t := interp (E _).
+    End interp.
+
+    Section compile.
+      Context {var : base_type_code -> Type}.
+
+      Fixpoint compilef {t} (e : @exprf (interp_flat_type_gen var) t) : @Syntax.exprf base_type_code interp_base_type op var t
+        := match e in exprf t return @Syntax.exprf _ _ _ _ t with
+           | Const _ x => Syntax.Const x
+           | Var _ x => Syntax.SmartVar x
+           | Op _ _ op args => Syntax.Op op (@compilef _ args)
+           | Let _ ex _ eC => Syntax.Let (@compilef _ ex) (fun x => @compilef _ (eC x))
+           | Pair _ ex _ ey => Syntax.Pair (@compilef _ ex) (@compilef _ ey)
+           | MatchPair _ _ ex _ eC => Syntax.Let (@compilef _ ex) (fun xy => @compilef _ (eC (fst xy) (snd xy)))
+           end.
+
+      Fixpoint compile {t} (e : @expr (interp_flat_type_gen var) t) : @Syntax.expr base_type_code interp_base_type op var t
+        := match e in expr t return @Syntax.expr _ _ _ _ t with
+           | Return _ x => Syntax.Return (compilef x)
+           | Abs a _ f => Syntax.Abs (fun x : var a => @compile _ (f x))
+           end.
+    End compile.
+
+    Definition Compile {t} (e : Expr t) : Syntax.Expr base_type_code interp_base_type op t
+      := fun var => compile (e _).
+
+    Section compile_correct.
+      Context (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst).
+
+      Lemma compilef_correct {t} (e : @exprf interp_flat_type t)
+      : Syntax.interpf base_type_code interp_base_type op interp_op (compilef e) = interpf interp_op e.
+      Proof.
+        induction e;
+          repeat match goal with
+                 | _ => reflexivity
+                 | _ => progress simpl in *
+                 | _ => rewrite interpf_SmartVar
+                 | _ => rewrite <- surjective_pairing
+                 | _ => progress rewrite_hyp *
+                 | [ |- context[let (x, y) := ?v in _] ]
+                   => rewrite (surjective_pairing v); cbv beta iota
+                 end.
+      Qed.
+
+      Lemma Compile_correct {t : flat_type} (e : @Expr t)
+      : Syntax.Interp base_type_code interp_base_type op interp_op (Compile e) = Interp interp_op e.
+      Proof.
+        unfold Interp, Compile, Syntax.Interp; simpl.
+        pose (e (interp_flat_type_gen interp_base_type)) as E.
+        repeat match goal with |- context[e ?f] => change (e f) with E end.
+        refine match E with
+               | Abs _ _ _ => fun x : Prop => x (* small inversions *)
+               | Return _ _ => _
+               end.
+        apply compilef_correct.
+      Qed.
+    End compile_correct.
+  End expr_param.
+End language.
+
+Global Arguments Const {_ _ _ _ _} _.
+Global Arguments Var {_ _ _ _ _} _.
+Global Arguments Op {_ _ _ _ _ _} _ _.
+Global Arguments Let {_ _ _ _ _} _ {_} _.
+Global Arguments MatchPair {_ _ _ _ _ _} _ {_} _.
+Global Arguments Pair {_ _ _ _ _} _ {_} _.
+Global Arguments Return {_ _ _ _ _} _.
+Global Arguments Abs {_ _ _ _ _ _} _.
diff --git a/src/Reflection/InterpProofs.v b/src/Reflection/InterpProofs.v
new file mode 100644
index 000000000..5790178e7
--- /dev/null
+++ b/src/Reflection/InterpProofs.v
@@ -0,0 +1,29 @@
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Util.Tactics.
+
+Local Open Scope ctype_scope.
+Section language.
+  Context (base_type_code : Type).
+
+  Local Notation flat_type := (flat_type base_type_code).
+  Local Notation type := (type base_type_code).
+  Let Tbase := @Tbase base_type_code.
+  Local Coercion Tbase : base_type_code >-> Syntax.flat_type.
+  Context (interp_base_type : base_type_code -> Type).
+  Context (op : flat_type (* input tuple *) -> flat_type (* output type *) -> Type).
+  Let interp_type := interp_type interp_base_type.
+  Let interp_flat_type := interp_flat_type_gen interp_base_type.
+  Context (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst).
+
+  Lemma interpf_SmartVar t v
+    : Syntax.interpf base_type_code interp_base_type op interp_op (SmartVar (t:=t) v) = v.
+  Proof.
+    unfold SmartVar; induction t;
+      repeat match goal with
+             | _ => reflexivity
+             | _ => progress simpl in *
+             | _ => progress rewrite_hyp *
+             | _ => rewrite <- surjective_pairing
+             end.
+  Qed.
+End language.
diff --git a/src/Reflection/Linearize.v b/src/Reflection/Linearize.v
new file mode 100644
index 000000000..b3ce3249b
--- /dev/null
+++ b/src/Reflection/Linearize.v
@@ -0,0 +1,101 @@
+(** * Linearize: Place all and only operations in let binders *)
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Util.Tactics.
+
+Local Open Scope ctype_scope.
+Section language.
+  Context (base_type_code : Type).
+  Context (interp_base_type : base_type_code -> Type).
+  Context (op : flat_type base_type_code -> flat_type base_type_code -> Type).
+
+  Local Notation flat_type := (flat_type base_type_code).
+  Local Notation type := (type base_type_code).
+  Let Tbase := @Tbase base_type_code.
+  Local Coercion Tbase : base_type_code >-> Syntax.flat_type.
+  Let interp_type := interp_type interp_base_type.
+  Let interp_flat_type := interp_flat_type_gen interp_base_type.
+  Local Notation Expr := (@Expr base_type_code interp_base_type op).
+
+  Section with_var.
+    Context {var : base_type_code -> Type}.
+    Local Notation exprf := (@exprf base_type_code interp_base_type op var).
+    Local Notation expr := (@expr base_type_code interp_base_type op var).
+
+    Section under_lets.
+      Fixpoint let_bind_const {t} (e : interp_flat_type t) {struct t}
+        : forall {tC} (C : interp_flat_type_gen var t -> exprf tC), exprf tC
+        := match t return forall (e : interp_flat_type t) {tC} (C : interp_flat_type_gen var t -> exprf tC), exprf tC with
+           | Prod A B => fun e _ C => @let_bind_const A (fst e) _ (fun x =>
+                                      @let_bind_const B (snd e) _ (fun y =>
+                                      C (x, y)))
+           | Syntax.Tbase _ => fun e _ C => Let (Const e) C
+           end e.
+
+      Fixpoint under_letsf {t} (e : exprf t)
+        : forall {tC} (C : interp_flat_type_gen var t -> exprf tC), exprf tC
+        := match e in Syntax.exprf _ _ _ t return forall {tC} (C : interp_flat_type_gen var t -> exprf tC), exprf tC with
+           | Let _ ex _ eC
+             => fun _ C => @under_letsf _ ex _ (fun v => @under_letsf _ (eC v) _ C)
+           | Const _ x => fun _ C => let_bind_const x C
+           | Var _ x => fun _ C => C x
+           | Op _ _ op args as e => fun _ C => Let e C
+           | Pair A x B y => fun _ C => @under_letsf A x _ (fun x =>
+                                        @under_letsf B y _ (fun y =>
+                                        C (x, y)))
+           end.
+    End under_lets.
+
+    Fixpoint linearizef {t} (e : exprf t) : exprf t
+      := match e in Syntax.exprf _ _ _ t return exprf t with
+         | Let _ ex _ eC
+           => under_letsf (@linearizef _ ex) (fun x => @linearizef _ (eC x))
+         | Const _ x => Const x
+         | Var _ x => Var x
+         | Op _ _ op args
+           => under_letsf (@linearizef _ args) (fun args => Let (Op op (SmartVar args)) SmartVar)
+         | Pair A ex B ey
+           => under_letsf (@linearizef _ ex) (fun x =>
+              under_letsf (@linearizef _ ey) (fun y =>
+              SmartVar (t:=Prod A B) (x, y)))
+         end.
+
+    Fixpoint linearize {t} (e : expr t) : expr t
+      := match e in Syntax.expr _ _ _ t return expr t with
+         | Return _ x => linearizef x
+         | Abs _ _ f => Abs (fun x => @linearize _ (f x))
+         end.
+  End with_var.
+
+  Section inline.
+    Context {var : base_type_code -> Type}.
+    Local Notation exprf := (@exprf base_type_code interp_base_type op).
+    Local Notation expr := (@expr base_type_code interp_base_type op).
+
+    Fixpoint inline_constf {t} (e : @exprf (@exprf var) t) : @exprf var t
+      := match e in Syntax.exprf _ _ _ t return @exprf var t with
+         | Let _ ex tC eC
+           => match @inline_constf _ ex in Syntax.exprf _ _ _ t' return (interp_flat_type_gen _ t' -> @exprf var tC) -> @exprf var tC with
+              | Const _ x => fun eC => eC (SmartConst (op:=op) (var:=var) x)
+              | ex => fun eC => Let ex (fun x => eC (SmartVarVar x))
+              end (fun x => @inline_constf _ (eC x))
+         | Var _ x => x
+         | Const _ x => Const x
+         | Pair _ ex _ ey => Pair (@inline_constf _ ex) (@inline_constf _ ey)
+         | Op _ _ op args => Op op (@inline_constf _ args)
+         end.
+
+    Fixpoint inline_const {t} (e : @expr (@exprf var) t) : @expr var t
+      := match e in Syntax.expr _ _ _ t return @expr var t with
+         | Return _ x => Return (inline_constf x)
+         | Abs _ _ f => Abs (fun x => @inline_const _ (f (Var x)))
+         end.
+  End inline.
+
+  Definition Linearize {t} (e : Expr t) : Expr t
+    := fun var => linearize (e _).
+  Definition InlineConst {t} (e : Expr t) : Expr t
+    := fun var => inline_const (e _).
+End language.
+
+Arguments Linearize {_ _ _ _} _ var.
+Arguments InlineConst {_ _ _ _} _ var.
diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v
new file mode 100644
index 000000000..1eac17675
--- /dev/null
+++ b/src/Reflection/Reify.v
@@ -0,0 +1,249 @@
+(** * Exact reification of PHOAS Representation of Gallina *)
+(** The reification procedure goes through [InputSyntax], which allows
+    judgmental equality of the denotation of the reified term. *)
+Require Import Coq.Strings.String.
+Require Import Crypto.Reflection.Syntax.
+Require Export Crypto.Reflection.InputSyntax.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Notations.
+
+Class reify {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify : T.
+Definition reify_var_for_in_is base_type_code {T} (x : T) (t : flat_type base_type_code) {eT} (e : eT) := False.
+Arguments reify_var_for_in_is _ {T} _ _ {eT} _.
+
+(** [reify] assumes that operations can be reified via the [reify_op]
+    typeclass, which gets passed the type family of operations, the
+    expression which is headed by an operation, and expects resolution
+    to fill in a number of arguments (which [reifyf] will
+    automatically curry), as well as the reified operator.
+
+    We also assume that types can be reified via the [reify] typeclass
+    with arguments [reify type <type to be reified>]. *)
+Class reify_op {opTF} (op_family : opTF) {opExprT} (opExpr : opExprT) (nargs : nat) {opT} (reified_op : opT)
+  := Build_reify_op : True.
+Ltac strip_type_cast term := lazymatch term with ?term' => term' end.
+Ltac reify_type T :=
+  lazymatch T with
+  | (?A -> ?B)%type
+    => let a := reify_type A in
+       let b := reify_type B in
+       constr:(@Arrow _ a b)
+  | prod ?A ?B
+    => let a := reify_type A in
+       let b := reify_type B in
+       constr:(@Prod _ a b)
+  | _
+    => let v := strip_type_cast (_ : reify type T) in
+       constr:(Tbase v)
+  end.
+Ltac reify_base_type T :=
+  let t := reify_type T in
+  lazymatch t with
+  | Tbase ?t => t
+  | ?t => t
+  end.
+
+Ltac reifyf_var x mkVar :=
+  lazymatch goal with
+  | _ : reify_var_for_in_is _ x ?t ?v |- _ => mkVar t v
+  | _ => lazymatch x with
+         | fst ?x' => reifyf_var x' ltac:(fun t v => lazymatch t with
+                                                     | Prod ?A ?B => mkVar A (fst v)
+                                                     end)
+         | snd ?x' => reifyf_var x' ltac:(fun t v => lazymatch t with
+                                                     | Prod ?A ?B => mkVar B (snd v)
+                                                     end)
+         end
+  end.
+
+Inductive reify_result_helper :=
+| finished_value {T} (res : T)
+| op_info {T} (res : T)
+| reification_unsuccessful.
+
+(** Change this with [Ltac reify_debug_level ::= constr:(1).] to get
+    more debugging. *)
+Ltac reify_debug_level := constr:(0).
+Module Import ReifyDebugNotations.
+  Open Scope string_scope.
+End ReifyDebugNotations.
+
+Ltac debug_enter_reifyf e :=
+  let lvl := reify_debug_level in
+  match lvl with
+  | S (S _) => cidtac2 "reifyf: Attempting to reify:" e
+  | _ => constr:(Set)
+  end.
+Ltac debug_enter_reify_abs e :=
+  let lvl := reify_debug_level in
+  match lvl with
+  | S (S _) => cidtac2 "reify_abs: Attempting to reify:" e
+  | _ => constr:(Set)
+  end.
+
+Ltac debug_enter_reify_rec :=
+  let lvl := reify_debug_level in
+  match lvl with
+  | S _ => idtac_goal
+  | _ => idtac
+  end.
+Ltac debug_leave_reify_rec e :=
+  let lvl := reify_debug_level in
+  match lvl with
+  | S _ => idtac "<infomsg>reifyf success:" e "</infomsg>"
+  | _ => idtac
+  end.
+
+Ltac reifyf base_type_code interp_base_type op var e :=
+  let reify_rec e := reifyf base_type_code interp_base_type op var e in
+  let mkLet ex eC := constr:(Let (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) ex eC) in
+  let mkPair ex ey := constr:(Pair (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) ex ey) in
+  let mkVar T ex := constr:(Var (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t:=T) ex) in
+  let mkConst T ex := constr:(Const (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t:=T) ex) in
+  let mkOp T retT op_code args := constr:(Op (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t1:=T) (tR:=retT) op_code args) in
+  let mkMatchPair tC ex eC := constr:(MatchPair (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (tC:=tC) ex eC) in
+  let reify_tag := constr:(@exprf base_type_code interp_base_type op var) in
+  let dummy := debug_enter_reifyf e in
+  lazymatch e with
+  | let x := ?ex in @?eC x =>
+    let ex := reify_rec ex in
+    let eC := reify_rec eC in
+    mkLet ex eC
+  | pair ?a ?b =>
+    let a := reify_rec a in
+    let b := reify_rec b in
+    mkPair a b
+  | (fun x : ?T => ?C) =>
+    let t := reify_type T in
+    (* Work around Coq 8.5 and 8.6 bug *)
+    (* <https://coq.inria.fr/bugs/show_bug.cgi?id=4998> *)
+    (* Avoid re-binding the Gallina variable referenced by Ltac [x] *)
+    (* even if its Gallina name matches a Ltac in this tactic. *)
+    let maybe_x := fresh x in
+    let not_x := fresh x in
+    lazymatch constr:(fun (x : T) (not_x : var t) (_ : reify_var_for_in_is base_type_code x t not_x) =>
+                        (_ : reify reify_tag C)) (* [C] here is an open term that references "x" by name *)
+    with fun _ v _ => @?C v => C end
+  | match ?ev with pair a b => @?eC a b end =>
+    let t := (let T := match type of eC with _ -> _ -> ?T => T end in reify_type T) in
+    let v := reify_rec ev in
+    let C := reify_rec eC in
+    mkMatchPair t v C
+  | ?x =>
+    let t := lazymatch type of x with ?t => reify_type t end in
+    let retv := match constr:(Set) with
+                | _ => let retv := reifyf_var x mkVar in constr:(finished_value retv)
+                | _ => let r := constr:(_ : reify_op op x _ _) in
+                       let t := type of r in
+                       constr:(op_info t)
+                | _ => let c := mkConst t x in
+                       constr:(finished_value c)
+                | _ => constr:(reification_unsuccessful)
+                end in
+    lazymatch retv with
+    | finished_value ?v => v
+    | op_info (reify_op _ _ ?nargs ?op_code)
+      => let tR := (let tR := type of x in reify_type tR) in
+         lazymatch nargs with
+         | 1%nat
+           => lazymatch x with
+              | ?f ?x0
+                => let a0T := (let t := type of x0 in reify_type t) in
+                   let a0 := reify_rec x0 in
+                   mkOp a0T tR op_code a0
+              end
+         | 2%nat
+           => lazymatch x with
+              | ?f ?x0 ?x1
+                => let a0T := (let t := type of x0 in reify_type t) in
+                   let a0 := reify_rec x0 in
+                   let a1T := (let t := type of x1 in reify_type t) in
+                   let a1 := reify_rec x1 in
+                   let args := mkPair a0 a1 in
+                   mkOp (@Prod _ a0T a1T) tR op_code args
+              end
+         | 3%nat
+           => lazymatch x with
+              | ?f ?x0 ?x1 ?x2
+                => let a0T := (let t := type of x0 in reify_type t) in
+                   let a0 := reify_rec x0 in
+                   let a1T := (let t := type of x1 in reify_type t) in
+                   let a1 := reify_rec x1 in
+                   let a2T := (let t := type of x2 in reify_type t) in
+                   let a2 := reify_rec x2 in
+                   let args := let a01 := mkPair a0 a1 in mkPair a01 a2 in
+                   mkOp (@Prod _ (@Prod _ a0T a1T) a2T) tR op_code args
+              end
+         | _ => cfail2 "Unsupported number of operation arguments in reifyf:"%string nargs
+         end
+    | reification_unsuccessful
+      => cfail2 "Failed to reify:"%string x
+    end
+  end.
+
+Hint Extern 0 (reify (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e)
+=> (debug_enter_reify_rec; let e := reifyf base_type_code interp_base_type op var e in debug_leave_reify_rec e; eexact e) : typeclass_instances.
+
+(** For reification including [Abs] *)
+Class reify_abs {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify_abs : T.
+Ltac reify_abs base_type_code interp_base_type op var e :=
+  let reify_rec e := reify_abs base_type_code interp_base_type op var e in
+  let reifyf_term e := reifyf base_type_code interp_base_type op var e in
+  let mkAbs src ef := constr:(Abs (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (src:=src) ef) in
+  let reify_tag := constr:(@exprf base_type_code interp_base_type op var) in
+  let dummy := debug_enter_reify_abs e in
+  lazymatch e with
+  | (fun x : ?T => ?C) =>
+    let t := reify_base_type T in
+    (* Work around Coq 8.5 and 8.6 bug *)
+    (* <https://coq.inria.fr/bugs/show_bug.cgi?id=4998> *)
+    (* Avoid re-binding the Gallina variable referenced by Ltac [x] *)
+    (* even if its Gallina name matches a Ltac in this tactic. *)
+    let maybe_x := fresh x in
+    let not_x := fresh x in
+    lazymatch constr:(fun (x : T) (not_x : var (Tbase t)) (_ : reify_var_for_in_is base_type_code x (Tbase t) not_x) =>
+                        (_ : reify_abs reify_tag C)) (* [C] here is an open term that references "x" by name *)
+    with fun _ v _ => @?C v => mkAbs t C end
+  | ?x =>
+    reifyf_term x
+  end.
+
+Hint Extern 0 (reify_abs (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e)
+=> (debug_enter_reify_rec; let e := reify_abs base_type_code interp_base_type op var e in debug_leave_reify_rec e; eexact e) : typeclass_instances.
+
+Ltac Reify' base_type_code interp_base_type op e :=
+  lazymatch constr:(fun (var : flat_type base_type_code -> Type) => (_ : reify_abs (@exprf base_type_code interp_base_type op var) e)) with
+    (fun var => ?C) => constr:(fun (var : flat_type base_type_code -> Type) => C) (* copy the term but not the type cast *)
+  end.
+Ltac Reify base_type_code interp_base_type op e :=
+  let r := Reify' base_type_code interp_base_type op e in
+  constr:(InputSyntax.Compile base_type_code interp_base_type op r).
+
+Ltac lhs_of_goal := lazymatch goal with |- ?R ?LHS ?RHS => LHS end.
+Ltac rhs_of_goal := lazymatch goal with |- ?R ?LHS ?RHS => RHS end.
+
+Ltac Reify_rhs base_type_code interp_base_type op interp_op :=
+  let rhs := rhs_of_goal in
+  let RHS := Reify base_type_code interp_base_type op rhs in
+  transitivity (Syntax.Interp base_type_code interp_base_type op interp_op RHS);
+  [
+  | etransitivity; (* first we strip off the [InputSyntax.Compile]
+                      bit; Coq is bad at inferring the type, so we
+                      help it out by providing it *)
+    [ lazymatch goal with
+      | [ |- @Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op (@Tflat _ ?t) (@Compile _ _ _ _ ?e) = _ ]
+        => exact (@InputSyntax.Compile_correct base_type_code interp_base_type op interp_op t e)
+      end
+    | ((* now we unfold the interpretation function, including the
+          parameterized bits; we assume that [hnf] is enough to unfold
+          the interpretation functions that we're parameterized
+          over. *)
+      lazymatch goal with
+      | [ |- @InputSyntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t ?e = _ ]
+        => let interp_base_type' := (eval hnf in interp_base_type) in
+           let interp_op' := (eval hnf in interp_op) in
+           change interp_base_type with interp_base_type';
+           change interp_op with interp_op'
+      end;
+      cbv iota beta delta [InputSyntax.Interp interp_type interp_type_gen interp_flat_type_gen interp interpf]; simplify_projections; reflexivity) ] ].
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v
new file mode 100644
index 000000000..d14705979
--- /dev/null
+++ b/src/Reflection/Syntax.v
@@ -0,0 +1,208 @@
+(** * PHOAS Representation of Gallina *)
+Require Import Coq.Strings.String.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Notations.
+
+(** We parameterize the language over a type of basic type codes (for
+    things like [Z], [word], [bool]), as well as a type of n-ary
+    operations returning one value, and n-ary operations returning two
+    values. *)
+Delimit Scope ctype_scope with ctype.
+Local Open Scope ctype_scope.
+Delimit Scope expr_scope with expr.
+Local Open Scope expr_scope.
+Section language.
+  Context (base_type_code : Type).
+
+  Inductive flat_type := Tbase (_ : base_type_code) | Prod (x y : flat_type).
+  Bind Scope ctype_scope with flat_type.
+
+  Inductive type := Tflat (_ : flat_type) | Arrow (x : base_type_code) (y : type).
+  Bind Scope ctype_scope with type.
+
+  Global Coercion Tflat : flat_type >-> type.
+  Infix "*" := Prod : ctype_scope.
+  Notation "A -> B" := (Arrow A B) : ctype_scope.
+  Local Coercion Tbase : base_type_code >-> flat_type.
+
+  Section interp.
+    Section type.
+      Context (interp_flat_type : flat_type -> Type).
+      Fixpoint interp_type_gen (t : type) :=
+        match t with
+        | Tflat t => interp_flat_type t
+        | Arrow x y => (interp_flat_type x -> interp_type_gen y)%type
+        end.
+    End type.
+    Section flat_type.
+      Context (interp_base_type : base_type_code -> Type).
+      Fixpoint interp_flat_type_gen (t : flat_type) :=
+        match t with
+        | Tbase t => interp_base_type t
+        | Prod x y => prod (interp_flat_type_gen x) (interp_flat_type_gen y)
+        end.
+      Definition interp_type := interp_type_gen interp_flat_type_gen.
+    End flat_type.
+  End interp.
+
+  Section expr_param.
+    Context (interp_base_type : base_type_code -> Type).
+    Context (op : flat_type (* input tuple *) -> flat_type (* output type *) -> Type).
+    Local Notation interp_type := (interp_type interp_base_type).
+    Local Notation interp_flat_type := (interp_flat_type_gen interp_base_type).
+    Section expr.
+      Context {var : base_type_code -> Type}.
+
+      (** N.B. [Let] binds the components of a pair to separate variables, and does so recursively *)
+      Inductive exprf : flat_type -> Type :=
+      | Const {t : flat_type} : interp_type t -> exprf t
+      | Var {t} : var t -> exprf t
+      | Op {t1 tR} : op t1 tR -> exprf t1 -> exprf tR
+      | Let : forall {tx}, exprf tx -> forall {tC}, (interp_flat_type_gen var tx -> exprf tC) -> exprf tC
+      | Pair : forall {t1}, exprf t1 -> forall {t2}, exprf t2 -> exprf (Prod t1 t2).
+      Bind Scope expr_scope with exprf.
+      Inductive expr : type -> Type :=
+      | Return {t} : exprf t -> expr t
+      | Abs {src dst} : (var src -> expr dst) -> expr (Arrow src dst).
+      Bind Scope expr_scope with expr.
+      Global Coercion Return : exprf >-> expr.
+      (** Sometimes, we want to deal with partially-interpreted
+          expressions, things like [prod (exprf A) (exprf B)] rather
+          than [exprf (Prod A B)], or like [prod (var A) (var B)] when
+          we start with the type [Prod A B].  These convenience
+          functions let us recurse on the type in only one place, and
+          replace one kind of pairing operator (be it [pair] or [Pair]
+          or anything else) with another kind, and simultaneously
+          mapping a function over the base values (e.g., [Var] (for
+          turning [var] into [exprf]) or [Const] (for turning
+          [interp_base_type] into [exprf])). *)
+      Fixpoint smart_interp_flat_map {f g}
+               (h : forall x, f x -> g (Tbase x))
+               (pair : forall A B, g A -> g B -> g (Prod A B))
+               {t}
+        : interp_flat_type_gen f t -> g t
+        := match t return interp_flat_type_gen f t -> g t with
+           | Tbase _ => h _
+           | Prod A B => fun v => pair _ _
+                                       (@smart_interp_flat_map f g h pair A (fst v))
+                                       (@smart_interp_flat_map f g h pair B (snd v))
+           end.
+      (** [SmartVar] is like [Var], except that it inserts
+          pair-projections and [Pair] as necessary to handle
+          [flat_type], and not just [base_type_code] *)
+      Definition SmartVar {t} : interp_flat_type_gen var t -> exprf t
+        := @smart_interp_flat_map var exprf (fun t => Var) (fun A B x y => Pair x y) t.
+      Definition SmartVarVar {t} : interp_flat_type_gen var t -> interp_flat_type_gen exprf t
+        := @smart_interp_flat_map var (interp_flat_type_gen exprf) (fun t => Var) (fun A B x y => pair x y) t.
+      Definition SmartConst {t} : interp_flat_type t -> interp_flat_type_gen exprf t
+        := @smart_interp_flat_map _ (interp_flat_type_gen exprf) (fun t => Const) (fun A B x y => pair x y) t.
+    End expr.
+
+    Definition Expr (t : type) := forall var, @expr var t.
+
+    Section interp.
+      Context (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst).
+
+      Fixpoint interpf {t} (e : @exprf interp_flat_type t) : interp_flat_type t
+        := match e in exprf t return interp_flat_type t with
+           | Const _ x => x
+           | Var _ x => x
+           | Op _ _ op args => @interp_op _ _ op (@interpf _ args)
+           | Let _ ex _ eC => let x := @interpf _ ex in @interpf _ (eC x)
+           | Pair _ ex _ ey => (@interpf _ ex, @interpf _ ey)
+           end.
+      Fixpoint interp {t} (e : @expr interp_type t) : interp_type t
+        := match e in expr t return interp_type t with
+           | Return _ x => interpf x
+           | Abs _ _ f => fun x => @interp _ (f x)
+           end.
+
+      Definition Interp {t} (E : Expr t) : interp_type t := interp (E _).
+    End interp.
+
+    Section map.
+      Context {var1 var2 : base_type_code -> Type}.
+      Context (fvar12 : forall t, var1 t -> var2 t)
+              (fvar21 : forall t, var2 t -> var1 t).
+
+      Fixpoint mapf_interp_flat_type_gen {t} (e : interp_flat_type_gen var2 t) {struct t}
+        : interp_flat_type_gen var1 t
+        := match t return interp_flat_type_gen _ t -> interp_flat_type_gen _ t with
+           | Tbase _ => fvar21 _
+           | Prod x y => fun xy => (@mapf_interp_flat_type_gen _ (fst xy),
+                                    @mapf_interp_flat_type_gen _ (snd xy))
+           end e.
+
+      Fixpoint mapf {t} (e : @exprf var1 t) : @exprf var2 t
+        := match e in exprf t return exprf t with
+           | Const _ x => Const x
+           | Var _ x => Var (fvar12 _ x)
+           | Op _ _ op args => Op op (@mapf _ args)
+           | Let _ ex _ eC => Let (@mapf _ ex) (fun x => @mapf _ (eC (mapf_interp_flat_type_gen x)))
+           | Pair _ ex _ ey => Pair (@mapf _ ex) (@mapf _ ey)
+           end.
+    End map.
+
+    Section wf.
+      Context {var1 var2 : base_type_code -> Type}.
+
+      Local Notation eP := (fun t => var1 t * var2 t)%type (only parsing).
+      Local Notation "x == y" := (existT eP _ (x, y)).
+      Fixpoint flatten_binding_list {t} (x : interp_flat_type_gen var1 t) (y : interp_flat_type_gen var2 t) : list (sigT eP)
+        := (match t return interp_flat_type_gen var1 t -> interp_flat_type_gen var2 t -> list _ with
+            | Tbase _ => fun x y => (x == y) :: nil
+            | Prod t0 t1 => fun x y => @flatten_binding_list _ (fst x) (fst y) ++ @flatten_binding_list _ (snd x) (snd y)
+            end x y)%list.
+
+      Inductive wff : list (sigT eP) -> forall {t}, @exprf var1 t -> @exprf var2 t -> Prop :=
+      | WfConst : forall t G n, @wff G t (Const n) (Const n)
+      | WfVar : forall G (t : base_type_code) x x', List.In (x == x') G -> @wff G t (Var x) (Var x')
+      | WfOp : forall G {t} {tR} (e : @exprf var1 t) (e' : @exprf var2 t) op,
+          wff G e e'
+          -> wff G (Op (tR := tR) op e) (Op (tR := tR) op e')
+      | WfLet : forall G t1 t2 e1 e1' (e2 : interp_flat_type_gen var1 t1 -> @exprf var1 t2) e2',
+          wff G e1 e1'
+          -> (forall x1 x2, wff (flatten_binding_list x1 x2 ++ G) (e2 x1) (e2' x2))
+          -> wff G (Let e1 e2) (Let e1' e2')
+      | WfPair : forall G {t1} {t2} (e1: @exprf var1 t1) (e2: @exprf var1 t2)
+                        (e1': @exprf var2 t1) (e2': @exprf var2 t2),
+          wff G e1 e1'
+          -> wff G e2 e2'
+          -> wff G (Pair e1 e2) (Pair e1' e2').
+      Inductive wf : list (sigT eP) -> forall {t}, @expr var1 t -> @expr var2 t -> Prop :=
+      | WfReturn : forall t G e e', @wff G t e e' -> wf G (Return e) (Return e')
+      | WfAbs : forall A B G e e',
+          (forall x x', @wf ((x == x') :: G) B (e x) (e' x'))
+          -> @wf G (Arrow A B) (Abs e) (Abs e').
+    End wf.
+
+    Definition Wf {t} (E : @Expr t) := forall var1 var2, wf nil (E var1) (E var2).
+
+    Axiom Wf_admitted : forall {t} (E:Expr t), @Wf t E.
+  End expr_param.
+End language.
+Global Arguments Prod {_} _ _.
+Global Arguments Arrow {_} _ _.
+Global Arguments Tbase {_} _.
+Infix "*" := (@Prod _) : ctype_scope.
+Notation "A -> B" := (@Arrow _ A B) : ctype_scope.
+
+Ltac admit_Wf := apply Wf_admitted.
+
+Global Arguments Const {_ _ _ _ _} _.
+Global Arguments Var {_ _ _ _ _} _.
+Global Arguments SmartVar {_ _ _ _ _} _.
+Global Arguments SmartVarVar {_ _ _ _ _} _.
+Global Arguments SmartConst {_ _ _ _ _} _.
+Global Arguments Op {_ _ _ _ _ _} _ _.
+Global Arguments Let {_ _ _ _ _} _ {_} _.
+Global Arguments Pair {_ _ _ _ _} _ {_} _.
+Global Arguments Return {_ _ _ _ _} _.
+Global Arguments Abs {_ _ _ _ _ _} _.
+Global Arguments interp_flat_type_gen {_} _ _.
+Global Arguments interp_type {_} _ _.
+
+Notation "'slet' x := A 'in' b" := (Let A (fun x => b)) : expr_scope.
+Notation "'λ'  x .. y , t" := (Abs (fun x => .. (Abs (fun y => t%expr)) ..)) : expr_scope.
+Notation "( x , y , .. , z )" := (Pair .. (Pair x%expr y%expr) .. z%expr) : expr_scope.
diff --git a/src/Reflection/TestCase.v b/src/Reflection/TestCase.v
new file mode 100644
index 000000000..7511bb750
--- /dev/null
+++ b/src/Reflection/TestCase.v
@@ -0,0 +1,119 @@
+Require Import Crypto.Reflection.Syntax.
+Require Export Crypto.Reflection.Reify.
+Require Import Crypto.Reflection.InputSyntax.
+Require Crypto.Reflection.Linearize.
+Require Import Crypto.Reflection.WfReflective.
+
+Import ReifyDebugNotations.
+
+Inductive base_type := Tnat.
+Definition interp_base_type (v : base_type) : Type :=
+  match v with
+  | Tnat => nat
+  end.
+Local Notation tnat := (Tbase Tnat).
+Inductive op : flat_type base_type -> flat_type base_type -> Type :=
+| Add : op (Prod tnat tnat) tnat
+| Mul : op (Prod tnat tnat) tnat.
+Definition interp_op src dst (f : op src dst) : interp_flat_type_gen interp_base_type src -> interp_flat_type_gen interp_base_type dst
+  := match f with
+     | Add => fun xy => fst xy + snd xy
+     | Mul => fun xy => fst xy * snd xy
+     end%nat.
+
+Global Instance: forall x y, reify_op op (x + y)%nat 2 Add := fun _ _ => I.
+Global Instance: forall x y, reify_op op (x * y)%nat 2 Mul := fun _ _ => I.
+Global Instance: reify type nat := Tnat.
+
+Ltac Reify' e := Reify.Reify' base_type interp_base_type op e.
+Ltac Reify e := Reify.Reify base_type interp_base_type op e.
+Ltac Reify_rhs := Reify.Reify_rhs base_type interp_base_type op interp_op.
+
+(*Ltac reify_debug_level ::= constr:(2).*)
+
+Goal (flat_type base_type -> Type) -> False.
+  intro var.
+  let x := reifyf base_type interp_base_type op var 1%nat in pose x.
+  let x := Reify' 1%nat in unify x (fun var => Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1).
+  let x := reifyf base_type interp_base_type op var (1 + 1)%nat in pose x.
+  let x := Reify' (1 + 1)%nat in unify x (fun var => Op Add (Pair (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1))).
+  let x := reify_abs base_type interp_base_type op var (fun x => x + 1)%nat in pose x.
+  let x := Reify' (fun x => x + 1)%nat in unify x (fun var => Abs (fun y => Op Add (Pair (Var y) (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1)))).
+  let x := reifyf base_type interp_base_type op var (let '(a, b) := (1, 1) in a + b)%nat in pose x.
+  let x := reifyf base_type interp_base_type op var (let '(a, b, c) := (1, 1, 1) in a + b + c)%nat in pose x.
+  let x := Reify' (fun x => let '(a, b) := (1, 1) in a + x)%nat in let x := (eval vm_compute in x) in pose x.
+  let x := Reify' (fun x => let '(a, b) := (1, 1) in a + x)%nat in
+  unify x (fun var => Abs (fun x' =>
+                          let c1 := (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) in
+                          MatchPair (tC:=tnat) (Pair c1 c1)
+                                    (fun x0 _ : var tnat => Op Add (Pair (Var x0) (Var x'))))).
+  let x := reifyf base_type interp_base_type op var (let x := 5 in let y := 6 in (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in pose x.
+  let x := Reify' (fun x y => (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in pose x.
+Abort.
+
+
+Goal (0 = let x := 1+2 in x*3)%nat.
+  Reify_rhs.
+Abort.
+
+Goal (0 = let x := 1 in let y := 2 in x * y)%nat.
+  Reify_rhs.
+Abort.
+
+Import Linearize.
+
+Goal True.
+  let x := Reify (fun x y => (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in
+  pose (InlineConst (Linearize x)) as e.
+  vm_compute in e.
+Abort.
+
+Definition example_expr : Syntax.Expr base_type interp_base_type op (Tbase Tnat).
+Proof.
+  let x := Reify (let x := 1 in let y := 1 in (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in
+  exact x.
+Defined.
+
+Definition base_type_eq_semidec_transparent : forall t1 t2, option (t1 = t2)
+  := fun t1 t2 => match t1, t2 with
+               | Tnat, Tnat => Some eq_refl
+               end.
+Lemma base_type_eq_semidec_is_dec : forall t1 t2,
+    base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2.
+Proof.
+  intros t1 t2; destruct t1, t2; simpl; intros; congruence.
+Qed.
+Definition op_beq t1 tR : op t1 tR -> op t1 tR -> option pointed_Prop
+  := fun x y => match x, y with
+             | Add, Add => Some trivial
+             | Add, _ => None
+             | Mul, Mul => Some trivial
+             | Mul, _ => None
+             end.
+Lemma op_beq_bl t1 tR (x y : op t1 tR)
+  : match op_beq t1 tR x y with
+    | Some p => to_prop p
+    | None => False
+    end -> x = y.
+Proof.
+  destruct x; simpl.
+  { refine match y with Add => _ | _ => _ end; tauto. }
+  { refine match y with Add => _ | _ => _ end; tauto. }
+Qed.
+
+Ltac reflect_Wf := WfReflective.reflect_Wf base_type_eq_semidec_is_dec op_beq_bl.
+
+Lemma example_expr_wf_slow : Wf _ _ _ example_expr.
+Proof.
+  Time (vm_compute; intros;
+          repeat match goal with
+                 | [ |- wf _ _ _ _ _ _ ] => constructor; intros
+                 | [ |- wff _ _ _ _ _ _ ] => constructor; intros
+                 | [ |- List.In _ _ ] => vm_compute
+                 | [ |- ?x = ?x \/ _ ] => left; reflexivity
+                 | [ |- ?x = ?y \/ _ ] => right
+                 end). (* 0.036 s *)
+Qed.
+
+Lemma example_expr_wf : Wf _ _ _ example_expr.
+Proof. Time reflect_Wf. (* 0.008 s *) Qed.
diff --git a/src/Reflection/WfReflective.v b/src/Reflection/WfReflective.v
new file mode 100644
index 000000000..34a139643
--- /dev/null
+++ b/src/Reflection/WfReflective.v
@@ -0,0 +1,507 @@
+(** * A reflective Version of [Wf] proofs *)
+(** Because every constructor of [Syntax.wff] stores the syntax tree
+    being proven well-formed, a proof that a syntax tree is
+    well-formed is quadratic in the size of the syntax tree.  (Tacking
+    an extra term on to the head of the syntax tree requires an extra
+    constructor of [Syntax.wff], and that constructor stores the
+    entirety of the new syntax tree.)
+
+    In practice, this makes proving well-formedness of large trees
+    very slow.  To remedy this, we provide an alternative type
+    ([reflect_wffT]) that implies [Syntax.wff], but is only linear in
+    the size of the syntax tree, with a coefficient less than 1.
+
+    The idea is that, since we already know the syntax-tree arguments
+    to the constructors (and, moreover, already fully know the shape
+    of the [Syntax.wff] proof, because it will exactly match the shape
+    of the syntax tree), the proof doesn't have to store any of that
+    information.  It only has to store the genuinely new information
+    in [Syntax.wff], namely, that the constants don't depend on the
+    [var] argument (i.e., that the constants in the same location in
+    the two expressions are equal), and that there are no free nor
+    mismatched variables (i.e., that the variables in the same
+    location in the two expressions are in the relevant list of
+    binders).  We can make the further optimization of storing the
+    location in the list of each binder, so that all that's left to
+    verify is that the locations line up correctly.
+
+    Since there is no way to assign list locations (De Bruijn indices)
+    after the fact (that is, once we have an [exprf var t] rather than
+    an [Expr t]), we instead start from an expression where [var] is
+    enriched with De Bruijn indices, and talk about [Syntax.wff] of
+    that expression stripped of its De Bruijn indices.  Since this
+    procedure is only expected to work on concrete syntax trees, we
+    will be able to simply check by unification to check that
+    stripping the indices results in the term that we started with.
+
+    The interface of this file is that, to prove a [Syntax.Wf] goal,
+    you invoke the tactic [reflect_Wf base_type_eq_semidec_is_dec
+    op_beq_bl], where:
+
+    - [base_type_eq_semidec_is_dec : forall t1 t2,
+       base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2] for
+       some [base_type_eq_semidec_transparent : forall t1 t2 :
+       base_type_code, option (t1 = t2)], and
+
+    - [op_beq_bl : forall t1 tR x y, prop_of_option (op_beq t1 tR x y)
+      -> x = y] for some [op_beq : forall t1 tR, op t1 tR -> op t1 tR
+      -> option pointed_Prop] *)
+
+Require Import Coq.Arith.Arith Coq.Logic.Eqdep_dec.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Util.Notations Crypto.Util.Tactics Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod Crypto.Util.Decidable Crypto.Util.ListUtil.
+Require Export Crypto.Util.PointedProp. (* export for the [bool >-> option pointed_Prop] coercion *)
+Require Export Crypto.Util.FixCoqMistakes.
+
+
+Section language.
+  (** To be able to optimize away so much of the [Syntax.wff] proof,
+      we must be able to decide a few things: equality of base types,
+      and equality of operator codes.  Since we will be casting across
+      the equality proofs of base types, we require that this
+      semi-decider give transparent proofs.  (This requirement is not
+      enforced, but it will block [vm_compute] when trying to use the
+      lemma in this file.) *)
+  Context (base_type_code : Type).
+  Context (interp_base_type : base_type_code -> Type).
+  Context (base_type_eq_semidec_transparent : forall t1 t2 : base_type_code, option (t1 = t2)).
+  Context (base_type_eq_semidec_is_dec : forall t1 t2, base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2).
+  Context (op : flat_type base_type_code -> flat_type base_type_code -> Type).
+  (** In practice, semi-deciding equality of operators should either
+      return [Some trivial] or [None], and not make use of the
+      generality of [pointed_Prop].  However, we need to use
+      [pointed_Prop] internally because we need to talk about equality
+      of things of type [var t], for [var : base_type_code -> Type].
+      It does not hurt to allow extra generality in [op_beq]. *)
+  Context (op_beq : forall t1 tR, op t1 tR -> op t1 tR -> option pointed_Prop).
+  Context (op_beq_bl : forall t1 tR x y, prop_of_option (op_beq t1 tR x y) -> x = y).
+  Context {var1 var2 : base_type_code -> Type}.
+
+  Local Notation eP := (fun t => var1 (fst t) * var2 (snd t))%type (only parsing).
+
+  (* convenience notations that fill in some arguments used across the section *)
+  Local Notation flat_type := (flat_type base_type_code).
+  Local Notation type := (type base_type_code).
+  Let Tbase := @Tbase base_type_code.
+  Local Coercion Tbase : base_type_code >-> Syntax.flat_type.
+  Local Notation interp_type := (interp_type interp_base_type).
+  Local Notation interp_flat_type := (interp_flat_type_gen interp_base_type).
+  Local Notation exprf := (@exprf base_type_code interp_base_type op).
+  Local Notation expr := (@expr base_type_code interp_base_type op).
+
+  Local Ltac inversion_base_type_code_step :=
+    match goal with
+    | [ H : ?x = ?x :> base_type_code |- _ ]
+      => assert (H = eq_refl) by eapply UIP_dec, dec_rel_of_semidec_rel, base_type_eq_semidec_is_dec; subst H
+    | [ H : ?x = ?y :> base_type_code |- _ ] => subst x || subst y
+    end.
+  Local Ltac inversion_base_type_code := repeat inversion_base_type_code_step.
+
+  (* lift [base_type_eq_semidec_transparent] across [flat_type] *)
+  Fixpoint flat_type_eq_semidec_transparent (t1 t2 : flat_type) : option (t1 = t2)
+    := match t1, t2 return option (t1 = t2) with
+       | Syntax.Tbase t1, Syntax.Tbase t2
+         => option_map (@f_equal _ _ Tbase _ _)
+                      (base_type_eq_semidec_transparent t1 t2)
+       | Syntax.Tbase _, _ => None
+       | Prod A B, Prod A' B'
+         => match flat_type_eq_semidec_transparent A A', flat_type_eq_semidec_transparent B B' with
+           | Some p, Some q => Some (f_equal2 Prod p q)
+           | _, _ => None
+           end
+       | Prod _ _, _ => None
+       end.
+  Fixpoint type_eq_semidec_transparent (t1 t2 : type) : option (t1 = t2)
+    := match t1, t2 return option (t1 = t2) with
+       | Syntax.Tflat t1, Syntax.Tflat t2
+         => option_map (@f_equal _ _ (@Tflat _) _ _)
+                      (flat_type_eq_semidec_transparent t1 t2)
+       | Syntax.Tflat _, _ => None
+       | Arrow A B, Arrow A' B'
+         => match base_type_eq_semidec_transparent A A', type_eq_semidec_transparent B B' with
+           | Some p, Some q => Some (f_equal2 (@Arrow base_type_code) p q)
+           | _, _ => None
+           end
+       | Arrow _ _, _ => None
+       end.
+  Lemma base_type_eq_semidec_transparent_refl t : base_type_eq_semidec_transparent t t = Some eq_refl.
+  Proof.
+    clear -base_type_eq_semidec_is_dec.
+    pose proof (base_type_eq_semidec_is_dec t t).
+    destruct (base_type_eq_semidec_transparent t t); intros; try intuition congruence.
+    inversion_base_type_code; reflexivity.
+  Qed.
+  Lemma flat_type_eq_semidec_transparent_refl t : flat_type_eq_semidec_transparent t t = Some eq_refl.
+  Proof.
+    clear -base_type_eq_semidec_is_dec.
+    induction t as [t | A B IHt]; simpl.
+    { rewrite base_type_eq_semidec_transparent_refl; reflexivity. }
+    { rewrite_hyp !*; reflexivity. }
+  Qed.
+  Lemma type_eq_semidec_transparent_refl t : type_eq_semidec_transparent t t = Some eq_refl.
+  Proof.
+    clear -base_type_eq_semidec_is_dec.
+    induction t as [t | A B IHt]; simpl.
+    { rewrite flat_type_eq_semidec_transparent_refl; reflexivity. }
+    { rewrite base_type_eq_semidec_transparent_refl; rewrite_hyp !*; reflexivity. }
+  Qed.
+
+  Definition op_beq' t1 tR t1' tR' (x : op t1 tR) (y : op t1' tR') : option pointed_Prop
+    := match flat_type_eq_semidec_transparent t1 t1', flat_type_eq_semidec_transparent tR tR' with
+       | Some p, Some q
+         => match p in (_ = t1'), q in (_ = tR') return op t1' tR' -> _ with
+           | eq_refl, eq_refl => fun y => op_beq _ _ x y
+           end y
+       | _, _ => None
+       end.
+
+  (** While [Syntax.wff] is parameterized over a list of [sigT (fun t
+      => var1 t * var2 t)], it is simpler here to make everything
+      heterogenous, rather than trying to mix homogenous and
+      heterogenous things.† Thus we parameterize our [reflect_wffT]
+      over a list of [sigT (fun t => var1 (fst t) * var2 (snd t))],
+      and write a function ([duplicate_type]) that turns the former
+      into the latter.
+
+      † This is an instance of the general theme that abstraction
+        barriers are important.  Here we enforce the abstraction
+        barrier that our input decision procedures are homogenous, but
+        all of our internal code is strictly heterogenous.  This
+        allows us to contain the conversions between homogenous and
+        heterogenous code to a few functions: [op_beq'],
+        [eq_type_and_var], [eq_type_and_const], and to the statement
+        about [Syntax.wff] itself.  *)
+
+  Definition eq_semidec_and_gen {T} (semidec : forall x y : T, option (x = y))
+             (t t' : T) (f : T -> Type) (x : f t) (x' : f t')
+    : option pointed_Prop
+    := match semidec t t' with
+       | Some p
+         => Some (inject (eq_rect _ f x _ p = x'))
+       | None => None
+       end.
+
+  (* Here is where we use the generality of [pointed_Prop], to say
+     that two things of type [var1] are equal, and two things of type
+     [var2] are equal. *)
+  Definition eq_type_and_var : sigT eP -> sigT eP -> option pointed_Prop
+    := fun x y => (eq_semidec_and_gen
+                  base_type_eq_semidec_transparent _ _ var1 (fst (projT2 x)) (fst (projT2 y))
+                /\ eq_semidec_and_gen
+                    base_type_eq_semidec_transparent _ _ var2 (snd (projT2 x)) (snd (projT2 y)))%option_pointed_prop.
+  Definition eq_type_and_const (t t' : flat_type) (x : interp_flat_type t) (y : interp_flat_type t')
+    : option pointed_Prop
+    := eq_semidec_and_gen
+         flat_type_eq_semidec_transparent _ _ interp_flat_type x y.
+
+  Definition duplicate_type (ls : list (sigT (fun t => var1 t * var2 t)%type)) : list (sigT eP)
+    := List.map (fun v => existT eP (projT1 v, projT1 v) (projT2 v)) ls.
+
+  Lemma duplicate_type_app ls ls'
+    : (duplicate_type (ls ++ ls') = duplicate_type ls ++ duplicate_type ls')%list.
+  Proof. apply List.map_app. Qed.
+  Lemma duplicate_type_length ls
+    : List.length (duplicate_type ls) = List.length ls.
+  Proof. apply List.map_length. Qed.
+  Lemma duplicae_type_in t v ls
+    : List.In (existT _ (t, t) v) (duplicate_type ls) -> List.In (existT _ t v) ls.
+  Proof.
+    unfold duplicate_type; rewrite List.in_map_iff.
+    intros [ [? ?] [? ?] ].
+    inversion_sigma; inversion_prod; inversion_base_type_code; subst; simpl.
+    assumption.
+  Qed.
+  Lemma duplicate_type_not_in G t t0 v (H : base_type_eq_semidec_transparent t t0 = None)
+    : ~List.In (existT _ (t, t0) v) (duplicate_type G).
+  Proof.
+    apply base_type_eq_semidec_is_dec in H.
+    clear -H; intro H'.
+    induction G as [|? ? IHG]; simpl in *; destruct H';
+      intuition; congruence.
+  Qed.
+
+  Definition preflatten_binding_list2 t1 t2 : option (forall (x : interp_flat_type_gen var1 t1) (y : interp_flat_type_gen var2 t2), list (sigT (fun t => var1 t * var2 t)%type))
+    := match flat_type_eq_semidec_transparent t1 t2 with
+       | Some p
+         => Some (fun x y
+                 => let x := eq_rect _ (interp_flat_type_gen var1) x _ p in
+                   flatten_binding_list base_type_code x y)
+       | None => None
+       end.
+  Definition flatten_binding_list2 t1 t2 : option (forall (x : interp_flat_type_gen var1 t1) (y : interp_flat_type_gen var2 t2), list (sigT eP))
+    := option_map (fun f x y => duplicate_type (f x y)) (preflatten_binding_list2 t1 t2).
+  (** This function adds De Bruijn indices to variables *)
+  Fixpoint natize_interp_flat_type_gen var t (base : nat) (v : interp_flat_type_gen var t) {struct t}
+    : nat * interp_flat_type_gen (fun t : base_type_code => nat * var t)%type t
+    := match t return interp_flat_type_gen var t -> nat * interp_flat_type_gen _ t with
+       | Prod A B => fun v => let ret := @natize_interp_flat_type_gen _ B base (snd v) in
+                          let base := fst ret in
+                          let b := snd ret in
+                          let ret := @natize_interp_flat_type_gen _ A base (fst v) in
+                          let base := fst ret in
+                          let a := snd ret in
+                          (base, (a, b))
+       | Syntax.Tbase t => fun v => (S base, (base, v))
+       end v.
+  Arguments natize_interp_flat_type_gen {var t} _ _.
+  Lemma length_natize_interp_flat_type_gen1 {t} (base : nat) (v1 : interp_flat_type_gen var1 t) (v2 : interp_flat_type_gen var2 t)
+    : fst (natize_interp_flat_type_gen base v1) = length (flatten_binding_list base_type_code v1 v2) + base.
+  Proof.
+    revert base; induction t; simpl; [ reflexivity | ].
+    intros; rewrite List.app_length, <- plus_assoc.
+    rewrite_hyp <- ?*; reflexivity.
+  Qed.
+  Lemma length_natize_interp_flat_type_gen2 {t} (base : nat) (v1 : interp_flat_type_gen var1 t) (v2 : interp_flat_type_gen var2 t)
+    : fst (natize_interp_flat_type_gen base v2) = length (flatten_binding_list base_type_code v1 v2) + base.
+  Proof.
+    revert base; induction t; simpl; [ reflexivity | ].
+    intros; rewrite List.app_length, <- plus_assoc.
+    rewrite_hyp <- ?*; reflexivity.
+  Qed.
+
+  (* This function strips De Bruijn indices from expressions *)
+  Fixpoint unnatize_exprf {var t} (base : nat) (e : @exprf (fun t => nat * var t)%type t) : @exprf var t
+    := match e in @Syntax.exprf _ _ _ _ t return exprf t with
+       | Const _ x => Const x
+       | Var _ x => Var (snd x)
+       | Op _ _ op args => Op op (@unnatize_exprf _ _ base args)
+       | Let _ ex _ eC => Let (@unnatize_exprf _ _ base ex)
+                             (fun x => let v := natize_interp_flat_type_gen base x in
+                                    @unnatize_exprf _ _ (fst v) (eC (snd v)))
+       | Pair _ x _ y => Pair (@unnatize_exprf _ _ base x) (@unnatize_exprf _ _ base y)
+       end.
+  Fixpoint unnatize_expr {var t} (base : nat) (e : @expr (fun t => nat * var t)%type t) : @expr var t
+    := match e in @Syntax.expr _ _ _ _ t return expr t with
+       | Return _ x => unnatize_exprf base x
+       | Abs tx tR f => Abs (fun x : var tx => let v := natize_interp_flat_type_gen (t:=tx) base x in
+                                           @unnatize_expr _ _ (fst v) (f (snd v)))
+       end.
+
+  Fixpoint reflect_wffT (G : list (sigT (fun t => var1 (fst t) * var2 (snd t))%type))
+           {t1 t2 : flat_type}
+           (e1 : @exprf (fun t => nat * var1 t)%type t1) (e2 : @exprf (fun t => nat * var2 t)%type t2)
+           {struct e1}
+    : option pointed_Prop
+    := match e1, e2 return option _ with
+       | Const t0 x, Const t1 y
+         => match flat_type_eq_semidec_transparent t0 t1 with
+           | Some p => Some (inject (eq_rect _ interp_flat_type x _ p = y))
+           | None => None
+           end
+       | Const _ _, _ => None
+       | Var t0 x, Var t1 y
+         => match beq_nat (fst x) (fst y), List.nth_error G (List.length G - S (fst x)) with
+           | true, Some v => eq_type_and_var v (existT _ (t0, t1) (snd x, snd y))
+           | _, _ => None
+           end
+       | Var _ _, _ => None
+       | Op t1 tR op args, Op t1' tR' op' args'
+         => match @reflect_wffT G t1 t1' args args', op_beq' t1 tR t1' tR' op op' with
+           | Some p, Some q => Some (p /\ q)%pointed_prop
+           | _, _ => None
+           end
+       | Op _ _ _ _, _ => None
+       | Let tx ex tC eC, Let tx' ex' tC' eC'
+         => match @reflect_wffT G tx tx' ex ex', @flatten_binding_list2 tx tx', flat_type_eq_semidec_transparent tC tC' with
+           | Some p, Some G0, Some _
+             => Some (p /\ inject (forall (x : interp_flat_type_gen var1 tx) (x' : interp_flat_type_gen var2 tx'),
+                                    match @reflect_wffT (G0 x x' ++ G)%list _ _
+                                                       (eC (snd (natize_interp_flat_type_gen (List.length G) x)))
+                                                       (eC' (snd (natize_interp_flat_type_gen (List.length G) x'))) with
+                                    | Some p => to_prop p
+                                    | None => False
+                                    end))
+           | _, _, _ => None
+           end
+       | Let _ _ _ _, _ => None
+       | Pair tx ex ty ey, Pair tx' ex' ty' ey'
+         => match @reflect_wffT G tx tx' ex ex', @reflect_wffT G ty ty' ey ey' with
+           | Some p, Some q => Some (p /\ q)
+           | _, _ => None
+           end
+       | Pair _ _ _ _, _ => None
+       end%pointed_prop.
+
+    Fixpoint reflect_wfT (G : list (sigT (fun t => var1 (fst t) * var2 (snd t))%type))
+           {t1 t2 : type}
+           (e1 : @expr (fun t => nat * var1 t)%type t1) (e2 : @expr (fun t => nat * var2 t)%type t2)
+           {struct e1}
+    : option pointed_Prop
+    := match e1, e2 return option _ with
+       | Return _ x, Return _ y
+         => reflect_wffT G x y
+       | Return _ _, _ => None
+       | Abs tx tR f, Abs tx' tR' f'
+         => match @flatten_binding_list2 tx tx', type_eq_semidec_transparent tR tR' with
+           | Some G0, Some _
+             => Some (inject (forall (x : interp_flat_type_gen var1 tx) (x' : interp_flat_type_gen var2 tx'),
+                                match @reflect_wfT (G0 x x' ++ G)%list _ _
+                                                   (f (snd (natize_interp_flat_type_gen (List.length G) x)))
+                                                   (f' (snd (natize_interp_flat_type_gen (List.length G) x'))) with
+                                | Some p => to_prop p
+                                | None => False
+                                end))
+           | _, _ => None
+           end
+       | Abs _ _ _, _ => None
+       end%pointed_prop.
+
+  Local Ltac handle_op_beq_correct :=
+    repeat match goal with
+           | [ H : op_beq ?t1 ?tR ?x ?y = _ |- _ ]
+             => let H' := fresh in
+               pose proof (op_beq_bl t1 tR x y) as H'; rewrite H in H'; clear H
+           end.
+  Local Ltac t_step :=
+    match goal with
+    | _ => progress unfold eq_type_and_var, op_beq', flatten_binding_list2, preflatten_binding_list2, option_map, and_option_pointed_Prop, eq_semidec_and_gen in *
+    | _ => progress simpl in *
+    | _ => progress break_match
+    | _ => progress subst
+    | _ => progress inversion_option
+    | _ => progress inversion_pointed_Prop
+    | _ => congruence
+    | _ => tauto
+    | _ => progress intros
+    | _ => progress handle_op_beq_correct
+    | _ => progress specialize_by tauto
+    | [ v : sigT _ |- _ ] => destruct v
+    | [ v : prod _ _ |- _ ] => destruct v
+    | [ H : forall x x', _ |- wff _ _ _ (flatten_binding_list _ ?x1 ?x2 ++ _)%list _ _ ]
+      => specialize (H x1 x2)
+    | [ H : forall x x', _ |- wf _ _ _ (existT _ _ (?x1, ?x2) :: _)%list _ _ ]
+      => specialize (H x1 x2)
+    | [ H : and _ _ |- _ ] => destruct H
+    | [ H : context[duplicate_type (_ ++ _)%list] |- _ ]
+      => rewrite duplicate_type_app in H
+    | [ H : context[List.length (duplicate_type _)] |- _ ]
+      => rewrite duplicate_type_length in H
+    | [ H : context[List.length (_ ++ _)%list] |- _ ]
+      => rewrite List.app_length in H
+    | [ |- wff _ _ _ _ (unnatize_exprf (fst _) _) (unnatize_exprf (fst _) _) ]
+      => erewrite length_natize_interp_flat_type_gen1, length_natize_interp_flat_type_gen2; eassumption
+    | [ |- wf _ _ _ _ (unnatize_exprf (fst _) _) (unnatize_exprf (fst _) _) ]
+      => erewrite length_natize_interp_flat_type_gen1, length_natize_interp_flat_type_gen2; eassumption
+    | [ |- @wf _ _ _ _ _ _ (Syntax.Tflat _ _) _ _ ] => constructor
+    | [ |- @wf _ _ _ _ _ _ _ (Syntax.Abs _) (Syntax.Abs _) ] => constructor
+    | [ H : base_type_eq_semidec_transparent _ _ = None |- False ] => eapply duplicate_type_not_in; eassumption
+    | [ H : List.nth_error _ _ = Some _ |- _ ] => apply List.nth_error_In in H
+    | [ H : List.In _ (duplicate_type _) |- _ ] => apply duplicae_type_in in H
+    | [ H : context[match _ with _ => _ end] |- _ ] => revert H; progress break_match
+    | [ |- wff _ _ _ _ _ _ ] => constructor
+    | _ => progress unfold and_pointed_Prop in *
+    end.
+  Local Ltac t := repeat t_step.
+  Fixpoint reflect_wff (G : list (sigT (fun t => var1 t * var2 t)%type))
+           {t1 t2 : flat_type}
+           (e1 : @exprf (fun t => nat * var1 t)%type t1) (e2 : @exprf (fun t => nat * var2 t)%type t2)
+           {struct e1}
+    : match reflect_wffT (duplicate_type G) e1 e2, flat_type_eq_semidec_transparent t1 t2 with
+      | Some reflective_obligation, Some p
+        => to_prop reflective_obligation
+          -> @wff base_type_code interp_base_type op var1 var2 G t2 (eq_rect _ exprf (unnatize_exprf (List.length G) e1) _ p) (unnatize_exprf (List.length G) e2)
+      | _, _ => True
+      end.
+  Proof.
+    destruct e1 as [ | | ? ? ? args | tx ex tC eC | ? ex ? ey ],
+                   e2 as [ | | ? ? ? args' | tx' ex' tC' eC' | ? ex' ? ey' ]; simpl; try solve [ exact I ];
+      [ clear reflect_wff
+      | clear reflect_wff
+      | specialize (reflect_wff G _ _ args args')
+      | pose proof (reflect_wff G _ _ ex ex');
+        pose proof (fun x x'
+                    => match preflatten_binding_list2 tx tx' as v return match v with Some _ => _ | None => True end with
+                      | Some G0
+                        => reflect_wff
+                            (G0 x x' ++ G)%list _ _
+                            (eC (snd (natize_interp_flat_type_gen (length (duplicate_type G)) x)))
+                            (eC' (snd (natize_interp_flat_type_gen (length (duplicate_type G)) x')))
+                      | None => I
+                      end);
+        clear reflect_wff
+      | pose proof (reflect_wff G _ _ ex ex'); pose proof (reflect_wff G _ _ ey ey'); clear reflect_wff ].
+    { t. }
+    { t. }
+    { t. }
+    { t. }
+    { t. }
+  Qed.
+  Fixpoint reflect_wf (G : list (sigT (fun t => var1 t * var2 t)%type))
+           {t1 t2 : type}
+           (e1 : @expr (fun t => nat * var1 t)%type t1) (e2 : @expr (fun t => nat * var2 t)%type t2)
+    : match reflect_wfT (duplicate_type G) e1 e2, type_eq_semidec_transparent t1 t2 with
+      | Some reflective_obligation, Some p
+        => to_prop reflective_obligation
+          -> @wf base_type_code interp_base_type op var1 var2 G t2 (eq_rect _ expr (unnatize_expr (List.length G) e1) _ p) (unnatize_expr (List.length G) e2)
+      | _, _ => True
+      end.
+  Proof.
+    destruct e1 as [ t1 e1 | tx tR f ],
+                   e2 as [ t2 e2 | tx' tR' f' ]; simpl; try solve [ exact I ];
+      [ clear reflect_wf;
+        pose proof (@reflect_wff G t1 t2 e1 e2)
+      | pose proof (fun x x'
+                    => match preflatten_binding_list2 tx tx' as v return match v with Some _ => _ | None => True end with
+                      | Some G0
+                        => reflect_wf
+                            (G0 x x' ++ G)%list _ _
+                            (f (snd (natize_interp_flat_type_gen (length (duplicate_type G)) x)))
+                            (f' (snd (natize_interp_flat_type_gen (length (duplicate_type G)) x')))
+                      | None => I
+                      end);
+        clear reflect_wf ].
+    { t. }
+    { t. }
+  Qed.
+End language.
+
+Section Wf.
+  Context (base_type_code : Type)
+          (interp_base_type : base_type_code -> Type)
+          (base_type_eq_semidec_transparent : forall t1 t2 : base_type_code, option (t1 = t2))
+          (base_type_eq_semidec_is_dec : forall t1 t2, base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2)
+          (op : flat_type base_type_code -> flat_type base_type_code -> Type)
+          (op_beq : forall t1 tR, op t1 tR -> op t1 tR -> option pointed_Prop)
+          (op_beq_bl : forall t1 tR x y, prop_of_option (op_beq t1 tR x y) -> x = y)
+          {t : type base_type_code}
+          (e : @Expr base_type_code interp_base_type op t).
+
+  (** Leads to smaller proofs, but is less generally applicable *)
+  Theorem reflect_Wf_unnatize
+    : (forall var1 var2,
+          prop_of_option (@reflect_wfT base_type_code interp_base_type base_type_eq_semidec_transparent op op_beq var1 var2 nil t t (e _) (e _)))
+      -> Wf _ _ _ (fun var => unnatize_expr base_type_code interp_base_type op 0 (e (fun t => (nat * var t)%type))).
+  Proof.
+    intros H var1 var2; specialize (H var1 var2).
+    pose proof (@reflect_wf base_type_code interp_base_type base_type_eq_semidec_transparent base_type_eq_semidec_is_dec op op_beq op_beq_bl var1 var2 nil t t (e _) (e _)) as H'.
+    rewrite type_eq_semidec_transparent_refl in H' by assumption; simpl in *.
+    edestruct reflect_wfT; simpl in *; tauto.
+  Qed.
+
+  (** Leads to larger proofs (an extra constant factor which is the
+      size of the expression tree), but more generally applicable *)
+  Theorem reflect_Wf
+    : (forall var1 var2,
+          unnatize_expr base_type_code interp_base_type op 0 (e (fun t => (nat * var1 t)%type)) = e _
+          /\ prop_of_option (@reflect_wfT base_type_code interp_base_type base_type_eq_semidec_transparent op op_beq var1 var2 nil t t (e _) (e _)))
+      -> Wf _ _ _ e.
+  Proof.
+    intros H var1 var2.
+    rewrite <- (proj1 (H var1 var2)), <- (proj1 (H var2 var2)).
+    apply reflect_Wf_unnatize, H.
+  Qed.
+End Wf.
+
+
+Ltac generalize_reflect_Wf base_type_eq_semidec_is_dec op_beq_bl :=
+  lazymatch goal with
+  | [ |- @Wf ?base_type_code ?interp_base_type ?op ?t ?e ]
+    => generalize (@reflect_Wf_unnatize base_type_code interp_base_type _ base_type_eq_semidec_is_dec op _ op_beq_bl t e)
+  end.
+Ltac use_reflect_Wf := vm_compute; let H := fresh in intro H; apply H; clear H.
+Ltac fin_reflect_Wf := repeat constructor.
+(** The tactic [reflect_Wf] is the main tactic of this file, used to
+    prove [Syntax.Wf] goals *)
+Ltac reflect_Wf base_type_eq_semidec_is_dec op_beq_bl :=
+  generalize_reflect_Wf base_type_eq_semidec_is_dec op_beq_bl;
+  use_reflect_Wf; fin_reflect_Wf.