Helper definitions and theorems for constructing linear arithmetic proofs.

source
@[reducible, inline]
abbrev Nat.Linear.Var :
Type
Equations

- Nat.Linear.Var = Nat

Instances For

source
@[reducible, inline]
abbrev Nat.Linear.Context :
Type
Equations

- Nat.Linear.Context = Lean.RArray Nat

Instances For

source
def Nat.Linear.fixedVar :
Nat

When encoding polynomials. We use `fixedVar` for encoding numerals. The denotation of `fixedVar` is always `1`.

Equations

- Nat.Linear.fixedVar = 100000000

Instances For

source
def Nat.Linear.Var.denote (ctx : Context) (v : Var) :
Nat
Equations

- Nat.Linear.Var.denote ctx v = bif v == Nat.Linear.fixedVar then 1 else Lean.RArray.get ctx v

Instances For

source
inductive Nat.Linear.Expr :
Type

- num (v : Nat) : Expr
- var (i : Var) : Expr
- add (a b : Expr) : Expr
- mulL (k : Nat) (a : Expr) : Expr
- mulR (a : Expr) (k : Nat) : Expr

Instances For

source
instance Nat.Linear.instInhabitedExpr :
Inhabited Expr
Equations

- Nat.Linear.instInhabitedExpr = { default := Nat.Linear.instInhabitedExpr.default }

source
def Nat.Linear.instInhabitedExpr.default :
Expr
Equations

- Nat.Linear.instInhabitedExpr.default = Nat.Linear.Expr.num default

Instances For

source
instance Nat.Linear.instBEqExpr :
BEq Expr
Equations

- Nat.Linear.instBEqExpr = { beq := Nat.Linear.instBEqExpr.beq }

source
def Nat.Linear.instBEqExpr.beq :
Expr → Expr → Bool
Equations

- Nat.Linear.instBEqExpr.beq (Nat.Linear.Expr.num a) (Nat.Linear.Expr.num b) = (a == b)
- Nat.Linear.instBEqExpr.beq (Nat.Linear.Expr.var a) (Nat.Linear.Expr.var b) = (a == b)
- Nat.Linear.instBEqExpr.beq (a.add a_1) (b.add b_1) = (Nat.Linear.instBEqExpr.beq a b && Nat.Linear.instBEqExpr.beq a_1 b_1)
- Nat.Linear.instBEqExpr.beq (Nat.Linear.Expr.mulL a a_1) (Nat.Linear.Expr.mulL b b_1) = (a == b && Nat.Linear.instBEqExpr.beq a_1 b_1)
- Nat.Linear.instBEqExpr.beq (a.mulR a_1) (b.mulR b_1) = (Nat.Linear.instBEqExpr.beq a b && a_1 == b_1)
- Nat.Linear.instBEqExpr.beq x✝¹ x✝ = false

Instances For

source
def Nat.Linear.Expr.denote (ctx : Context) :
Expr → Nat
Equations

- Nat.Linear.Expr.denote ctx (a.add b) = (Nat.Linear.Expr.denote ctx a).add (Nat.Linear.Expr.denote ctx b)
- Nat.Linear.Expr.denote ctx (Nat.Linear.Expr.num k) = k
- Nat.Linear.Expr.denote ctx (Nat.Linear.Expr.var v) = Nat.Linear.Var.denote ctx v
- Nat.Linear.Expr.denote ctx (Nat.Linear.Expr.mulL k e) = k.mul (Nat.Linear.Expr.denote ctx e)
- Nat.Linear.Expr.denote ctx (e.mulR k) = (Nat.Linear.Expr.denote ctx e).mul k

Instances For

source
@[reducible, inline]
abbrev Nat.Linear.Poly :
Type
Equations

- Nat.Linear.Poly = List (Nat × Nat.Linear.Var)

Instances For

source
def Nat.Linear.Poly.denote (ctx : Context) (p : Poly) :
Nat
Equations

- Nat.Linear.Poly.denote ctx [] = 0
- Nat.Linear.Poly.denote ctx ((k, v) :: p_2) = (k.mul (Nat.Linear.Var.denote ctx v)).add (Nat.Linear.Poly.denote ctx p_2)

