Init.Data.Nat.Linear

source

@[inline]

abbrev Nat.Linear.Var :

Type

Equations

Nat.Linear.Var = Nat

! Helper definitions and theorems for constructing linear arithmetic proofs.

source

@[inline]

abbrev Nat.Linear.Context :

Type

Equations

Nat.Linear.Context = List Nat

source

def Nat.Linear.fixedVar :

Nat

Equations

Nat.Linear.fixedVar = 100000000

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

source

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

Nat

Equations

Nat.Linear.Var.denote ctx v = cond (v == Nat.Linear.fixedVar) 1 (Nat.Linear.Var.denote.go ctx v)

source

def Nat.Linear.Var.denote.go :

List Nat → Nat → Nat

Equations

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

source

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

source

instance Nat.Linear.instInhabitedExpr :

Inhabited Nat.Linear.Expr

Equations

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

source

def Nat.Linear.Expr.denote (ctx : Nat.Linear.Context) :

Nat.Linear.Expr → Nat

Equations

Nat.Linear.Expr.denote ctx (Nat.Linear.Expr.add a b) = Nat.add (Nat.Linear.Expr.denote ctx a) (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) = Nat.mul k (Nat.Linear.Expr.denote ctx e)
Nat.Linear.Expr.denote ctx (Nat.Linear.Expr.mulR e k) = Nat.mul (Nat.Linear.Expr.denote ctx e) k

source

@[inline]

abbrev Nat.Linear.Poly :

Type

Equations

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

source

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) = Nat.add (Nat.mul k (Nat.Linear.Var.denote ctx v)) (Nat.Linear.Poly.denote ctx p_2)

source

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) = cond (Nat.blt v v_1) ((k, v) :: (k_1, v_1) :: p_2) ((k_1, v_1) :: Nat.Linear.Poly.insertSorted k v p_2)

source

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

Nat.Linear.Poly

Equations

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

source

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

source

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' => cond (v == v') ((Nat.add k k', v) :: p') ((k, v) :: (k', v') :: p')

source

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

Nat.Linear.Poly

Equations

Nat.Linear.Poly.mul k p = cond (k == 0) [] (cond (k == 1) p (Nat.Linear.Poly.mul.go k p))

source

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) = (Nat.mul k k_1, v) :: Nat.Linear.Poly.mul.go k p_1

source

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

Nat.Linear.Poly × Nat.Linear.Poly

Equations

Nat.Linear.Poly.cancelAux 0 m₁ m₂ r₁ r₂ = (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)
Nat.Linear.Poly.cancelAux (Nat.succ fuel_2) m₁ [] r₁ r₂ = (List.reverse r₁ ++ m₁, List.reverse r₂)
Nat.Linear.Poly.cancelAux (Nat.succ fuel_2) [] m₂ r₁ r₂ = (List.reverse r₁, List.reverse r₂ ++ m₂)
Nat.Linear.Poly.cancelAux (Nat.succ fuel_2) ((k₁, v₁) :: m₁_2) ((k₂, v₂) :: m₂_2) r₁ r₂ = cond (Nat.blt v₁ v₂) (Nat.Linear.Poly.cancelAux fuel_2 m₁_2 ((k₂, v₂) :: m₂_2) ((k₁, v₁) :: r₁) r₂) (cond (Nat.blt v₂ v₁) (Nat.Linear.Poly.cancelAux fuel_2 ((k₁, v₁) :: m₁_2) m₂_2 r₁ ((k₂, v₂) :: r₂)) (cond (Nat.blt k₁ k₂) (Nat.Linear.Poly.cancelAux fuel_2 m₁_2 m₂_2 r₁ ((Nat.sub k₂ k₁, v₁) :: r₂)) (cond (Nat.blt k₂ k₁) (Nat.Linear.Poly.cancelAux fuel_2 m₁_2 m₂_2 ((Nat.sub k₁ k₂, v₁) :: r₁) r₂) (Nat.Linear.Poly.cancelAux fuel_2 m₁_2 m₂_2 r₁ r₂))))

source

def Nat.Linear.hugeFuel :

Nat

Equations

Nat.Linear.hugeFuel = 1000000

source

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

Nat.Linear.Poly × Nat.Linear.Poly

Equations

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

source

def Nat.Linear.Poly.isNum? (p : Nat.Linear.Poly) :

Option Nat

Equations

Nat.Linear.Poly.isNum? p = match p with | [] => some 0 | [(k, v)] => cond (v == Nat.Linear.fixedVar) (some k) none | x => none

source

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

Bool

Equations

Nat.Linear.Poly.isZero p = match p with | [] => true | x => false

source

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

Bool

Equations

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

source

noncomputable 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)

source

noncomputable 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)

source

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

