Skip to content

Commit

Permalink
refactor(data/real/ereal): add a two-argument induction principle (#1…
Browse files Browse the repository at this point in the history 
…8481)

We use exactly the same induction process whenever proving anything about `*` on `ereal`, so we may as well package it into a helper lemma.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
  • Loading branch information
@eric-wieser @sgouezel
eric-wieser and sgouezel committed Feb 24, 2023
1 parent 8e57ff9 commit 634284e
Showing 1 changed file with 134 additions and 104 deletions.
238 changes: 134 additions & 104 deletions src/data/real/ereal.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,10 @@ def real.to_ereal : ℝ → ereal := some ∘ some

namespace ereal

-- things unify with `with_bot.decidable_lt` later if we we don't provide this explicitly.
instance decidable_lt : decidable_rel ((<) : ereal → ereal → Prop) :=
with_bot.decidable_lt

-- TODO: Provide explicitly, otherwise it is inferred noncomputably from `complete_linear_order`
instance : has_top ereal := ⟨some ⊤⟩

Expand Down Expand Up @@ -121,6 +125,42 @@ protected def mul : ereal → ereal → ereal

instance : has_mul ereal := ⟨ereal.mul⟩

/-- Induct on two ereals by performing case splits on the sign of one whenever the other is
infinite. -/
@[elab_as_eliminator]
lemma induction₂ {P : ereal → ereal → Prop}
(top_top : P ⊤ ⊤)
(top_pos : ∀ x : ℝ, 0 < x → P ⊤ x)
(top_zero : P ⊤ 0)
(top_neg : ∀ x : ℝ, x < 0 → P ⊤ x)
(top_bot : P ⊤ ⊥)
(pos_top : ∀ x : ℝ, 0 < x → P x ⊤)
(pos_bot : ∀ x : ℝ, 0 < x → P x ⊥)
(zero_top : P 0 ⊤)
(coe_coe : ∀ x y : ℝ, P x y)
(zero_bot : P 0 ⊥)
(neg_top : ∀ x : ℝ, x < 0 → P x ⊤)
(neg_bot : ∀ x : ℝ, x < 0 → P x ⊥)
(bot_top : P ⊥ ⊤)
(bot_pos : ∀ x : ℝ, 0 < x → P ⊥ x)
(bot_zero : P ⊥ 0)
(bot_neg : ∀ x : ℝ, x < 0 → P ⊥ x)
(bot_bot : P ⊥ ⊥) :
∀ x y, P x y
| ⊥ ⊥ := bot_bot
| ⊥ (y : ℝ) :=
by { rcases lt_trichotomy 0 y with hy|rfl|hy, exacts [bot_pos y hy, bot_zero, bot_neg y hy] }
| ⊥ ⊤ := bot_top
| (x : ℝ) ⊥ :=
by { rcases lt_trichotomy 0 x with hx|rfl|hx, exacts [pos_bot x hx, zero_bot, neg_bot x hx] }
| (x : ℝ) (y : ℝ) := coe_coe _ _
| (x : ℝ) ⊤ :=
by { rcases lt_trichotomy 0 x with hx|rfl|hx, exacts [pos_top x hx, zero_top, neg_top x hx] }
| ⊤ ⊥ := top_bot
| ⊤ (y : ℝ) :=
by { rcases lt_trichotomy 0 y with hy|rfl|hy, exacts [top_pos y hy, top_zero, top_neg y hy] }
| ⊤ ⊤ := top_top

