Lean4
/-- If the symm congruence table (`symmCongruences` field) has congruent expression to `e`, add the
equality to the todo list. If not, add `e` to the symm congruence table. -/
def addSymmCongruenceTable (e : Expr) : CCM Unit := do
let some (rel, lhs, rhs) ← e.relSidesIfSymm? |
failure
let k ← mkSymmCongruencesKey lhs rhs
let newP := (e, rel)
if let some ps := (← get).symmCongruences[k]? then
for p in ps do
if ← compareSymm newP p then
-- Found new equivalence: `e ~ p.1`
-- 1. Update `cgRoot` field for `e`
let some currEntry ← getEntry e |
failure
let newEntry := { currEntry with cgRoot := p.1 }
modify fun ccs =>
{ ccs with entries := ccs.entries.insert e newEntry }
-- 2. Put new equivalence in the TODO queue
-- NOTE(gabriel): support for symmetric relations is pretty much broken,
-- since it ignores all arguments except the last two ones.
-- e.g. this would claim that `ModEq n a b` and `ModEq m a b` are equivalent.
-- Whitelist some relations to contain breakage:
if rel == ``Eq || e.getAppNumArgs == 2 then
pushEq e p.1 .congr
checkEqTrue e
return
modify fun ccs => { ccs with symmCongruences := ccs.symmCongruences.insert k (newP :: ps) }
checkEqTrue e
else
modify fun ccs => { ccs with symmCongruences := ccs.symmCongruences.insert k [newP] }
checkEqTrue e
