proving things about functions defined by cases

Stream: new members

[Keefer Rowan]

How do I complete the following?

noncomputable def f : ℕ → ℕ :=
begin
    intro x,
    have : decidable (x = 5),
        apply classical.prop_decidable,
    cases this,
        exact 1,
        exact 2
end

example : f 5 = 1 :=
begin
    sorry,
end

I don't know what tactic to use to try to split into the cases by which f was defined.

Also, is there a way to clean up my definition to get rid of the have : decidable (x=5)?

Note: I know that I don't need classical reasoning for decidability of = in nat, but this is just an example.

[Bhavik Mehta]

Here's how I'd write your example:

def f (n : ℕ) : ℕ :=
if n = 5
  then 1
  else 2

example : f 5 = 1 :=
rfl

[Bhavik Mehta]

You can use the split_ifs tactic in more complex examples to break up an if in general

[Bhavik Mehta]

You could alternatively do:

def f : ℕ → ℕ
| 5 := 1
| _ := 2

example : f 5 = 1 :=
rfl

[Bhavik Mehta]

Alternatively,

def f (n : ℕ) : ℕ :=
begin
  by_cases (n = 5),
  { exact 1 },
  { exact 2 }
end

example : f 5 = 1 :=
rfl

[Keefer Rowan]

@Bhavik Mehta Thanks for the info on cleaning up the definitions.

Lean isn't recognizing split_ifs; what should I import to make it work?

[Mario Carneiro]

import tactic gets you a bunch of things

[Mario Carneiro]

the precise import is import tactic.split_ifs

[Keefer Rowan]

I'm getting file 'tactic' not found in the LEAN_PATH

[Keefer Rowan]

I'm not using anything from mathlib right now, likely has something to do with that. Do I need to read about the mathlib projects thing to get this to work?

[Bryan Gin-ge Chen]

Yes, see the instructions here.

[Jalex Stark]

Keefer Rowan said:

I'm not using anything from mathlib right now, likely has something to do with that. Do I need to read about the mathlib projects thing to get this to work?

It may sound scary but actually should be pretty easy, if you follow instructions precisely you should be able to start using mathlib in just a few minutes without entering more than 10 terminal commands

[Keefer Rowan]

Ok, I'll start working on it

[Keefer Rowan]

split_ifs isn't working.

Here's where I am; I can't come up with a shorter example (and this is reasonably short and self-contained) so here it is:

import tactic

open classical function

attribute [instance] classical.prop_decidable

universes u v
variables {α : Type u} {β : Type v}

def injection (f : α → β) : Prop :=
    ∀ x y, f x = f y → x = y

def left_inv (f : α → β) (g : β → α) : Prop :=
    g ∘ f  = id

def has_left_inv (f : α → β) : Prop :=
    ∃ g, left_inv f g


noncomputable def left_inv_func [h₁ : inhabited α] (f : α → β) : β → α :=
begin
    intro b,
    by_cases (b ∈ set.image f set.univ),
        {unfold set.image has_mem.mem set.mem set_of at h,
        exact some h},
        {exact h₁.default}
end

theorem injection_left_inv_iff [inhabited α] {f : α → β} : injection f ↔ has_left_inv f :=
begin
    split; intro h,
        {let g:= left_inv_func f,
        apply exists.intro g,
        unfold left_inv,
        unfold comp,
        apply funext,
        intro x,
        simp,
        split_ifs,}
end

I'm getting the error: no if-then-else expressions to split. How should I finish this proof?

[Mario Carneiro]

You should not use tactics to define data (the function left_inv_func)

[Mario Carneiro]

instead, use \lam b, if h : b ∈ set.image f set.univ then some h else h₁.default

[Mario Carneiro]

and then the theorem can use split_ifs profitably

[Yury G. Kudryashov]

I assumed that this tactic will generate the same definition.

[Yury G. Kudryashov]

@Keefer Rowan You can always look at the actual definition using #print left_inv_func

[Keefer Rowan]

Non-tactic definition:

noncomputable def function.left_inv_func : Π {α : Type u} {β : Type v} [h₁ : inhabited α], (α → β) → β → α :=
λ {α : Type u} {β : Type v} [h₁ : inhabited α] (f : α → β) (b : β),
  dite (b ∈ f '' set.univ) (λ (h : b ∈ f '' set.univ), some h) (λ (h : b ∉ f '' set.univ), default α)

Tactic definition :

noncomputable def function.left_inv_func : Π {α : Type u} {β : Type v} [h₁ : inhabited α], (α → β) → β → α :=
λ {α : Type u} {β : Type v} [h₁ : inhabited α] (f : α → β) (b : β),
  dite (b ∈ f '' set.univ) (λ (h : b ∈ f '' set.univ), some _) (λ (h : b ∉ f '' set.univ), default α)

They are indeed the same, and so I'm still stuck. Even with the non-tactic definition, split_ifs doesn't work.

[Mario Carneiro]

When you call split_ifs, dite should be visible in the goal

[Reid Barton]

It looks like you are not unfolding left_inv_func, so there is no if visible.

[Yury G. Kudryashov]

BTW, we already have this as inv_fun_on/inv_fun in logic/function/basic

[Keefer Rowan]

Ok, I assumed it would do the unfolding, but it is (mostly) working after unfolding, however, I can only get the unfold to work if if I have:

theorem injection_left_inv_iff [inhabited α] {f : α → β} : injection f ↔ has_left_inv f :=
begin
    split; intro h,
        {let g := left_inv_func f,
        apply exists.intro g,
        unfold left_inv,
        unfold comp,
        apply funext,
        intro x,
        simp,
        unfold left_inv_func,}
end

If I introduce to the notation let g := left_inv_func f e.g. in

theorem injection_left_inv_iff [inhabited α] {f : α → β} : injection f ↔ has_left_inv f :=
begin
    split; intro h,
        {
apply exists.intro (left_inv_func f),
        unfold left_inv,
        unfold comp,
        apply funext,
        intro x,
        simp,
        unfold left_inv_func,}
end

[Mario Carneiro]

you have to unfold g as well if you make a let

[Mario Carneiro]

unfortunately unfold doesn't work on let but dsimp only [g] should

[Keefer Rowan]

Sorry a bit confused by those two messages together. How do I unfold g? By dsimp only [g]?

[Mario Carneiro]

yes

[Keefer Rowan]

Ok thanks! It's all coming together now!

[Scott Morrison]

Arguably split_ifs should be more aggressive, so that if it fails to find an if statement it does some amount of unfolding. Where and how much to unfold, of course, is unclear.

[Johan Commelin]

Maybe it could take some arguments? So that

dsimp [foo, bar, quux], split_ifs

can be written as

split_ifs [foo, bar, quux]