max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: update proofs after stage0 update for #7140

Browse source
This commit is contained in:
Joachim Breitner 2025-02-19 19:28:55 +01:00 • committed by Sebastian Ullrich
parent eeb74ecf4d
commit 5bee3288ac
2 changed files with 37 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
src/Init/Data/Int/Linear.lean
View file

@ -430,26 +430,30 @@ attribute [local simp] RawRelCnstr.denote RawRelCnstr.norm Expr.denote
theorem Expr.denote_toPoly'_go (ctx : Context) (e : Expr) :
(toPoly'.go k e p).denote ctx = k * e.denote ctx + p.denote ctx := by
induction k, e using Expr.toPoly'.go.induct generalizing p with
| case1 k k' =>
simp only [toPoly'.go]
by_cases h : k' == 0
· simp [h, eq_of_beq h]
· simp [h, Var.denote]
| case2 k i => simp [toPoly'.go]
| case3 k a b iha ihb => simp [toPoly'.go, iha, ihb]
| case4 k a b iha ihb =>
| case1 k k' h =>
simp only [toPoly'.go, h, cond_true]
simp [eq_of_beq h]
| case2 k k' h =>
simp only [toPoly'.go, h, cond_false]
simp [Var.denote]
| case3 k i => simp [toPoly'.go]
| case4 k a b iha ihb => simp [toPoly'.go, iha, ihb]
| case5 k a b iha ihb =>
simp [toPoly'.go, iha, ihb, Int.mul_sub]
rw [Int.sub_eq_add_neg, ←Int.neg_mul, Int.add_assoc]
| case5 k k' a ih
| case6 k a k' ih =>
simp only [toPoly'.go]
by_cases h : k' == 0
· simp [h, eq_of_beq h]
· simp [h, cond_false, Int.mul_assoc]
simp at ih
rw [ih]
rw [Int.mul_assoc, Int.mul_comm k']
| case7 k a ih => simp [toPoly'.go, ih]
| case6 k k' a h
| case8 k a k' h =>
simp only [toPoly'.go, h, cond_false]
simp [eq_of_beq h]
| case7 k a k' h ih =>
simp only [toPoly'.go, h, cond_false]
simpa [denote, ← Int.mul_assoc] using ih
| case9 k a h h ih =>
simp only [toPoly'.go, h, cond_false]
simp only [mul_def, denote]
rw [Int.mul_comm (denote _ _) _]
simpa [Int.mul_assoc] using ih
| case10 k a ih => simp [toPoly'.go, ih]
theorem Expr.denote_toPoly (ctx : Context) (e : Expr) : e.toPoly.denote ctx = e.denote ctx := by
simp [toPoly, toPoly', Expr.denote_toPoly'_go]

27
src/Init/Data/Nat/Linear.lean
View file

@ -431,19 +431,22 @@ attribute [local simp] Poly.denote_le_cancel_eq
theorem Expr.denote_toPoly_go (ctx : Context) (e : Expr) :
(toPoly.go k e p).denote ctx = k * e.denote ctx + p.denote ctx := by
induction k, e using Expr.toPoly.go.induct generalizing p with
| case1 k k' =>
simp only [toPoly.go]
by_cases h : k' == 0
· simp [h, eq_of_beq h]
· simp [h, Var.denote]
| case2 k i => simp [toPoly.go]
| case3 k a b iha ihb => simp [toPoly.go, iha, ihb]
| case4 k k' a ih
| case5 k a k' ih =>
| case1 k k' h =>
simp [toPoly.go, eq_of_beq h]
| case2 k k' h =>
simp [toPoly.go, h, Var.denote]
| case3 k i => simp [toPoly.go]
| case4 k a b iha ihb => simp [toPoly.go, iha, ihb]
| case5 k k' a h => simp [toPoly.go, h, eq_of_beq h]
| case6 k a k' h ih =>
simp only [toPoly.go, denote, mul_eq]
by_cases h : k' == 0
· simp [h, eq_of_beq h]
· simp [h, cond_false, ih, Nat.mul_assoc]
simp [h, cond_false, ih, Nat.mul_assoc]
| case7 k a k' h =>
simp only [toPoly.go, denote, mul_eq]
simp [h, eq_of_beq h]
| case8 k a k' h ih =>
simp only [toPoly.go, denote, mul_eq]
simp [h, cond_false, ih, Nat.mul_assoc]
theorem Expr.denote_toPoly (ctx : Context) (e : Expr) : e.toPoly.denote ctx = e.denote ctx := by
simp [toPoly, Expr.denote_toPoly_go]