define a function by cases

Stream: maths

[Joseph Corneli]

I know about function.restrict, which allows me to take a function and look at it over a subtype, but what about going the other way, and building up a function from components? E.g., suppose I want to define $\chi_{[0,1]}$ which is 1 on $[0,1]$ and 0 elsewhere?

[Chris Hughes]

import data.real.basic data.set.intervals

def f (x : ℝ) : ℝ :=
if x ∈ set.Icc (0 : ℝ) 1 then 1 else 0

[Joseph Corneli]

thanks

[Joseph Corneli]

I wonder why I did not retain this information after reading TIPL.

[Joseph Corneli]

Probably it was a case of too much new stuff all at once.

[Joseph Corneli]

Actually, Lean complains about the code above:

failed to synthesize type class instance for
x : ℝ
⊢ decidable (x ∈ set.Icc 0 1)

[Chris Hughes]

Put this at the start of your file.
local attribute [instance] classical.prop_decidable

[Joseph Corneli]

Nice, it works now.

[Joseph Corneli]

Thanks Chris.

[Joseph Corneli]

Maybe you can guess what my next question is. I'm stuck again.

import data.real.basic data.set.intervals topology.basic analysis.exponential
local attribute [instance] classical.prop_decidable

noncomputable def unit_indicator (x : ℝ) : ℝ := if x ∈ set.Icc (0 : ℝ) 1 then 1 else 0

noncomputable def on_unit := function.restrict unit_indicator (set.Icc (0 : ℝ) 1)

lemma on_unit_cont : continuous on_unit :=
begin
  unfold on_unit function.restrict unit_indicator,
  -- ...
end

[Chris Hughes]

lemma on_unit_eq_one : on_unit = (λ x, 1) := funext (λ x, if_pos x.property)

lemma on_unit_cont : continuous on_unit :=
begin
  rw on_unit_eq_one,
  exact continuous_const,
  -- ...
end

[Joseph Corneli]

Aha, "function extensionality" is great

[Joseph Corneli]

Denied by Haskellists IIUC

[Joseph Corneli]

Here's another related question. Why can't I unfold fake_abs here?

import data.real.basic data.set.intervals topology.basic analysis.exponential
local attribute [instance] classical.prop_decidable

open real

noncomputable def fake_abs (x : ℝ) : ℝ := if x ≤ 0 then -x else x

lemma fake_abs_is_abs : fake_abs = (λ x, abs x)  :=
begin
unfold fake_abs,
sorry,
end

I get

simplify tactic failed to simplify
state:
⊢ fake_abs = λ (x : ℝ), abs x

[Chris Hughes]

unfold does simp using the equation lemmas. Try looking at the output of this

noncomputable def fake_abs (x : ℝ) : ℝ := if x ≤ 0 then -x else x

noncomputable def fake_abs' : ℝ → ℝ := λ x, if x ≤ 0 then -x else x

#print fake_abs.equations._eqn_1

#print fake_abs'.equations._eqn_1

unfold fake_abs' will have the behaviour you want, due to the different equation lemma.

[Kevin Buzzard]

This also makes progress:

import data.real.basic data.set.intervals topology.basic analysis.exponential
local attribute [instance] classical.prop_decidable

open real

noncomputable def fake_abs (x : ℝ) : ℝ := if x ≤ 0 then -x else x

lemma fake_abs_is_abs : fake_abs = (λ x, abs x)  :=
begin
  ext,
  unfold fake_abs,
  sorry
end

Note: #print prefix fake_abs.equations prints the equation lemmas for your fake_abs.

[Kevin Buzzard]

The way you set it up, unfold can only make progress when faced with something of the form fake_abs x (and not just fakeabs); this is what the functional extensionality tactic gives you.

[Joseph Corneli]

I could prove that fake_abs is equal to abs, but I've gotten stuck with the continuity part of the exercise.

import data.real.basic data.set.intervals topology.basic analysis.exponential tactic.fin_cases
local attribute [instance] classical.prop_decidable

open real

-- Use the version that will unfold properly
noncomputable def fake_abs : ℝ → ℝ := λ x, if x < 0 then -x else x

lemma fake_abs_is_abs : fake_abs = (λ x, abs x)  :=
begin
unfold fake_abs abs,
funext,
by_cases x < 0,
simp [if_pos h],
have he : -x > 0, from neg_pos_of_neg h,
have hl : -x > x, from lt_trans h he,
have hm : max x (-x) = -x, from max_eq_right_of_lt hl,
exact hm.symm,
simp [if_neg h],
have he : 0 ≤ x, from begin simp at h, exact h, end,
have hl : -x ≤ 0, from neg_nonpos_of_nonneg he,
have hll : -x ≤ x, from le_trans hl he,
have hm : max x (-x) = x, from max_eq_left hll,
exact hm.symm,
end

lemma continuous_fake_abs : continuous fake_abs := begin
unfold fake_abs,
-- ⊢ continuous (λ (x : ℝ), ite (x < 0) (-x) x)
end

[Joseph Corneli]

I guess I could break this down into two lemmas, each similar to on_unit_eq_one from before.

[Reid Barton]

You could try apply continuous_if--now you'll have several more things to prove

[Scott Olson]

I'm assuming it's against the spirit of the exercise to rw fake_abs_is_abs, apply continuous_abs?

[Joseph Corneli]

Right, and here I was thinking that continuous_if would be too much magic because the boundary would be in general too complicated.

[Joseph Corneli]

@Scott Olson :grinning_face_with_smiling_eyes:

[Reid Barton]

Identifying the boundary is the main work that you will have to do

[Reid Barton]

although I think it's also not that hard

[Joseph Corneli]

It should be interesting... a bit of topology sneaks in after all. Time for dinner here; thanks for the help.