# Parametric Higher-Order Abstract Syntax

In contrast to first-order encodings, higher-order encodings avoid explicit modeling of variable identity. Instead, the binding constructs of an object language (the language being formalized) can be represented using the binding constructs of the meta language (the language in which the formalization is done). The best known higher-order encoding is called higher-order abstract syntax (HOAS), and we can start by attempting to apply it directly in Lean.

Remark: this example is based on an example in the book Certified Programming with Dependent Types by Adam Chlipala.

Here is the definition of the simple type system for our programming language, a simply typed lambda calculus with natural numbers as the base type.

```inductive Ty: TypeTy where
| nat: Tynat
| fn: Ty → Ty → Tyfn : Ty: TypeTy → Ty: TypeTy → Ty: TypeTy```

We can write a function to translate `Ty` values to a Lean type — remember that types are first class, so can be calculated just like any other value. We mark `Ty.denote` as `[reducible]` to make sure the typeclass resolution procedure can unfold/reduce it. For example, suppose Lean is trying to synthesize a value for the instance `Add (Ty.denote Ty.nat)`. Since `Ty.denote` is marked as `[reducible]`, the typeclass resolution procedure can reduce `Ty.denote Ty.nat` to `Nat`, and use the builtin instance for `Add Nat` as the solution.

Recall that the term `a.denote` is sugar for `denote a` where `denote` is the function being defined. We call it the "dot notation".

```@[reducible] def Ty.denote: Ty → TypeTy.denote : Ty: TypeTy → Type: Type 1Type
| nat: Tynat    => Nat: TypeNat
| fn: Ty → Ty → Tyfn a: Tya b: Tyb => a: Tya.denote: Ty → Typedenote → b: Tyb.denote: Ty → Typedenote```

With HOAS, each object language binding construct is represented with a function of the meta language. Here is what we get if we apply that idea within an inductive definition of term syntax. However a naive encondig in Lean fails to meet the strict positivity restrictions imposed by the Lean kernel. An alternate higher-order encoding is parametric HOAS, as introduced by Washburn and Weirich for Haskell and tweaked by Adam Chlipala for use in Coq. The key idea is to parameterize the declaration by a type family `rep` standing for a "representation of variables."

```inductive Term': (Ty → Type) → Ty → TypeTerm' (rep: Ty → Typerep : Ty: TypeTy → Type: Type 1Type) : Ty: TypeTy → Type: Type 1Type
| var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep tyvar   : rep: Ty → Typerep ty: Tyty → Term': (Ty → Type) → Ty → TypeTerm' rep: Ty → Typerep ty: Tyty
| const: {rep : Ty → Type} → Nat → Term' rep Ty.natconst : Nat: TypeNat → Term': (Ty → Type) → Ty → TypeTerm' rep: Ty → Typerep .nat: Ty.nat
| plus: {rep : Ty → Type} → Term' rep Ty.nat → Term' rep Ty.nat → Term' rep Ty.natplus  : Term': (Ty → Type) → Ty → TypeTerm' rep: Ty → Typerep .nat: Ty.nat → Term': (Ty → Type) → Ty → TypeTerm' rep: Ty → Typerep .nat: Ty.nat → Term': (Ty → Type) → Ty → TypeTerm' rep: Ty → Typerep .nat: Ty.nat
| lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (Ty.fn dom ran)lam   : (rep: Ty → Typerep dom: Tydom → Term': (Ty → Type) → Ty → TypeTerm' rep: Ty → Typerep ran: Tyran) → Term': (Ty → Type) → Ty → TypeTerm' rep: Ty → Typerep (.fn: Ty → Ty → Ty.fn dom: Tydom ran: Tyran)
| app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (Ty.fn dom ran) → Term' rep dom → Term' rep ranapp   : Term': (Ty → Type) → Ty → TypeTerm' rep: Ty → Typerep (.fn: Ty → Ty → Ty.fn dom: Tydom ran: Tyran) → Term': (Ty → Type) → Ty → TypeTerm' rep: Ty → Typerep dom: Tydom → Term': (Ty → Type) → Ty → TypeTerm' rep: Ty → Typerep ran: Tyran
| let: {rep : Ty → Type} → {ty₁ ty₂ : Ty} → Term' rep ty₁ → (rep ty₁ → Term' rep ty₂) → Term' rep ty₂let   : Term': (Ty → Type) → Ty → TypeTerm' rep: Ty → Typerep ty₁: Tyty₁ → (rep: Ty → Typerep ty₁: Tyty₁ → Term': (Ty → Type) → Ty → TypeTerm' rep: Ty → Typerep ty₂: Tyty₂) → Term': (Ty → Type) → Ty → TypeTerm' rep: Ty → Typerep ty₂: Tyty₂```

