Zulip Chat Archive

Stream: new members

Topic: Simplify decidable.cases_on


view this post on Zulip 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').

view this post on Zulip Eric Wieser (Feb 09 2021 at 09:26):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 10 2021 at 17:30):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 10 2021 at 21:02):

You should use function.update for that

view this post on Zulip Mario Carneiro (Feb 10 2021 at 21:03):

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

view this post on Zulip Mario Carneiro (Feb 10 2021 at 21:04):

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

view this post on Zulip 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