From 4464a70a72eab8ebb7246ef1d64b9b425db08adf Mon Sep 17 00:00:00 2001 From: Alexander Ikonomou Date: Sun, 28 Sep 2025 09:58:46 +0200 Subject: [PATCH 1/5] Try out stuff for a circuit implementation --- AlgebraicComplexity/Circuit.lean | 105 +++++++++++++++++++++++++++++++ AlgebraicComplexity/Example.lean | 6 +- 2 files changed, 108 insertions(+), 3 deletions(-) create mode 100644 AlgebraicComplexity/Circuit.lean diff --git a/AlgebraicComplexity/Circuit.lean b/AlgebraicComplexity/Circuit.lean new file mode 100644 index 0000000..0f59832 --- /dev/null +++ b/AlgebraicComplexity/Circuit.lean @@ -0,0 +1,105 @@ +import Mathlib +import Std.Data.HashMap + +set_option linter.unusedTactic false + +-- x +-- + * +-- x1 x2 1 + +-- inductive Operation where +-- | Sum +-- | Prod +-- | None +-- +-- inductive MetaVar (n : ℕ) where +-- | Elem (e: ℝ) +-- | Var (x: Fin n) +-- +-- abbrev Context (n : ℕ) := Std.HashMap (Fin n) (MetaVar n) +-- +-- structure Circuit (n : ℕ) (C : Context n) where +-- identifier : Fin n +-- operation : Operation +-- operands : List (Fin n) +-- +-- def x1 : MetaVar 3 := MetaVar.Var (1) +-- def x2 : MetaVar 3 := MetaVar.Var (2) +-- def one : MetaVar 3 := MetaVar.Elem (1) +-- +-- def context : Context 3 := Std.HashMap.empty +-- |>.insert 1 x1 +-- |>.insert 2 x2 +-- |>.insert 3 one +-- +-- def x1_plus_x2 : Circuit 3 context := { +-- identifier := 4, +-- operation := Operation.Sum, +-- operands := [1, 2] +-- } +-- +-- def x2_plus_1 : Circuit 3 context := { +-- identifier := 5, +-- operation := Operation.Sum, +-- operands := [2, 3] +-- } +-- +-- def circuit : Circuit 3 context := { +-- identifier := 6, +-- operation := Operation.Prod, +-- operands := [2, 4, 5] +-- } +-- +-- @[simp] +-- noncomputable def evalCircuit (n : ℕ) +-- (Γ : Context n) +-- (c : Circuit n Γ) +-- : (MvPolynomial (Fin n) ℝ) := +-- 1 + +-- inductive Formula (α : Type u) (n : ℕ) where +-- | Var (x: Fin n) +-- | Add (g h: Formula α n): Formula α n +-- | Mult (g h: Formula α n): Formula α n +-- | Neg (g : Formula α n): Formula α n +-- | Const (c : α): Formula α n + +inductive MetaVar (n : ℕ) where + | Var (x: Fin n) + +-- (Γ : List (Sigma (ℕ -> (MetaVar n)))) + +inductive Gate (α : Type) where + | pair : α -> α -> Gate α + | cons : α -> Gate α -> Gate α + + +def g1 : Gate ℕ := .pair 1 2 +def g2 : Gate ℕ := .pair 1 2 + +inductive Circuit (n : ℕ) where + -- We want to keep our input variables separate for now. + | Var (x : Fin n) + | MetaVar (x : ℕ) + | Sum (c d : Circuit n) + | Prod (c d : Circuit n) + | Const (c : ℝ) + | Neg (g : Circuit n) + +def size (c: Circuit n) : ℕ := + match c with + | .Var _ => 0 + | .MetaVar _ => 0 + | .Sum c d => size c + size d + 1 + | .Prod c d => size c + size d + 1 + | .Const _ => 0 + | .Neg d => size d + 1 + +def depth (c: Circuit n) : ℕ := + match c with + | .Var _ => 0 + | .MetaVar _ => 0 + | .Sum c d => max (depth c) (depth d) + 1 + | .Prod c d => max (depth c) (depth d) + 1 + | .Const _ => 0 + | .Neg d => depth d + 1 diff --git a/AlgebraicComplexity/Example.lean b/AlgebraicComplexity/Example.lean index 863c0ec..8ce5b73 100644 --- a/AlgebraicComplexity/Example.lean +++ b/AlgebraicComplexity/Example.lean @@ -36,11 +36,11 @@ example : @depth ℝ 3 (C[-3.4] * (C[0] + V[2]) + (V[1] + C[1])) = 3 := by rfl example : @depth ℤ 3 (-C[3] * (V[1] + V[2])) = 2 := by rfl example : @evalToPolynomial ℝ 1 _ (C[1]) = 1 := by rfl -example : @evalToPolynomial Real 1 _ V[0] = X 1 := by rfl +example : @evalToPolynomial Real 1 _ V[0] = X 1 := by simp[evalToPolynomial] example : @evalToPolynomial ℤ 2 _ (-C[1]) = -1 := by rfl -example : @evalToPolynomial ℚ 2 _ (V[1] + C[1]) = X 1 + 1 := by rfl +example : @evalToPolynomial ℚ 2 _ (V[1] + C[1]) = X 1 + 1 := by simp[evalToPolynomial] example : @evalToPolynomial ℚ 2 _ (C[1] + C[0]) = 1 + 0 := by simp[evalToPolynomial] example : @evalToPolynomial ℝ 3 _ (C[-3] * (C[0] + V[2]) + V[1] + C[1]) = (C (-3)) * (0 + (X 2)) + (X 1) + 1 := by simp example : @evalToPolynomial ℚ 3 _ (C[-3] * (C[0] + V[2]) + (V[1] + C[1])) = (C (-3)) * (0 + (X 2)) + ((X 1) + 1) := by simp -example : @evalToPolynomial ℤ 3 _ (-C[3] * (V[1] + V[2])) = -3 * (X 1 + X 2) := by rfl +example : @evalToPolynomial ℤ 3 _ (-C[3] * (V[1] + V[2])) = -3 * (X 1 + X 2) := by simp[evalToPolynomial] From c99dabe7bf8f479d106dc9f95d8c7aaa70eca6bd Mon Sep 17 00:00:00 2001 From: Alexander Ikonomou Date: Sun, 28 Sep 2025 12:00:20 +0200 Subject: [PATCH 2/5] Add syntactic sugar --- AlgebraicComplexity/Circuit.lean | 36 +++++++++++++++++++++++++------- AlgebraicComplexity/Example.lean | 9 ++++++++ 2 files changed, 37 insertions(+), 8 deletions(-) diff --git a/AlgebraicComplexity/Circuit.lean b/AlgebraicComplexity/Circuit.lean index 0f59832..9eb8703 100644 --- a/AlgebraicComplexity/Circuit.lean +++ b/AlgebraicComplexity/Circuit.lean @@ -86,20 +86,40 @@ inductive Circuit (n : ℕ) where | Const (c : ℝ) | Neg (g : Circuit n) -def size (c: Circuit n) : ℕ := +def size' (c: Circuit n) : ℕ := match c with | .Var _ => 0 | .MetaVar _ => 0 - | .Sum c d => size c + size d + 1 - | .Prod c d => size c + size d + 1 + | .Sum c d => size' c + size' d + 1 + | .Prod c d => size' c + size' d + 1 | .Const _ => 0 - | .Neg d => size d + 1 + | .Neg d => size' d + 1 -def depth (c: Circuit n) : ℕ := +def depth' (c: Circuit n) : ℕ := match c with | .Var _ => 0 | .MetaVar _ => 0 - | .Sum c d => max (depth c) (depth d) + 1 - | .Prod c d => max (depth c) (depth d) + 1 + | .Sum c d => max (depth' c) (depth' d) + 1 + | .Prod c d => max (depth' c) (depth' d) + 1 | .Const _ => 0 - | .Neg d => depth d + 1 + | .Neg d => depth' d + 1 + +notation "Const[" val "]" => Circuit.Const val +notation "Var[" name "]" => Circuit.Var ⟨name, by decide⟩ +instance zero': Zero (Circuit n) where + zero := .Const 0 + +instance one': One (Circuit n) where + one := .Const 1 + +instance add': Add (Circuit n) where + add := .Sum + +instance neg': Neg (Circuit n) where + neg := .Neg + +instance sub': Sub (Circuit n) where + sub a b := a + (- b) + +instance mul'': Mul (Circuit n) where + mul := .Prod diff --git a/AlgebraicComplexity/Example.lean b/AlgebraicComplexity/Example.lean index 8ce5b73..bd800de 100644 --- a/AlgebraicComplexity/Example.lean +++ b/AlgebraicComplexity/Example.lean @@ -1,4 +1,5 @@ import AlgebraicComplexity.Formulas +import AlgebraicComplexity.Circuit import Mathlib open MvPolynomial @@ -44,3 +45,11 @@ example : @evalToPolynomial ℝ 3 _ (C[-3] * (C[0] + V[2]) + V[1] + C[1]) = (C (-3)) * (0 + (X 2)) + (X 1) + 1 := by simp example : @evalToPolynomial ℚ 3 _ (C[-3] * (C[0] + V[2]) + (V[1] + C[1])) = (C (-3)) * (0 + (X 2)) + ((X 1) + 1) := by simp example : @evalToPolynomial ℤ 3 _ (-C[3] * (V[1] + V[2])) = -3 * (X 1 + X 2) := by simp[evalToPolynomial] + +def circuit1 : Circuit 3 := Const[0] +def circuit2 : Circuit 0 := Const[1] +def circuit3 : Circuit 1 := Var[0] +def circuit4 : Circuit 1 := Const[1] + Const[1] * Var[0] +def circuit5 : Circuit 5 := -Const[1] +def circuit6 : Circuit 21 := -Const[1] * Var[4] + Var[20] + Var[0] +def circuit7 : Circuit 7 := -Const[1] * Const[3] + Const[5] From 9ef2e2b8c418d6da725a64fdf8eb0b4fdbf4e35a Mon Sep 17 00:00:00 2001 From: Alexander Ikonomou Date: Wed, 15 Oct 2025 09:26:23 +0200 Subject: [PATCH 3/5] evalToPolynomial' without context --- AlgebraicComplexity/Circuit.lean | 13 +++++++++++++ AlgebraicComplexity/Example.lean | 28 ++++++++++++++++++++++++++++ 2 files changed, 41 insertions(+) diff --git a/AlgebraicComplexity/Circuit.lean b/AlgebraicComplexity/Circuit.lean index 9eb8703..8d1a78d 100644 --- a/AlgebraicComplexity/Circuit.lean +++ b/AlgebraicComplexity/Circuit.lean @@ -1,8 +1,11 @@ import Mathlib import Std.Data.HashMap +import Lean set_option linter.unusedTactic false +open MvPolynomial + -- x -- + * -- x1 x2 1 @@ -123,3 +126,13 @@ instance sub': Sub (Circuit n) where instance mul'': Mul (Circuit n) where mul := .Prod + +@[simp] +noncomputable def evalToPolynomial' (circ: Circuit n) (context: Lean.AssocList ℕ (Circuit n)) : (MvPolynomial (Fin n) ℝ) := + match circ with + | .Var x => X x ^ 1 + | .MetaVar _ => 0 + | .Sum g h => evalToPolynomial' g context + evalToPolynomial' h context + | .Prod g h => evalToPolynomial' g context * evalToPolynomial' h context + | .Neg g => - evalToPolynomial' g context + | .Const c => MvPolynomial.C c diff --git a/AlgebraicComplexity/Example.lean b/AlgebraicComplexity/Example.lean index bd800de..46e1a7f 100644 --- a/AlgebraicComplexity/Example.lean +++ b/AlgebraicComplexity/Example.lean @@ -53,3 +53,31 @@ def circuit4 : Circuit 1 := Const[1] + Const[1] * Var[0] def circuit5 : Circuit 5 := -Const[1] def circuit6 : Circuit 21 := -Const[1] * Var[4] + Var[20] + Var[0] def circuit7 : Circuit 7 := -Const[1] * Const[3] + Const[5] + +example : @size' 1 Const[1] = 0 := by rfl +example : @size' 1 Var[0] = 0 := by rfl +example : @size' 2 (-Const[1]) = 1 := by rfl +example : @size' 2 (Var[0] + Const[1]) = 1 := by rfl +example : @size' 2 (Const[1] + Const[0]) = 1 := by rfl +example : @size' 3 (Const[-3.4] * (Const[0] + Var[2]) + Var[1] + Const[1]) = 4 := by rfl +example : @size' 3 (Const[-3.4] * (Const[0] + Var[2]) + (Var[1] + Const[1])) = 4 := by rfl +example : @size' 3 (-Const[3] * (Var[1] + Var[2])) = 3 := by rfl + +example : @depth' 1 Const[1] = 0 := by rfl +example : @depth' 1 Var[0] = 0 := by rfl +example : @depth' 2 (-Const[1]) = 1 := by rfl +example : @depth' 2 (Var[1] + Const[1]) = 1 := by rfl +example : @depth' 2 (Const[1] + Const[0]) = 1 := by rfl +example : @depth' 3 (Const[-3.4] * (Const[0] + Var[2]) + Var[1] + Const[1]) = 4 := by rfl +example : @depth' 3 (Const[-3.4] * (Const[0] + Var[2]) + (Var[1] + Const[1])) = 3 := by rfl +example : @depth' 3 (-Const[3] * (Var[1] + Var[2])) = 2 := by rfl + +example : @evalToPolynomial' 1 Const[1] Lean.AssocList.empty = 1 := by rfl +example : @evalToPolynomial' 1 Var[0] Lean.AssocList.empty = X 1 := by simp[evalToPolynomial'] +example : @evalToPolynomial' 3 (-Const[3] * (Var[1] + Var[2])) Lean.AssocList.empty = -3 * (X 1 + X 2) := by + simp[evalToPolynomial'] + . constructor + . rfl +example : @evalToPolynomial' 3 (-Var[1] * (Const[-4] + Var[2])) Lean.AssocList.empty = -X 1 * (-4 + X 2) := by + simp[evalToPolynomial'] + . constructor From 9af200c92027ce0c3e00c51540c88ce3f354de0e Mon Sep 17 00:00:00 2001 From: Alexander Ikonomou Date: Thu, 16 Oct 2025 09:53:29 +0200 Subject: [PATCH 4/5] Try to fix errors --- AlgebraicComplexity/Circuit.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/AlgebraicComplexity/Circuit.lean b/AlgebraicComplexity/Circuit.lean index 8d1a78d..33e1974 100644 --- a/AlgebraicComplexity/Circuit.lean +++ b/AlgebraicComplexity/Circuit.lean @@ -5,6 +5,7 @@ import Lean set_option linter.unusedTactic false open MvPolynomial +open Lean -- x -- + * @@ -128,11 +129,13 @@ instance mul'': Mul (Circuit n) where mul := .Prod @[simp] -noncomputable def evalToPolynomial' (circ: Circuit n) (context: Lean.AssocList ℕ (Circuit n)) : (MvPolynomial (Fin n) ℝ) := +noncomputable def evalToPolynomial' (circ: Circuit n) (context: AssocList ℕ (Circuit n)) : (MvPolynomial (Fin n) ℝ) := match circ with | .Var x => X x ^ 1 - | .MetaVar _ => 0 + | .MetaVar x => match (AssocList.find? x context) with + | some p => evalToPolynomial' p context + | none => 0 | .Sum g h => evalToPolynomial' g context + evalToPolynomial' h context | .Prod g h => evalToPolynomial' g context * evalToPolynomial' h context | .Neg g => - evalToPolynomial' g context - | .Const c => MvPolynomial.C c + | .Const c => C c From 05082215a57cdc22f304057010a433ea6e1f34ab Mon Sep 17 00:00:00 2001 From: Alexander Ikonomou Date: Thu, 16 Oct 2025 09:54:32 +0200 Subject: [PATCH 5/5] Copy PHOAS file for circuits --- AlgebraicComplexity/Circuit_PHOAS.lean | 286 +++++++++++++++++++++++++ 1 file changed, 286 insertions(+) create mode 100644 AlgebraicComplexity/Circuit_PHOAS.lean diff --git a/AlgebraicComplexity/Circuit_PHOAS.lean b/AlgebraicComplexity/Circuit_PHOAS.lean new file mode 100644 index 0000000..7fb7a3d --- /dev/null +++ b/AlgebraicComplexity/Circuit_PHOAS.lean @@ -0,0 +1,286 @@ +/-! +# 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](http://adam.chlipala.net/cpdt/) 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 where + | nat + | fn : Ty → Ty → Ty + +/-! +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 → Type + | nat => Nat + | fn a b => a.denote → b.denote + +/-! +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' (rep : Ty → Type) : Ty → Type + | var : rep ty → Term' rep ty + | const : Nat → Term' rep .nat + | plus : Term' rep .nat → Term' rep .nat → Term' rep .nat + | lam : (rep dom → Term' rep ran) → Term' rep (.fn dom ran) + | app : Term' rep (.fn dom ran) → Term' rep dom → Term' rep ran + | let : Term' rep ty₁ → (rep ty₁ → Term' rep ty₂) → Term' rep ty₂ + +/-! +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 : Ty) := (rep : Ty → Type) → Term' rep ty + +/-! +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)) := fun _rep => + .lam fun x => .lam fun y => .plus (.var x) (.var y) + +def three_the_hard_way : Term nat := fun rep => + .app (.app (add rep) (.const 1)) (.const 2) + +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 : Ty) := {rep : Ty → Type} → Term' rep ty + +def add : Term (fn nat (fn nat nat)) := + .lam fun x => .lam fun y => .plus (.var x) (.var y) + +def three_the_hard_way : Term nat := + .app (.app add (.const 1)) (.const 2) + +/-! +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 : Term' (fun _ => Unit) ty → Nat + | .var _ => 1 + | .const _ => 0 + | .plus a b => countVars a + countVars b + | .app f a => countVars f + countVars a + | .lam b => countVars (b ()) + | .let a b => countVars a + countVars (b ()) + +/-! We can now easily prove that `add` has two variables by +using reflexivity -/ + +example : countVars add = 2 := + rfl + +/-! +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 (e : Term' (fun _ => String) ty) (i : Nat := 1) : String := + match e with + | .var s => s + | .const n => toString n + | .app f a => s!"({pretty f i} {pretty a i})" + | .plus a b => s!"({pretty a i} + {pretty b i})" + | .lam f => + let x := s!"x_{i}" + s!"(fun {x} => {pretty (f x) (i+1)})" + | .let a b => + let x := s!"x_{i}" + s!"(let {x} := {pretty a i}; => {pretty (b x) (i+1)}" + +#eval pretty three_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 : Term' (Term' rep) ty → Term' rep ty + | .var e => e + | .const n => .const n + | .plus a b => .plus (squash a) (squash b) + | .lam f => .lam fun x => squash (f (.var x)) + | .app f a => .app (squash f) (squash a) + | .let a b => .let (squash a) fun x => squash (b (.var 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 (ty1 ty2 : Ty) := {rep : Ty → Type} → rep ty1 → Term' rep ty2 + +/-! +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 (e : Term1 ty1 ty2) (e' : Term ty1) : Term ty2 := + squash (e e') + +/-! +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 pretty <| subst (fun x => .plus (.var x) (.const 5)) three_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 : Term' Ty.denote ty → ty.denote + | .var x => x + | .const n => n + | .plus a b => denote a + denote b + | .app f a => denote f (denote a) + | .lam f => fun x => denote (f x) + | .let a b => denote (b (denote a)) + +example : denote three_the_hard_way = 3 := + rfl + +/-! +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 : Term' rep ty → Term' rep ty + | .var x => .var x + | .const n => .const n + | .app f a => .app (constFold f) (constFold a) + | .lam f => .lam fun x => constFold (f x) + | .let a b => .let (constFold a) fun x => constFold (b x) + | .plus a b => + match constFold a, constFold b with + | .const n, .const m => .const (n+m) + | a', b' => .plus a' b' + +/-! +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 simplifier +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 (e : Term' Ty.denote ty) : denote (constFold e) = denote e := by + induction e with simp [*] + | plus a b iha ihb => + split + next he₁ he₂ => simp [← iha, ← ihb, he₁, he₂] + next => simp [iha, ihb]