Lean accepts this definition because our embedded functions now merely take variables as arguments, instead of arbitrary terms. One might wonder whether there is an easy loophole to exploit here, instantiating the parameter `rep` as term itself. However, to do that, we would need to choose a variable representation for this nested mention of term, and so on through an infinite descent into term arguments.

We write the final type of a closed term using polymorphic quantification over all possible choices of `rep` type family

```open Ty (nat fn)

namespace FirstTry

def Term: Ty → Type 1Term (ty: Tyty : Ty: TypeTy) := (rep: Ty → Typerep : Ty: TypeTy → Type: Type 1Type) → Term': (Ty → Type) → Ty → TypeTerm' rep: Ty → Typerep ty: Tyty```

In the next two example, note how each is written as a function over a `rep` choice, such that the specific choice has no impact on the structure of the term.

```def add: Term (fn nat (fn nat nat))add : Term: Ty → Type 1Term (fn: Ty → Ty → Tyfn nat: Tynat (fn: Ty → Ty → Tyfn nat: Tynat nat: Tynat)) := fun _rep: Ty → Type_rep =>
.lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (fn dom ran).lam fun x: _rep natx => .lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (fn dom ran).lam fun y: _rep naty => .plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat.plus (.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty.var x: _rep natx) (.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty.var y: _rep naty)

def three_the_hard_way: Term natthree_the_hard_way : Term: Ty → Type 1Term nat: Tynat := fun rep: Ty → Typerep =>
.app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (fn dom ran) → Term' rep dom → Term' rep ran.app (.app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (fn dom ran) → Term' rep dom → Term' rep ran.app (add: Term (fn nat (fn nat nat))add rep: Ty → Typerep) (.const: {rep : Ty → Type} → Nat → Term' rep nat.const 1: Nat1)) (.const: {rep : Ty → Type} → Nat → Term' rep nat.const 2: Nat2)

end FirstTry```

The argument `rep` does not even appear in the function body for `add`. How can that be? By giving our terms expressive types, we allow Lean to infer many arguments for us. In fact, we do not even need to name the `rep` argument! By using Lean implicit arguments and lambdas, we can completely hide `rep` in these examples.

```def Term: Ty → Type 1Term (ty: Tyty : Ty: TypeTy) := {rep: Ty → Typerep : Ty: TypeTy → Type: Type 1Type} → Term': (Ty → Type) → Ty → TypeTerm' rep: Ty → Typerep ty: Tyty

def add: Term (fn nat (fn nat nat))add : Term: Ty → Type 1Term (fn: Ty → Ty → Tyfn nat: Tynat (fn: Ty → Ty → Tyfn nat: Tynat nat: Tynat)) :=
.lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (fn dom ran).lam fun x: rep✝ natx => .lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (fn dom ran).lam fun y: rep✝ naty => .plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat.plus (.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty.var x: rep✝ natx) (.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty.var y: rep✝ naty)

def three_the_hard_way: Term natthree_the_hard_way : Term: Ty → Type 1Term nat: Tynat :=
.app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (fn dom ran) → Term' rep dom → Term' rep ran.app (.app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (fn dom ran) → Term' rep dom → Term' rep ran.app add: Term (fn nat (fn nat nat))add (.const: {rep : Ty → Type} → Nat → Term' rep nat.const 1: Nat1)) (.const: {rep : Ty → Type} → Nat → Term' rep nat.const 2: Nat2)```

It may not be at all obvious that the PHOAS representation admits the crucial computable operations. The key to effective deconstruction of PHOAS terms is one principle: treat the `rep` parameter as an unconstrained choice of which data should be annotated on each variable. We will begin with a simple example, that of counting how many variable nodes appear in a PHOAS term. This operation requires no data annotated on variables, so we simply annotate variables with `Unit` values. Note that, when we go under binders in the cases for `lam` and `let`, we must provide the data value to annotate on the new variable we pass beneath. For our current choice of `Unit` data, we always pass `()`.