Nat.Linear.Poly

Equations

Nat.Linear.Poly.combineAux 0 p₁ p₂ = p₁ ++ p₂
Nat.Linear.Poly.combineAux (Nat.succ fuel_2) p₁ [] = p₁
Nat.Linear.Poly.combineAux (Nat.succ fuel_2) [] p₂ = p₂
Nat.Linear.Poly.combineAux (Nat.succ fuel_2) ((k₁, v₁) :: m₁_1) ((k₂, v₂) :: m₂_1) = cond (Nat.blt v₁ v₂) ((k₁, v₁) :: Nat.Linear.Poly.combineAux fuel_2 m₁_1 ((k₂, v₂) :: m₂_1)) (cond (Nat.blt v₂ v₁) ((k₂, v₂) :: Nat.Linear.Poly.combineAux fuel_2 ((k₁, v₁) :: m₁_1) m₂_1) ((Nat.add k₁ k₂, v₁) :: Nat.Linear.Poly.combineAux fuel_2 m₁_1 m₂_1))

source

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

Nat.Linear.Poly

Equations

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

source

def Nat.Linear.Expr.toPoly :

Nat.Linear.Expr → Nat.Linear.Poly

Equations

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

source

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

Nat.Linear.Poly

Equations

Nat.Linear.Poly.norm p = Nat.Linear.Poly.fuse (Nat.Linear.Poly.sort p)

source

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

Nat.Linear.Poly

Equations

Nat.Linear.Expr.toNormPoly e = Nat.Linear.Poly.norm (Nat.Linear.Expr.toPoly e)

source

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

Nat.Linear.Expr

Equations

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

source

structure Nat.Linear.PolyCnstr :

Type

source

instance Nat.Linear.instBEqPolyCnstr :

BEq Nat.Linear.PolyCnstr

Equations

Nat.Linear.instBEqPolyCnstr = { beq := [anonymous] }

source

noncomputable instance Nat.Linear.instLawfulBEqPolyCnstrInstBEqPolyCnstr :

LawfulBEq Nat.Linear.PolyCnstr

Equations

Nat.Linear.instLawfulBEqPolyCnstrInstBEqPolyCnstr = Nat.Linear.instLawfulBEqPolyCnstrInstBEqPolyCnstr.proof_1

source

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 }

source

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

Nat.Linear.PolyCnstr

Equations

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

source

structure Nat.Linear.ExprCnstr :

Type

source

noncomputable def Nat.Linear.PolyCnstr.denote (ctx : Nat.Linear.Context) (c : Nat.Linear.PolyCnstr) :

Prop

Equations

Nat.Linear.PolyCnstr.denote ctx c = cond c.eq (Nat.Linear.Poly.denote_eq ctx (c.lhs, c.rhs)) (Nat.Linear.Poly.denote_le ctx (c.lhs, c.rhs))

source

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

Nat.Linear.PolyCnstr

Equations

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

source

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

Bool

Equations

Nat.Linear.PolyCnstr.isUnsat c = cond c.eq (Nat.Linear.Poly.isZero c.lhs && Nat.Linear.Poly.isNonZero c.rhs || Nat.Linear.Poly.isNonZero c.lhs && Nat.Linear.Poly.isZero c.rhs) (Nat.Linear.Poly.isNonZero c.lhs && Nat.Linear.Poly.isZero c.rhs)

source

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

Bool

Equations

Nat.Linear.PolyCnstr.isValid c = cond c.eq (Nat.Linear.Poly.isZero c.lhs && Nat.Linear.Poly.isZero c.rhs) (Nat.Linear.Poly.isZero c.lhs)

source

noncomputable def Nat.Linear.ExprCnstr.denote (ctx : Nat.Linear.Context) (c : Nat.Linear.ExprCnstr) :

Prop

Equations

Nat.Linear.ExprCnstr.denote ctx c = cond c.eq (Nat.Linear.Expr.denote ctx c.lhs = Nat.Linear.Expr.denote ctx c.rhs) (Nat.Linear.Expr.denote ctx c.lhs ≤ Nat.Linear.Expr.denote ctx c.rhs)

source

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

Nat.Linear.PolyCnstr

Equations

Nat.Linear.ExprCnstr.toPoly c = { eq := c.eq, lhs := Nat.Linear.Expr.toPoly c.lhs, rhs := Nat.Linear.Expr.toPoly c.rhs }

source

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

Nat.Linear.PolyCnstr

Equations

Nat.Linear.ExprCnstr.toNormPoly c = match Nat.Linear.Poly.cancel (Nat.Linear.Expr.toNormPoly c.lhs) (Nat.Linear.Expr.toNormPoly c.rhs) with | (lhs, rhs) => { eq := c.eq, lhs := lhs, rhs := rhs }

