Lean4
/-- Finds a contradictory `≠`-fact whose `.lhs` and `.rhs` belong to the same strongly connected
component in the `≤`-graph, implying they must be equal, and then uses it to derive `False`. -/
def findContradictionWithNe (graph : Graph) (idxToAtom : Std.HashMap Nat Expr) (facts : Array AtomicFact) :
MetaM <| Option Expr := do
let scc := graph.findSCCs
for fact in facts do
let .ne lhs rhs neProof := fact |
continue
if scc[lhs]! != scc[rhs]! then
continue
let some pf1 ← graph.buildTransitiveLeProof idxToAtom lhs rhs |
panic! "Cannot find path in strongly connected component"
let some pf2 ← graph.buildTransitiveLeProof idxToAtom rhs lhs |
panic! "Cannot find path in strongly connected component"
let pf3 ← mkAppM ``le_antisymm #[pf1, pf2]
return some <| mkApp neProof pf3
return none
