polyrith

IEqHyp

data IEqHyp

A polyrith hypothesis ieq a b c: eval a = eval b, used with coefficient polynomial c.

ieqHolds

def ieqHolds (ρ : List Int) (l : List IEqHyp) : Type

The proposition that every equation hypothesis in the list holds under the environment.

ieqSum

def ieqSum (l : List IEqHyp) : IntExpr

The combination Σ cᵢ·(aᵢ − bᵢ) of the hypotheses as an integer expression.

prZeroStep

theorem prZeroStep (c : Int) (b : Int) : Int.add (Int.mul c (Int.add b (Int.neg b))) (pos zero) = pos zero

c·(b − b) + 0 = 0 over Int; a step lemma for prSumZero.

prSumZero

def prSumZero (ρ : List Int) (l : List IEqHyp) (pf : ieqHolds ρ l) : intEval ρ (ieqSum l) = pos zero

When all hypotheses hold, the combination Σ cᵢ·(aᵢ − bᵢ) evaluates to zero.

prMulCancel

def prMulCancel (L : Nat) (x : Int) : Int.mul (pos (succ L)) x = pos zero -> x = pos zero

Int has no zero divisors by positive constants: (L+1)·x = 0 implies x = 0.

prOfDiffR

theorem prOfDiffR (a : Int) (b : Int) : a = Int.add (Int.add a (Int.neg b)) b

a = (a − b) + b over Int.

prZeroAdd

theorem prZeroAdd (b : Int) : Int.add (pos zero) b = b

0 + b = b over Int.

prOfDiff

def prOfDiff (a : Int) (b : Int) (p : Int.add a (Int.neg b) = pos zero) : a = b

a − b = 0 implies a = b over Int.

polyrithEq

def polyrithEq (ρ : List Int) (l : List IEqHyp) (pf : ieqHolds ρ l) (a : IntExpr) (b : IntExpr) (L : Nat) (cert : intCheckL (imul (inum (succ L)) (iadd a (ineg b))) (ieqSum l) = intCheckR (imul (inum (succ L)) (iadd a (ineg b))) (ieqSum l)) : intEval ρ a = intEval ρ b

The certificate the polyrith tactic produces: if (L+1)·(a − b) equals a combination of the hypotheses as polynomials, then a = b.

polyrithTestPower

def polyrithTestPower (p : Int) (v : Int) (i : Int) (r : Int) (h1 : p = Int.mul v i) (h2 : v = Int.mul i r) : p = Int.mul (Int.mul i i) r

Example of using polyrithEq directly to combine two equations without the tactic.