Simplify decidable.cases_on

Stream: new members

[Horatiu Cheval]

I have a function

def f : ∀ (n m : ℕ), Prop := λ (n m : ℕ),
    decidable.cases_on (nat.decidable_eq n m)
    (λ h : n ≠ m, false)
    (λ h : n = m, true)

and I want to prove something like ∀ (n : ℕ), f n n.
So far, my solution is

example : ∀ (n : ℕ), f n n :=
begin
    intros n,
    unfold f,
    have : n = n := by simp,
    have : nat.decidable_eq n n = decidable.is_true this := by simp,
    rw this,
    simp,
end

but it seems too convoluted. Is there a better way?

Also, I noticed if I instead define

def f' : ∀ (n m : ℕ), Prop := λ (n m : ℕ),
    if n = m then true else false

then simp [f'] is enough to solve the goal, even though both f and f' unfold to the same expression (after unfolding ite in the case of f').

[Eric Wieser]

There is probably a missing simp lemma to convert decidable.cases_on into dite

[Horatiu Cheval]

Indeed, some simp lemmas for simple cases like this did what I needed. Thanks, I think I understand simp better now

[Eric Wieser]

In general though, you should use if ... then ... else instead of decidable.cases_on

[Horatiu Cheval]

I don't think I can. Essentially, what I'm trying to write is of the form def f (α β : Type) (x : α) := if α = β then cast x to β else ....
But cast needs an argument h : α = β which if ... then ... else hides. Maybe there is a way and I just couldn't figure it out.

[Mario Carneiro]

You should use function.update for that

[Mario Carneiro]

You can get a proof out from the if using if h : α = β then .. else .. btw

[Mario Carneiro]

that's dite (for "dependent if-then-else")

[Horatiu Cheval]

I see, that simplifies my code a lot, thanks!