From d8ad343885d87f6ab6715ee443f0db826d1286d1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Apr 2022 23:04:29 -0700 Subject: [PATCH] test: add `Expr.eq_of_toPoly_eq` --- tests/playground/som.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/tests/playground/som.lean b/tests/playground/som.lean index 36798302c3..88d5f2c975 100644 --- a/tests/playground/som.lean +++ b/tests/playground/som.lean @@ -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