Lean4
/-- The single step of `simplifyAC`.
Simplifies an expression `e` by either simplifying one argument to the AC operator, or the whole
expression. -/
def simplifyACStep (e : ACApps) : CCM (Option (ACApps × DelayedExpr)) := do
if let .apps _ args := e then
for h : i in [:args.size]do
if i == 0 || args[i] != (args[i - 1]'(Nat.lt_of_le_of_lt (i.sub_le 1) h.2.1)) then
let some ae := (← get).acEntries[args[i]]? |
failure
let occs := ae.RLHSOccs
let mut Rlhs? : Option ACApps := none
for Rlhs in occs do
if Rlhs.isSubset e then
Rlhs? := some Rlhs
break
if let some Rlhs := Rlhs? then
let some (Rrhs, H) := (← get).acR[Rlhs]? |
failure
return (some <| ← simplifyACCore e Rlhs Rrhs H)
else if let some p := (← get).acR[e]? then
return some p
return none
