Lean4
/-- Adds edges to the `≤`-graph using two types of facts:
1. Each fact `¬ (x < y)` allows to add the edge `(x, y)` when `y` is reachable from `x` in the
graph.
2. Each fact `x ⊔ y = z` allows to add the edge `(z, s)` when `s` is reachable from both `x`
and `y`.
We repeat the process until no more edges can be added. -/
def updateGraphWithNltInfSup (g : Graph) (idxToAtom : Std.HashMap Nat Expr) (facts : Array AtomicFact) : MetaM Graph :=
do
let nltFacts := facts.filter fun fact => fact matches .nlt ..
let mut usedNltFacts : Vector Bool _ := .replicate nltFacts.size false
let infSupFacts := facts.filter fun fact => fact matches .isInf .. | .isSup ..
let mut g := g
repeat
do
let mut changed : Bool := false
for h : i in [:nltFacts.size]do
if usedNltFacts[i] then
continue
let .nlt lhs rhs proof := nltFacts[i] |
panic! "Non-nlt fact in nltFacts."
let some pf ← g.buildTransitiveLeProof idxToAtom lhs rhs |
continue
g := g.addEdge ⟨rhs, lhs, ← mkAppM ``le_of_not_lt_le #[proof, pf]⟩
changed := true
usedNltFacts := usedNltFacts.set i true
for fact in infSupFacts do
for idx in [:g.size]do
match fact with
| .isSup lhs rhs sup =>
let some pf1 ← g.buildTransitiveLeProof idxToAtom lhs idx |
continue
let some pf2 ← g.buildTransitiveLeProof idxToAtom rhs idx |
continue
if (← g.buildTransitiveLeProof idxToAtom sup idx).isNone then
g := g.addEdge ⟨sup, idx, ← mkAppM ``sup_le #[pf1, pf2]⟩
changed := true
| .isInf lhs rhs inf =>
let some pf1 ← g.buildTransitiveLeProof idxToAtom idx lhs |
continue
let some pf2 ← g.buildTransitiveLeProof idxToAtom idx rhs |
continue
if (← g.buildTransitiveLeProof idxToAtom idx inf).isNone then
g := g.addEdge ⟨idx, inf, ← mkAppM ``le_inf #[pf1, pf2]⟩
changed := true
| _ =>
panic! "Non-isInf or isSup fact in infSupFacts."
if !changed then
break
return g
