Simplifying decidable propositions

Stream: new members

[Pedro Minicz]

How do I simplify decidable propositions?

[Pedro Minicz]

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

[Pedro Minicz]

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.

[Pedro Minicz]

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

[Jalex Stark]

norm_num closes the goal

[Jalex Stark]

split_ifs does something useful

[Jalex Stark]

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

[Jalex Stark]

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

[Pedro Minicz]

Thank you! if_pos/if_neg work perfectly!

[Jalex Stark]

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

[Jalex Stark]

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

[Pedro Minicz]

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 }

[Pedro Minicz]

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

[Bryan Gin-ge Chen]

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 }

[Pedro Minicz]

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

[Reid Barton]

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

[Pedro Minicz]

Thanks that works perfectly.

[Pedro Minicz]

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

[Scott Morrison]

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.