Helper definitions and theorems for constructing linear arithmetic proofs.

@[reducible, inline]

abbrev Nat.Linear.Var : Type

Equations

• Nat.Linear.Var = Nat

@[reducible, inline]

abbrev Nat.Linear.Context : Type

Equations

• Nat.Linear.Context = List Nat

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

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

Equations

• Nat.Linear.Var.denote ctx v = bif v == Nat.Linear.fixedVar then 1 else Nat.Linear.Var.denote.go ctx v

def Nat.Linear.Var.denote.go : List Nat → Nat → Nat

Equations

• Nat.Linear.Var.denote.go [] x = 0
• Nat.Linear.Var.denote.go (a :: tail) 0 = a
• Nat.Linear.Var.denote.go (head :: as) i.succ = Nat.Linear.Var.denote.go as i

inductive Nat.Linear.Expr : Type

• num: Nat → Nat.Linear.Expr
• var: Nat.Linear.Var → Nat.Linear.Expr
• add: Nat.Linear.Expr → Nat.Linear.Expr → Nat.Linear.Expr
• mulL: Nat → Nat.Linear.Expr → Nat.Linear.Expr
• mulR: Nat.Linear.Expr → Nat → Nat.Linear.Expr

instance Nat.Linear.instInhabitedExpr : Inhabited Nat.Linear.Expr

Equations

• Nat.Linear.instInhabitedExpr = { default := Nat.Linear.Expr.num default }

def Nat.Linear.Expr.denote (ctx : Nat.Linear.Context) : Nat.Linear.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

@[reducible, inline]

abbrev Nat.Linear.Poly : Type

Equations

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

def Nat.Linear.Poly.denote (ctx : Nat.Linear.Context) (p : Nat.Linear.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)

def Nat.Linear.Poly.insertSorted (k : Nat) (v : Nat.Linear.Var) (p : Nat.Linear.Poly) : Nat.Linear.Poly

Equations

• Nat.Linear.Poly.insertSorted k v [] = [(k, v)]
• Nat.Linear.Poly.insertSorted k v ((k_1, v_1) :: p_2) = bif Nat.blt v v_1 then (k, v) :: (k_1, v_1) :: p_2 else (k_1, v_1) :: Nat.Linear.Poly.insertSorted k v p_2

def Nat.Linear.Poly.sort (p : Nat.Linear.Poly) : Nat.Linear.Poly

Equations

• p.sort = Nat.Linear.Poly.sort.go p []

def Nat.Linear.Poly.sort.go (p r : Nat.Linear.Poly) : Nat.Linear.Poly

Equations

• Nat.Linear.Poly.sort.go [] r = r
• Nat.Linear.Poly.sort.go ((k, v) :: p_2) r = Nat.Linear.Poly.sort.go p_2 (Nat.Linear.Poly.insertSorted k v r)

def Nat.Linear.Poly.fuse (p : Nat.Linear.Poly) : Nat.Linear.Poly

Equations

• Nat.Linear.Poly.fuse [] = []
• Nat.Linear.Poly.fuse ((k, v) :: p_2) = match Nat.Linear.Poly.fuse p_2 with | [] => [(k, v)] | (k', v') :: p' => bif v == v' then (k.add k', v) :: p' else (k, v) :: (k', v') :: p'

def Nat.Linear.Poly.mul (k : Nat) (p : Nat.Linear.Poly) : Nat.Linear.Poly

Equations

• Nat.Linear.Poly.mul k p = bif k == 0 then [] else bif k == 1 then p else Nat.Linear.Poly.mul.go k p

def Nat.Linear.Poly.mul.go (k : Nat) : Nat.Linear.Poly → Nat.Linear.Poly

Equations

• Nat.Linear.Poly.mul.go k [] = []
• Nat.Linear.Poly.mul.go k ((k_1, v) :: p_1) = (k.mul k_1, v) :: Nat.Linear.Poly.mul.go k p_1

def Nat.Linear.Poly.cancelAux (fuel : Nat) (m₁ m₂ r₁ r₂ : Nat.Linear.Poly) : Nat.Linear.Poly × Nat.Linear.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₂)