```def countVars: {ty : Ty} → Term' (fun x => Unit) ty → NatcountVars : Term': (Ty → Type) → Ty → TypeTerm' (fun _: Ty_ => Unit: TypeUnit) ty: Tyty → Nat: TypeNat
| .var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty.var _    => 1: Nat1
| .const: {rep : Ty → Type} → Nat → Term' rep nat.const _  => 0: Nat0
| .plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat.plus a: Term' (fun x => Unit) nata b: Term' (fun x => Unit) natb => countVars: {ty : Ty} → Term' (fun x => Unit) ty → NatcountVars a: Term' (fun x => Unit) nata + countVars: {ty : Ty} → Term' (fun x => Unit) ty → NatcountVars b: Term' (fun x => Unit) natb
| .app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (fn dom ran) → Term' rep dom → Term' rep ran.app f: Term' (fun x => Unit) (fn dom✝ ty)f a: Term' (fun x => Unit) dom✝a  => countVars: {ty : Ty} → Term' (fun x => Unit) ty → NatcountVars f: Term' (fun x => Unit) (fn dom✝ ty)f + countVars: {ty : Ty} → Term' (fun x => Unit) ty → NatcountVars a: Term' (fun x => Unit) dom✝a
| .lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (fn dom ran).lam b: Unit → Term' (fun x => Unit) ran✝b    => countVars: {ty : Ty} → Term' (fun x => Unit) ty → NatcountVars (b: Unit → Term' (fun x => Unit) ran✝b (): Unit())
| .let: {rep : Ty → Type} → {ty₁ ty₂ : Ty} → Term' rep ty₁ → (rep ty₁ → Term' rep ty₂) → Term' rep ty₂.let a: Term' (fun x => Unit) ty₁✝a b: Unit → Term' (fun x => Unit) tyb  => countVars: {ty : Ty} → Term' (fun x => Unit) ty → NatcountVars a: Term' (fun x => Unit) ty₁✝a + countVars: {ty : Ty} → Term' (fun x => Unit) ty → NatcountVars (b: Unit → Term' (fun x => Unit) tyb (): Unit())```

We can now easily prove that `add` has two variables by using reflexivity

```example: countVars add = 2example : countVars: {ty : Ty} → Term' (fun x => Unit) ty → NatcountVars add: Term (fn nat (fn nat nat))add = 2: Nat2 :=
rfl: ∀ {α : Type} {a : α}, a = arfl```

Here is another example, translating PHOAS terms into strings giving a first-order rendering. To implement this translation, the key insight is to tag variables with strings, giving their names. The function takes as an additional input `i` which is used to create variable names for binders. We also use the string interpolation available in Lean. For example, `s!"x_{i}"` is expanded to `"x_" ++ toString i`.

```def pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → Stringpretty (e: Term' (fun x => String) tye : Term': (Ty → Type) → Ty → TypeTerm' (fun _: Ty_ => String: TypeString) ty: Tyty) (i: optParam Nat 1i : Nat: TypeNat := 1: Nat1) : String: TypeString :=
match e: Term' (fun x => String) tye with
| .var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty.var s: Strings     => s: Strings
| .const: {rep : Ty → Type} → Nat → Term' rep nat.const n: Natn   => toString: {α : Type} → [self : ToString α] → α → StringtoString n: Natn
| .app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (fn dom ran) → Term' rep dom → Term' rep ran.app f: Term' (fun x => String) (fn dom✝ ty)f a: Term' (fun x => String) dom✝a   => s!"({pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → Stringpretty f: Term' (fun x => String) (fn dom✝ ty)f i: optParam Nat 1i} {pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → Stringpretty a: Term' (fun x => String) dom✝a i: optParam Nat 1i})"
| .plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat.plus a: Term' (fun x => String) nata b: Term' (fun x => String) natb  => s!"({pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → Stringpretty a: Term' (fun x => String) nata i: optParam Nat 1i} + {pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → Stringpretty b: Term' (fun x => String) natb i: optParam Nat 1i})"
| .lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (fn dom ran).lam f: String → Term' (fun x => String) ran✝f     =>
let x: Stringx := s!"x_{i: optParam Nat 1i}"
s!"(fun {x: Stringx} => {pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → Stringpretty (f: String → Term' (fun x => String) ran✝f x: Stringx) (i: optParam Nat 1i+1: Nat1)})"
| .let: {rep : Ty → Type} → {ty₁ ty₂ : Ty} → Term' rep ty₁ → (rep ty₁ → Term' rep ty₂) → Term' rep ty₂.let a: Term' (fun x => String) ty₁✝a b: String → Term' (fun x => String) tyb  =>
let x: Stringx := s!"x_{i: optParam Nat 1i}"
s!"(let {x: Stringx} := {pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → Stringpretty a: Term' (fun x => String) ty₁✝a i: optParam Nat 1i}; => {pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → Stringpretty (b: String → Term' (fun x => String) tyb x: Stringx) (i: optParam Nat 1i+1: Nat1)}"

#eval"(((fun x_1 => (fun x_2 => (x_1 + x_2))) 1) 2)"
pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → Stringpretty three_the_hard_way: Term natthree_the_hard_way```

