simplifying proofs with inductive case analysis

Stream: new members

[Nada Amin]

I am wondering how I can simplify a proof in Lean. I got it down to the following: https://github.com/HarvardPL/cs152-lecture-code/blob/main/code01.lean, but the proof of the theorem still feels tedious, while the Dafny version has an automated (trivial & empty!) proof: https://github.com/HarvardPL/cs152-lecture-code/blob/main/code01.dfy

What are the principles/tricks to simplify such proofs in Lean?

[Nada Amin]

Nada Amin said:

I am wondering how I can simplify a proof in Lean. I got it down to the following: https://github.com/HarvardPL/cs152-lecture-code/blob/main/code01.lean, but the proof of the theorem still feels tedious, while the Dafny version has an automated (trivial & empty!) proof: https://github.com/HarvardPL/cs152-lecture-code/blob/main/code01.dfy

What are the principles/tricks to simplify such proofs in Lean?

[Nada Amin]

I forwarded the conversation to new members. Sorry for the noise.

[Nada Amin]

Correction: the dafny proof that the optimizer preserves the semantic is not entirely automatic, it has the inductive sketch, but that's all. The proof of optimality of the optimizer is automatic though, but I didn't do that in Lean yet, because I'd first like to understand how to automate proofs better. Thanks!

[Notification Bot]

2 messages were moved here from #lean4 > simplifying proofs with inductive case analysis by Eric Wieser.

[Arthur Adjedj]

This looks like the sort of proofs that grind should (hopefully) be able to produce automatically in a short future. I had a go at trying to solve it using the tactic, but it still failed on some branches. I'm guessing some lemmas (e.g Int.zero_mul) still need to get tagged with the right attributes in Core for the tactic to work seemlessly on such examples. In any case, here is a shorter proof relying on grind:

set_option grind.warning false
-- Theorem: optimizer preserves semantics
theorem optimize_preserves_semantics (e : Expr) (env : Env) :
  evaluate (optimize e) env = evaluate e env := by
  induction e <;> simp [optimize, evaluate]
  · grind [evaluate,optimize]
  · split
    · rename_i ih₁ ih₂ _ _ eq
      rw [←ih₁,eq]
      simp only [evaluate, Int.zero_mul]
    · rename_i ih₁ ih₂ _ _ eq _
      rw [←ih₁,←ih₂,eq]
      simp only [evaluate, Int.mul_zero]
    · rename_i ih₁ ih₂ _ _ eq _
      rw [←ih₁,←ih₂,eq]
      simp only [evaluate, Int.one_mul]
    · rename_i ih₁ ih₂ _ _ eq _ _
      rw [←ih₁,←ih₂,eq]
      simp only [evaluate, Int.mul_one]
    · grind [evaluate,optimize]

[Nada Amin]

Thanks, this looks like a great start. I'll be sure to look into grind.

[Nada Amin]

Thanks again for showing me grind! I played with it, and the code below works for all the cases but multiplication. What does multiplication require? Do we have to explicitly use the lemmas Int.one_mul and Int.mul_one?

theorem optimize_preserves_semantics (e : Expr) (env : Env) :
  evaluate (optimize e) env = evaluate e env := by
  induction e <;> simp [optimize, evaluate]
  · grind (config := { trace := true, ring := true, ringSteps := 10, splits := 15, ematch := 15, gen := 15, splitMatch := true }) [evaluate, optimize]
  <;> simp_all [evaluate, optimize]

Thanks, again!

[Kevin Buzzard]

