Lean4
/-- If the congruence table (`congruences` field) has congruent expression to `e`, add the
equality to the todo list. If not, add `e` to the congruence table. -/
def addCongruenceTable (e : Expr) : CCM Unit := do
guard e.isApp
let k ← mkCongruencesKey e
if let some es := (← get).congruences[k]? then
for oldE in es do
if ← isCongruent e oldE then
-- Found new equivalence: `e ~ oldE`
-- 1. Update `cgRoot` field for `e`
let some currEntry ← getEntry e |
failure
let newEntry := { currEntry with cgRoot := oldE }
modify fun ccs =>
{ ccs with entries := ccs.entries.insert e newEntry }
-- 2. Put new equivalence in the todo queue
-- TODO(Leo): check if the following line is a bottleneck
let heqProof ← (!·) <$> pureIsDefEq (← inferType e) (← inferType oldE)
pushTodo e oldE .congr heqProof
return
modify fun ccs => { ccs with congruences := ccs.congruences.insert k (e :: es) }
else
modify fun ccs => { ccs with congruences := ccs.congruences.insert k [e] }
