-- FPCourse/Unit2/Week04_AlgebraicDatatypes.lean
import Mathlib.Data.Option.Basic
import Mathlib.Logic.Basic

Week 4: Algebraic Datatypes

Sum types and product types

Lean's inductive keyword lets us define new types by listing their constructors. The resulting type is either a sum (one of several alternatives) or a product (bundling several fields) — or both.

These are called algebraic datatypes because they obey the same algebraic laws as sums and products of numbers: a type with n values of type A and m values of type B as alternatives has n + m values.

namespace Week04

4.1 Enumeration types (pure sums)

inductive Direction where
  | North | South | East | West
deriving Repr, DecidableEq

#eval Direction.North      -- Direction.North
example : Direction.North ≠ Direction.South := by decide

4.2 Record types (pure products)

structure Point where
  x : Float
  y : Float
deriving Repr

def origin : Point := { x := 0.0, y := 0.0 }

4.3 Option: the prototypical proof-carrying type

Option α is either none (no value) or some a (a value a : α). It is Lean's answer to null.

But notice: Option.get does not simply hope the value is present. Its type requires a proof:

def Option.get : (o : Option α) → o.isSome = true → α

The caller must supply evidence before the function will run. This is the proof-carrying pattern from Week 1, now applied to a realistic data type.

-- Option.get requires a proof.
def safeHead (xs : List α) (h : xs ≠ []) : α :=
  xs.head h

-- For concrete lists, `decide` produces the proof.
#eval safeHead [1, 2, 3] (by decide)    -- 1

-- Option.map: lift a function into an optional context
-- Specification: ∀ f o, (Option.map f o).isSome = o.isSome
theorem option_map_isSome (f : α → β) :
    ∀ o : Option α, (Option.map f o).isSome = o.isSome :=
  fun o => Option.recOn o rfl (fun _ => rfl)

4.4 ∀ and ∃ in datatype specifications

When we define a new type, its specifications typically quantify over all values of that type. Here is the vocabulary:

-- ∀ example: a property of all options
theorem none_map_always_none (f : α → β) :
    Option.map f none = none :=
  rfl

-- ∃ example: witness a specific value satisfying a property
example : ∃ n : Nat, n > 100 := ⟨101, by decide⟩

private def factorial' : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * factorial' n

example : ∃ n : Nat, factorial' n > 1000 :=
  ⟨7, by decide⟩

4.5 Recursive types: expressions

A recursive inductive type refers to itself in its constructor arguments. This is how we build trees, lists, and other inductively structured data.

inductive Expr where
  | num  : Int → Expr
  | add  : Expr → Expr → Expr
  | mul  : Expr → Expr → Expr
  | neg  : Expr → Expr
deriving Repr

-- Evaluation by structural recursion on Expr.
-- The function is named `eval` deliberately: it IS evaluation —
-- the process of reducing an expression tree to its integer value.
def Expr.eval : Expr → Int
  | .num n    => n
  | .add e₁ e₂ => e₁.eval + e₂.eval
  | .mul e₁ e₂ => e₁.eval * e₂.eval
  | .neg e    => -e.eval

-- Evaluation trace: Expr.eval (.add (.num 3) (.mul (.num 4) (.num 5)))
--   ↝ (.num 3).eval + (.mul (.num 4) (.num 5)).eval    -- add clause
--   ↝ 3 + (.mul (.num 4) (.num 5)).eval                -- num clause
--   ↝ 3 + ((.num 4).eval * (.num 5).eval)              -- mul clause
--   ↝ 3 + (4 * 5)                                      -- num clause ×2
--   ↝ 3 + 20 ↝ 23                                      -- arithmetic
#eval Expr.eval (.add (.num 3) (.mul (.num 4) (.num 5)))  -- 23

-- Specification: eval distributes over add.
-- Evaluation: (.add e₁ e₂).eval ↝ e₁.eval + e₂.eval by the add clause.
-- Both sides are definitionally equal, so rfl applies.
theorem eval_add (e₁ e₂ : Expr) :
    (Expr.add e₁ e₂).eval = e₁.eval + e₂.eval :=
  rfl

4.6 The template principle

Every inductive type T has a corresponding elimination principle: to define a function from T, provide one clause per constructor. The types of the clauses are determined by the constructor signatures.

For Expr:

• A clause for num n — has access to n : Int
• A clause for add e₁ e₂ — has access to both subexpressions and their recursively computed results
• A clause for mul e₁ e₂ — same
• A clause for neg e — access to e and its result

This is the template principle: the type tells you the shape of the function.

Exercises

1. Define an inductive type Shape with constructors for Circle (radius : Float), Rectangle (width height : Float), and Triangle (base height : Float).

2. Define a function area : Shape → Float.

3. State (as a Prop) the specification: "the area of any circle with radius r equals π * r * r." You may use Float.pi from Lean. (We will not prove this — Float lacks decidable equality. But we can state it.)

4. Add a sub : Expr → Expr → Expr constructor and extend eval. State its specification as a ∀ proposition.

5. Use ∃ to state: "there exists an Expr that evaluates to 42." Prove it by providing a witness.

end Week04