It is not necessary to convert to a different representation to support many common operations on terms. For instance, we can implement substitution of terms for variables. The key insight here is to tag variables with terms, so that, on encountering a variable, we can simply replace it by the term in its tag. We will call this function initially on a term with exactly one free variable, tagged with the appropriate substitute. During recursion, new variables are added, but they are only tagged with their own term equivalents. Note that this function squash is parameterized over a specific `rep` choice.

```def squash: {rep : Ty → Type} → {ty : Ty} → Term' (Term' rep) ty → Term' rep tysquash : Term': (Ty → Type) → Ty → TypeTerm' (Term': (Ty → Type) → Ty → TypeTerm' rep: Ty → Typerep) ty: Tyty → Term': (Ty → Type) → Ty → TypeTerm' rep: Ty → Typerep ty: Tyty
| .var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty.var e: Term' rep tye    => e: Term' rep tye
| .const: {rep : Ty → Type} → Nat → Term' rep nat.const n: Natn  => .const: {rep : Ty → Type} → Nat → Term' rep nat.const n: Natn
| .plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat.plus a: Term' (Term' rep) nata b: Term' (Term' rep) natb => .plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat.plus (squash: {rep : Ty → Type} → {ty : Ty} → Term' (Term' rep) ty → Term' rep tysquash a: Term' (Term' rep) nata) (squash: {rep : Ty → Type} → {ty : Ty} → Term' (Term' rep) ty → Term' rep tysquash b: Term' (Term' rep) natb)
| .lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (fn dom ran).lam f: Term' rep dom✝ → Term' (Term' rep) ran✝f    => .lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (fn dom ran).lam fun x: rep dom✝x => squash: {rep : Ty → Type} → {ty : Ty} → Term' (Term' rep) ty → Term' rep tysquash (f: Term' rep dom✝ → Term' (Term' rep) ran✝f (.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty.var x: rep dom✝x))
| .app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (fn dom ran) → Term' rep dom → Term' rep ran.app f: Term' (Term' rep) (fn dom✝ ty)f a: Term' (Term' rep) dom✝a  => .app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (fn dom ran) → Term' rep dom → Term' rep ran.app (squash: {rep : Ty → Type} → {ty : Ty} → Term' (Term' rep) ty → Term' rep tysquash f: Term' (Term' rep) (fn dom✝ ty)f) (squash: {rep : Ty → Type} → {ty : Ty} → Term' (Term' rep) ty → Term' rep tysquash a: Term' (Term' rep) dom✝a)
| .let: {rep : Ty → Type} → {ty₁ ty₂ : Ty} → Term' rep ty₁ → (rep ty₁ → Term' rep ty₂) → Term' rep ty₂.let a: Term' (Term' rep) ty₁✝a b: Term' rep ty₁✝ → Term' (Term' rep) tyb  => .let: {rep : Ty → Type} → {ty₁ ty₂ : Ty} → Term' rep ty₁ → (rep ty₁ → Term' rep ty₂) → Term' rep ty₂.let (squash: {rep : Ty → Type} → {ty : Ty} → Term' (Term' rep) ty → Term' rep tysquash a: Term' (Term' rep) ty₁✝a) fun x: rep ty₁✝x => squash: {rep : Ty → Type} → {ty : Ty} → Term' (Term' rep) ty → Term' rep tysquash (b: Term' rep ty₁✝ → Term' (Term' rep) tyb (.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty.var x: rep ty₁✝x))```

