expressions.lean

-- An exercise from _Theorem Proving In Lean_.
-- https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#exercises

namespace expressions
  -- 6. Consider the following type of arithmetic expressions. The idea is that
  --    `var n` is a variable, v_n, and `const n` is the constant whose value
  --    is n.
  inductive aexpr : Type
  | const : ℕ → aexpr
  | var : ℕ → aexpr
  | plus : aexpr → aexpr → aexpr
  | times : aexpr → aexpr → aexpr

  open aexpr

  namespace aexpr
    -- Write a function that evaluates such an expression, evaluating each `var
    -- n` to `v n`.
    def aeval (env : ℕ → ℕ) : aexpr → ℕ
    | (const n) := n
    | (var k) := env k
    | (plus a b) := aeval a + aeval b
    | (times a b) := aeval a * aeval b

    -- Implement “constant fusion,” a procedure that simplifies subterms like
    -- 5 + 7 to 12.
    def simp_const : aexpr → aexpr
    | (plus (const n₁) (const n₂))  := const (n₁ + n₂)
    | (times (const n₁) (const n₂)) := const (n₁ * n₂)
    | e                             := e

    -- Using the auxiliary function simp_const, define a function
    -- “fuse”: to simplify a plus or a times, first simplify the arguments
    -- recursively, and then apply simp_const to try to simplify the result.
    def fuse : aexpr → aexpr
    | (plus a b)  := simp_const (plus (simp_const a) (simp_const b))
    | (times a b) := simp_const (times (simp_const a) (simp_const b))
    | e           := e

    -- simp_const does not affect the meaning of an expression!
    theorem simp_const_eq (v : ℕ → ℕ) :
      ∀ e : aexpr, aeval v (simp_const e) = aeval v e
    := begin
      intro e, cases e,
      case plus : a b {
        cases a,
        case const : av {
          cases b,
          all_goals { refl }
        },
        all_goals { refl }
      },
      case times : a b {
        cases a,
        case const : av {
          cases b,
          all_goals { refl }
        },
        all_goals { refl }
      },
      all_goals { refl }
    end

    -- fuse does not affect the meaning of an expression!
    theorem fuse_eq (v : ℕ → ℕ) :
      ∀ e : aexpr, aeval v (fuse e) = aeval v e
    := begin
      intro e, cases e,
      case const : v { refl },
      case var : v { refl },
      case plus : a b {
        exact calc
          aeval v (fuse (plus a b)) = aeval v (simp_const (plus (simp_const a) (simp_const b))) : by refl
          ... = aeval v (plus (simp_const a) (simp_const b)) : by rw simp_const_eq
          ... = aeval v (simp_const a) + aeval v (simp_const b) : by refl
          ... = aeval v a + aeval v b : by rw [simp_const_eq, simp_const_eq]
          ... = aeval v (plus a b) : by refl
      },
      case times : a b {
        exact calc
          aeval v (fuse (times a b)) = aeval v (simp_const (times (simp_const a) (simp_const b))) : by refl
          ... = aeval v (times (simp_const a) (simp_const b)) : by rw simp_const_eq
          ... = aeval v (simp_const a) * aeval v (simp_const b) : by refl
          ... = aeval v a * aeval v b : by rw [simp_const_eq, simp_const_eq]
          ... = aeval v (times a b) : by refl
      }
    end
  end aexpr
end expressions

Your fuse definition would not recursively simplify into all terms. For example:
#reduce fuse $ plus (plus (plus (const 1) (const 7)) (const 2)) (times (const 3) (const 4))
should be
const 22
while your definition gives
plus (plus (plus (const 1) (const 7)) (const 2)) (const 12)