def Nat.Linear.hugeFuel : Nat

Equations

• Nat.Linear.hugeFuel = 1000000

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

Equations

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

def Nat.Linear.Poly.isNum? (p : Nat.Linear.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

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

Equations

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

def Nat.Linear.Poly.isNonZero (p : Nat.Linear.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

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

Equations

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

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

Equations

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

def Nat.Linear.Poly.combineAux (fuel : Nat) (p₁ p₂ : Nat.Linear.Poly) : Nat.Linear.Poly

Equations

• One or more equations did not get rendered due to their size.
• Nat.Linear.Poly.combineAux 0 p₁ p₂ = p₁ ++ p₂
• Nat.Linear.Poly.combineAux fuel_2.succ p₁ [] = p₁
• Nat.Linear.Poly.combineAux fuel_2.succ [] p₂ = p₂

def Nat.Linear.Poly.combine (p₁ p₂ : Nat.Linear.Poly) : Nat.Linear.Poly

Equations

• p₁.combine p₂ = Nat.Linear.Poly.combineAux Nat.Linear.hugeFuel p₁ p₂

def Nat.Linear.Expr.toPoly : Nat.Linear.Expr → Nat.Linear.Poly

Equations

• (Nat.Linear.Expr.num k).toPoly = bif k == 0 then [] else [(k, Nat.Linear.fixedVar)]
• (Nat.Linear.Expr.var i).toPoly = [(1, i)]
• (a.add b).toPoly = a.toPoly ++ b.toPoly
• (Nat.Linear.Expr.mulL k a).toPoly = Nat.Linear.Poly.mul k a.toPoly
• (a.mulR k).toPoly = Nat.Linear.Poly.mul k a.toPoly

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

Equations

• p.norm = p.sort.fuse

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

Equations

• e.toNormPoly = e.toPoly.norm

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

Equations

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

structure Nat.Linear.PolyCnstr : Type

• eq : Bool
• lhs : Nat.Linear.Poly
• rhs : Nat.Linear.Poly

instance Nat.Linear.instBEqPolyCnstr : BEq Nat.Linear.PolyCnstr

Equations

• Nat.Linear.instBEqPolyCnstr = { beq := Nat.Linear.beqPolyCnstr✝ }

instance Nat.Linear.instLawfulBEqPolyCnstr : LawfulBEq Nat.Linear.PolyCnstr

Equations

• Nat.Linear.instLawfulBEqPolyCnstr = ⋯

def Nat.Linear.PolyCnstr.mul (k : Nat) (c : Nat.Linear.PolyCnstr) : Nat.Linear.PolyCnstr

Equations

• Nat.Linear.PolyCnstr.mul k c = { eq := c.eq, lhs := Nat.Linear.Poly.mul k c.lhs, rhs := Nat.Linear.Poly.mul k c.rhs }

def Nat.Linear.PolyCnstr.combine (c₁ c₂ : Nat.Linear.PolyCnstr) : Nat.Linear.PolyCnstr

Equations

• c₁.combine c₂ = match (c₁.lhs.combine c₂.lhs).cancel (c₁.rhs.combine c₂.rhs) with | (lhs, rhs) => { eq := c₁.eq && c₂.eq, lhs := lhs, rhs := rhs }

structure Nat.Linear.ExprCnstr : Type

• eq : Bool
• lhs : Nat.Linear.Expr
• rhs : Nat.Linear.Expr

def Nat.Linear.PolyCnstr.denote (ctx : Nat.Linear.Context) (c : Nat.Linear.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)

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

Equations

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

def Nat.Linear.PolyCnstr.isUnsat (c : Nat.Linear.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

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

Equations

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

def Nat.Linear.ExprCnstr.denote (ctx : Nat.Linear.Context) (c : Nat.Linear.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

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

Equations

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

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

Equations

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

@[reducible, inline]

abbrev Nat.Linear.Certificate : Type

Equations

• Nat.Linear.Certificate = List (Nat × Nat.Linear.ExprCnstr)

def Nat.Linear.Certificate.combineHyps (c : Nat.Linear.PolyCnstr) (hs : Nat.Linear.Certificate) : Nat.Linear.PolyCnstr

Equations

• Nat.Linear.Certificate.combineHyps c [] = c
• Nat.Linear.Certificate.combineHyps c ((k, c') :: hs_2) = Nat.Linear.Certificate.combineHyps (c.combine (Nat.Linear.PolyCnstr.mul (k.add 1) c'.toNormPoly)) hs_2

def Nat.Linear.Certificate.combine (hs : Nat.Linear.Certificate) : Nat.Linear.PolyCnstr

Equations

• Nat.Linear.Certificate.combine [] = { eq := true, lhs := [], rhs := [] }
• Nat.Linear.Certificate.combine ((k, c') :: hs_2) = Nat.Linear.Certificate.combineHyps (Nat.Linear.PolyCnstr.mul (k.add 1) c'.toNormPoly) hs_2

def Nat.Linear.Certificate.denote (ctx : Nat.Linear.Context) (c : Nat.Linear.Certificate) : Prop

Equations

• Nat.Linear.Certificate.denote ctx [] = False
• Nat.Linear.Certificate.denote ctx ((k, c') :: hs_1) = (Nat.Linear.ExprCnstr.denote ctx c' → Nat.Linear.Certificate.denote ctx hs_1)

def Nat.Linear.monomialToExpr (k : Nat) (v : Nat.Linear.Var) : Nat.Linear.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)

def Nat.Linear.Poly.toExpr (p : Nat.Linear.Poly) : Nat.Linear.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

def Nat.Linear.Poly.toExpr.go (e : Nat.Linear.Expr) (p : Nat.Linear.Poly) : Nat.Linear.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

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

Equations

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

theorem Nat.Linear.Poly.denote_insertSorted (ctx : Nat.Linear.Context) (k : Nat) (v : Nat.Linear.Var) (p : Nat.Linear.Poly) : Nat.Linear.Poly.denote ctx (Nat.Linear.Poly.insertSorted k v p) = Nat.Linear.Poly.denote ctx p + k * Nat.Linear.Var.denote ctx v

theorem Nat.Linear.Poly.denote_sort_go (ctx : Nat.Linear.Context) (p r : Nat.Linear.Poly) : Nat.Linear.Poly.denote ctx (Nat.Linear.Poly.sort.go p r) = Nat.Linear.Poly.denote ctx p + Nat.Linear.Poly.denote ctx r

theorem Nat.Linear.Poly.denote_sort (ctx : Nat.Linear.Context) (m : Nat.Linear.Poly) : Nat.Linear.Poly.denote ctx m.sort = Nat.Linear.Poly.denote ctx m

theorem Nat.Linear.Poly.denote_append (ctx : Nat.Linear.Context) (p q : Nat.Linear.Poly) : Nat.Linear.Poly.denote ctx (p ++ q) = Nat.Linear.Poly.denote ctx p + Nat.Linear.Poly.denote ctx q

theorem Nat.Linear.Poly.denote_cons (ctx : Nat.Linear.Context) (k : Nat) (v : Nat.Linear.Var) (p : Nat.Linear.Poly) : Nat.Linear.Poly.denote ctx ((k, v) :: p) = k * Nat.Linear.Var.denote ctx v + Nat.Linear.Poly.denote ctx p

theorem Nat.Linear.Poly.denote_reverseAux (ctx : Nat.Linear.Context) (p q : Nat.Linear.Poly) : Nat.Linear.Poly.denote ctx (List.reverseAux p q) = Nat.Linear.Poly.denote ctx (p ++ q)

theorem Nat.Linear.Poly.denote_reverse (ctx : Nat.Linear.Context) (p : Nat.Linear.Poly) : Nat.Linear.Poly.denote ctx (List.reverse p) = Nat.Linear.Poly.denote ctx p

theorem Nat.Linear.Poly.denote_fuse (ctx : Nat.Linear.Context) (p : Nat.Linear.Poly) : Nat.Linear.Poly.denote ctx p.fuse = Nat.Linear.Poly.denote ctx p

theorem Nat.Linear.Poly.denote_mul (ctx : Nat.Linear.Context) (k : Nat) (p : Nat.Linear.Poly) : Nat.Linear.Poly.denote ctx (Nat.Linear.Poly.mul k p) = k * Nat.Linear.Poly.denote ctx p

theorem Nat.Linear.Poly.denote_eq_cancelAux (ctx : Nat.Linear.Context) (fuel : Nat) (m₁ m₂ r₁ r₂ : Nat.Linear.Poly) (h : Nat.Linear.Poly.denote_eq ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)) : Nat.Linear.Poly.denote_eq ctx (Nat.Linear.Poly.cancelAux fuel m₁ m₂ r₁ r₂)

theorem Nat.Linear.Poly.of_denote_eq_cancelAux (ctx : Nat.Linear.Context) (fuel : Nat) (m₁ m₂ r₁ r₂ : Nat.Linear.Poly) (h : Nat.Linear.Poly.denote_eq ctx (Nat.Linear.Poly.cancelAux fuel m₁ m₂ r₁ r₂)) : Nat.Linear.Poly.denote_eq ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)

theorem Nat.Linear.Poly.denote_eq_cancel {ctx : Nat.Linear.Context} {m₁ m₂ : Nat.Linear.Poly} (h : Nat.Linear.Poly.denote_eq ctx (m₁, m₂)) : Nat.Linear.Poly.denote_eq ctx (m₁.cancel m₂)

theorem Nat.Linear.Poly.of_denote_eq_cancel {ctx : Nat.Linear.Context} {m₁ m₂ : Nat.Linear.Poly} (h : Nat.Linear.Poly.denote_eq ctx (m₁.cancel m₂)) : Nat.Linear.Poly.denote_eq ctx (m₁, m₂)

theorem Nat.Linear.Poly.denote_eq_cancel_eq (ctx : Nat.Linear.Context) (m₁ m₂ : Nat.Linear.Poly) : Nat.Linear.Poly.denote_eq ctx (m₁.cancel m₂) = Nat.Linear.Poly.denote_eq ctx (m₁, m₂)

theorem Nat.Linear.Poly.denote_le_cancelAux (ctx : Nat.Linear.Context) (fuel : Nat) (m₁ m₂ r₁ r₂ : Nat.Linear.Poly) (h : Nat.Linear.Poly.denote_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)) : Nat.Linear.Poly.denote_le ctx (Nat.Linear.Poly.cancelAux fuel m₁ m₂ r₁ r₂)

theorem Nat.Linear.Poly.of_denote_le_cancelAux (ctx : Nat.Linear.Context) (fuel : Nat) (m₁ m₂ r₁ r₂ : Nat.Linear.Poly) (h : Nat.Linear.Poly.denote_le ctx (Nat.Linear.Poly.cancelAux fuel m₁ m₂ r₁ r₂)) : Nat.Linear.Poly.denote_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)

theorem Nat.Linear.Poly.denote_le_cancel {ctx : Nat.Linear.Context} {m₁ m₂ : Nat.Linear.Poly} (h : Nat.Linear.Poly.denote_le ctx (m₁, m₂)) : Nat.Linear.Poly.denote_le ctx (m₁.cancel m₂)

theorem Nat.Linear.Poly.of_denote_le_cancel {ctx : Nat.Linear.Context} {m₁ m₂ : Nat.Linear.Poly} (h : Nat.Linear.Poly.denote_le ctx (m₁.cancel m₂)) : Nat.Linear.Poly.denote_le ctx (m₁, m₂)

theorem Nat.Linear.Poly.denote_le_cancel_eq (ctx : Nat.Linear.Context) (m₁ m₂ : Nat.Linear.Poly) : Nat.Linear.Poly.denote_le ctx (m₁.cancel m₂) = Nat.Linear.Poly.denote_le ctx (m₁, m₂)

theorem Nat.Linear.Poly.denote_combineAux (ctx : Nat.Linear.Context) (fuel : Nat) (p₁ p₂ : Nat.Linear.Poly) : Nat.Linear.Poly.denote ctx (Nat.Linear.Poly.combineAux fuel p₁ p₂) = Nat.Linear.Poly.denote ctx p₁ + Nat.Linear.Poly.denote ctx p₂

theorem Nat.Linear.Poly.denote_combine (ctx : Nat.Linear.Context) (p₁ p₂ : Nat.Linear.Poly) : Nat.Linear.Poly.denote ctx (p₁.combine p₂) = Nat.Linear.Poly.denote ctx p₁ + Nat.Linear.Poly.denote ctx p₂

theorem Nat.Linear.Expr.denote_toPoly (ctx : Nat.Linear.Context) (e : Nat.Linear.Expr) : Nat.Linear.Poly.denote ctx e.toPoly = Nat.Linear.Expr.denote ctx e

theorem Nat.Linear.Expr.eq_of_toNormPoly (ctx : Nat.Linear.Context) (a b : Nat.Linear.Expr) (h : a.toNormPoly = b.toNormPoly) : Nat.Linear.Expr.denote ctx a = Nat.Linear.Expr.denote ctx b

theorem Nat.Linear.Expr.of_cancel_eq (ctx : Nat.Linear.Context) (a b c d : Nat.Linear.Expr) (h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)) : (Nat.Linear.Expr.denote ctx a = Nat.Linear.Expr.denote ctx b) = (Nat.Linear.Expr.denote ctx c = Nat.Linear.Expr.denote ctx d)