source

@[inline]

abbrev Nat.Linear.Certificate :

Type

Equations

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

source

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 (Nat.Linear.PolyCnstr.combine c (Nat.Linear.PolyCnstr.mul (Nat.add k 1) (Nat.Linear.ExprCnstr.toNormPoly c'))) hs_2

source

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

Nat.Linear.PolyCnstr

Equations

Nat.Linear.Certificate.combine hs = match hs with | [] => { eq := true, lhs := [], rhs := [] } | (k, c) :: hs => Nat.Linear.Certificate.combineHyps (Nat.Linear.PolyCnstr.mul (Nat.add k 1) (Nat.Linear.ExprCnstr.toNormPoly c)) hs

source

noncomputable 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)

source

def Nat.Linear.monomialToExpr (k : Nat) (v : Nat.Linear.Var) :

Nat.Linear.Expr

Equations

Nat.Linear.monomialToExpr k v = cond (v == Nat.Linear.fixedVar) (Nat.Linear.Expr.num k) (cond (k == 1) (Nat.Linear.Expr.var v) (Nat.Linear.Expr.mulL k (Nat.Linear.Expr.var v)))

source

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

Nat.Linear.Expr

Equations

Nat.Linear.Poly.toExpr p = match p with | [] => Nat.Linear.Expr.num 0 | (k, v) :: p => Nat.Linear.Poly.toExpr.go (Nat.Linear.monomialToExpr k v) p

source

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 (Nat.Linear.Expr.add e (Nat.Linear.monomialToExpr k v)) p_2

source

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

Nat.Linear.ExprCnstr

Equations

Nat.Linear.PolyCnstr.toExpr c = { eq := c.eq, lhs := Nat.Linear.Poly.toExpr c.lhs, rhs := Nat.Linear.Poly.toExpr c.rhs }

source

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

source

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

source

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

Nat.Linear.Poly.denote ctx (Nat.Linear.Poly.sort m) = Nat.Linear.Poly.denote ctx m

source

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

Nat.Linear.Poly.denote ctx (p ++ q) = Nat.Linear.Poly.denote ctx p + Nat.Linear.Poly.denote ctx q

source

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

source

theorem Nat.Linear.Poly.denote_reverseAux (ctx : Nat.Linear.Context) (p : Nat.Linear.Poly) (q : Nat.Linear.Poly) :

Nat.Linear.Poly.denote ctx (List.reverseAux p q) = Nat.Linear.Poly.denote ctx (p ++ q)

source

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

source

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

Nat.Linear.Poly.denote ctx (Nat.Linear.Poly.fuse p) = Nat.Linear.Poly.denote ctx p

source

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

source

theorem Nat.Linear.Poly.denote_eq_cancelAux (ctx : Nat.Linear.Context) (fuel : Nat) (m₁ : Nat.Linear.Poly) (m₂ : Nat.Linear.Poly) (r₁ : Nat.Linear.Poly) (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₂)

source

theorem Nat.Linear.Poly.of_denote_eq_cancelAux (ctx : Nat.Linear.Context) (fuel : Nat) (m₁ : Nat.Linear.Poly) (m₂ : Nat.Linear.Poly) (r₁ : Nat.Linear.Poly) (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₂)

source

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

Nat.Linear.Poly.denote_eq ctx (Nat.Linear.Poly.cancel m₁ m₂)

source

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

Nat.Linear.Poly.denote_eq ctx (m₁, m₂)

source

theorem Nat.Linear.Poly.denote_eq_cancel_eq (ctx : Nat.Linear.Context) (m₁ : Nat.Linear.Poly) (m₂ : Nat.Linear.Poly) :

Nat.Linear.Poly.denote_eq ctx (Nat.Linear.Poly.cancel m₁ m₂) = Nat.Linear.Poly.denote_eq ctx (m₁, m₂)

source

theorem Nat.Linear.Poly.denote_le_cancelAux (ctx : Nat.Linear.Context) (fuel : Nat) (m₁ : Nat.Linear.Poly) (m₂ : Nat.Linear.Poly) (r₁ : Nat.Linear.Poly) (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₂)

source

theorem Nat.Linear.Poly.of_denote_le_cancelAux (ctx : Nat.Linear.Context) (fuel : Nat) (m₁ : Nat.Linear.Poly) (m₂ : Nat.Linear.Poly) (r₁ : Nat.Linear.Poly) (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₂)

source

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

Nat.Linear.Poly.denote_le ctx (Nat.Linear.Poly.cancel m₁ m₂)

source

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

Nat.Linear.Poly.denote_le ctx (m₁, m₂)

source

theorem Nat.Linear.Poly.denote_le_cancel_eq (ctx : Nat.Linear.Context) (m₁ : Nat.Linear.Poly) (m₂ : Nat.Linear.Poly) :

Nat.Linear.Poly.denote_le ctx (Nat.Linear.Poly.cancel m₁ m₂) = Nat.Linear.Poly.denote_le ctx (m₁, m₂)

source

theorem Nat.Linear.Poly.denote_combineAux (ctx : Nat.Linear.Context) (fuel : Nat) (p₁ : Nat.Linear.Poly) (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₂

source

theorem Nat.Linear.Poly.denote_combine (ctx : Nat.Linear.Context) (p₁ : Nat.Linear.Poly) (p₂ : Nat.Linear.Poly) :

Nat.Linear.Poly.denote ctx (Nat.Linear.Poly.combine p₁ p₂) = Nat.Linear.Poly.denote ctx p₁ + Nat.Linear.Poly.denote ctx p₂

source

theorem Nat.Linear.Expr.denote_toPoly (ctx : Nat.Linear.Context) (e : Nat.Linear.Expr) :

Nat.Linear.Poly.denote ctx (Nat.Linear.Expr.toPoly e) = Nat.Linear.Expr.denote ctx e

source

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

Nat.Linear.Expr.denote ctx a = Nat.Linear.Expr.denote ctx b

source

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

(Nat.Linear.Expr.denote ctx a = Nat.Linear.Expr.denote ctx b) = (Nat.Linear.Expr.denote ctx c = Nat.Linear.Expr.denote ctx d)

source

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

(Nat.Linear.Expr.denote ctx a ≤ Nat.Linear.Expr.denote ctx b) = (Nat.Linear.Expr.denote ctx c ≤ Nat.Linear.Expr.denote ctx d)

source

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

(Nat.Linear.Expr.denote ctx a < Nat.Linear.Expr.denote ctx b) = (Nat.Linear.Expr.denote ctx c < Nat.Linear.Expr.denote ctx d)

source

theorem Nat.Linear.ExprCnstr.toPoly_norm_eq (c : Nat.Linear.ExprCnstr) :

Nat.Linear.PolyCnstr.norm (Nat.Linear.ExprCnstr.toPoly c) = Nat.Linear.ExprCnstr.toNormPoly c

source

theorem Nat.Linear.ExprCnstr.denote_toPoly (ctx : Nat.Linear.Context) (c : Nat.Linear.ExprCnstr) :

Nat.Linear.PolyCnstr.denote ctx (Nat.Linear.ExprCnstr.toPoly c) = Nat.Linear.ExprCnstr.denote ctx c

source

theorem Nat.Linear.ExprCnstr.denote_toNormPoly (ctx : Nat.Linear.Context) (c : Nat.Linear.ExprCnstr) :

Nat.Linear.PolyCnstr.denote ctx (Nat.Linear.ExprCnstr.toNormPoly c) = Nat.Linear.ExprCnstr.denote ctx c

source

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

source

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

source

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

Nat.Linear.PolyCnstr.denote ctx (Nat.Linear.PolyCnstr.combine c₁ c₂)

source

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

Nat.Linear.Poly.isNum? p = some k → Nat.Linear.Poly.denote ctx p = k

source

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

Nat.Linear.Poly.denote ctx p = 0

source

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

Nat.Linear.Poly.denote ctx p > 0

source

theorem Nat.Linear.PolyCnstr.eq_false_of_isUnsat (ctx : Nat.Linear.Context) {c : Nat.Linear.PolyCnstr} :

Nat.Linear.PolyCnstr.isUnsat c = true → Nat.Linear.PolyCnstr.denote ctx c = False

source

theorem Nat.Linear.PolyCnstr.eq_true_of_isValid (ctx : Nat.Linear.Context) {c : Nat.Linear.PolyCnstr} :

Nat.Linear.PolyCnstr.isValid c = true → Nat.Linear.PolyCnstr.denote ctx c = True

source

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

Nat.Linear.ExprCnstr.denote ctx c = False

source

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

Nat.Linear.ExprCnstr.denote ctx c = True

source

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

source

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

Nat.Linear.Certificate.denote ctx cs

source

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

Nat.Linear.Certificate.denote ctx cs

source

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

source

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

source

theorem Nat.Linear.Poly.denote_toExpr (ctx : Nat.Linear.Context) (p : Nat.Linear.Poly) :

Nat.Linear.Expr.denote ctx (Nat.Linear.Poly.toExpr p) = Nat.Linear.Poly.denote ctx p

source

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

Nat.Linear.ExprCnstr.denote ctx c = Nat.Linear.ExprCnstr.denote ctx d

source

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

Nat.Linear.Expr.denote ctx e = Nat.Linear.Expr.denote ctx e'