Documentation

Init.Data.Nat.Linear

Helper definitions and theorems for constructing linear arithmetic proofs.

@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For

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

Equations
Instances For
Equations
• = bif then 1 else
Instances For
Equations
Instances For
• num:
• var:
• mulL:
• mulR:
Instances For
Equations
Instances For
@[reducible, inline]
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
• p.sort =
Instances For
Equations
Instances For
Equations
Instances For
Equations
• = bif k == 0 then [] else bif k == 1 then p else
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
• p₁.cancel p₂ =
Instances For
Equations
• p.isNum? = match p with | [] => some 0 | [(k, v)] => bif then some k else none | x => none
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
• = p₁ ++ p₂
Instances For
Equations
• p₁.combine p₂ =
Instances For
Equations
Instances For
Equations
• p.norm = p.sort.fuse
Instances For
Equations
• e.toNormPoly = e.toPoly.norm
Instances For
Equations
Instances For
Equations
Equations
Instances For
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 }
Instances For
Equations
Instances For
Equations
• c.norm = match c.lhs.sort.fuse.cancel c.rhs.sort.fuse with | (lhs, rhs) => { eq := c.eq, lhs := lhs, rhs := rhs }
Instances For
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
Equations
• c.isValid = bif c.eq then c.lhs.isZero && c.rhs.isZero else c.lhs.isZero
Instances For
Equations
• c.toPoly = { eq := c.eq, lhs := c.lhs.toPoly, rhs := c.rhs.toPoly }
Instances For
Equations
• c.toNormPoly = match c.lhs.toNormPoly.cancel c.rhs.toNormPoly with | (lhs, rhs) => { eq := c.eq, lhs := lhs, rhs := rhs }
Instances For
@[reducible, inline]
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
• = bif then else bif k == 1 then else
Instances For
Equations
• p.toExpr = match p with | [] => | (k, v) :: p =>
Instances For
Equations
Instances For
Equations
• c.toExpr = { eq := c.eq, lhs := c.lhs.toExpr, rhs := c.rhs.toExpr }
Instances For
theorem Nat.Linear.Expr.eq_of_toNormPoly (ctx : Nat.Linear.Context) (a : Nat.Linear.Expr) (b : Nat.Linear.Expr) (h : a.toNormPoly = b.toNormPoly) :
=
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 : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)) :
( = ) = ( = )
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 : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)) :
( ) = ( )
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 : a.inc.toNormPoly.cancel b.toNormPoly = (c.inc.toPoly, d.toPoly)) :
( < ) = ( < )
theorem Nat.Linear.ExprCnstr.toPoly_norm_eq (c : Nat.Linear.ExprCnstr) :
c.toPoly.norm = c.toNormPoly
theorem Nat.Linear.Poly.isNum?_eq_some (ctx : Nat.Linear.Context) {p : Nat.Linear.Poly} {k : Nat} :
p.isNum? = some k = k
theorem Nat.Linear.Poly.of_isNonZero (ctx : Nat.Linear.Context) {p : Nat.Linear.Poly} (h : p.isNonZero = true) :
> 0
theorem Nat.Linear.Expr.eq_of_toNormPoly_eq (ctx : Nat.Linear.Context) (e : Nat.Linear.Expr) (e' : Nat.Linear.Expr) (h : (e.toNormPoly == e'.toPoly) = true) :
=
def Nat.elimOffset {α : Sort u} (a : Nat) (b : Nat) (k : Nat) (h₁ : a + k = b + k) (h₂ : a = bα) :
α
Equations
• a.elimOffset b k h₁ h₂ = h₂
Instances For