Stream: maths

Topic: has_mul instance for option?

Koundinya Vajjha (Jul 10 2019 at 20:55):

Does option have a has_mul instance?

I've been trying to prove the following:

lemma to_nnreal_mul (a b : ennreal) : ennreal.to_nnreal (a * b) = (ennreal.to_nnreal a)*(ennreal.to_nnreal b) := sorry


But after cases on both a and b I want to simplify the none * some term and the others, but I am stuck. Any suggetions?

Chris Hughes (Jul 10 2019 at 21:09):

none is defeq to \top, and there should be lemmas about that. Probably rfl will prove it. There might be a special version of cases for ennreal

Koundinya Vajjha (Jul 10 2019 at 21:21):

I'm stuck on ennreal.to_nnreal (some a * some b) = a * b.

Sebastien Gouezel (Jul 10 2019 at 21:43):

lemma to_nnreal_mul (a b : ennreal) :
ennreal.to_nnreal (a * b) = (ennreal.to_nnreal a) * (ennreal.to_nnreal b) :=
begin
cases a; cases b,
{ simp [none_eq_top] },
{ by_cases h : b = 0; simp [none_eq_top, some_eq_coe, h, top_mul] },
{ by_cases h : a = 0; simp [none_eq_top, some_eq_coe, h, mul_top] },
{ simp [some_eq_coe, coe_mul.symm, -coe_mul] }
end


We should probably add a simp attribute to none_eq_top and some_eq_coe, by the way.

Last updated: May 14 2021 at 20:13 UTC