Instances For

source
def Nat.Linear.Poly.insert (k : Nat) (v : Var) (p : Poly) :
Poly
Equations

- One or more equations did not get rendered due to their size.
- Nat.Linear.Poly.insert k v [] = [(k, v)]

Instances For

source
def Nat.Linear.Poly.norm (p : Poly) :
Poly
Equations

- p.norm = Nat.Linear.Poly.norm.go p []

Instances For

source
def Nat.Linear.Poly.norm.go (p r : Poly) :
Poly
Equations

- Nat.Linear.Poly.norm.go [] r = r
- Nat.Linear.Poly.norm.go ((k, v) :: p_2) r = Nat.Linear.Poly.norm.go p_2 (Nat.Linear.Poly.insert k v r)

Instances For

source
def Nat.Linear.Poly.cancelAux (fuel : Nat) (m₁ m₂ r₁ r₂ : Poly) :
Poly × Poly
Equations

- One or more equations did not get rendered due to their size.
- Nat.Linear.Poly.cancelAux 0 m₁ m₂ r₁ r₂ = (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)
- Nat.Linear.Poly.cancelAux fuel_2.succ m₁ [] r₁ r₂ = (List.reverse r₁ ++ m₁, List.reverse r₂)
- Nat.Linear.Poly.cancelAux fuel_2.succ [] m₂ r₁ r₂ = (List.reverse r₁, List.reverse r₂ ++ m₂)

Instances For

source
def Nat.Linear.hugeFuel :
Nat
Equations

- Nat.Linear.hugeFuel = 1000000

Instances For

source
def Nat.Linear.Poly.cancel (p₁ p₂ : Poly) :
Poly × Poly
Equations

- p₁.cancel p₂ = Nat.Linear.Poly.cancelAux Nat.Linear.hugeFuel p₁ p₂ [] []

Instances For

source
def Nat.Linear.Poly.isNum? (p : Poly) :
Option Nat
Equations

- Nat.Linear.Poly.isNum? [] = some 0
- Nat.Linear.Poly.isNum? [(k, v)] = bif v == Nat.Linear.fixedVar then some k else none
- p.isNum? = none

Instances For

source
def Nat.Linear.Poly.isZero (p : Poly) :
Bool
Equations

- Nat.Linear.Poly.isZero [] = true
- p.isZero = false

Instances For

source
def Nat.Linear.Poly.isNonZero (p : Poly) :
Bool
Equations

- Nat.Linear.Poly.isNonZero [] = false
- Nat.Linear.Poly.isNonZero ((k, v) :: p_2) = bif v == Nat.Linear.fixedVar then decide (k > 0) else Nat.Linear.Poly.isNonZero p_2

Instances For

source
def Nat.Linear.Poly.denote_eq (ctx : Context) (mp : Poly × Poly) :
Prop
Equations

- Nat.Linear.Poly.denote_eq ctx mp = (Nat.Linear.Poly.denote ctx mp.fst = Nat.Linear.Poly.denote ctx mp.snd)

Instances For

source
def Nat.Linear.Poly.denote_le (ctx : Context) (mp : Poly × Poly) :
Prop
Equations

- Nat.Linear.Poly.denote_le ctx mp = (Nat.Linear.Poly.denote ctx mp.fst ≤ Nat.Linear.Poly.denote ctx mp.snd)

Instances For

source
def Nat.Linear.Expr.toPoly (e : Expr) :
Poly
Equations

- e.toPoly = Nat.Linear.Expr.toPoly.go 1 e []

Instances For

source
def Nat.Linear.Expr.toPoly.go (coeff : Nat) :
Expr → Poly → Poly
Equations

