dsimp 使用例：算術式を簡略化する関数

Expr という名前はあまりよくないかもしれない

inductive Expr where
  | const : Nat → Expr
  | plus : Expr → Expr → Expr
  | times : Expr → Expr → Expr
deriving Repr

open Expr

def eval : Expr → Nat
  | const n => n
  | plus e₁ e₂  => eval e₁ + eval e₂
  | times e₁ e₂ => eval e₁ * eval e₂

def simpConst : Expr → Expr
  | plus (const n₁) (const n₂)  => const (n₁ + n₂)
  | times (const n₁) (const n₂) => const (n₁ * n₂)
  | e => e

def fuse : Expr → Expr
  | plus e₁ e₂ => simpConst (plus (fuse e₁) (fuse e₂))
  | times e₁ e₂ => simpConst (times (fuse e₁) (fuse e₂))
  | e => e

theorem fuse_in_const {e : Expr} : ∃ n, fuse e = .const n := by
  induction e with
  | const n => exists n
  | plus e₁ e₂ ih₁ ih₂ => 
    dsimp [fuse]
    obtain ⟨n₁, ih₁⟩ := ih₁
    obtain ⟨n₂, ih₂⟩ := ih₂
    rw [ih₁, ih₂]
    dsimp [simpConst]
    exists n₁ + n₂
  | times e₁ e₂ ih₁ ih₂ =>
    dsimp [fuse]
    obtain ⟨n₁, ih₁⟩ := ih₁
    obtain ⟨n₂, ih₂⟩ := ih₂
    rw [ih₁, ih₂]
    dsimp [simpConst]
    exists n₁ * n₂

lean-ja / lean-by-example

dsimp 使用例：算術式を簡略化する関数 #360