Lean4
/-- Preprocesses facts for linear orders. Replaces `x < y`, `¬ (x ≤ y)`, `¬ (x < y)`, and `x = y`
with equivalent facts involving only `≤` and `≠`. For each fact `x = y ⊔ z` adds `y ≤ x`
and `z ≤ x` facts, and similarly for `⊓`. -/
def preprocessFactsLinear (facts : Array AtomicFact) (idxToAtom : Std.HashMap Nat Expr) : MetaM <| Array AtomicFact :=
do
let mut res : Array AtomicFact := #[]
for fact in facts do
match fact with
| .lt lhs rhs proof =>
res := res.push <| .ne lhs rhs (← mkAppM ``ne_of_lt #[proof])
res := res.push <| .le lhs rhs (← mkAppM ``le_of_lt #[proof])
| .nle lhs rhs proof =>
res := res.push <| .ne lhs rhs (← mkAppM ``ne_of_not_le #[proof])
res := res.push <| .le rhs lhs (← mkAppM ``le_of_not_ge #[proof])
| .nlt lhs rhs proof =>
res := res.push <| .le rhs lhs (← mkAppM ``le_of_not_gt #[proof])
| .eq lhs rhs proof =>
res := res.push <| .le lhs rhs (← mkAppM ``le_of_eq #[proof])
res := res.push <| .le rhs lhs (← mkAppM ``ge_of_eq #[proof])
| .isSup lhs rhs sup =>
res := res.push <| .le lhs sup (← mkAppOptM ``le_sup_left #[none, none, idxToAtom.get! lhs, idxToAtom.get! rhs])
res := res.push <| .le rhs sup (← mkAppOptM ``le_sup_right #[none, none, idxToAtom.get! lhs, idxToAtom.get! rhs])
res := res.push fact
| .isInf lhs rhs inf =>
res := res.push <| .le inf lhs (← mkAppOptM ``inf_le_left #[none, none, idxToAtom.get! lhs, idxToAtom.get! rhs])
res := res.push <| .le inf rhs (← mkAppOptM ``inf_le_right #[none, none, idxToAtom.get! lhs, idxToAtom.get! rhs])
res := res.push fact
| _ =>
res := res.push fact
return res