(grind is still a WIP tactic, it hasn't even been announced as ready yet)

[Nada Amin]

Ah, ok. Do you recommend I look into other tactics or patterns for tedious case analysis? Thanks!

[Kevin Buzzard]

I don't know anything about how to do case analyses like this, I just thought it was worth clarifying that grind currently has no documentation, is unfinished, and is being actively worked on right now (you can see many Lean 4 PRs recently about this tactic), just so you were clear on its current status.

[Nada Amin]

OK, cool, thanks. It sounds fun to dig more deeply into its internals.

[Nada Amin]

Oh, OK. I was using grind on just the remaining add case, instead of all the remaining cases by using · instead of <;>.

Here is a working proof:

theorem optimize_preserves_semantics (e : Expr) (env : Env) :
  evaluate (optimize e) env = evaluate e env := by
  induction e <;> simp [optimize, evaluate]
  <;> grind (config := {  ring := true }) [evaluate, optimize]

[Nada Amin]

I updated the dev from above with the automatic proof. Unfortunately, I can't figure out grind for the next proof, which is slightly less trivial (optimize_optimal). Will continue...

[Nada Amin]

I did a case by case proof of the second lemma:

theorem optimize_optimal (e : Expr) :
  optimal (optimize e) := by
  induction e
  case const n =>
    simp [optimize, optimal]
  case var x =>
    simp [optimize, optimal]
  case add e₁ e₂ h₁ h₂ =>
    simp [optimal, optimize]
    split <;> intros
    · simp [optimal]
    · rw [h₂]
    · rw [h₁]
    · simp [optimal, optimize]
      rw [h₁, h₂]
      apply And.intro
        rfl
        rfl
  case mul e₁ e₂ h₁ h₂ =>
    simp [optimal, optimize]
    split <;> intros
    · simp [optimal]
    · simp [optimal]
    · simp [optimal]
    · rw [h₂]
    · rw [h₁]
    · simp [optimal, optimize]
      rw [h₁, h₂]
      apply And.intro
        rfl
        rfl

Still looking for simplifications on this one. Thanks for any tips!

[Arthur Adjedj]

The following works:

theorem optimize_optimal (e : Expr) :
  optimal (optimize e) := by
  induction e <;> simp [optimize, optimal] <;> split <;> simp [optimal, *]

[Arthur Adjedj]

BTW, rewording optimal as an inductive predicate makes grind solve it:

-- Datatype for arithmetic expressions
inductive Expr where
  | const : Int → Expr                 -- Constants like 5
  | var : String → Expr                -- Variables like "x"
  | add : Expr → Expr → Expr           -- Addition (e₁ + e₂)
  | mul : Expr → Expr → Expr           -- Multiplication (e₁ * e₂)
  deriving Repr
open Expr

-- Environment type (maps variable names to values)
def Env := String → Int

-- Evaluator function
def evaluate : Expr → Env → Int
  | const n, _ => n               -- A constant evaluates to itself
  | var x, env => env x           -- A variable evaluates to its value in the environment
  | add e₁ e₂, env => evaluate e₁ env + evaluate e₂ env  -- Addition evaluates recursively
  | mul e₁ e₂, env => evaluate e₁ env * evaluate e₂ env  -- Multiplication evaluates recursively too

-- Optimizer to remove additions by 0 & multiplication by 1, and to simplify multiplication by 0
def optimize : Expr → Expr
  | const n => const n       -- Constants remain unchanged
  | var x => var x           -- Variables remain unchanged
  | add e₁ e₂ =>
    let e₁' := optimize e₁
    let e₂' := optimize e₂
    match e₁', e₂' with
    | const n₁, const n₂ => const (n₁ + n₂)
    | const 0, e => e            -- 0 + e => e
    | e, const 0 => e            -- e + 0 => e
    | _, _ => add e₁' e₂'        -- Otherwise keep the optimized addition
  | mul e₁ e₂ =>
    let e₁' := optimize e₁
    let e₂' := optimize e₂
    match e₁', e₂' with
    | const n₁, const n₂ => const (n₁ * n₂)
    | const 0, _ => const 0 -- 0 * e => 0
    | _, const 0 => const 0 -- e * 0 => 0
    | const 1, e => e            -- 1 * e => e
    | e, const 1 => e            -- e * 1 => e
    | _, _ => mul e₁' e₂'        -- Otherwise keep the optimized multiplication


-- Theorem: optimizer preserves semantics
-- Thanks to Arthur Adjedj for pointing out the new grind tactic
set_option grind.warning false
theorem optimize_preserves_semantics (e : Expr) (env : Env) :
  evaluate (optimize e) env = evaluate e env := by
  induction e <;> grind (config := {  ring := true }) [evaluate, optimize]

@[grind cases]
inductive NotOptimal : Expr → Prop
  | addConst : NotOptimal (add (const c₁) (const c₂))
  | addLeftZero : NotOptimal  (add (const 0) e)
  | addLeftRight : NotOptimal (add e (const 0))
  | addNotOptiLeft : NotOptimal e₁ → NotOptimal (add e₁ e₂)
  | addNotOptiRight : NotOptimal e₂ → NotOptimal (add e₁ e₂)
  | mulConst : NotOptimal (mul (const c₁) (const c₂))
  | mulLeftZero  : NotOptimal (mul (const 0) e)
  | mulLeftRight : NotOptimal (mul e (const 0))
  | mulOneZero  : NotOptimal (mul (const 1) e)
  | mulOneRight : NotOptimal (mul e (const 1))
  | mulNotOptiLeft : NotOptimal e₁ → NotOptimal (mul e₁ e₂)
  | mulNotOptiRight : NotOptimal e₂ → NotOptimal (mul e₁ e₂)

theorem optimize_optimal (e : Expr) :
  ¬ NotOptimal (optimize e) := by
  induction e <;> grind +ring [optimize,optimal]

[Nada Amin]

Arthur Adjedj said:

The following works:

theorem optimize_optimal (e : Expr) :
  optimal (optimize e) := by
  induction e <;> simp [optimize, optimal] <;> split <;> simp [optimal, *]

Thanks! The use of * is neat.

[Nada Amin]

It's interesting that grind works with an inductive definition of NotOptimal. Do you have any intuition why this is easier for grind? I would have thought that the double negation would make it harder.

Thanks so much for exploring the space of solutions with me!

[Nada Amin]

Aesop also works nicely here.

import Aesop

-- Datatype for arithmetic expressions
@[aesop safe [constructors, cases]]
inductive Expr where
  | const : Int → Expr                 -- Constants like 5
  | var : String → Expr                -- Variables like "x"
  | add : Expr → Expr → Expr           -- Addition (e₁ + e₂)
  | mul : Expr → Expr → Expr           -- Multiplication (e₁ * e₂)
  deriving Repr

-- Environment type (maps variable names to values)
def Env := String → Int

-- Evaluator function
@[aesop safe]
def evaluate : Expr → Env → Int
  | Expr.const n, _ => n               -- A constant evaluates to itself
  | Expr.var x, env => env x           -- A variable evaluates to its value in the environment
  | Expr.add e₁ e₂, env => evaluate e₁ env + evaluate e₂ env  -- Addition evaluates recursively
  | Expr.mul e₁ e₂, env => evaluate e₁ env * evaluate e₂ env  -- Multiplication evaluates recursively too

-- Optimizer to remove additions by 0 & multiplication by 1, and to simplify multiplication by 0
@[aesop safe]
def optimize : Expr → Expr
  | Expr.const n => Expr.const n       -- Constants remain unchanged
  | Expr.var x => Expr.var x           -- Variables remain unchanged
  | Expr.add e₁ e₂ =>
    let e₁' := optimize e₁
    let e₂' := optimize e₂
    match e₁', e₂' with
    | Expr.const n₁, Expr.const n₂ => Expr.const (n₁ + n₂)
    | Expr.const 0, e => e            -- 0 + e => e
    | e, Expr.const 0 => e            -- e + 0 => e
    | _, _ => Expr.add e₁' e₂'        -- Otherwise keep the optimized addition
  | Expr.mul e₁ e₂ =>
    let e₁' := optimize e₁
    let e₂' := optimize e₂
    match e₁', e₂' with
    | Expr.const n₁, Expr.const n₂ => Expr.const (n₁ * n₂)
    | Expr.const 0, _ => Expr.const 0 -- 0 * e => 0
    | _, Expr.const 0 => Expr.const 0 -- e * 0 => 0
    | Expr.const 1, e => e            -- 1 * e => e
    | e, Expr.const 1 => e            -- e * 1 => e
    | _, _ => Expr.mul e₁' e₂'        -- Otherwise keep the optimized multiplication


theorem optimize_preserves_semantics (e : Expr) (env : Env) :
  evaluate (optimize e) env = evaluate e env := by
  aesop

-- Predicate defining an optimally optimized expression
def optimal : Expr → Bool
  | Expr.const _ => true
  | Expr.var _ => true
  | Expr.add (Expr.const _) (Expr.const _) => false
  | Expr.add (Expr.const 0) _ => false
  | Expr.add _ (Expr.const 0) => false
  | Expr.add e₁ e₂ => optimal e₁ && optimal e₂
  | Expr.mul (Expr.const _) (Expr.const _) => false
  | Expr.mul (Expr.const 0) _ => false
  | Expr.mul _ (Expr.const 0) => false
  | Expr.mul (Expr.const 1) _ => false
  | Expr.mul _ (Expr.const 1) => false
  | Expr.mul e₁ e₂ => optimal e₁ && optimal e₂

-- Theorem: optimizer produces optimital expressions
theorem optimize_optimal (e : Expr) :
  optimal (optimize e) := by
  aesop

[Nada Amin]

Oh, nevermind, it looks like the max number of heartbeat was reached for each theorem.