- Nat.Linear.Expr.toPoly.go coeff (Nat.Linear.Expr.num k) = bif k == 0 then id else fun (x : Nat.Linear.Poly) => (coeff * k, Nat.Linear.fixedVar) :: x
- Nat.Linear.Expr.toPoly.go coeff (Nat.Linear.Expr.var i) = fun (x : Nat.Linear.Poly) => (coeff, i) :: x
- Nat.Linear.Expr.toPoly.go coeff (a.add b) = Nat.Linear.Expr.toPoly.go coeff a ∘ Nat.Linear.Expr.toPoly.go coeff b
- Nat.Linear.Expr.toPoly.go coeff (Nat.Linear.Expr.mulL k a) = bif k == 0 then id else Nat.Linear.Expr.toPoly.go (coeff * k) a
- Nat.Linear.Expr.toPoly.go coeff (a.mulR k) = bif k == 0 then id else Nat.Linear.Expr.toPoly.go (coeff * k) a

Instances For

source
def Nat.Linear.Expr.toNormPoly (e : Expr) :
Poly
Equations

- e.toNormPoly = e.toPoly.norm

Instances For

source
def Nat.Linear.Expr.inc (e : Expr) :
Expr
Equations

- e.inc = e.add (Nat.Linear.Expr.num 1)

Instances For

source
structure Nat.Linear.PolyCnstr :
Type

- eq : Bool
- lhs : Poly
- rhs : Poly

Instances For

source
instance Nat.Linear.instBEqPolyCnstr :
BEq PolyCnstr
Equations

- Nat.Linear.instBEqPolyCnstr = { beq := Nat.Linear.instBEqPolyCnstr.beq }

source
def Nat.Linear.instBEqPolyCnstr.beq :
PolyCnstr → PolyCnstr → Bool
Equations