theorem Nat.Linear.Expr.of_cancel_le (ctx : Nat.Linear.Context) (a b c d : Nat.Linear.Expr) (h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)) : (Nat.Linear.Expr.denote ctx a ≤ Nat.Linear.Expr.denote ctx b) = (Nat.Linear.Expr.denote ctx c ≤ Nat.Linear.Expr.denote ctx d)

theorem Nat.Linear.Expr.of_cancel_lt (ctx : Nat.Linear.Context) (a b c d : Nat.Linear.Expr) (h : a.inc.toNormPoly.cancel b.toNormPoly = (c.inc.toPoly, d.toPoly)) : (Nat.Linear.Expr.denote ctx a < Nat.Linear.Expr.denote ctx b) = (Nat.Linear.Expr.denote ctx c < Nat.Linear.Expr.denote ctx d)

theorem Nat.Linear.ExprCnstr.toPoly_norm_eq (c : Nat.Linear.ExprCnstr) : c.toPoly.norm = c.toNormPoly

theorem Nat.Linear.ExprCnstr.denote_toPoly (ctx : Nat.Linear.Context) (c : Nat.Linear.ExprCnstr) : Nat.Linear.PolyCnstr.denote ctx c.toPoly = Nat.Linear.ExprCnstr.denote ctx c