To define the final substitution function over terms with single free variables, we define `Term1`, an analogue to Term that we defined before for closed terms.

`def Term1: Ty → Ty → Type 1Term1 (ty1: Tyty1 ty2: Tyty2 : Ty: TypeTy) := {rep: Ty → Typerep : Ty: TypeTy → Type: Type 1Type} → rep: Ty → Typerep ty1: Tyty1 → Term': (Ty → Type) → Ty → TypeTerm' rep: Ty → Typerep ty2: Tyty2`

Substitution is defined by (1) instantiating a `Term1` to tag variables with terms and (2) applying the result to a specific term to be substituted. Note how the parameter `rep` of `squash` is instantiated: the body of `subst` is itself a polymorphic quantification over `rep`, standing for a variable tag choice in the output term; and we use that input to compute a tag choice for the input term.

```def subst: {ty1 ty2 : Ty} → Term1 ty1 ty2 → Term ty1 → Term ty2subst (e: Term1 ty1 ty2e : Term1: Ty → Ty → Type 1Term1 ty1: Tyty1 ty2: Tyty2) (e': Term ty1e' : Term: Ty → Type 1Term ty1: Tyty1) : Term: Ty → Type 1Term ty2: Tyty2 :=
squash: {rep : Ty → Type} → {ty : Ty} → Term' (Term' rep) ty → Term' rep tysquash (e: Term1 ty1 ty2e e': Term ty1e')```

We can view `Term1` as a term with hole. In the following example, `(fun x => plus (var x) (const 5))` can be viewed as the term `plus _ (const 5)` where the hole `_` is instantiated by `subst` with `three_the_hard_way`

```#eval"((((fun x_1 => (fun x_2 => (x_1 + x_2))) 1) 2) + 5)"
pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → Stringpretty <| subst: {ty1 ty2 : Ty} → Term1 ty1 ty2 → Term ty1 → Term ty2subst (fun x: rep✝ natx => .plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat.plus (.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty.var x: rep✝ natx) (.const: {rep : Ty → Type} → Nat → Term' rep nat.const 5: Nat5)) three_the_hard_way: Term natthree_the_hard_way```

One further development, which may seem surprising at first, is that we can also implement a usual term denotation function, when we tag variables with their denotations.

The attribute `[simp]` instructs Lean to always try to unfold `denote` applications when one applies the `simp` tactic. We also say this is a hint for the Lean term simplifier.

```@[simp] def denote: {ty : Ty} → Term' Ty.denote ty → Ty.denote tydenote : Term': (Ty → Type) → Ty → TypeTerm' Ty.denote: Ty → TypeTy.denote ty: Tyty → ty: Tyty.denote: Ty → Typedenote
| .var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty.var x: Ty.denote tyx    => x: Ty.denote tyx
| .const: {rep : Ty → Type} → Nat → Term' rep nat.const n: Natn  => n: Natn
| .plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat.plus a: Term' Ty.denote nata b: Term' Ty.denote natb => denote: {ty : Ty} → Term' Ty.denote ty → Ty.denote tydenote a: Term' Ty.denote nata + denote: {ty : Ty} → Term' Ty.denote ty → Ty.denote tydenote b: Term' Ty.denote natb
| .app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (fn dom ran) → Term' rep dom → Term' rep ran.app f: Term' Ty.denote (fn dom✝ ty)f a: Term' Ty.denote dom✝a  => denote: {ty : Ty} → Term' Ty.denote ty → Ty.denote tydenote f: Term' Ty.denote (fn dom✝ ty)f (denote: {ty : Ty} → Term' Ty.denote ty → Ty.denote tydenote a: Term' Ty.denote dom✝a)
| .lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (fn dom ran).lam f: Ty.denote dom✝ → Term' Ty.denote ran✝f    => fun x: Ty.denote dom✝x => denote: {ty : Ty} → Term' Ty.denote ty → Ty.denote tydenote (f: Ty.denote dom✝ → Term' Ty.denote ran✝f x: Ty.denote dom✝x)
| .let: {rep : Ty → Type} → {ty₁ ty₂ : Ty} → Term' rep ty₁ → (rep ty₁ → Term' rep ty₂) → Term' rep ty₂.let a: Term' Ty.denote ty₁✝a b: Ty.denote ty₁✝ → Term' Ty.denote tyb  => denote: {ty : Ty} → Term' Ty.denote ty → Ty.denote tydenote (b: Ty.denote ty₁✝ → Term' Ty.denote tyb (denote: {ty : Ty} → Term' Ty.denote ty → Ty.denote tydenote a: Term' Ty.denote ty₁✝a))

example: denote three_the_hard_way = 3example : denote: {ty : Ty} → Term' Ty.denote ty → Ty.denote tydenote three_the_hard_way: Term natthree_the_hard_way = 3: Ty.denote nat3 :=
rfl: ∀ {α : Type} {a : α}, a = arfl```

