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
simp [f'] is enough to solve the goal, even though both
f' unfold to the same expression (after unfolding
ite in the case of
Eric Wieser (Feb 09 2021 at 09:26):
There is probably a missing simp lemma to convert decidable.cases_on into
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
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):
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