theorem Nat.Linear.ExprCnstr.denote_toNormPoly (ctx : Nat.Linear.Context) (c : Nat.Linear.ExprCnstr) : Nat.Linear.PolyCnstr.denote ctx c.toNormPoly = Nat.Linear.ExprCnstr.denote ctx c

theorem Nat.Linear.Poly.mul.go_denote (ctx : Nat.Linear.Context) (k : Nat) (p : Nat.Linear.Poly) : Nat.Linear.Poly.denote ctx (Nat.Linear.Poly.mul.go k p) = k * Nat.Linear.Poly.denote ctx p

theorem Nat.Linear.PolyCnstr.denote_mul (ctx : Nat.Linear.Context) (k : Nat) (c : Nat.Linear.PolyCnstr) : Nat.Linear.PolyCnstr.denote ctx (Nat.Linear.PolyCnstr.mul (k + 1) c) = Nat.Linear.PolyCnstr.denote ctx c

theorem Nat.Linear.PolyCnstr.denote_combine {ctx : Nat.Linear.Context} {c₁ c₂ : Nat.Linear.PolyCnstr} (h₁ : Nat.Linear.PolyCnstr.denote ctx c₁) (h₂ : Nat.Linear.PolyCnstr.denote ctx c₂) : Nat.Linear.PolyCnstr.denote ctx (c₁.combine c₂)