To summarize, the PHOAS representation has all the expressive power of more standard encodings (e.g., using de Bruijn indices), and a variety of translations are actually much more pleasant to implement than usual, thanks to the novel ability to tag variables with data.

We now define the constant folding optimization that traverses a term if replaces subterms such as `plus (const m) (const n)` with `const (n+m)`.

```@[simp] def constFold: {rep : Ty → Type} → {ty : Ty} → Term' rep ty → Term' rep tyconstFold : Term': (Ty → Type) → Ty → TypeTerm' rep: Ty → Typerep ty: Tyty → Term': (Ty → Type) → Ty → TypeTerm' rep: Ty → Typerep ty: Tyty
| .var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty.var x: rep tyx    => .var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty.var x: rep tyx
| .const: {rep : Ty → Type} → Nat → Term' rep nat.const n: Natn  => .const: {rep : Ty → Type} → Nat → Term' rep nat.const n: Natn
| .app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (fn dom ran) → Term' rep dom → Term' rep ran.app f: Term' rep (fn dom✝ ty)f a: Term' rep dom✝a  => .app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (fn dom ran) → Term' rep dom → Term' rep ran.app (constFold: {rep : Ty → Type} → {ty : Ty} → Term' rep ty → Term' rep tyconstFold f: Term' rep (fn dom✝ ty)f) (constFold: {rep : Ty → Type} → {ty : Ty} → Term' rep ty → Term' rep tyconstFold a: Term' rep dom✝a)
| .lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (fn dom ran).lam f: rep dom✝ → Term' rep ran✝f    => .lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (fn dom ran).lam fun x: rep dom✝x => constFold: {rep : Ty → Type} → {ty : Ty} → Term' rep ty → Term' rep tyconstFold (f: rep dom✝ → Term' rep ran✝f x: rep dom✝x)
| .let: {rep : Ty → Type} → {ty₁ ty₂ : Ty} → Term' rep ty₁ → (rep ty₁ → Term' rep ty₂) → Term' rep ty₂.let a: Term' rep ty₁✝a b: rep ty₁✝ → Term' rep tyb  => .let: {rep : Ty → Type} → {ty₁ ty₂ : Ty} → Term' rep ty₁ → (rep ty₁ → Term' rep ty₂) → Term' rep ty₂.let (constFold: {rep : Ty → Type} → {ty : Ty} → Term' rep ty → Term' rep tyconstFold a: Term' rep ty₁✝a) fun x: rep ty₁✝x => constFold: {rep : Ty → Type} → {ty : Ty} → Term' rep ty → Term' rep tyconstFold (b: rep ty₁✝ → Term' rep tyb x: rep ty₁✝x)
| .plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat.plus a: Term' rep nata b: Term' rep natb =>
match constFold: {rep : Ty → Type} → {ty : Ty} → Term' rep ty → Term' rep tyconstFold a: Term' rep nata, constFold: {rep : Ty → Type} → {ty : Ty} → Term' rep ty → Term' rep tyconstFold b: Term' rep natb with
| .const: {rep : Ty → Type} → Nat → Term' rep nat.const n: Natn, .const: {rep : Ty → Type} → Nat → Term' rep nat.const m: Natm => .const: {rep : Ty → Type} → Nat → Term' rep nat.const (n: Natn+m: Natm)
| a': Term' rep nata',       b': Term' rep natb'       => .plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat.plus a': Term' rep nata' b': Term' rep natb'```

