Zulip Chat Archive

Stream: new members

Topic: Simplifying decidable propositions


view this post on Zulip Pedro Minicz (Jun 14 2020 at 02:06):

How do I simplify decidable propositions?

view this post on Zulip Pedro Minicz (Jun 14 2020 at 02:06):

def f (n : ) : bool :=
  if n = 0 then tt else if n = 1 then tt else ff

example : f 1 = tt :=
begin
  unfold f,
  sorry
end

view this post on Zulip Pedro Minicz (Jun 14 2020 at 02:07):

On sorry the goal is ite (1 = 0) tt (ite (1 = 1) tt ff) = tt. I know that 0 ≠ 1, so how do I simplify past the first ite.

view this post on Zulip Pedro Minicz (Jun 14 2020 at 02:09):

I know that comp_val can close this particular goal, but it wouldn't be able to if the whole expression wasn't computable.

view this post on Zulip Jalex Stark (Jun 14 2020 at 02:11):

norm_num closes the goal

view this post on Zulip Jalex Stark (Jun 14 2020 at 02:11):

split_ifs does something useful

view this post on Zulip Jalex Stark (Jun 14 2020 at 02:12):

example : f 1 = tt :=
begin
  unfold f,
  split_ifs; simp,
end

view this post on Zulip Jalex Stark (Jun 14 2020 at 02:13):

I think this is closer to the answer you were looking for,

def f (n : ) : bool :=
  if n = 0 then tt else if n = 1 then tt else ff

example : f 1 = tt :=
begin
  unfold f,
  rw if_neg, swap, { norm_num },
  rw if_pos, refl,
end

view this post on Zulip Pedro Minicz (Jun 14 2020 at 02:15):

Thank you! if_pos/if_neg work perfectly!

view this post on Zulip Jalex Stark (Jun 14 2020 at 02:19):

split_ifs does something like "rw with if_pos or if_neg at all the ites in the goal"

view this post on Zulip Jalex Stark (Jun 14 2020 at 02:19):

well, that's my mental model of it, tactic#split_ifs can say something more accurate

view this post on Zulip Pedro Minicz (Jun 14 2020 at 02:45):

Is there a tactic that does something like this:

import data.real.basic

def f (n : ) : bool :=
  if n = 0 then tt else if n = 1 then tt else ff

example :  n > 1, f n = ff
| 0 h := false.elim (not_lt_bot h)
| 1 h := false.elim (irrefl 1 h)
| (n+2) h := by { simp [f], split, cc, linarith }

view this post on Zulip Pedro Minicz (Jun 14 2020 at 02:47):

I'd like to have a convenient cases on , without having to apply casesmultiple times or refine a monstrous λ x, match x with ... end.

view this post on Zulip Bryan Gin-ge Chen (Jun 14 2020 at 02:58):

For this example, you don't need to pattern match at all:

import data.real.basic

def f (n : ) : bool :=
  if n = 0 then tt else if n = 1 then tt else ff

example {n : } (h : n > 1) : f n = ff :=
 by { simp [f], split; linarith }

view this post on Zulip Pedro Minicz (Jun 14 2020 at 03:02):

Yes, I am aware. It is just a toy example for demonstration.

view this post on Zulip Reid Barton (Jun 14 2020 at 03:08):

For a small number of cases you could write rcases n with _|_|_|_... otherwise it depends on what you want to do.

view this post on Zulip Pedro Minicz (Jun 14 2020 at 03:23):

Thanks that works perfectly.

view this post on Zulip Pedro Minicz (Jun 14 2020 at 03:24):

I had tried rcases n with ⟨_|_|_⟩ with no success. Good to know rcases can handle it.

view this post on Zulip Scott Morrison (Jun 14 2020 at 04:13):

Occasionally it's useful to do something like by_cases h : x < 5 and then in the "true" branch, interval_cases h, which explodes into individual cases.


Last updated: May 08 2021 at 18:17 UTC