# Zulip Chat Archive

## Stream: new members

### Topic: Simplify decidable.cases_on

#### Horatiu Cheval (Feb 09 2021 at 09:23):

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 (Feb 09 2021 at 09:26):

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

#### Horatiu Cheval (Feb 10 2021 at 17:13):

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

#### Eric Wieser (Feb 10 2021 at 17:30):

In general though, you should use `if ... then ... else`

instead of `decidable.cases_on`

#### Horatiu Cheval (Feb 10 2021 at 21:01):

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 (Feb 10 2021 at 21:02):

You should use `function.update`

for that

#### Mario Carneiro (Feb 10 2021 at 21:03):

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

btw

#### Mario Carneiro (Feb 10 2021 at 21:04):

that's `dite`

(for "dependent if-then-else")

#### Horatiu Cheval (Feb 10 2021 at 21:19):

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

Last updated: May 14 2021 at 06:16 UTC