The correctness of the `constFold` is proved using induction, case-analysis, and the term simplifier. We prove all cases but the one for `plus` using `simp [*]`. This tactic instructs the term simplifier to use hypotheses such as `a = b` as rewriting/simplications rules. We use the `split` to break the nested `match` expression in the `plus` case into two cases. The local variables `iha` and `ihb` are the induction hypotheses for `a` and `b`. The modifier `←` in a term simplifier argument instructs the term simplier to use the equation as a rewriting rule in the "reverse direction. That is, given `h : a = b`, `← h` instructs the term simplifier to rewrite `b` subterms to `a`.

```theorem constFold_sound: ∀ {ty : Ty} (e : Term' Ty.denote ty), denote (constFold e) = denote econstFold_sound (e: Term' Ty.denote tye : Term': (Ty → Type) → Ty → TypeTerm' Ty.denote: Ty → TypeTy.denote ty: Tyty) : denote: {ty : Ty} → Term' Ty.denote ty → Ty.denote tydenote (constFold: {rep : Ty → Type} → {ty : Ty} → Term' rep ty → Term' rep tyconstFold e: Term' Ty.denote tye) = denote: {ty : Ty} → Term' Ty.denote ty → Ty.denote tydenote e: Term' Ty.denote tye := byGoals accomplished! 🐙
induction e: Term' Ty.denote tye withty: Tye: Term' Ty.denote tydenote (constFold e) = denote e simp [*]Goals accomplished! 🐙
| plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep natplus a: Term' Ty.denote nata b: Term' Ty.denote natb iha: denote (constFold a) = denote aiha ihb: denote (constFold b) = denote bihb =>ty: Tya, b: Term' Ty.denote natiha: denote (constFold a) = denote aihb: denote (constFold b) = denote bplusdenote
(match constFold a, constFold b with
| Term'.const n, Term'.const m => Term'.const (n + m)
| a', b' => Term'.plus a' b') =
denote a + denote b
splitty: Tya, b: Term' Ty.denote natiha: denote (constFold a) = denote aihb: denote (constFold b) = denote bx✝¹, x✝: Term' Ty.denote natn✝, m✝: Natheq✝¹: constFold a = Term'.const n✝heq✝: constFold b = Term'.const m✝plus.h_1denote (Term'.const (n✝ + m✝)) = denote a + denote bty: Tya, b: Term' Ty.denote natiha: denote (constFold a) = denote aihb: denote (constFold b) = denote bx✝², x✝¹: Term' Ty.denote natx✝: ∀ (n m : Nat), constFold a = Term'.const n → constFold b = Term'.const m → Falseplus.h_2denote (Term'.plus (constFold a) (constFold b)) = denote a + denote b
next he₁: constFold a = Term'.const n✝he₁ he₂: constFold b = Term'.const m✝he₂ =>ty: Tya, b: Term' Ty.denote natiha: denote (constFold a) = denote aihb: denote (constFold b) = denote bx✝¹, x✝: Term' Ty.denote natn✝, m✝: Natheq✝¹: constFold a = Term'.const n✝heq✝: constFold b = Term'.const m✝plus.h_1denote (Term'.const (n✝ + m✝)) = denote a + denote bty: Tya, b: Term' Ty.denote natiha: denote (constFold a) = denote aihb: denote (constFold b) = denote bx✝², x✝¹: Term' Ty.denote natx✝: ∀ (n m : Nat), constFold a = Term'.const n → constFold b = Term'.const m → Falseplus.h_2denote (Term'.plus (constFold a) (constFold b)) = denote a + denote b simp [← iha: denote (constFold a) = denote aiha, ← ihb: denote (constFold b) = denote bihb, he₁: constFold a = Term'.const n✝he₁, he₂: constFold b = Term'.const m✝he₂]Goals accomplished! 🐙
next =>ty: Tya, b: Term' Ty.denote natiha: denote (constFold a) = denote aihb: denote (constFold b) = denote bx✝², x✝¹: Term' Ty.denote natx✝: ∀ (n m : Nat), constFold a = Term'.const n → constFold b = Term'.const m → Falseplus.h_2denote (Term'.plus (constFold a) (constFold b)) = denote a + denote b simp [iha: denote (constFold a) = denote aiha, ihb: denote (constFold b) = denote bihb]Goals accomplished! 🐙```