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

test: add Expr.eq_of_toPoly_eq

Browse source
This commit is contained in:
Leonardo de Moura 2022-04-20 23:04:29 -07:00
parent 6bdeb6c9cb
commit d8ad343885
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
tests/playground/som.lean
View file

@ -216,3 +216,8 @@ theorem Expr.toPoly_denote (ctx : Context α) (e : Expr) : e.toPoly.denote ctx =
| add a b => simp! [Poly.add_denote, *]
| mul a b => simp! [Poly.mul_denote, *]
| sub a b => simp! [Poly.add_denote, *, sub_def, Poly.neg_denote, mul_one, mul_comm]
theorem Expr.eq_of_toPoly_eq (ctx : Context α) (a b : Expr) (h : a.toPoly == b.toPoly) : a.denote ctx = b.denote ctx := by
have h := congrArg (Poly.denote ctx) (eq_of_beq h)
simp [toPoly_denote] at h
assumption