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