- Nat.Linear.instBEqPolyCnstr.beq { eq := a, lhs := a_1, rhs := a_2 } { eq := b, lhs := b_1, rhs := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
- Nat.Linear.instBEqPolyCnstr.beq x✝¹ x✝ = false

Instances For

source
instance Nat.Linear.instReflBEqPolyCnstr :
ReflBEq PolyCnstr
source
instance Nat.Linear.instLawfulBEqPolyCnstr :
LawfulBEq PolyCnstr
source
structure Nat.Linear.ExprCnstr :
Type

- eq : Bool
- lhs : Expr
- rhs : Expr

Instances For

source
def Nat.Linear.PolyCnstr.denote (ctx : Context) (c : PolyCnstr) :
Prop
Equations

- Nat.Linear.PolyCnstr.denote ctx c = bif c.eq then Nat.Linear.Poly.denote_eq ctx (c.lhs, c.rhs) else Nat.Linear.Poly.denote_le ctx (c.lhs, c.rhs)

Instances For

source
def Nat.Linear.PolyCnstr.norm (c : PolyCnstr) :
PolyCnstr
Equations

- c.norm = match c.lhs.norm.cancel c.rhs.norm with | (lhs, rhs) => { eq := c.eq, lhs := lhs, rhs := rhs }

Instances For

source
def Nat.Linear.PolyCnstr.isUnsat (c : PolyCnstr) :
Bool
Equations

- c.isUnsat = bif c.eq then c.lhs.isZero && c.rhs.isNonZero || c.lhs.isNonZero && c.rhs.isZero else c.lhs.isNonZero && c.rhs.isZero

Instances For

source
def Nat.Linear.PolyCnstr.isValid (c : PolyCnstr) :
Bool
Equations

- c.isValid = bif c.eq then c.lhs.isZero && c.rhs.isZero else c.lhs.isZero

Instances For

source
def Nat.Linear.ExprCnstr.denote (ctx : Context) (c : ExprCnstr) :
Prop
Equations

- Nat.Linear.ExprCnstr.denote ctx c = bif c.eq then Nat.Linear.Expr.denote ctx c.lhs = Nat.Linear.Expr.denote ctx c.rhs else Nat.Linear.Expr.denote ctx c.lhs ≤ Nat.Linear.Expr.denote ctx c.rhs

Instances For

source
def Nat.Linear.ExprCnstr.toPoly (c : ExprCnstr) :
PolyCnstr
Equations

- c.toPoly = { eq := c.eq, lhs := c.lhs.toPoly, rhs := c.rhs.toPoly }

Instances For

source
def Nat.Linear.ExprCnstr.toNormPoly (c : ExprCnstr) :
PolyCnstr
Equations

- c.toNormPoly = match c.lhs.toNormPoly.cancel c.rhs.toNormPoly with | (lhs, rhs) => { eq := c.eq, lhs := lhs, rhs := rhs }

Instances For

source
def Nat.Linear.monomialToExpr (k : Nat) (v : Var) :
Expr
Equations

- Nat.Linear.monomialToExpr k v = bif v == Nat.Linear.fixedVar then Nat.Linear.Expr.num k else bif k == 1 then Nat.Linear.Expr.var v else Nat.Linear.Expr.mulL k (Nat.Linear.Expr.var v)

Instances For

source
def Nat.Linear.Poly.toExpr (p : Poly) :
Expr
Equations

- Nat.Linear.Poly.toExpr [] = Nat.Linear.Expr.num 0
- Nat.Linear.Poly.toExpr ((k, v) :: p_2) = Nat.Linear.Poly.toExpr.go (Nat.Linear.monomialToExpr k v) p_2

Instances For

source
def Nat.Linear.Poly.toExpr.go (e : Expr) (p : Poly) :
Expr
Equations

- Nat.Linear.Poly.toExpr.go e [] = e
- Nat.Linear.Poly.toExpr.go e ((k, v) :: p_2) = Nat.Linear.Poly.toExpr.go (e.add (Nat.Linear.monomialToExpr k v)) p_2

Instances For

source
def Nat.Linear.PolyCnstr.toExpr (c : PolyCnstr) :
ExprCnstr
Equations

- c.toExpr = { eq := c.eq, lhs := c.lhs.toExpr, rhs := c.rhs.toExpr }

Instances For

source
theorem Nat.Linear.Poly.denote_insert (ctx : Context) (k : Nat) (v : Var) (p : Poly) :
denote ctx (insert k v p) = denote ctx p + k * Var.denote ctx v
source
theorem Nat.Linear.Poly.denote_norm_go (ctx : Context) (p r : Poly) :
denote ctx (norm.go p r) = denote ctx p + denote ctx r
source
theorem Nat.Linear.Poly.denote_sort (ctx : Context) (m : Poly) :
denote ctx m.norm = denote ctx m
source
theorem Nat.Linear.Poly.denote_append (ctx : Context) (p q : Poly) :
denote ctx (p ++ q) = denote ctx p + denote ctx q
source
theorem Nat.Linear.Poly.denote_cons (ctx : Context) (k : Nat) (v : Var) (p : Poly) :
denote ctx ((k, v) :: p) = k * Var.denote ctx v + denote ctx p
source
theorem Nat.Linear.Poly.denote_reverse (ctx : Context) (p : Poly) :
denote ctx (List.reverse p) = denote ctx p
source
theorem Nat.Linear.Poly.denote_eq_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r₂ : Poly) (h : denote_eq ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)) :
denote_eq ctx (cancelAux fuel m₁ m₂ r₁ r₂)
source
theorem Nat.Linear.Poly.of_denote_eq_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r₂ : Poly) (h : denote_eq ctx (cancelAux fuel m₁ m₂ r₁ r₂)) :
denote_eq ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)
source
theorem Nat.Linear.Poly.denote_eq_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_eq ctx (m₁, m₂)) :
denote_eq ctx (m₁.cancel m₂)
source
theorem Nat.Linear.Poly.of_denote_eq_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_eq ctx (m₁.cancel m₂)) :
denote_eq ctx (m₁, m₂)
source
theorem Nat.Linear.Poly.denote_eq_cancel_eq (ctx : Context) (m₁ m₂ : Poly) :
denote_eq ctx (m₁.cancel m₂) = denote_eq ctx (m₁, m₂)
source
theorem Nat.Linear.Poly.denote_le_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r₂ : Poly) (h : denote_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)) :
denote_le ctx (cancelAux fuel m₁ m₂ r₁ r₂)
source
theorem Nat.Linear.Poly.of_denote_le_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r₂ : Poly) (h : denote_le ctx (cancelAux fuel m₁ m₂ r₁ r₂)) :
denote_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)
source
theorem Nat.Linear.Poly.denote_le_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_le ctx (m₁, m₂)) :
denote_le ctx (m₁.cancel m₂)
source
theorem Nat.Linear.Poly.of_denote_le_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_le ctx (m₁.cancel m₂)) :
denote_le ctx (m₁, m₂)
source
theorem Nat.Linear.Poly.denote_le_cancel_eq (ctx : Context) (m₁ m₂ : Poly) :
denote_le ctx (m₁.cancel m₂) = denote_le ctx (m₁, m₂)
source
theorem Nat.Linear.Expr.denote_toPoly_go {k : Nat} {p : Poly} (ctx : Context) (e : Expr) :
Poly.denote ctx (toPoly.go k e p) = k * denote ctx e + Poly.denote ctx p
source
theorem Nat.Linear.Expr.denote_toPoly (ctx : Context) (e : Expr) :
Poly.denote ctx e.toPoly = denote ctx e
source
theorem Nat.Linear.Expr.eq_of_toNormPoly (ctx : Context) (a b : Expr) (h : a.toNormPoly = b.toNormPoly) :
denote ctx a = denote ctx b
source
theorem Nat.Linear.Expr.of_cancel_eq (ctx : Context) (a b c d : Expr) (h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)) :
(denote ctx a = denote ctx b) = (denote ctx c = denote ctx d)
source
theorem Nat.Linear.Expr.of_cancel_le (ctx : Context) (a b c d : Expr) (h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)) :
(denote ctx a ≤ denote ctx b) = (denote ctx c ≤ denote ctx d)
source
theorem Nat.Linear.Expr.of_cancel_lt (ctx : Context) (a b c d : Expr) (h : a.inc.toNormPoly.cancel b.toNormPoly = (c.inc.toPoly, d.toPoly)) :
(denote ctx a < denote ctx b) = (denote ctx c < denote ctx d)
source
theorem Nat.Linear.ExprCnstr.toPoly_norm_eq (c : ExprCnstr) :
c.toPoly.norm = c.toNormPoly
source
theorem Nat.Linear.ExprCnstr.denote_toPoly (ctx : Context) (c : ExprCnstr) :
PolyCnstr.denote ctx c.toPoly = denote ctx c
source
theorem Nat.Linear.ExprCnstr.denote_toNormPoly (ctx : Context) (c : ExprCnstr) :
PolyCnstr.denote ctx c.toNormPoly = denote ctx c
source
theorem Nat.Linear.Poly.of_isZero (ctx : Context) {p : Poly} (h : p.isZero = true) :
denote ctx p = 0
source
theorem Nat.Linear.Poly.of_isNonZero (ctx : Context) {p : Poly} (h : p.isNonZero = true) :
denote ctx p > 0
source
theorem Nat.Linear.PolyCnstr.eq_false_of_isUnsat (ctx : Context) {c : PolyCnstr} :
c.isUnsat = true → denote ctx c = False
source
theorem Nat.Linear.PolyCnstr.eq_true_of_isValid (ctx : Context) {c : PolyCnstr} :
c.isValid = true → denote ctx c = True
source
theorem Nat.Linear.ExprCnstr.eq_false_of_isUnsat (ctx : Context) (c : ExprCnstr) (h : c.toNormPoly.isUnsat = true) :
denote ctx c = False
source
theorem Nat.Linear.ExprCnstr.eq_true_of_isValid (ctx : Context) (c : ExprCnstr) (h : c.toNormPoly.isValid = true) :
denote ctx c = True
source
theorem Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq (ctx : Context) (c d : ExprCnstr) (h : (c.toNormPoly == d.toPoly) = true) :
denote ctx c = denote ctx d
source
theorem Nat.Linear.Expr.eq_of_toNormPoly_eq (ctx : Context) (e e' : Expr) (h : (e.toNormPoly == e'.toPoly) = true) :
denote ctx e = denote ctx e'
source
def Nat.elimOffset {α : Sort u} (a b k : Nat) (h₁ : a + k = b + k) (h₂ : a = b → α) :
α
Equations

- a.elimOffset b k h₁ h₂ = h₂ ⋯

Instances For