/-! `ereal` with its multiplication is a `comm_monoid_with_zero`. However, the proof of
associativity by hand is extremely painful (with 125 cases...). Instead, we will deduce it later
on from the facts that the absolute value and the sign are multiplicative functions taking value
Expand Down Expand Up @@ -695,54 +735,57 @@ bot_mul_of_neg (ereal.coe_neg'.2 h)

lemma to_real_mul {x y : ereal} : to_real (x * y) = to_real x * to_real y :=
begin
induction x using ereal.rec; induction y using ereal.rec,
{ simp only [bot_mul_bot, to_real_top, to_real_bot, mul_zero] },
{ rcases lt_trichotomy 0 y with hy|rfl|hy,
{ simp only [bot_mul_coe_of_pos hy, to_real_bot, zero_mul] },
{ simp only [coe_zero, mul_zero, to_real_zero] },
{ simp only [bot_mul_coe_of_neg hy, to_real_top, to_real_bot, zero_mul] } },
{ simp only [bot_mul_top, to_real_bot, to_real_top, mul_zero] },
{ rcases lt_trichotomy 0 x with hx|rfl|hx,
{ simp only [coe_mul_bot_of_pos hx, to_real_bot, mul_zero] },
{ simp only [coe_zero, zero_mul, to_real_zero] },
{ simp only [coe_mul_bot_of_neg hx, to_real_top, to_real_bot, mul_zero] } },
{ simp only [← coe_mul, to_real_coe] },
{ rcases lt_trichotomy 0 x with hx|rfl|hx,
{ simp only [coe_mul_top_of_pos hx, to_real_top, mul_zero] },
{ simp only [coe_zero, zero_mul, to_real_zero] },
{ simp only [coe_mul_top_of_neg hx, to_real_top, to_real_bot, mul_zero] } },
{ simp only [top_mul_bot, to_real_bot, mul_zero] },
{ rcases lt_trichotomy 0 y with hy|rfl|hy,
{ simp only [top_mul_coe_of_pos hy, to_real_top, zero_mul] },
{ simp only [coe_zero, mul_zero, to_real_zero] },
{ simp only [top_mul_coe_of_neg hy, to_real_top, to_real_bot, zero_mul] } },
{ simp only [top_mul_top, to_real_top, mul_zero] }
-- TODO: replace with `induction using` in Lean 4, which supports multiple premises
with_cases
{ apply @induction₂ (λ x y, to_real (x * y) = to_real x * to_real y) };
propagate_tags { try { dsimp only} },
case [top_zero, bot_zero, zero_top, zero_bot] { all_goals { simp only [zero_mul, mul_zero,
to_real_zero] } },
case coe_coe : x y { norm_cast },
case top_top { rw [top_mul_top, to_real_top, mul_zero] },
case top_bot { rw [top_mul_bot, to_real_top, to_real_bot, zero_mul] },
case bot_top { rw [bot_mul_top, to_real_bot, zero_mul] },
case bot_bot { rw [bot_mul_bot, to_real_top, to_real_bot, zero_mul] },
case pos_bot : x hx
{ rw [to_real_bot, to_real_coe, coe_mul_bot_of_pos hx, to_real_bot, mul_zero] },
case neg_bot : x hx
{ rw [to_real_bot, to_real_coe, coe_mul_bot_of_neg hx, to_real_top, mul_zero] },
case pos_top : x hx
{ rw [to_real_top, to_real_coe, coe_mul_top_of_pos hx, to_real_top, mul_zero] },
case neg_top : x hx
{ rw [to_real_top, to_real_coe, coe_mul_top_of_neg hx, to_real_bot, mul_zero] },
case top_pos : y hy
{ rw [to_real_top, to_real_coe, top_mul_coe_of_pos hy, to_real_top, zero_mul] },
case top_neg : y hy
{ rw [to_real_top, to_real_coe, top_mul_coe_of_neg hy, to_real_bot, zero_mul] },
case bot_pos : y hy
{ rw [to_real_bot, to_real_coe, bot_mul_coe_of_pos hy, to_real_bot, zero_mul] },
case bot_neg : y hy
{ rw [to_real_bot, to_real_coe, bot_mul_coe_of_neg hy, to_real_top, zero_mul] },
end

protected lemma neg_mul (x y : ereal) : -x * y = -(x * y) :=
begin
induction x using ereal.rec; induction y using ereal.rec,
{ refl },
{ rcases lt_trichotomy 0 y with hy | rfl | hy,
{ rw [bot_mul_coe_of_pos hy, neg_bot, top_mul_coe_of_pos hy] },
{ rw [coe_zero, mul_zero, mul_zero, neg_zero] },
{ rw [bot_mul_coe_of_neg hy, neg_bot, neg_top, top_mul_coe_of_neg hy] } },
{ refl },
{ rcases lt_trichotomy 0 x with hx | rfl | hx,
{ rw [coe_mul_bot_of_pos hx, neg_bot, ← coe_neg, coe_mul_bot_of_neg (neg_neg_of_pos hx)], },
{ rw [coe_zero, zero_mul, neg_zero, zero_mul] },
{ rw [coe_mul_bot_of_neg hx, neg_top, ← coe_neg, coe_mul_bot_of_pos (neg_pos_of_neg hx)], }, },
{ norm_cast, exact neg_mul _ _, },
{ rcases lt_trichotomy 0 x with hx | rfl | hx,
{ rw [coe_mul_top_of_pos hx, neg_top, ← coe_neg, coe_mul_top_of_neg (neg_neg_of_pos hx)], },
{ rw [coe_zero, zero_mul, neg_zero, zero_mul] },
{ rw [coe_mul_top_of_neg hx, neg_bot, ← coe_neg, coe_mul_top_of_pos (neg_pos_of_neg hx)], }, },
{ refl },
{ rcases lt_trichotomy 0 y with hy | rfl | hy,
{ rw [top_mul_coe_of_pos hy, neg_top, bot_mul_coe_of_pos hy] },
{ rw [coe_zero, mul_zero, mul_zero, neg_zero] },
{ rw [top_mul_coe_of_neg hy, neg_top, neg_bot, bot_mul_coe_of_neg hy] } },
{ refl }
-- TODO: replace with `induction using` in Lean 4, which supports multiple premises
with_cases
{ apply @induction₂ (λ x y, -x * y = -(x * y)) };
propagate_tags { try { dsimp only} },
case [top_top, bot_top, top_bot, bot_bot] { all_goals { refl } },
case [top_zero, bot_zero, zero_top, zero_bot]
{ all_goals { simp only [zero_mul, mul_zero, neg_zero] } },
case coe_coe : x y { norm_cast, exact neg_mul _ _, },
case pos_bot : x hx
{ rw [coe_mul_bot_of_pos hx, neg_bot, ← coe_neg, coe_mul_bot_of_neg (neg_neg_of_pos hx)] },
case neg_bot : x hx
{ rw [coe_mul_bot_of_neg hx, neg_top, ← coe_neg, coe_mul_bot_of_pos (neg_pos_of_neg hx)] },
case pos_top : x hx
{ rw [coe_mul_top_of_pos hx, neg_top, ← coe_neg, coe_mul_top_of_neg (neg_neg_of_pos hx)] },
case neg_top : x hx
{ rw [coe_mul_top_of_neg hx, neg_bot, ← coe_neg, coe_mul_top_of_pos (neg_pos_of_neg hx)] },
case top_pos : y hy { rw [top_mul_coe_of_pos hy, neg_top, bot_mul_coe_of_pos hy] },
case top_neg : y hy { rw [top_mul_coe_of_neg hy, neg_top, neg_bot, bot_mul_coe_of_neg hy] },
case bot_pos : y hy { rw [bot_mul_coe_of_pos hy, neg_bot, top_mul_coe_of_pos hy] },
case bot_neg : y hy { rw [bot_mul_coe_of_neg hy, neg_bot, neg_top, top_mul_coe_of_neg hy] },
end

instance : has_distrib_neg ereal :=
Expand Down Expand Up @@ -783,75 +826,62 @@ by rcases lt_trichotomy 0 x with hx | rfl | hx; simp [abs_def]

@[simp] lemma abs_mul (x y : ereal) : (x * y).abs = x.abs * y.abs :=
begin
symmetry,
induction x using ereal.rec; induction y using ereal.rec,
{ refl },
{ rcases lt_trichotomy 0 y with hy|rfl|hy,
{ simp only [bot_mul_coe_of_pos hy, hy.ne', abs_bot, with_top.top_mul, ne.def, abs_eq_zero_iff,
coe_eq_zero, not_false_iff] },
{ simp only [coe_zero, abs_zero, mul_zero] },
{ simp only [bot_mul_coe_of_neg hy, hy.ne, abs_bot, with_top.top_mul, ne.def, abs_eq_zero_iff,
coe_eq_zero, not_false_iff, abs_top] } },
{ refl },
{ rcases lt_trichotomy 0 x with hx|rfl|hx,
{ simp only [coe_mul_bot_of_pos hx, hx.ne', abs_bot, with_top.mul_top, ne.def, abs_eq_zero_iff,
coe_eq_zero, not_false_iff] },
{ simp only [coe_zero, abs_zero, zero_mul] },
{ simp only [coe_mul_bot_of_neg hx, hx.ne, abs_bot, with_top.mul_top, ne.def, abs_eq_zero_iff,
coe_eq_zero, not_false_iff, abs_top] } },
{ simp only [← coe_mul, ereal.abs, abs_mul, ennreal.of_real_mul (abs_nonneg _)] },
{ rcases lt_trichotomy 0 x with hx|rfl|hx,
{ simp only [coe_mul_top_of_pos hx, hx.ne', with_top.mul_top, ne.def, abs_eq_zero_iff,
coe_eq_zero, not_false_iff, abs_top] },
{ simp only [coe_zero, abs_zero, zero_mul] },
{ simp only [coe_mul_top_of_neg hx, hx.ne, abs_bot, with_top.mul_top, ne.def, abs_eq_zero_iff,
coe_eq_zero, not_false_iff, abs_top] } },
{ refl },
{ rcases lt_trichotomy 0 y with hy|rfl|hy,
{ simp only [top_mul_coe_of_pos hy, hy.ne', with_top.top_mul, ne.def, abs_eq_zero_iff,
coe_eq_zero, not_false_iff, abs_top] },
{ simp only [coe_zero, abs_zero, mul_zero] },
{ simp only [top_mul_coe_of_neg hy, hy.ne, abs_bot, with_top.top_mul, ne.def, abs_eq_zero_iff,
coe_eq_zero, not_false_iff, abs_top] } },
{ refl }
-- TODO: replace with `induction using` in Lean 4, which supports multiple premises
with_cases
{ apply @induction₂ (λ x y, (x * y).abs = x.abs * y.abs) };
propagate_tags { try { dsimp only} },
case [top_top, bot_top, top_bot, bot_bot] { all_goals { refl } },
case [top_zero, bot_zero, zero_top, zero_bot] { all_goals { simp only [zero_mul, mul_zero,
abs_zero] } },
case coe_coe : x y { simp only [← coe_mul, ereal.abs, abs_mul,
ennreal.of_real_mul (abs_nonneg _)], },
case pos_bot : x hx { simp only [coe_mul_bot_of_pos hx, hx.ne', abs_bot, with_top.mul_top, ne.def,
abs_eq_zero_iff, coe_eq_zero, not_false_iff] },
case neg_bot : x hx { simp only [coe_mul_bot_of_neg hx, hx.ne, abs_bot, with_top.mul_top, ne.def,
abs_eq_zero_iff, coe_eq_zero, not_false_iff, abs_top] },
case pos_top : x hx { simp only [coe_mul_top_of_pos hx, hx.ne', with_top.mul_top, ne.def,
abs_eq_zero_iff, coe_eq_zero, not_false_iff, abs_top] },
case neg_top : x hx { simp only [coe_mul_top_of_neg hx, hx.ne, abs_bot, with_top.mul_top, ne.def,
abs_eq_zero_iff, coe_eq_zero, not_false_iff, abs_top] },
case top_pos : y hy { simp only [top_mul_coe_of_pos hy, hy.ne', with_top.top_mul, ne.def,
abs_eq_zero_iff, coe_eq_zero, not_false_iff, abs_top] },
case top_neg : y hy { simp only [top_mul_coe_of_neg hy, hy.ne, abs_bot, with_top.top_mul, ne.def,
abs_eq_zero_iff, coe_eq_zero, not_false_iff, abs_top] },
case bot_pos : y hy { simp only [bot_mul_coe_of_pos hy, hy.ne', abs_bot, with_top.top_mul, ne.def,
abs_eq_zero_iff, coe_eq_zero, not_false_iff] },
case bot_neg : y hy { simp only [bot_mul_coe_of_neg hy, hy.ne, abs_bot, with_top.top_mul, ne.def,
abs_eq_zero_iff, coe_eq_zero, not_false_iff, abs_top] },
end

/-! ### Sign -/

@[simp] lemma sign_top : sign (⊤ : ereal) = sign_type.pos := rfl
@[simp] lemma sign_bot : sign (⊥ : ereal) = sign_type.neg := rfl
@[simp] lemma sign_top : sign (⊤ : ereal) = 1 := rfl
@[simp] lemma sign_bot : sign (⊥ : ereal) = -1 := rfl
@[simp] lemma sign_coe (x : ℝ) : sign (x : ereal) = sign x :=
by simp only [sign, order_hom.coe_fun_mk, ereal.coe_pos, ereal.coe_neg']

@[simp] lemma sign_mul (x y : ereal) : sign (x * y) = sign x * sign y :=
begin
induction x using ereal.rec; induction y using ereal.rec,
{ refl },
{ rcases lt_trichotomy 0 y with hy|rfl|hy,
{ simp only [bot_mul_coe_of_pos hy, hy, sign_coe, sign_pos, mul_one] },
{ simp only [coe_zero, mul_zero, sign_zero] },
{ simp only [bot_mul_coe_of_neg hy, hy, sign_top, sign_type.pos_eq_one, sign_bot,
sign_type.neg_eq_neg_one, sign_coe, sign_neg, mul_neg, mul_one, neg_neg] } },
{ refl },
{ rcases lt_trichotomy 0 x with hx|rfl|hx,
{ simp only [coe_mul_bot_of_pos hx, hx, sign_bot, sign_type.neg_eq_neg_one, sign_coe, sign_pos,
mul_neg, mul_one] },
{ simp only [coe_zero, zero_mul, sign_zero] },
{ simp only [coe_mul_bot_of_neg hx, hx, sign_top, sign_type.pos_eq_one, sign_coe, sign_neg,
sign_bot, sign_type.neg_eq_neg_one, mul_neg, mul_one, neg_neg] } },
{ simp only [← coe_mul, sign_coe, sign_mul] },
{ rcases lt_trichotomy 0 x with hx|rfl|hx,
{ simp only [coe_mul_top_of_pos hx, hx, sign_coe, sign_pos, mul_one, zero_lt_top]},
{ simp only [coe_zero, zero_mul, sign_zero] },
{ simp only [coe_mul_top_of_neg hx, hx, sign_top, sign_type.pos_eq_one, sign_coe, sign_neg,
sign_bot, sign_type.neg_eq_neg_one, mul_one] } },
{ refl },
{ rcases lt_trichotomy 0 y with hy|rfl|hy,
{ simp only [top_mul_coe_of_pos hy, hy, sign_coe, sign_pos, mul_one] },
{ simp only [coe_zero, mul_zero, sign_zero] },
{ simp only [top_mul_coe_of_neg hy, hy, sign_top, sign_type.pos_eq_one, sign_bot,
sign_type.neg_eq_neg_one, sign_coe, sign_neg, mul_neg, mul_one]} },
{ refl }
-- TODO: replace with `induction using` in Lean 4, which supports multiple premises
with_cases
{ apply @induction₂ (λ x y, sign (x * y) = sign x * sign y) };
propagate_tags { try { dsimp only} },
case [top_top, bot_top, top_bot, bot_bot] { all_goals { refl } },
case [top_zero, bot_zero, zero_top, zero_bot] { all_goals { simp only [zero_mul, mul_zero,
sign_zero] } },
case coe_coe : x y { simp only [← coe_mul, sign_coe, sign_mul], },
case pos_bot : x hx { simp_rw [coe_mul_bot_of_pos hx, sign_coe, sign_pos hx, one_mul] },
case neg_bot : x hx { simp_rw [coe_mul_bot_of_neg hx, sign_coe, sign_neg hx, sign_top, sign_bot,
neg_one_mul, neg_neg] },
case pos_top : x hx { simp_rw [coe_mul_top_of_pos hx, sign_coe, sign_pos hx, one_mul] },
case neg_top : x hx { simp_rw [coe_mul_top_of_neg hx, sign_coe, sign_neg hx, sign_top, sign_bot,
mul_one] },
case top_pos : y hy { simp_rw [top_mul_coe_of_pos hy, sign_coe, sign_pos hy, mul_one] },
case top_neg : y hy { simp_rw [top_mul_coe_of_neg hy, sign_coe, sign_neg hy, sign_top, sign_bot,
one_mul] },
case bot_pos : y hy { simp_rw [bot_mul_coe_of_pos hy, sign_coe, sign_pos hy, mul_one] },
case bot_neg : y hy { simp_rw [bot_mul_coe_of_neg hy, sign_coe, sign_neg hy, sign_top, sign_bot,
neg_one_mul, neg_neg] },
end

lemma sign_mul_abs (x : ereal) :
Expand Down

0 comments on commit 634284e

Please sign in to comment.