From 427564e0c64bf9ac480124f215d95f24aa22ae00 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 8 Oct 2020 15:41:14 +0000 Subject: [PATCH] chore(algebra/monoid_algebra): Fix TODO about unwanted unfolding (#4532) For whatever reason, supplying `zero` and `add` explicitly makes the proofs work inline. This TODO was added by @johoelzl in f09abb1c47a846c33c0e996ffa9bf12951b40b15. --- src/algebra/monoid_algebra.lean | 56 +++++++++++---------------------- 1 file changed, 18 insertions(+), 38 deletions(-) diff --git a/src/algebra/monoid_algebra.lean b/src/algebra/monoid_algebra.lean index 99421db1bef04..392d4c43ed3fc 100644 --- a/src/algebra/monoid_algebra.lean +++ b/src/algebra/monoid_algebra.lean @@ -117,35 +117,25 @@ instance : has_one (monoid_algebra k G) := lemma one_def : (1 : monoid_algebra k G) = single 1 1 := rfl --- TODO: the simplifier unfolds 0 in the instance proof! -protected lemma zero_mul (f : monoid_algebra k G) : 0 * f = 0 := -by simp only [mul_def, sum_zero_index] - -protected lemma mul_zero (f : monoid_algebra k G) : f * 0 = 0 := -by simp only [mul_def, sum_zero_index, sum_zero] - -private lemma left_distrib (a b c : monoid_algebra k G) : a * (b + c) = a * b + a * c := -by simp only [mul_def, sum_add_index, mul_add, mul_zero, single_zero, single_add, - eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_add] - -private lemma right_distrib (a b c : monoid_algebra k G) : (a + b) * c = a * c + b * c := -by simp only [mul_def, sum_add_index, add_mul, mul_zero, zero_mul, single_zero, - single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_zero, sum_add] - instance : semiring (monoid_algebra k G) := { one := 1, mul := (*), + zero := 0, + add := (+), one_mul := assume f, by simp only [mul_def, one_def, sum_single_index, zero_mul, single_zero, sum_zero, zero_add, one_mul, sum_single], mul_one := assume f, by simp only [mul_def, one_def, sum_single_index, mul_zero, single_zero, sum_zero, add_zero, mul_one, sum_single], - zero_mul := monoid_algebra.zero_mul, - mul_zero := monoid_algebra.mul_zero, + zero_mul := assume f, by simp only [mul_def, sum_zero_index], + mul_zero := assume f, by simp only [mul_def, sum_zero_index, sum_zero], mul_assoc := assume f g h, by simp only [mul_def, sum_sum_index, sum_zero_index, sum_add_index, sum_single_index, single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff, add_mul, mul_add, add_assoc, mul_assoc, zero_mul, mul_zero, sum_zero, sum_add], - left_distrib := left_distrib, - right_distrib := right_distrib, + left_distrib := assume f g h, by simp only [mul_def, sum_add_index, mul_add, mul_zero, + single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_add], + right_distrib := assume f g h, by simp only [mul_def, sum_add_index, add_mul, mul_zero, zero_mul, + single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_zero, + sum_add], .. finsupp.add_comm_monoid } @[simp] lemma single_mul_single {a₁ a₂ : G} {b₁ b₂ : k} : @@ -502,35 +492,25 @@ instance : has_one (add_monoid_algebra k G) := lemma one_def : (1 : add_monoid_algebra k G) = single 0 1 := rfl --- TODO: the simplifier unfolds 0 in the instance proof! -protected lemma zero_mul (f : add_monoid_algebra k G) : 0 * f = 0 := -by simp only [mul_def, sum_zero_index] - -protected lemma mul_zero (f : add_monoid_algebra k G) : f * 0 = 0 := -by simp only [mul_def, sum_zero_index, sum_zero] - -private lemma left_distrib (a b c : add_monoid_algebra k G) : a * (b + c) = a * b + a * c := -by simp only [mul_def, sum_add_index, mul_add, mul_zero, single_zero, single_add, - eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_add] - -private lemma right_distrib (a b c : add_monoid_algebra k G) : (a + b) * c = a * c + b * c := -by simp only [mul_def, sum_add_index, add_mul, mul_zero, zero_mul, single_zero, - single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_zero, sum_add] - instance : semiring (add_monoid_algebra k G) := { one := 1, mul := (*), + zero := 0, + add := (+), one_mul := assume f, by simp only [mul_def, one_def, sum_single_index, zero_mul, single_zero, sum_zero, zero_add, one_mul, sum_single], mul_one := assume f, by simp only [mul_def, one_def, sum_single_index, mul_zero, single_zero, sum_zero, add_zero, mul_one, sum_single], - zero_mul := add_monoid_algebra.zero_mul, - mul_zero := add_monoid_algebra.mul_zero, + zero_mul := assume f, by simp only [mul_def, sum_zero_index], + mul_zero := assume f, by simp only [mul_def, sum_zero_index, sum_zero], mul_assoc := assume f g h, by simp only [mul_def, sum_sum_index, sum_zero_index, sum_add_index, sum_single_index, single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff, add_mul, mul_add, add_assoc, mul_assoc, zero_mul, mul_zero, sum_zero, sum_add], - left_distrib := left_distrib, - right_distrib := right_distrib, + left_distrib := assume f g h, by simp only [mul_def, sum_add_index, mul_add, mul_zero, + single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_add], + right_distrib := assume f g h, by simp only [mul_def, sum_add_index, add_mul, mul_zero, zero_mul, + single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_zero, + sum_add], .. finsupp.add_comm_monoid } lemma single_mul_single {a₁ a₂ : G} {b₁ b₂ : k} :