theorem Nat.Linear.Poly.isNum?_eq_some (ctx : Nat.Linear.Context) {p : Nat.Linear.Poly} {k : Nat} : p.isNum? = some k → Nat.Linear.Poly.denote ctx p = k

theorem Nat.Linear.Poly.of_isZero (ctx : Nat.Linear.Context) {p : Nat.Linear.Poly} (h : p.isZero = true) : Nat.Linear.Poly.denote ctx p = 0

theorem Nat.Linear.Poly.of_isNonZero (ctx : Nat.Linear.Context) {p : Nat.Linear.Poly} (h : p.isNonZero = true) : Nat.Linear.Poly.denote ctx p > 0

theorem Nat.Linear.PolyCnstr.eq_false_of_isUnsat (ctx : Nat.Linear.Context) {c : Nat.Linear.PolyCnstr} : c.isUnsat = true → Nat.Linear.PolyCnstr.denote ctx c = False

theorem Nat.Linear.PolyCnstr.eq_true_of_isValid (ctx : Nat.Linear.Context) {c : Nat.Linear.PolyCnstr} : c.isValid = true → Nat.Linear.PolyCnstr.denote ctx c = True

theorem Nat.Linear.ExprCnstr.eq_false_of_isUnsat (ctx : Nat.Linear.Context) (c : Nat.Linear.ExprCnstr) (h : c.toNormPoly.isUnsat = true) : Nat.Linear.ExprCnstr.denote ctx c = False

