# Zulip Chat Archive

## Stream: maths

### Topic: define a function by cases

#### Joseph Corneli (Apr 11 2019 at 11:39):

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 (Apr 11 2019 at 11:42):

import data.real.basic data.set.intervals def f (x : ℝ) : ℝ := if x ∈ set.Icc (0 : ℝ) 1 then 1 else 0

#### Joseph Corneli (Apr 11 2019 at 11:45):

thanks

#### Joseph Corneli (Apr 11 2019 at 11:49):

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

#### Joseph Corneli (Apr 11 2019 at 11:50):

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

#### Joseph Corneli (Apr 11 2019 at 11:52):

Actually, Lean complains about the code above:

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

#### Chris Hughes (Apr 11 2019 at 11:53):

Put this at the start of your file.

`local attribute [instance] classical.prop_decidable`

#### Joseph Corneli (Apr 11 2019 at 11:56):

Nice, it works now.

#### Joseph Corneli (Apr 11 2019 at 11:57):

Thanks Chris.

#### Joseph Corneli (Apr 11 2019 at 12:12):

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 (Apr 11 2019 at 12:17):

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 (Apr 11 2019 at 12:19):

Aha, "function extensionality" is great

#### Joseph Corneli (Apr 11 2019 at 12:20):

Denied by Haskellists IIUC

#### Joseph Corneli (Apr 11 2019 at 15:54):

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 (Apr 11 2019 at 15:58):

`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 (Apr 11 2019 at 16:14):

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 (Apr 11 2019 at 16:15):

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 (Apr 11 2019 at 17:58):

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 (Apr 11 2019 at 18:04):

I guess I could break this down into two lemmas, each similar to `on_unit_eq_one`

from before.

#### Reid Barton (Apr 11 2019 at 18:06):

You could try `apply continuous_if`

--now you'll have several more things to prove

#### Scott Olson (Apr 11 2019 at 18:07):

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

?

#### Joseph Corneli (Apr 11 2019 at 18:07):

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 (Apr 11 2019 at 18:09):

@Scott Olson :grinning_face_with_smiling_eyes:

#### Reid Barton (Apr 11 2019 at 18:11):

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

#### Reid Barton (Apr 11 2019 at 18:11):

although I think it's also not that hard

#### Joseph Corneli (Apr 11 2019 at 18:14):

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

Last updated: May 10 2021 at 06:13 UTC