Lean4
/-- `proveFalseByLinarith` is the main workhorse of `linarith`.
Given a list `l` of proofs of `tᵢ Rᵢ 0`,
it tries to derive a contradiction from `l` and use this to produce a proof of `False`.
`oracle : CertificateOracle` is used to search for a certificate of unsatisfiability.
The returned certificate is a map `m` from hypothesis indices to natural number coefficients.
If our set of hypotheses has the form `{tᵢ Rᵢ 0}`,
then the elimination process should have guaranteed that
1.\ `∑ (m i)*tᵢ = 0`,
with at least one `i` such that `m i > 0` and `Rᵢ` is `<`.
We have also that
2.\ `∑ (m i)*tᵢ < 0`,
since for each `i`, `(m i)*tᵢ ≤ 0` and at least one is strictly negative.
So we conclude a contradiction `0 < 0`.
It remains to produce proofs of (1) and (2). (1) is verified by calling the provided `discharger`
tactic, which is typically `ring`. We prove (2) by folding over the set of hypotheses.
`transparency : TransparencyMode` controls the transparency level with which atoms are identified.
-/
def proveFalseByLinarith (transparency : TransparencyMode) (oracle : CertificateOracle) (discharger : TacticM Unit) :
MVarId → List Expr → MetaM Expr
| _, [] => throwError"no args to linarith"
| g, l@(h :: _) => do
Lean.Core.checkSystem decl_name%.toString
let l' ← detailTrace "addNegEqProofs" <| addNegEqProofs l
let inputs ← detailTrace "mkNegOneLtZeroProof" <| return (← mkNegOneLtZeroProof (← typeOfIneqProof h)) :: l'.reverse
trace[linarith.detail]"inputs:{indentD <| toMessageData (← inputs.mapM inferType)}"
let (comps, max_var) ← detailTrace "linearFormsAndMaxVar" <| linearFormsAndMaxVar transparency inputs
trace[linarith.detail]"comps:{indentD <| toMessageData comps}"
let certificate : Std.HashMap Nat Nat ←
withTraceNode `linarith (return m! "{exceptEmoji ·} Invoking oracle")
(do
let certificate ←
try
oracle.produceCertificate comps max_var
catch e =>
trace[linarith]
throwError"linarith failed to find a contradiction"
trace[linarith]"found a contradiction: {certificate.toList}"
return certificate)
let (sm, zip) ←
withTraceNode `linarith (return m! "{exceptEmoji ·} Building final expression")
(do
let enum_inputs := inputs.zipIdx
let zip := enum_inputs.filterMap fun ⟨e, n⟩ => (certificate[n]?).map (e, ·)
let mls ←
zip.mapM fun ⟨e, n⟩ => do
mulExpr n
(← leftOfIneqProof e)
-- `sm` is the sum of input terms, scaled to cancel out all variables.
let sm ← addExprs mls
trace[linarith]"{indentD sm}\nshould be both 0 and negative"
return (sm, zip))
let sm_eq_zero ← detailTrace "proveEqZeroUsing" <| proveEqZeroUsing discharger sm
let sm_lt_zero ← detailTrace "mkLTZeroProof" <| mkLTZeroProof zip
detailTrace "Linarith.lt_irrefl" do
-- this is a contradiction.
let pftp ← inferType sm_lt_zero
let ⟨_, nep, _⟩ ← g.rewrite pftp sm_eq_zero
let pf' ← mkAppM ``Eq.mp #[nep, sm_lt_zero]
mkAppM ``Linarith.lt_irrefl #[pf']
where/-- Log `f` under `linarith.detail`, with exception emojis and the provided name. -/
detailTrace {α} (s : String) (f : MetaM α) : MetaM α :=
withTraceNode `linarith.detail (return m!"{(exceptEmoji ·)} {s}") f
