Helper definitions and theorems for constructing linear arithmetic proofs.
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₂))
:
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₂)
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₂))
:
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₂)
theorem
Nat.Linear.Expr.eq_of_toNormPoly
(ctx : Context)
(a b : Expr)
(h : a.toNormPoly = b.toNormPoly)
: