lean/ExprSpec.lean

-- File: lean/ExprSpec.lean
-- Expression Evaluator Specification
-- Agents migrate a C recursive-descent evaluator to Rust.
-- Division by zero returns none (Option Int), not a panic.

namespace ExprSpec

inductive Op
  | Add | Sub | Mul | Div
  deriving BEq, DecidableEq, Repr

inductive Expr
  | Lit (n : Int)
  | BinOp (op : Op) (l r : Expr)
  deriving BEq, DecidableEq, Repr

-- Evaluate a binary operation; division by zero yields none
def evalBinOp (op : Op) (a b : Int) : Option Int :=
  match op with
  | .Add => some (a + b)
  | .Sub => some (a - b)
  | .Mul => some (a * b)
  | .Div => if b = 0 then none else some (a / b)

-- Recursively evaluate an expression tree; propagate none on div-by-zero
def evalExpr : Expr → Option Int
  | .Lit n => some n
  | .BinOp op l r =>
    match evalExpr l, evalExpr r with
    | some a, some b => evalBinOp op a b
    | _, _ => none

-- Division by zero always returns none
theorem division_by_zero (a : Int) : evalBinOp .Div a 0 = none := by
  simp [evalBinOp]

-- DRT checks
example : evalBinOp .Add 3 4 = some 7 := by native_decide
example : evalBinOp .Sub 10 3 = some 7 := by native_decide
example : evalBinOp .Mul 3 4 = some 12 := by native_decide
example : evalBinOp .Div 10 2 = some 5 := by native_decide
example : evalBinOp .Div 10 0 = none := by native_decide
example : evalExpr (.Lit 42) = some 42 := by native_decide
example : evalExpr (.BinOp .Add (.Lit 1) (.Lit 2)) = some 3 := by native_decide
example : evalExpr (.BinOp .Div (.Lit 5) (.Lit 0)) = none := by native_decide

end ExprSpec