feat: helper theorem for normalizing non-commutative semirings (#10419)
This PR adds the helper theorem `eq_normS_nc` for normalizing non-commutative semirings. We will use this theorem to justify normalization steps in the `grind ring` module.
This commit is contained in:
Leonardo de Moura
GitHub
parent
4c1830e5ae
commit
20873d5d72
1 changed files with 229 additions and 39 deletions
|
|
@ -49,6 +49,19 @@ def Expr.toPolyS : Expr → CommRing.Poly
|
|||
| .natCast n => .num n
|
||||
| .sub .. | .neg .. | .intCast .. => .num 0
|
||||
|
||||
def Expr.toPolyS_nc : Expr → CommRing.Poly
|
||||
| .num n => .num n.natAbs
|
||||
| .var x => CommRing.Poly.ofVar x
|
||||
| .add a b => a.toPolyS_nc.combine b.toPolyS_nc
|
||||
| .mul a b => a.toPolyS_nc.mul_nc b.toPolyS_nc
|
||||
| .pow a k =>
|
||||
match a with
|
||||
| .num n => .num (n.natAbs ^ k)
|
||||
| .var x => CommRing.Poly.ofMon (.mult {x, k} .unit)
|
||||
| _ => a.toPolyS_nc.pow_nc k
|
||||
| .natCast n => .num n
|
||||
| .sub .. | .neg .. | .intCast .. => .num 0
|
||||
|
||||
end CommRing
|
||||
|
||||
namespace CommRing
|
||||
|
|
@ -82,15 +95,15 @@ def Poly.denoteS [Semiring α] (ctx : Context α) (p : Poly) : α :=
|
|||
|
||||
attribute [local simp] natCast_one natCast_zero zero_mul mul_zero one_mul mul_one add_zero zero_add denoteSInt_eq
|
||||
|
||||
theorem Poly.denoteS_ofMon {α} [CommSemiring α] (ctx : Context α) (m : Mon)
|
||||
theorem Poly.denoteS_ofMon {α} [Semiring α] (ctx : Context α) (m : Mon)
|
||||
: denoteS ctx (ofMon m) = m.denote ctx := by
|
||||
simp [ofMon, denoteS]
|
||||
|
||||
theorem Poly.denoteS_ofVar {α} [CommSemiring α] (ctx : Context α) (x : Var)
|
||||
theorem Poly.denoteS_ofVar {α} [Semiring α] (ctx : Context α) (x : Var)
|
||||
: denoteS ctx (ofVar x) = x.denote ctx := by
|
||||
simp [ofVar, denoteS_ofMon, Mon.denote_ofVar]
|
||||
|
||||
theorem Poly.denoteS_addConst {α} [CommSemiring α] (ctx : Context α) (p : Poly) (k : Int)
|
||||
theorem Poly.denoteS_addConst {α} [Semiring α] (ctx : Context α) (p : Poly) (k : Int)
|
||||
: k ≥ 0 → p.NonnegCoeffs → (addConst p k).denoteS ctx = p.denoteS ctx + k.toNat := by
|
||||
simp [addConst, cond_eq_if]; split
|
||||
next => subst k; simp
|
||||
|
|
@ -103,7 +116,7 @@ theorem Poly.denoteS_addConst {α} [CommSemiring α] (ctx : Context α) (p : Pol
|
|||
intro _ h; cases h
|
||||
next h₁ h₂ => simp [*, add_assoc]
|
||||
|
||||
theorem Poly.denoteS_insert {α} [CommSemiring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
|
||||
theorem Poly.denoteS_insert {α} [Semiring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
|
||||
: k ≥ 0 → p.NonnegCoeffs → (insert k m p).denoteS ctx = k.toNat * m.denote ctx + p.denoteS ctx := by
|
||||
simp [insert, cond_eq_if] <;> split
|
||||
next => simp [*]
|
||||
|
|
@ -130,13 +143,13 @@ theorem Poly.denoteS_insert {α} [CommSemiring α] (ctx : Context α) (k : Int)
|
|||
intro hk hn; cases hn; rename_i hn₁ hn₂
|
||||
rw [ih hk hn₂, add_left_comm]
|
||||
|
||||
theorem Poly.denoteS_concat {α} [CommSemiring α] (ctx : Context α) (p₁ p₂ : Poly)
|
||||
theorem Poly.denoteS_concat {α} [Semiring α] (ctx : Context α) (p₁ p₂ : Poly)
|
||||
: p₁.NonnegCoeffs → p₂.NonnegCoeffs → (concat p₁ p₂).denoteS ctx = p₁.denoteS ctx + p₂.denoteS ctx := by
|
||||
fun_induction concat <;> intro h₁ h₂; simp [*, denoteS]
|
||||
next => cases h₁; rw [add_comm, denoteS_addConst] <;> assumption
|
||||
next ih => cases h₁; next hn₁ hn₂ => rw [denoteS, denoteS, ih hn₂ h₂, add_assoc]
|
||||
|
||||
theorem Poly.denoteS_mulConst {α} [CommSemiring α] (ctx : Context α) (k : Int) (p : Poly)
|
||||
theorem Poly.denoteS_mulConst {α} [Semiring α] (ctx : Context α) (k : Int) (p : Poly)
|
||||
: k ≥ 0 → p.NonnegCoeffs → (mulConst k p).denoteS ctx = k.toNat * p.denoteS ctx := by
|
||||
simp [mulConst, cond_eq_if] <;> split
|
||||
next => simp [denoteS, *, zero_mul]
|
||||
|
|
@ -150,30 +163,7 @@ theorem Poly.denoteS_mulConst {α} [CommSemiring α] (ctx : Context α) (k : Int
|
|||
intro h₁ h₂; cases h₂; rename_i h₂ h₃
|
||||
rw [Int.toNat_mul, natCast_mul, left_distrib, mul_assoc, ih h₁ h₃] <;> assumption
|
||||
|
||||
theorem Poly.denoteS_mulMon {α} [CommSemiring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
|
||||
: k ≥ 0 → p.NonnegCoeffs → (mulMon k m p).denoteS ctx = k.toNat * m.denote ctx * p.denoteS ctx := by
|
||||
simp [mulMon, cond_eq_if] <;> split
|
||||
next => simp [denoteS, *]
|
||||
next =>
|
||||
split
|
||||
next h =>
|
||||
intro h₁ h₂
|
||||
simp at h; simp [*, Mon.denote, denoteS_mulConst _ _ _ h₁ h₂]
|
||||
next =>
|
||||
fun_induction mulMon.go <;> simp [denoteS, *]
|
||||
next h => simp +zetaDelta at h; simp [*]
|
||||
next =>
|
||||
intro h₁ h₂; cases h₂
|
||||
rw [Int.toNat_mul]
|
||||
simp [natCast_mul, CommSemiring.mul_comm, CommSemiring.mul_left_comm, mul_assoc]
|
||||
assumption; assumption
|
||||
next ih =>
|
||||
intro h₁ h₂; cases h₂; rename_i h₂ h₃
|
||||
rw [Int.toNat_mul]
|
||||
simp [Mon.denote_mul, natCast_mul, left_distrib, CommSemiring.mul_left_comm, mul_assoc, ih h₁ h₃]
|
||||
assumption; assumption
|
||||
|
||||
theorem Poly.denoteS_combine {α} [CommSemiring α] (ctx : Context α) (p₁ p₂ : Poly)
|
||||
theorem Poly.denoteS_combine {α} [Semiring α] (ctx : Context α) (p₁ p₂ : Poly)
|
||||
: p₁.NonnegCoeffs → p₂.NonnegCoeffs → (combine p₁ p₂).denoteS ctx = p₁.denoteS ctx + p₂.denoteS ctx := by
|
||||
unfold combine; generalize hugeFuel = fuel
|
||||
fun_induction combine.go
|
||||
|
|
@ -206,6 +196,93 @@ theorem Poly.denoteS_combine {α} [CommSemiring α] (ctx : Context α) (p₁ p
|
|||
rename_i h₂
|
||||
simp [denoteS, ih h₁ h₂, add_left_comm, add_assoc]
|
||||
|
||||
theorem Poly.denoteS_mulMon {α} [CommSemiring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
|
||||
: k ≥ 0 → p.NonnegCoeffs → (mulMon k m p).denoteS ctx = k.toNat * m.denote ctx * p.denoteS ctx := by
|
||||
simp [mulMon, cond_eq_if] <;> split
|
||||
next => simp [denoteS, *]
|
||||
next =>
|
||||
split
|
||||
next h =>
|
||||
intro h₁ h₂
|
||||
simp at h; simp [*, Mon.denote, denoteS_mulConst _ _ _ h₁ h₂]
|
||||
next =>
|
||||
fun_induction mulMon.go <;> simp [denoteS, *]
|
||||
next h => simp +zetaDelta at h; simp [*]
|
||||
next =>
|
||||
intro h₁ h₂; cases h₂
|
||||
rw [Int.toNat_mul]
|
||||
simp [natCast_mul, CommSemiring.mul_comm, CommSemiring.mul_left_comm, mul_assoc]
|
||||
assumption; assumption
|
||||
next ih =>
|
||||
intro h₁ h₂; cases h₂; rename_i h₂ h₃
|
||||
rw [Int.toNat_mul]
|
||||
simp [Mon.denote_mul, natCast_mul, left_distrib, CommSemiring.mul_left_comm, mul_assoc, ih h₁ h₃]
|
||||
assumption; assumption
|
||||
|
||||
theorem Poly.addConst_NonnegCoeffs {p : Poly} {k : Int} : k ≥ 0 → p.NonnegCoeffs → (p.addConst k).NonnegCoeffs := by
|
||||
simp [addConst, cond_eq_if]; split
|
||||
next => intros; assumption
|
||||
fun_induction addConst.go
|
||||
next h _ => intro _ h; cases h; constructor; apply Int.add_nonneg <;> assumption
|
||||
next ih => intro h₁ h₂; cases h₂; constructor; assumption; apply ih <;> assumption
|
||||
|
||||
theorem Poly.insert_Nonneg (k : Int) (m : Mon) (p : Poly) : k ≥ 0 → p.NonnegCoeffs → (p.insert k m).NonnegCoeffs := by
|
||||
intro h₁ h₂
|
||||
fun_cases Poly.insert
|
||||
next => assumption
|
||||
next => apply Poly.addConst_NonnegCoeffs <;> assumption
|
||||
next =>
|
||||
fun_induction Poly.insert.go
|
||||
next => constructor <;> assumption
|
||||
next => cases h₂; assumption
|
||||
next => simp +zetaDelta; cases h₂; constructor; omega; assumption
|
||||
next => constructor <;> assumption
|
||||
next ih =>
|
||||
cases h₂; constructor
|
||||
next => assumption
|
||||
next => apply ih; assumption
|
||||
|
||||
theorem Poly.denoteS_mulMon_nc_go {α} [Semiring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly) (acc : Poly)
|
||||
: k ≥ 0 → p.NonnegCoeffs → acc.NonnegCoeffs
|
||||
→ (mulMon_nc.go k m p acc).denoteS ctx = k.toNat * m.denote ctx * p.denoteS ctx + acc.denoteS ctx := by
|
||||
fun_induction mulMon_nc.go with simp [*]
|
||||
| case1 acc k' =>
|
||||
intro h₁ h₂ h₃; cases h₂
|
||||
have : k * k' ≥ 0 := by apply Int.mul_nonneg <;> assumption
|
||||
simp [denoteS_insert, denoteS, Int.toNat_mul, Semiring.natCast_mul, Semiring.mul_assoc, *]
|
||||
rw [← Semiring.natCast_mul_comm]
|
||||
| case2 acc k' m' p ih =>
|
||||
intro h₁ h₂ h₃; rcases h₂
|
||||
next _ h₂ =>
|
||||
have : k * k' ≥ 0 := by apply Int.mul_nonneg <;> assumption
|
||||
have : (insert (k * k') (m.mul_nc m') acc).NonnegCoeffs := by apply Poly.insert_Nonneg <;> assumption
|
||||
rw [ih h₁ h₂ this]
|
||||
simp [denoteS_insert, Int.toNat_mul, Semiring.natCast_mul, denoteS, left_distrib, Mon.denote_mul_nc, *]
|
||||
simp only [← Semiring.add_assoc]
|
||||
congr 1
|
||||
rw [Semiring.add_comm]
|
||||
congr 1
|
||||
rw [Semiring.natCast_mul_left_comm]
|
||||
conv => enter [1, 1]; rw [Semiring.natCast_mul_comm]
|
||||
simp [Semiring.mul_assoc]
|
||||
|
||||
theorem Poly.num_zero_NonnegCoeffs : (num 0).NonnegCoeffs := by
|
||||
apply NonnegCoeffs.num; simp
|
||||
|
||||
theorem Poly.denoteS_mulMon_nc {α} [Semiring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
|
||||
: k ≥ 0 → p.NonnegCoeffs → (mulMon_nc k m p).denoteS ctx = k.toNat * m.denote ctx * p.denoteS ctx := by
|
||||
simp [mulMon_nc, cond_eq_if] <;> split
|
||||
next => simp [denoteS, *]
|
||||
next =>
|
||||
split
|
||||
next h =>
|
||||
intro h₁ h₂
|
||||
simp at h; simp [*, Mon.denote, denoteS_mulConst _ _ _ h₁ h₂]
|
||||
next =>
|
||||
intro h₁ h₂
|
||||
have := Poly.denoteS_mulMon_nc_go ctx k m p (.num 0) h₁ h₂ Poly.num_zero_NonnegCoeffs
|
||||
simp [this, denoteS]
|
||||
|
||||
theorem Poly.mulConst_NonnegCoeffs {p : Poly} {k : Int} : k ≥ 0 → p.NonnegCoeffs → (p.mulConst k).NonnegCoeffs := by
|
||||
simp [mulConst, cond_eq_if]; split
|
||||
next => intros; constructor; decide
|
||||
|
|
@ -232,12 +309,29 @@ theorem Poly.mulMon_NonnegCoeffs {p : Poly} {k : Int} (m : Mon) : k ≥ 0 → p.
|
|||
apply Int.mul_nonneg <;> assumption
|
||||
apply ih <;> assumption
|
||||
|
||||
theorem Poly.addConst_NonnegCoeffs {p : Poly} {k : Int} : k ≥ 0 → p.NonnegCoeffs → (p.addConst k).NonnegCoeffs := by
|
||||
simp [addConst, cond_eq_if]; split
|
||||
next => intros; assumption
|
||||
fun_induction addConst.go
|
||||
next h _ => intro _ h; cases h; constructor; apply Int.add_nonneg <;> assumption
|
||||
next ih => intro h₁ h₂; cases h₂; constructor; assumption; apply ih <;> assumption
|
||||
theorem Poly.mulMon_nc_go_NonnegCoeffs {p : Poly} {k : Int} (m : Mon) {acc : Poly}
|
||||
: k ≥ 0 → p.NonnegCoeffs → acc.NonnegCoeffs → (Poly.mulMon_nc.go k m p acc).NonnegCoeffs := by
|
||||
intro h₁ h₂ h₃
|
||||
fun_induction Poly.mulMon_nc.go
|
||||
next k' =>
|
||||
cases h₂
|
||||
have : k*k' ≥ 0 := by apply Int.mul_nonneg <;> assumption
|
||||
apply Poly.insert_Nonneg <;> assumption
|
||||
next ih =>
|
||||
cases h₂; next h₂ =>
|
||||
apply ih; assumption
|
||||
apply insert_Nonneg
|
||||
next => apply Int.mul_nonneg <;> assumption
|
||||
next => assumption
|
||||
|
||||
theorem Poly.mulMon_nc_NonnegCoeffs {p : Poly} {k : Int} (m : Mon) : k ≥ 0 → p.NonnegCoeffs → (p.mulMon_nc k m).NonnegCoeffs := by
|
||||
simp [mulMon_nc, cond_eq_if]; split
|
||||
next => intros; constructor; decide
|
||||
split
|
||||
next => intros; apply mulConst_NonnegCoeffs <;> assumption
|
||||
intro h₁ h₂
|
||||
apply Poly.mulMon_nc_go_NonnegCoeffs; assumption; assumption
|
||||
exact Poly.num_zero_NonnegCoeffs
|
||||
|
||||
theorem Poly.concat_NonnegCoeffs {p₁ p₂ : Poly} : p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.concat p₂).NonnegCoeffs := by
|
||||
fun_induction Poly.concat
|
||||
|
|
@ -285,14 +379,40 @@ theorem Poly.mul_NonnegCoeffs {p₁ p₂ : Poly} : p₁.NonnegCoeffs → p₂.No
|
|||
unfold mul; intros; apply mul_go_NonnegCoeffs
|
||||
assumption; assumption; constructor; decide
|
||||
|
||||
theorem Poly.mul_nc_go_NonnegCoeffs (p₁ p₂ acc : Poly)
|
||||
: p₁.NonnegCoeffs → p₂.NonnegCoeffs → acc.NonnegCoeffs → (mul_nc.go p₂ p₁ acc).NonnegCoeffs := by
|
||||
fun_induction mul_nc.go
|
||||
next =>
|
||||
intro h₁ h₂ h₃
|
||||
cases h₁; rename_i h₁
|
||||
have := mulConst_NonnegCoeffs h₁ h₂
|
||||
apply combine_NonnegCoeffs <;> assumption
|
||||
next ih =>
|
||||
intro h₁ h₂ h₃
|
||||
cases h₁
|
||||
apply ih
|
||||
assumption; assumption
|
||||
apply Poly.combine_NonnegCoeffs; assumption
|
||||
apply Poly.mulMon_nc_NonnegCoeffs <;> assumption
|
||||
|
||||
theorem Poly.mul_nc_NonnegCoeffs {p₁ p₂ : Poly} : p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.mul_nc p₂).NonnegCoeffs := by
|
||||
unfold mul_nc; intros; apply mul_nc_go_NonnegCoeffs
|
||||
assumption; assumption; constructor; decide
|
||||
|
||||
theorem Poly.pow_NonnegCoeffs {p : Poly} (k : Nat) : p.NonnegCoeffs → (p.pow k).NonnegCoeffs := by
|
||||
fun_induction Poly.pow
|
||||
next => intros; constructor; decide
|
||||
next => intros; assumption
|
||||
next ih => intro h; apply mul_NonnegCoeffs; assumption; apply ih; assumption
|
||||
|
||||
theorem Poly.num_zero_NonnegCoeffs : (num 0).NonnegCoeffs := by
|
||||
apply NonnegCoeffs.num; simp
|
||||
theorem Poly.pow_nc_NonnegCoeffs {p : Poly} (k : Nat) : p.NonnegCoeffs → (p.pow_nc k).NonnegCoeffs := by
|
||||
fun_induction Poly.pow_nc
|
||||
next => intros; constructor; decide
|
||||
next => intros; assumption
|
||||
next ih =>
|
||||
intro h; apply mul_nc_NonnegCoeffs
|
||||
next => apply ih; assumption
|
||||
next => assumption
|
||||
|
||||
theorem Poly.denoteS_mul_go {α} [CommSemiring α] (ctx : Context α) (p₁ p₂ acc : Poly)
|
||||
: p₁.NonnegCoeffs → p₂.NonnegCoeffs → acc.NonnegCoeffs → (mul.go p₂ p₁ acc).denoteS ctx = acc.denoteS ctx + p₁.denoteS ctx * p₂.denoteS ctx := by
|
||||
|
|
@ -315,6 +435,27 @@ theorem Poly.denoteS_mul {α} [CommSemiring α] (ctx : Context α) (p₁ p₂ :
|
|||
intro h₁ h₂
|
||||
simp [mul, denoteS_mul_go, denoteS, Poly.num_zero_NonnegCoeffs, *]
|
||||
|
||||
theorem Poly.denoteS_mul_nc_go {α} [Semiring α] (ctx : Context α) (p₁ p₂ acc : Poly)
|
||||
: p₁.NonnegCoeffs → p₂.NonnegCoeffs → acc.NonnegCoeffs → (mul_nc.go p₂ p₁ acc).denoteS ctx = acc.denoteS ctx + p₁.denoteS ctx * p₂.denoteS ctx := by
|
||||
fun_induction mul_nc.go <;> intro h₁ h₂ h₃
|
||||
next k =>
|
||||
cases h₁; rename_i h₁
|
||||
have := p₂.mulConst_NonnegCoeffs h₁ h₂
|
||||
simp [denoteS, denoteS_combine, denoteS_mulConst, *]
|
||||
next acc a m p ih =>
|
||||
cases h₁; rename_i h₁ h₁'
|
||||
have := p₂.mulMon_nc_NonnegCoeffs m h₁ h₂
|
||||
have := acc.combine_NonnegCoeffs h₃ this
|
||||
replace ih := ih h₁' h₂ this
|
||||
rw [ih, denoteS_combine, denoteS_mulMon_nc]
|
||||
simp [denoteS, add_assoc, right_distrib]
|
||||
all_goals assumption
|
||||
|
||||
theorem Poly.denoteS_mul_nc {α} [Semiring α] (ctx : Context α) (p₁ p₂ : Poly)
|
||||
: p₁.NonnegCoeffs → p₂.NonnegCoeffs → (mul_nc p₁ p₂).denoteS ctx = p₁.denoteS ctx * p₂.denoteS ctx := by
|
||||
intro h₁ h₂
|
||||
simp [mul_nc, denoteS_mul_nc_go, denoteS, Poly.num_zero_NonnegCoeffs, *]
|
||||
|
||||
theorem Poly.denoteS_pow {α} [CommSemiring α] (ctx : Context α) (p : Poly) (k : Nat)
|
||||
: p.NonnegCoeffs → (pow p k).denoteS ctx = p.denoteS ctx ^ k := by
|
||||
fun_induction pow <;> intro h₁
|
||||
|
|
@ -326,6 +467,17 @@ theorem Poly.denoteS_pow {α} [CommSemiring α] (ctx : Context α) (p : Poly) (k
|
|||
assumption
|
||||
apply Poly.pow_NonnegCoeffs; assumption
|
||||
|
||||
theorem Poly.denoteS_pow_nc {α} [Semiring α] (ctx : Context α) (p : Poly) (k : Nat)
|
||||
: p.NonnegCoeffs → (pow_nc p k).denoteS ctx = p.denoteS ctx ^ k := by
|
||||
fun_induction pow_nc <;> intro h₁
|
||||
next => simp [denoteS, pow_zero]
|
||||
next => simp [pow_succ, pow_zero]
|
||||
next ih =>
|
||||
replace ih := ih h₁
|
||||
rw [denoteS_mul_nc, ih, pow_succ]
|
||||
apply Poly.pow_nc_NonnegCoeffs; assumption
|
||||
assumption
|
||||
|
||||
theorem Expr.toPolyS_NonnegCoeffs {e : Expr} : e.toPolyS.NonnegCoeffs := by
|
||||
fun_induction toPolyS
|
||||
next => constructor; apply Int.natCast_nonneg
|
||||
|
|
@ -336,10 +488,24 @@ theorem Expr.toPolyS_NonnegCoeffs {e : Expr} : e.toPolyS.NonnegCoeffs := by
|
|||
next => constructor; decide; constructor; decide
|
||||
next => apply Poly.pow_NonnegCoeffs; assumption
|
||||
next => constructor; apply Int.ofNat_zero_le
|
||||
all_goals constructor; apply Int.le_refl
|
||||
all_goals exact Poly.num_zero_NonnegCoeffs
|
||||
|
||||
attribute [local simp] Expr.toPolyS_NonnegCoeffs
|
||||
|
||||
theorem Expr.toPolyS_nc_NonnegCoeffs {e : Expr} : e.toPolyS_nc.NonnegCoeffs := by
|
||||
fun_induction toPolyS_nc
|
||||
next => constructor; apply Int.natCast_nonneg
|
||||
next => simp [Poly.ofVar, Poly.ofMon]; constructor; decide; constructor; decide
|
||||
next => apply Poly.combine_NonnegCoeffs <;> assumption
|
||||
next => apply Poly.mul_nc_NonnegCoeffs <;> assumption
|
||||
next => constructor; apply Int.pow_nonneg; apply Int.natCast_nonneg
|
||||
next => constructor; decide; constructor; decide
|
||||
next => apply Poly.pow_nc_NonnegCoeffs; assumption
|
||||
next => constructor; apply Int.ofNat_zero_le
|
||||
all_goals exact Poly.num_zero_NonnegCoeffs
|
||||
|
||||
attribute [local simp] Expr.toPolyS_nc_NonnegCoeffs
|
||||
|
||||
theorem Expr.denoteS_toPolyS {α} [CommSemiring α] (ctx : Context α) (e : Expr)
|
||||
: e.toPolyS.denoteS ctx = e.denoteS ctx := by
|
||||
fun_induction toPolyS <;> simp [denoteS, Poly.denoteS, Poly.denoteS_ofVar, denoteSInt_eq]
|
||||
|
|
@ -354,6 +520,20 @@ theorem Expr.denoteS_toPolyS {α} [CommSemiring α] (ctx : Context α) (e : Expr
|
|||
next ih => rw [Poly.denoteS_pow, ih]; apply toPolyS_NonnegCoeffs
|
||||
next => simp [Semiring.natCast_eq_ofNat]
|
||||
|
||||
theorem Expr.denoteS_toPolyS_nc {α} [Semiring α] (ctx : Context α) (e : Expr)
|
||||
: e.toPolyS_nc.denoteS ctx = e.denoteS ctx := by
|
||||
fun_induction Expr.toPolyS_nc <;> simp [denoteS, Poly.denoteS, Poly.denoteS_ofVar, denoteSInt_eq]
|
||||
next => simp [Semiring.ofNat_eq_natCast]
|
||||
next => simp [Poly.denoteS_combine] <;> simp [*]
|
||||
next => simp [Poly.denoteS_mul_nc] <;> simp [*]
|
||||
next => rw [Int.toNat_pow_of_nonneg, Semiring.natCast_pow, Int.toNat_natCast, ← Semiring.ofNat_eq_natCast]
|
||||
apply Int.natCast_nonneg
|
||||
next => simp [Poly.ofMon, Poly.denoteS, denoteSInt_eq, Power.denote_eq, Mon.denote,
|
||||
Semiring.natCast_zero, Semiring.natCast_one, Semiring.one_mul,
|
||||
CommRing.Var.denote, Var.denote, Semiring.mul_one]
|
||||
next ih => rw [Poly.denoteS_pow_nc, ih]; apply toPolyS_nc_NonnegCoeffs
|
||||
next => simp [Semiring.natCast_eq_ofNat]
|
||||
|
||||
def eq_normS_cert (lhs rhs : Expr) : Bool :=
|
||||
lhs.toPolyS == rhs.toPolyS
|
||||
|
||||
|
|
@ -364,6 +544,16 @@ theorem eq_normS {α} [CommSemiring α] (ctx : Context α) (lhs rhs : Expr)
|
|||
simp [Expr.denoteS_toPolyS, *] at h
|
||||
assumption
|
||||
|
||||
def eq_normS_nc_cert (lhs rhs : Expr) : Bool :=
|
||||
lhs.toPolyS_nc == rhs.toPolyS_nc
|
||||
|
||||
theorem eq_normS_nc {α} [Semiring α] (ctx : Context α) (lhs rhs : Expr)
|
||||
: eq_normS_nc_cert lhs rhs → lhs.denoteS ctx = rhs.denoteS ctx := by
|
||||
simp [eq_normS_nc_cert]; intro h
|
||||
replace h := congrArg (Poly.denoteS ctx) h
|
||||
simp [Expr.denoteS_toPolyS_nc, *] at h
|
||||
assumption
|
||||
|
||||
end CommRing
|
||||
|
||||
namespace Ring.OfSemiring
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue