reduced unfolding in simp leads reduces simp-power

[tobiasgrosser]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Before 16bc6eb was committed, simp unfolded definitions with all-constant inputs to a level that allowed relatively complex evaluators to fold away completely. I am unsure if this is desired and how to obtain a similar effect with the changed simp implementation.

universe u

inductive Circuit (α : Type u) : Type u
  | tru : Circuit α
  | fals : Circuit α
  | var : Bool → α → Circuit α
  | and : Circuit α → Circuit α → Circuit α
  | or : Circuit α → Circuit α → Circuit α
  | xor : Circuit α → Circuit α → Circuit α
deriving Repr

namespace Circuit
variable {α : Type u}

@[simp]
def eval : Circuit α → (α → Bool) → Bool
  | tru, _ => true
  | fals, _ => false
  | var b x, f => if b then f x else !(f x)
  | and c₁ c₂, f => (eval c₁ f) && (eval c₂ f)
  | or c₁ c₂, f => (eval c₁ f) || (eval c₂ f)
  | xor c₁ c₂, f => Bool.xor (eval c₁ f) (eval c₂ f)

def simplifyAnd : Circuit α → Circuit α → Circuit α
  | tru, c => c
  | c, tru => c
  | fals, _ => fals
  | _, fals => fals
  | c₁, c₂ => and c₁ c₂
instance : AndOp (Circuit α) := ⟨Circuit.simplifyAnd⟩

def simplifyOr : Circuit α → Circuit α → Circuit α
  | tru, _ => tru
  | _, tru => tru
  | fals, c => c
  | c, fals => c
  | c₁, c₂ => or c₁ c₂
instance : OrOp (Circuit α) := ⟨Circuit.simplifyOr⟩

def simplifyNot : Circuit α → Circuit α
  | tru => fals
  | fals => tru
  | xor a b => xor (simplifyNot a) b
  | and a b => or (simplifyNot a) (simplifyNot b)
  | or a b => and (simplifyNot a) (simplifyNot b)
  | var b a => var (!b) a
instance : Complement (Circuit α) := ⟨Circuit.simplifyNot⟩

def simplifyXor : Circuit α → Circuit α → Circuit α
  | fals, c => c
  | c, fals => c
  | tru, c => ~~~ c
  | c, tru => ~~~ c
  | c₁, c₂ => xor c₁ c₂
instance : Xor (Circuit α) := ⟨Circuit.simplifyXor⟩

open Sum

structure FSM (arity : Type) : Type 1 where
  ( α  : Type )
  ( nextBitCirc : Option α → Circuit (α ⊕ arity) )

def add : FSM Bool :=
  { α := Unit,
    nextBitCirc := fun a =>
      match a with
      | some () =>
             (Circuit.var true (inr true)  &&& Circuit.var true (inr false))
             ||| (Circuit.var true (inr true)  &&& Circuit.var true (inl ()))
             ||| (Circuit.var true (inr false) &&& Circuit.var true (inl ()))
      | none => Circuit.var true (inr true) ^^^
                Circuit.var true (inr false) ^^^
                Circuit.var true (inl ()) }

theorem add_nextBitCirc_some_eval :
    (add.nextBitCirc (some ())).eval =
      fun x => x (inr true) && x (inr false) || x (inr true)
        && x (inl ()) || x (inr false) && x (inl ()) := by
  /-
  simp only [Circuit.eval]
  Lean 4.16.0-nightly-2024-12-20
  Target: arm64-apple-darwin23.6.0 macOS

  ⊢ (fun x =>
      (((if True then x (inr true) else !x (inr true)) && if True then x (inr false) else !x (inr false)) ||
          (if True then x (inr true) else !x (inr true)) && if True then x (inl ()) else !x (inl ())) ||
        (if True then x (inr false) else !x (inr false)) && if True then x (inl ()) else !x (inl ())) =
    fun x => x (inr true) && x (inr false) || x (inr true) && x (inl ()) || x (inr false) && x (inl ())

  with
  Lean 4.16.0-nightly-2024-12-24
  Target: x86_64-unknown-linux-gnu
  simp has no effect

  -/
  simp only [Circuit.eval]
  simp -- closes the goal with 2024-12-20 but not 2024-12-24.

Steps to Reproduce

1. Copy file in lean editor
2. Observe that goal is not closed

Expected behavior:

It would be nice if the goal would be closed.

Actual behavior:

The goal is not closed and it is not even possible to unfold Circuit.eval. However, unfolding Circuit.eval was also not possible with the old version.

The degree of unfolding simp by default was impressive beforehand, and I am unsure how it was done. I tried to use simp +ground:

theorem add_nextBitCirc_some_eval :
    (add.nextBitCirc (some ())).eval =
      fun x => x (inr true) && x (inr false) || x (inr true)
        && x (inl ()) || x (inr false) && x (inl ()) := by
  /-
  ((((var true (inr true)).simplifyAnd (var true (inr false))).simplifyOr
          ((var true (inr true)).simplifyAnd (var true (inl PUnit.unit)))).simplifyOr
      ((var true (inr false)).simplifyAnd (var true (inl PUnit.unit)))).eval
  -/
  simp +ground only [Circuit.eval, add]
  /-
  failed to rewrite using equation theorems for 'Circuit.eval'. Try rewriting with 'Circuit.eval.eq_def'.
  -/
  rw [Circuit.eval]

which does something sensible, but I still cannot unfold Circuit.eval.

Versions

Lean 4.16.0-nightly-2024-12-20
Target: arm64-apple-darwin23.6.0 macOS

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[tobiasgrosser]

This issue has been discussed and resolved in https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Magic.20simp.20unfolding/near/490756711.