# Deriving a proof of false #

`linarith`

uses an untrusted oracle to produce a certificate of unsatisfiability.
It needs to do some proof reconstruction work to turn this into a proof term.
This file implements the reconstruction.

## Main declarations #

The public facing declaration in this file is `proveFalseByLinarith`

.

Typesafe conversion of `n : ℕ`

to `Q($α)`

.

## Equations

- Qq.ofNatQ α x n = match n with | 0 => q(0) | 1 => q(1) | k.succ.succ => let_fun lit := Lean.mkRawNatLit n; let_fun k := Lean.mkRawNatLit k; q(OfNat.ofNat «$lit»)

## Instances For

### Auxiliary functions for assembling proofs #

A typesafe version of `mulExpr`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`mulExpr n e`

creates an `Expr`

representing `n*e`

.
When elaborated, the coefficient will be a native numeral of the same type as `e`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

A type-safe analogue of `addExprs`

.

## Equations

- Linarith.addExprs' _inst x = match x with | [] => q(0) | h :: t => Linarith.addExprs'.go _inst h t

## Instances For

Inner loop for `addExprs'`

.

## Equations

- Linarith.addExprs'.go _inst p [] = p
- Linarith.addExprs'.go _inst p [q] = q(«$p» + «$q»)
- Linarith.addExprs'.go _inst p (q :: t) = Linarith.addExprs'.go _inst q(«$p» + «$q») t

## Instances For

`addExprs L`

creates an `Expr`

representing the sum of the elements of `L`

, associated left.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

If our goal is to add together two inequalities `t1 R1 0`

and `t2 R2 0`

,
`addIneq R1 R2`

produces the strength of the inequality in the sum `R`

,
along with the name of a lemma to apply in order to conclude `t1 + t2 R 0`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`mkLTZeroProof coeffs pfs`

takes a list of proofs of the form `tᵢ Rᵢ 0`

,
paired with coefficients `cᵢ`

.
It produces a proof that `∑cᵢ * tᵢ R 0`

, where `R`

is as strong as possible.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`step c pf npf coeff`

assumes that `pf`

is a proof of `t1 R1 0`

and `npf`

is a proof
of `t2 R2 0`

. It uses `mkSingleCompZeroOf`

to prove `t1 + coeff*t2 R 0`

, and returns `R`

along with this proof.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

If `prf`

is a proof of `t R s`

, `leftOfIneqProof prf`

returns `t`

.

## Equations

- Linarith.leftOfIneqProof prf = do let __do_lift ← Lean.Meta.inferType prf let __discr ← Linarith.getRelSides __do_lift match __discr with | (t, snd) => pure t

## Instances For

If `prf`

is a proof of `t R s`

, `typeOfIneqProof prf`

returns the type of `t`

.

## Equations

- Linarith.typeOfIneqProof prf = do let __do_lift ← Linarith.leftOfIneqProof prf Lean.Meta.inferType __do_lift

## Instances For

`mkNegOneLtZeroProof tp`

returns a proof of `-1 < 0`

,
where the numerals are natively of type `tp`

.

## Equations

- Linarith.mkNegOneLtZeroProof tp = do let zero_lt_one ← Lean.Meta.mkAppOptM `zero_lt_one #[some tp, none, none, none, none, none] Lean.Meta.mkAppM `neg_neg_of_pos #[zero_lt_one]

## Instances For

`addNegEqProofs l`

inspects the list of proofs `l`

for proofs of the form `t = 0`

. For each such
proof, it adds a proof of `-t = 0`

to the list.

## Equations

- One or more equations did not get rendered due to their size.
- Linarith.addNegEqProofs [] = pure []

## Instances For

`proveEqZeroUsing tac e`

tries to use `tac`

to construct a proof of `e = 0`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

#### The main method #

`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`

.

An oracle is used to search for a certificate of unsatisfiability.
In the current implementation, this is the Fourier Motzkin elimination routine in
`Elimination.lean`

, but other oracles could easily be swapped in.

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 `discharger`

tactic
of the `LinarithConfig`

object, which is typically `ring`

. We prove (2) by folding over the
set of hypotheses.

## Equations

- One or more equations did not get rendered due to their size.