theorem Nat.Linear.ExprCnstr.eq_true_of_isValid (ctx : Nat.Linear.Context) (c : Nat.Linear.ExprCnstr) (h : c.toNormPoly.isValid = true) : Nat.Linear.ExprCnstr.denote ctx c = True

theorem Nat.Linear.Certificate.of_combineHyps (ctx : Nat.Linear.Context) (c : Nat.Linear.PolyCnstr) (cs : Nat.Linear.Certificate) (h : Nat.Linear.PolyCnstr.denote ctx (Nat.Linear.Certificate.combineHyps c cs) → False) : Nat.Linear.PolyCnstr.denote ctx c → Nat.Linear.Certificate.denote ctx cs

theorem Nat.Linear.Certificate.of_combine (ctx : Nat.Linear.Context) (cs : Nat.Linear.Certificate) (h : Nat.Linear.PolyCnstr.denote ctx cs.combine → False) : Nat.Linear.Certificate.denote ctx cs

theorem Nat.Linear.Certificate.of_combine_isUnsat (ctx : Nat.Linear.Context) (cs : Nat.Linear.Certificate) (h : cs.combine.isUnsat = true) : Nat.Linear.Certificate.denote ctx cs

theorem Nat.Linear.denote_monomialToExpr (ctx : Nat.Linear.Context) (k : Nat) (v : Nat.Linear.Var) : Nat.Linear.Expr.denote ctx (Nat.Linear.monomialToExpr k v) = k * Nat.Linear.Var.denote ctx v

theorem Nat.Linear.Poly.denote_toExpr_go (ctx : Nat.Linear.Context) (e : Nat.Linear.Expr) (p : Nat.Linear.Poly) : Nat.Linear.Expr.denote ctx (Nat.Linear.Poly.toExpr.go e p) = Nat.Linear.Expr.denote ctx e + Nat.Linear.Poly.denote ctx p

theorem Nat.Linear.Poly.denote_toExpr (ctx : Nat.Linear.Context) (p : Nat.Linear.Poly) : Nat.Linear.Expr.denote ctx p.toExpr = Nat.Linear.Poly.denote ctx p

theorem Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq (ctx : Nat.Linear.Context) (c d : Nat.Linear.ExprCnstr) (h : (c.toNormPoly == d.toPoly) = true) : Nat.Linear.ExprCnstr.denote ctx c = Nat.Linear.ExprCnstr.denote ctx d

theorem Nat.Linear.Expr.eq_of_toNormPoly_eq (ctx : Nat.Linear.Context) (e e' : Nat.Linear.Expr) (h : (e.toNormPoly == e'.toPoly) = true) : Nat.Linear.Expr.denote ctx e = Nat.Linear.Expr.denote ctx e'

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₂ ⋯