@@ -23,6 +23,7 @@ namespace Int.Linear
abbrev Var : = Nat
abbrev Context : = Lean . RArray Int
@[ expose ]
def Var . denote ( ctx : Context ) ( v : Var ) : Int : =
ctx . get v
@@ -36,6 +37,7 @@ inductive Expr where
| mulR ( a : Expr ) ( k : Int )
deriving Inhabited , BEq
@[ expose ]
def Expr . denote ( ctx : Context ) : Expr → Int
| . add a b = > Int . add ( denote ctx a ) ( denote ctx b )
| . sub a b = > Int . sub ( denote ctx a ) ( denote ctx b )
@@ -50,6 +52,7 @@ inductive Poly where
| add ( k : Int ) ( v : Var ) ( p : Poly )
deriving BEq
@[ expose ]
def Poly . denote ( ctx : Context ) ( p : Poly ) : Int : =
match p with
| . num k = > k
@@ -59,6 +62,7 @@ def Poly.denote (ctx : Context) (p : Poly) : Int :=
Similar to `Poly.denote`, but produces a denotation better for `simp +arith`.
Remark: we used to convert `Poly` back into `Expr` to achieve that.
-/
@[ expose ]
def Poly . denote' ( ctx : Context ) ( p : Poly ) : Int : =
match p with
| . num k = > k
@@ -84,11 +88,13 @@ theorem Poly.denote'_eq_denote (ctx : Context) (p : Poly) : p.denote' ctx = p.de
theorem Poly . denote'_add ( ctx : Context ) ( a : Int ) ( x : Var ) ( p : Poly ) : ( Poly . add a x p ) . denote' ctx = a * x . denote ctx + p . denote ctx : = by
simp [ Poly . denote'_eq_denote , denote ]
@[ expose ]
def Poly . addConst ( p : Poly ) ( k : Int ) : Poly : =
match p with
| . num k' = > . num ( k + k' )
| . add k' v' p = > . add k' v' ( addConst p k )
@[ expose ]
def Poly . insert ( k : Int ) ( v : Var ) ( p : Poly ) : Poly : =
match p with
| . num k' = > . add k v ( . num k' )
@@ -104,16 +110,19 @@ def Poly.insert (k : Int) (v : Var) (p : Poly) : Poly :=
. add k' v' ( insert k v p )
/-- Normalizes the given polynomial by fusing monomial and constants. -/
@[ expose ]
def Poly . norm ( p : Poly ) : Poly : =
match p with
| . num k = > . num k
| . add k v p = > ( norm p ) . insert k v
@[ expose ]
def Poly . append ( p₁ p₂ : Poly ) : Poly : =
match p₁ with
| . num k₁ = > p₂ . addConst k₁
| . add k x p₁ = > . add k x ( append p₁ p₂ )
@[ expose ]
def Poly . combine' ( fuel : Nat ) ( p₁ p₂ : Poly ) : Poly : =
match fuel with
| 0 = > p₁ . append p₂
@@ -133,10 +142,12 @@ def Poly.combine' (fuel : Nat) (p₁ p₂ : Poly) : Poly :=
else
. add a₂ x₂ ( combine' fuel ( . add a₁ x₁ p₁ ) p₂ )
@[ expose ]
def Poly . combine ( p₁ p₂ : Poly ) : Poly : =
combine' 100000000 p₁ p₂
/-- Converts the given expression into a polynomial. -/
@[ expose ]
def Expr . toPoly' ( e : Expr ) : Poly : =
go 1 e ( . num 0 )
where
@@ -150,6 +161,7 @@ where
| . neg a = > go ( - coeff ) a
/-- Converts the given expression into a polynomial, and then normalizes it. -/
@[ expose ]
def Expr . norm ( e : Expr ) : Poly : =
e . toPoly' . norm
@@ -159,6 +171,7 @@ Examples:
- `cdiv 7 3` returns `3`
- `cdiv ( - 7) 3` returns ` - 2`.
-/
@[ expose ]
def cdiv ( a b : Int ) : Int : =
- ( ( - a ) / b )
@@ -173,6 +186,7 @@ See theorem `cdiv_add_cmod`. We also have
- b < cmod a b ≤ 0
```
-/
@[ expose ]
def cmod ( a b : Int ) : Int : =
- ( ( - a ) % b )
@@ -219,6 +233,7 @@ theorem cdiv_eq_div_of_divides {a b : Int} (h : a % b = 0) : a/b = cdiv a b := b
next = > rw [ Int . mul_eq_mul_right_iff h ] at this ; assumption
/-- Returns the constant of the given linear polynomial. -/
@[ expose ]
def Poly . getConst : Poly → Int
| . num k = > k
| . add _ _ p = > getConst p
@@ -230,6 +245,7 @@ Notes:
- We only use this function with `k`s that divides all coefficients.
- We use `cdiv` for the constant to implement the inequality tightening rule.
-/
@[ expose ]
def Poly . div ( k : Int ) : Poly → Poly
| . num k' = > . num ( cdiv k' k )
| . add k' x p = > . add ( k' / k ) x ( div k p )
@@ -238,6 +254,7 @@ def Poly.div (k : Int) : Poly → Poly
Returns `true` if `k` divides all coefficients and the constant of the given
linear polynomial.
-/
@[ expose ]
def Poly . divAll ( k : Int ) : Poly → Bool
| . num k' = > k' % k = = 0
| . add k' _ p = > k' % k = = 0 & & divAll k p
@@ -245,6 +262,7 @@ def Poly.divAll (k : Int) : Poly → Bool
/--
Returns `true` if `k` divides all coefficients of the given linear polynomial.
-/
@[ expose ]
def Poly . divCoeffs ( k : Int ) : Poly → Bool
| . num _ = > true
| . add k' _ p = > k' % k = = 0 & & divCoeffs k p
@@ -252,11 +270,13 @@ def Poly.divCoeffs (k : Int) : Poly → Bool
/--
`p.mul k` multiplies all coefficients and constant of the polynomial `p` by `k`.
-/
@[ expose ]
def Poly . mul' ( p : Poly ) ( k : Int ) : Poly : =
match p with
| . num k' = > . num ( k * k' )
| . add k' v p = > . add ( k * k' ) v ( mul' p k )
@[ expose ]
def Poly . mul ( p : Poly ) ( k : Int ) : Poly : =
if k = = 0 then
. num 0
@@ -386,6 +406,7 @@ theorem Expr.eq_of_norm_eq (ctx : Context) (e : Expr) (p : Poly) (h : e.norm ==
simp [ Poly . norm ] at h
simp [ * ]
@[ expose ]
def norm_eq_cert ( lhs rhs : Expr ) ( p : Poly ) : Bool : =
p = = ( lhs . sub rhs ) . norm
@@ -401,6 +422,7 @@ theorem norm_le (ctx : Context) (lhs rhs : Expr) (p : Poly) (h : norm_eq_cert lh
· exact Int . sub_nonpos_of_le
· exact Int . le_of_sub_nonpos
@[ expose ]
def norm_eq_var_cert ( lhs rhs : Expr ) ( x y : Var ) : Bool : =
( lhs . sub rhs ) . norm = = . add 1 x ( . add ( - 1 ) y ( . num 0 ) )
@@ -411,6 +433,7 @@ theorem norm_eq_var (ctx : Context) (lhs rhs : Expr) (x y : Var) (h : norm_eq_va
simp at h
rw [ ← Int . sub_eq_zero , h , ← @ Int . sub_eq_zero ( Var . denote ctx x ) , Int . sub_eq_add_neg ]
@[ expose ]
def norm_eq_var_const_cert ( lhs rhs : Expr ) ( x : Var ) ( k : Int ) : Bool : =
( lhs . sub rhs ) . norm = = . add 1 x ( . num ( - k ) )
@@ -429,6 +452,7 @@ private theorem mul_eq_zero_iff (a k : Int) (h₁ : k > 0) : k * a = 0 ↔ a = 0
theorem norm_eq_coeff' ( ctx : Context ) ( p p' : Poly ) ( k : Int ) : p = p' . mul k → k > 0 → ( p . denote ctx = 0 ↔ p' . denote ctx = 0 ) : = by
intro ; subst p ; intro h ; simp [ mul_eq_zero_iff , * ]
@[ expose ]
def norm_eq_coeff_cert ( lhs rhs : Expr ) ( p : Poly ) ( k : Int ) : Bool : =
( lhs . sub rhs ) . norm = = p . mul k & & k > 0
@@ -492,6 +516,7 @@ private theorem eq_of_norm_eq_of_divCoeffs {ctx : Context} {p₁ p₂ : Poly} {k
apply mul_add_cmod_le_iff
assumption
@[ expose ]
def norm_le_coeff_tight_cert ( lhs rhs : Expr ) ( p : Poly ) ( k : Int ) : Bool : =
let p' : = lhs . sub rhs | > . norm
k > 0 & & ( p' . divCoeffs k & & p = = p' . div k )
@@ -502,11 +527,13 @@ theorem norm_le_coeff_tight (ctx : Context) (lhs rhs : Expr) (p : Poly) (k : Int
rw [ norm_le ctx lhs rhs ( lhs . sub rhs ) . norm BEq . rfl , Poly . denote'_eq_denote ]
apply eq_of_norm_eq_of_divCoeffs
@[ expose ]
def Poly . isUnsatEq ( p : Poly ) : Bool : =
match p with
| . num k = > k != 0
| _ = > false
@[ expose ]
def Poly . isValidEq ( p : Poly ) : Bool : =
match p with
| . num k = > k = = 0
@@ -530,11 +557,13 @@ theorem eq_eq_true (ctx : Context) (lhs rhs : Expr) : (lhs.sub rhs).norm.isValid
rw [ ← Int . sub_eq_zero , h ]
assumption
@[ expose ]
def Poly . isUnsatLe ( p : Poly ) : Bool : =
match p with
| . num k = > k > 0
| _ = > false
@[ expose ]
def Poly . isValidLe ( p : Poly ) : Bool : =
match p with
| . num k = > k ≤ 0
@@ -595,6 +624,7 @@ private theorem poly_eq_zero_eq_false (ctx : Context) {p : Poly} {k : Int} : p.d
have high : = h₃
exact contra h₂ low high this
@[ expose ]
def unsatEqDivCoeffCert ( lhs rhs : Expr ) ( k : Int ) : Bool : =
let p : = ( lhs . sub rhs ) . norm
p . divCoeffs k & & k > 0 & & cmod p . getConst k < 0
@@ -621,6 +651,7 @@ private theorem gcd_dvd_step {k a b x : Int} (h : k ∣ ∣
have h₂ : gcd a k ∣ a * x : = Int . dvd_trans ( gcd_dvd_left a k ) ( Int . dvd_mul_right a x )
exact Int . dvd_iff_dvd_of_dvd_add h₁ | > . mp h₂
@[ expose ]
def Poly . gcdCoeffs : Poly → Int → Int
| . num _ , k = > k
| . add k' _ p , k = > gcdCoeffs p ( gcd k' k )
@@ -631,6 +662,7 @@ theorem Poly.gcd_dvd_const {ctx : Context} {p : Poly} {k : Int} (h : k ∣
rw [ Int . add_comm ] at h
exact ih ( gcd_dvd_step h )
@[ expose ]
def Poly . isUnsatDvd ( k : Int ) ( p : Poly ) : Bool : =
p . getConst % p . gcdCoeffs k != 0
@@ -668,9 +700,11 @@ theorem dvd_eq_false (ctx : Context) (k : Int) (e : Expr) (h : e.norm.isUnsatDvd
rw [ norm_dvd ctx k e e . norm BEq . rfl ]
apply dvd_eq_false' ctx k e . norm h
@[ expose ]
def dvd_coeff_cert ( k₁ : Int ) ( p₁ : Poly ) ( k₂ : Int ) ( p₂ : Poly ) ( k : Int ) : Bool : =
k != 0 & & ( k₁ = = k * k₂ & & p₁ = = p₂ . mul k )
@[ expose ]
def norm_dvd_gcd_cert ( k₁ : Int ) ( e₁ : Expr ) ( k₂ : Int ) ( p₂ : Poly ) ( k : Int ) : Bool : =
dvd_coeff_cert k₁ e₁ . norm k₂ p₂ k
@@ -702,6 +736,7 @@ private theorem dvd_gcd_of_dvd (d a x p : Int) (h : d ∣
rw [ Int . mul_assoc , Int . mul_assoc , ← Int . mul_sub ] at h
exists k₁ * k - k₂ * x
@[ expose ]
def dvd_elim_cert ( k₁ : Int ) ( p₁ : Poly ) ( k₂ : Int ) ( p₂ : Poly ) : Bool : =
match p₁ with
| . add a _ p = > k₂ = = gcd k₁ a & & p₂ = = p
@@ -764,6 +799,7 @@ private theorem dvd_solve_elim' {x : Int} {d₁ a₁ p₁ : Int} {d₂ a₂ p₂
rw [ h₃ , h₄ , Int . mul_assoc , Int . mul_assoc , ← Int . mul_sub ] at this
exact ⟨ k₄ * k₁ - k₃ * k₂ , this ⟩
@[ expose ]
def dvd_solve_combine_cert ( d₁ : Int ) ( p₁ : Poly ) ( d₂ : Int ) ( p₂ : Poly ) ( d : Int ) ( p : Poly ) ( g α β : Int ) : Bool : =
match p₁ , p₂ with
| . add a₁ x₁ p₁ , . add a₂ x₂ p₂ = >
@@ -785,6 +821,7 @@ theorem dvd_solve_combine (ctx : Context) (d₁ : Int) (p₁ : Poly) (d₂ : Int
rw [ Int . add_comm _ ( g * x₂ . denote ctx ) , Int . add_left_comm , ← Int . add_assoc , hd ]
exact dvd_solve_combine' hg . symm h₁ h₂
@[ expose ]
def dvd_solve_elim_cert ( d₁ : Int ) ( p₁ : Poly ) ( d₂ : Int ) ( p₂ : Poly ) ( d : Int ) ( p : Poly ) : Bool : =
match p₁ , p₂ with
| . add a₁ x₁ p₁ , . add a₂ x₂ p₂ = >
@@ -816,6 +853,7 @@ theorem le_norm (ctx : Context) (p₁ p₂ : Poly) (h : p₁.norm == p₂) : p
simp at h
simp [ * ]
@[ expose ]
def le_coeff_cert ( p₁ p₂ : Poly ) ( k : Int ) : Bool : =
k > 0 & & ( p₁ . divCoeffs k & & p₂ = = p₁ . div k )
@@ -824,6 +862,7 @@ theorem le_coeff (ctx : Context) (p₁ p₂ : Poly) (k : Int) : le_coeff_cert p
intro h₁ h₂ h₃
exact eq_of_norm_eq_of_divCoeffs h₁ h₂ h₃ | > . mp
@[ expose ]
def le_neg_cert ( p₁ p₂ : Poly ) : Bool : =
p₂ = = ( p₁ . mul ( - 1 ) | > . addConst 1 )
@@ -834,11 +873,13 @@ theorem le_neg (ctx : Context) (p₁ p₂ : Poly) : le_neg_cert p₁ p₂ → ¬
simp at h
exact h
@[ expose ]
def Poly . leadCoeff ( p : Poly ) : Int : =
match p with
| . add a _ _ = > a
| _ = > 1
@[ expose ]
def le_combine_cert ( p₁ p₂ p₃ : Poly ) : Bool : =
let a₁ : = p₁ . leadCoeff . natAbs
let a₂ : = p₂ . leadCoeff . natAbs
@@ -854,6 +895,7 @@ theorem le_combine (ctx : Context) (p₁ p₂ p₃ : Poly)
· rw [ ← Int . zero_mul ( Poly . denote ctx p₂ ) ] ; apply Int . mul_le_mul_of_nonpos_right < ; > simp [ * ]
· rw [ ← Int . zero_mul ( Poly . denote ctx p₁ ) ] ; apply Int . mul_le_mul_of_nonpos_right < ; > simp [ * ]
@[ expose ]
def le_combine_coeff_cert ( p₁ p₂ p₃ : Poly ) ( k : Int ) : Bool : =
let a₁ : = p₁ . leadCoeff . natAbs
let a₂ : = p₂ . leadCoeff . natAbs
@@ -883,6 +925,7 @@ theorem eq_norm (ctx : Context) (p₁ p₂ : Poly) (h : p₁.norm == p₂) : p
simp at h
simp [ * ]
@[ expose ]
def eq_coeff_cert ( p p' : Poly ) ( k : Int ) : Bool : =
p = = p' . mul k & & k > 0
@@ -893,6 +936,7 @@ theorem eq_coeff (ctx : Context) (p p' : Poly) (k : Int) : eq_coeff_cert p p' k
theorem eq_unsat ( ctx : Context ) ( p : Poly ) : p . isUnsatEq → p . denote' ctx = 0 → False : = by
simp [ Poly . isUnsatEq ] < ; > split < ; > simp
@[ expose ]
def eq_unsat_coeff_cert ( p : Poly ) ( k : Int ) : Bool : =
p . divCoeffs k & & k > 0 & & cmod p . getConst k < 0
@@ -902,6 +946,7 @@ theorem eq_unsat_coeff (ctx : Context) (p : Poly) (k : Int) : eq_unsat_coeff_cer
have h : = poly_eq_zero_eq_false ctx h₁ h₂ h₃ ; clear h₁ h₂ h₃
simp [ h ]
@[ expose ]
def Poly . coeff ( p : Poly ) ( x : Var ) : Int : =
match p with
| . add a y p = > bif x = = y then a else coeff p x
@@ -916,7 +961,8 @@ private theorem dvd_of_eq' {a x p : Int} : a*x + p = 0 → a ∣
rw [ Int . mul_comm , ← Int . neg_mul , Eq . comm , Int . mul_comm ] at h
exact ⟨ - x , h ⟩
private def abs ( x : Int ) : Int : =
@[ expose ]
def abs ( x : Int ) : Int : =
Int . ofNat x . natAbs
private theorem abs_dvd { a p : Int } ( h : a ∣ p ) : abs a ∣ p : = by
@@ -924,6 +970,7 @@ private theorem abs_dvd {a p : Int} (h : a ∣ ∣
· simp at h ; assumption
· simp [ Int . negSucc_eq ] at h ; assumption
@[ expose ]
def dvd_of_eq_cert ( x : Var ) ( p₁ : Poly ) ( d₂ : Int ) ( p₂ : Poly ) : Bool : =
let a : = p₁ . coeff x
d₂ = = abs a & & p₂ = = p₁ . insert ( - a ) x
@@ -950,6 +997,7 @@ private theorem eq_dvd_subst' {a x p d b q : Int} : a*x + p = 0 → d ∣
rw [ ← Int . mul_assoc ] at h
exact ⟨ z , h ⟩
@[ expose ]
def eq_dvd_subst_cert ( x : Var ) ( p₁ : Poly ) ( d₂ : Int ) ( p₂ : Poly ) ( d₃ : Int ) ( p₃ : Poly ) : Bool : =
let a : = p₁ . coeff x
let b : = p₂ . coeff x
@@ -979,6 +1027,7 @@ theorem eq_dvd_subst (ctx : Context) (x : Var) (p₁ : Poly) (d₂ : Int) (p₂
apply abs_dvd
simp [ this , Int . neg_mul ]
@[ expose ]
def eq_eq_subst_cert ( x : Var ) ( p₁ : Poly ) ( p₂ : Poly ) ( p₃ : Poly ) : Bool : =
let a : = p₁ . coeff x
let b : = p₂ . coeff x
@@ -991,6 +1040,7 @@ theorem eq_eq_subst (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃
intro h₁ h₂
simp [ * ]
@[ expose ]
def eq_le_subst_nonneg_cert ( x : Var ) ( p₁ : Poly ) ( p₂ : Poly ) ( p₃ : Poly ) : Bool : =
let a : = p₁ . coeff x
let b : = p₂ . coeff x
@@ -1006,6 +1056,7 @@ theorem eq_le_subst_nonneg (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly)
simp at h₂
simp [ * ]
@[ expose ]
def eq_le_subst_nonpos_cert ( x : Var ) ( p₁ : Poly ) ( p₂ : Poly ) ( p₃ : Poly ) : Bool : =
let a : = p₁ . coeff x
let b : = p₂ . coeff x
@@ -1022,6 +1073,7 @@ theorem eq_le_subst_nonpos (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly)
rw [ Int . mul_comm ]
assumption
@[ expose ]
def eq_of_core_cert ( p₁ : Poly ) ( p₂ : Poly ) ( p₃ : Poly ) : Bool : =
p₃ = = p₁ . combine ( p₂ . mul ( - 1 ) )
@@ -1031,6 +1083,7 @@ theorem eq_of_core (ctx : Context) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
intro ; subst p₃ ; simp
intro h ; rw [ h , Int . add_neg_eq_sub , Int . sub_self ]
@[ expose ]
def Poly . isUnsatDiseq ( p : Poly ) : Bool : =
match p with
| . num 0 = > true
@@ -1052,6 +1105,7 @@ theorem diseq_neg (ctx : Context) (p p' : Poly) : p' == p.mul (-1) → p.denote'
theorem diseq_unsat ( ctx : Context ) ( p : Poly ) : p . isUnsatDiseq → p . denote' ctx ≠ 0 → False : = by
simp [ Poly . isUnsatDiseq ] < ; > split < ; > simp
@[ expose ]
def diseq_eq_subst_cert ( x : Var ) ( p₁ : Poly ) ( p₂ : Poly ) ( p₃ : Poly ) : Bool : =
let a : = p₁ . coeff x
let b : = p₂ . coeff x
@@ -1071,6 +1125,7 @@ theorem diseq_of_core (ctx : Context) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
intro h ; rw [ ← Int . sub_eq_zero ] at h
rw [ Int . add_neg_eq_sub ] ; assumption
@[ expose ]
def eq_of_le_ge_cert ( p₁ p₂ : Poly ) : Bool : =
p₂ = = p₁ . mul ( - 1 )
@@ -1081,6 +1136,7 @@ theorem eq_of_le_ge (ctx : Context) (p₁ : Poly) (p₂ : Poly)
intro h₁ h₂
simp [ Int . eq_iff_le_and_ge , * ]
@[ expose ]
def le_of_le_diseq_cert ( p₁ : Poly ) ( p₂ : Poly ) ( p₃ : Poly ) : Bool : =
-- Remark: we can generate two different certificates in the future, and avoid the `||` in the certificate.
( p₂ = = p₁ | | p₂ = = p₁ . mul ( - 1 ) ) & &
@@ -1095,6 +1151,7 @@ theorem le_of_le_diseq (ctx : Context) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
next h = > have : = Int . lt_of_le_of_lt h₁ h ; simp at this
intro h ; cases h < ; > intro < ; > subst p₂ p₃ < ; > simp < ; > apply this
@[ expose ]
def diseq_split_cert ( p₁ p₂ p₃ : Poly ) : Bool : =
p₂ = = p₁ . addConst 1 & &
p₃ = = ( p₁ . mul ( - 1 ) ) . addConst 1
@@ -1113,6 +1170,7 @@ theorem diseq_split_resolve (ctx : Context) (p₁ p₂ p₃ : Poly)
intro h₁ h₂ h₃
exact ( diseq_split ctx p₁ p₂ p₃ h₁ h₂ ) . resolve_left h₃
@[ expose ]
def OrOver ( n : Nat ) ( p : Nat → Prop ) : Prop : =
match n with
| 0 = > False
@@ -1127,6 +1185,7 @@ theorem orOver_resolve {n p} : OrOver (n+1) p → ¬ p n → OrOver n p := by
· contradiction
· assumption
@[ expose ]
def OrOver_cases_type ( n : Nat ) ( p : Nat → Prop ) : Prop : =
match n with
| 0 = > p 0
@@ -1186,6 +1245,7 @@ private theorem cooper_dvd_left_core
rw [ this ] at h₃
exists k . toNat
@[ expose ]
def cooper_dvd_left_cert ( p₁ p₂ p₃ : Poly ) ( d : Int ) ( n : Nat ) : Bool : =
p₁ . casesOn ( fun _ = > false ) fun a x _ = >
p₂ . casesOn ( fun _ = > false ) fun b y _ = >
@@ -1194,11 +1254,13 @@ def cooper_dvd_left_cert (p₁ p₂ p₃ : Poly) (d : Int) (n : Nat) : Bool :=
. and ( a < 0 ) < | . and ( b > 0 ) < |
. and ( d > 0 ) < | n = = Int . lcm a ( a * d / Int . gcd ( a * d ) c )
@[ expose ]
def Poly . tail ( p : Poly ) : Poly : =
match p with
| . add _ _ p = > p
| _ = > p
@[ expose ]
def cooper_dvd_left_split ( ctx : Context ) ( p₁ p₂ p₃ : Poly ) ( d : Int ) ( k : Nat ) : Prop : =
let p : = p₁ . tail
let q : = p₂ . tail
@@ -1238,6 +1300,7 @@ theorem cooper_dvd_left (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (n : N
simp only [ denote'_addConst_eq ]
exact cooper_dvd_left_core ha hb hd h₁ h₂ h₃
@[ expose ]
def cooper_dvd_left_split_ineq_cert ( p₁ p₂ : Poly ) ( k : Int ) ( b : Int ) ( p' : Poly ) : Bool : =
let p : = p₁ . tail
let q : = p₂ . tail
@@ -1250,6 +1313,7 @@ theorem cooper_dvd_left_split_ineq (ctx : Context) (p₁ p₂ p₃ : Poly) (d :
simp [ cooper_dvd_left_split_ineq_cert , cooper_dvd_left_split ]
intros ; subst p' b ; simp [ denote'_mul_combine_mul_addConst_eq ] ; assumption
@[ expose ]
def cooper_dvd_left_split_dvd1_cert ( p₁ p' : Poly ) ( a : Int ) ( k : Int ) : Bool : =
a = = p₁ . leadCoeff & & p' = = p₁ . tail . addConst k
@@ -1258,6 +1322,7 @@ theorem cooper_dvd_left_split_dvd1 (ctx : Context) (p₁ p₂ p₃ : Poly) (d :
simp [ cooper_dvd_left_split_dvd1_cert , cooper_dvd_left_split ]
intros ; subst a p' ; simp ; assumption
@[ expose ]
def cooper_dvd_left_split_dvd2_cert ( p₁ p₃ : Poly ) ( d : Int ) ( k : Nat ) ( d' : Int ) ( p' : Poly ) : Bool : =
let p : = p₁ . tail
let s : = p₃ . tail
@@ -1287,12 +1352,14 @@ private theorem cooper_left_core
and_true ] at h
assumption
@[ expose ]
def cooper_left_cert ( p₁ p₂ : Poly ) ( n : Nat ) : Bool : =
p₁ . casesOn ( fun _ = > false ) fun a x _ = >
p₂ . casesOn ( fun _ = > false ) fun b y _ = >
. and ( x = = y ) < | . and ( a < 0 ) < | . and ( b > 0 ) < |
n = = a . natAbs
@[ expose ]
def cooper_left_split ( ctx : Context ) ( p₁ p₂ : Poly ) ( k : Nat ) : Prop : =
let p : = p₁ . tail
let q : = p₂ . tail
@@ -1320,6 +1387,7 @@ theorem cooper_left (ctx : Context) (p₁ p₂ : Poly) (n : Nat)
simp only [ denote'_addConst_eq ]
assumption
@[ expose ]
def cooper_left_split_ineq_cert ( p₁ p₂ : Poly ) ( k : Int ) ( b : Int ) ( p' : Poly ) : Bool : =
let p : = p₁ . tail
let q : = p₂ . tail
@@ -1332,6 +1400,7 @@ theorem cooper_left_split_ineq (ctx : Context) (p₁ p₂ : Poly) (k : Nat) (b :
simp [ cooper_left_split_ineq_cert , cooper_left_split ]
intros ; subst p' b ; simp [ denote'_mul_combine_mul_addConst_eq ] ; assumption
@[ expose ]
def cooper_left_split_dvd_cert ( p₁ p' : Poly ) ( a : Int ) ( k : Int ) : Bool : =
a = = p₁ . leadCoeff & & p' = = p₁ . tail . addConst k
@@ -1365,6 +1434,7 @@ private theorem cooper_dvd_right_core
exists k . toNat
simp only [ hlt , true_and , and_true , cast_toNat h₁ , h₃ , h₄ , h₅ ]
@[ expose ]
def cooper_dvd_right_cert ( p₁ p₂ p₃ : Poly ) ( d : Int ) ( n : Nat ) : Bool : =
p₁ . casesOn ( fun _ = > false ) fun a x _ = >
p₂ . casesOn ( fun _ = > false ) fun b y _ = >
@@ -1373,6 +1443,7 @@ def cooper_dvd_right_cert (p₁ p₂ p₃ : Poly) (d : Int) (n : Nat) : Bool :=
. and ( a < 0 ) < | . and ( b > 0 ) < |
. and ( d > 0 ) < | n = = Int . lcm b ( b * d / Int . gcd ( b * d ) c )
@[ expose ]
def cooper_dvd_right_split ( ctx : Context ) ( p₁ p₂ p₃ : Poly ) ( d : Int ) ( k : Nat ) : Prop : =
let p : = p₁ . tail
let q : = p₂ . tail
@@ -1405,6 +1476,7 @@ theorem cooper_dvd_right (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (n :
simp only [ denote'_addConst_eq , ← Int . neg_mul ]
exact cooper_dvd_right_core ha hb hd h₁ h₂ h₃
@[ expose ]
def cooper_dvd_right_split_ineq_cert ( p₁ p₂ : Poly ) ( k : Int ) ( a : Int ) ( p' : Poly ) : Bool : =
let p : = p₁ . tail
let q : = p₂ . tail
@@ -1417,6 +1489,7 @@ theorem cooper_dvd_right_split_ineq (ctx : Context) (p₁ p₂ p₃ : Poly) (d :
simp [ cooper_dvd_right_split_ineq_cert , cooper_dvd_right_split ]
intros ; subst a p' ; simp [ denote'_mul_combine_mul_addConst_eq ] ; assumption
@[ expose ]
def cooper_dvd_right_split_dvd1_cert ( p₂ p' : Poly ) ( b : Int ) ( k : Int ) : Bool : =
b = = p₂ . leadCoeff & & p' = = p₂ . tail . addConst k
@@ -1425,6 +1498,7 @@ theorem cooper_dvd_right_split_dvd1 (ctx : Context) (p₁ p₂ p₃ : Poly) (d :
simp [ cooper_dvd_right_split_dvd1_cert , cooper_dvd_right_split ]
intros ; subst b p' ; simp ; assumption
@[ expose ]
def cooper_dvd_right_split_dvd2_cert ( p₂ p₃ : Poly ) ( d : Int ) ( k : Nat ) ( d' : Int ) ( p' : Poly ) : Bool : =
let q : = p₂ . tail
let s : = p₃ . tail
@@ -1454,11 +1528,13 @@ private theorem cooper_right_core
and_true , Int . neg_zero ] at h
assumption
@[ expose ]
def cooper_right_cert ( p₁ p₂ : Poly ) ( n : Nat ) : Bool : =
p₁ . casesOn ( fun _ = > false ) fun a x _ = >
p₂ . casesOn ( fun _ = > false ) fun b y _ = >
. and ( x = = y ) < | . and ( a < 0 ) < | . and ( b > 0 ) < | n = = b . natAbs
@[ expose ]
def cooper_right_split ( ctx : Context ) ( p₁ p₂ : Poly ) ( k : Nat ) : Prop : =
let p : = p₁ . tail
let q : = p₂ . tail
@@ -1486,6 +1562,7 @@ theorem cooper_right (ctx : Context) (p₁ p₂ : Poly) (n : Nat)
simp only [ denote'_addConst_eq , ← Int . neg_mul ]
assumption
@[ expose ]
def cooper_right_split_ineq_cert ( p₁ p₂ : Poly ) ( k : Int ) ( a : Int ) ( p' : Poly ) : Bool : =
let p : = p₁ . tail
let q : = p₂ . tail
@@ -1498,6 +1575,7 @@ theorem cooper_right_split_ineq (ctx : Context) (p₁ p₂ : Poly) (k : Nat) (a
simp [ cooper_right_split_ineq_cert , cooper_right_split ]
intros ; subst a p' ; simp [ denote'_mul_combine_mul_addConst_eq ] ; assumption
@[ expose ]
def cooper_right_split_dvd_cert ( p₂ p' : Poly ) ( b : Int ) ( k : Int ) : Bool : =
b = = p₂ . leadCoeff & & p' = = p₂ . tail . addConst k
@@ -1587,6 +1665,7 @@ abbrev Poly.casesOnAdd (p : Poly) (k : Int → Var → Poly → Bool) : Bool :=
abbrev Poly . casesOnNum ( p : Poly ) ( k : Int → Bool ) : Bool : =
p . casesOn k ( fun _ _ _ = > false )
@[ expose ]
def cooper_unsat_cert ( p₁ p₂ p₃ : Poly ) ( d : Int ) ( α β : Int ) : Bool : =
p₁ . casesOnAdd fun k₁ x p₁ = >
p₂ . casesOnAdd fun k₂ y p₂ = >
@@ -1626,6 +1705,7 @@ theorem emod_nonneg (x y : Int) : y != 0 → -1 * (x % y) ≤ 0 := by
simp at this
assumption
@[ expose ]
def emod_le_cert ( y n : Int ) : Bool : =
y != 0 & & n = = 1 - y . natAbs
@@ -1708,6 +1788,7 @@ private theorem eq_neg_addConst_add (ctx : Context) (p : Poly)
rw [ Int . add_right_neg ]
simp
@[ expose ]
def dvd_le_tight_cert ( d : Int ) ( p₁ p₂ p₃ : Poly ) : Bool : =
let b₁ : = p₁ . getConst
let b₂ : = p₂ . getConst
@@ -1728,6 +1809,7 @@ theorem dvd_le_tight (ctx : Context) (d : Int) (p₁ p₂ p₃ : Poly)
simp only [ Poly . denote'_eq_denote ]
exact dvd_le_tight' hd
@[ expose ]
def dvd_neg_le_tight_cert ( d : Int ) ( p₁ p₂ p₃ : Poly ) : Bool : =
let b₁ : = p₁ . getConst
let b₂ : = p₂ . getConst
@@ -1764,6 +1846,7 @@ theorem le_norm_expr (ctx : Context) (lhs rhs : Expr) (p : Poly)
: norm_eq_cert lhs rhs p → lhs . denote ctx ≤ rhs . denote ctx → p . denote' ctx ≤ 0 : = by
intro h₁ h₂ ; rwa [ norm_le ctx lhs rhs p h₁ ] at h₂
@[ expose ]
def not_le_norm_expr_cert ( lhs rhs : Expr ) ( p : Poly ) : Bool : =
p = = ( ( ( lhs . sub rhs ) . norm ) . mul ( - 1 ) ) . addConst 1
@@ -1796,6 +1879,7 @@ theorem of_not_dvd (a b : Int) : a != 0 → ¬ (a ∣
simp [ h₁ ] at h₂
assumption
@[ expose ]
def le_of_le_cert ( p q : Poly ) ( k : Nat ) : Bool : =
q = = p . addConst ( - k )
@@ -1806,6 +1890,7 @@ theorem le_of_le (ctx : Context) (p q : Poly) (k : Nat)
simp [ Lean . Omega . Int . add_le_zero_iff_le_neg' ]
exact Int . le_trans h ( Int . ofNat_zero_le _ )
@[ expose ]
def not_le_of_le_cert ( p q : Poly ) ( k : Nat ) : Bool : =
q = = ( p . mul ( - 1 ) ) . addConst ( 1 + k )
@@ -1819,6 +1904,7 @@ theorem not_le_of_le (ctx : Context) (p q : Poly) (k : Nat)
rw [ ← Int . add_assoc , ← Int . add_assoc , Int . add_neg_cancel_right , Lean . Omega . Int . add_le_zero_iff_le_neg' ]
simp ; exact Int . le_trans h ( Int . ofNat_zero_le _ )
@[ expose ]
def eq_def_cert ( x : Var ) ( xPoly : Poly ) ( p : Poly ) : Bool : =
p = = . add ( - 1 ) x xPoly
@@ -1827,6 +1913,7 @@ theorem eq_def (ctx : Context) (x : Var) (xPoly : Poly) (p : Poly)
simp [ eq_def_cert ] ; intro _ h ; subst p ; simp [ h ]
rw [ ← Int . sub_eq_add_neg , Int . sub_self ]
@[ expose ]
def eq_def'_cert ( x : Var ) ( e : Expr ) ( p : Poly ) : Bool : =
p = = . add ( - 1 ) x e . norm
