unpacking ite / dite on one side of an equation

Stream: new members

[Kris Brown]

Hi, I'm trying to understand how to unpack an if-then-else function when it's nested in an equality statement. split_ifs isn't able to detect any if-then-else expressions to split. Is there a simple way to do this?

import data.fintype.basic
import data.equiv.basic
open equiv -- "perm x" is "equiv x x" AKA "x ≃ x"

-- Add two extra elems to the set being permuted.
def add_two_to_perm_forward {n: ℕ} (p : perm (fin n)) : fin (n+2) → fin(n+2) :=
    λ m : fin (n+2), if h: m.val < n then p.to_fun ⟨m.val, h⟩ else m
def add_two_to_perm_reverse {n: ℕ} (p : perm (fin n)) : fin (n+2) → fin(n+2) :=
    λ m : fin (n+2), if h: m.val < n then p.inv_fun ⟨m.val, h⟩ else m

-- Show that this new permutation has a left inverse
lemma add_two_leftinv {n : ℕ} (p : perm (fin n)) (m: fin (n+2)):
    add_two_to_perm_forward p (add_two_to_perm_reverse p m) = m
    :=  or.elim (decidable.em (m.val < n))
            (by begin
            intros h, -- m.val < n, should enter the IF branch
            rw add_two_to_perm_forward, rw add_two_to_perm_reverse,
            sorry end)
            (by begin
            intros h, -- ¬m.val < n, should enter the ELSE branch
            sorry end)

In the first branch my tactic state is

1 goal
n : ℕ,
p : perm (fin n),
m : fin (n + 2),
h : m.val < n
⊢ (λ (m : fin (n + 2)),
       dite (m.val < n) (λ (h : m.val < n), ↑(p.to_fun ⟨m.val, h⟩)) (λ (h : ¬m.val < n), m))
      ((λ (m : fin (n + 2)),
          dite (m.val < n) (λ (h : m.val < n), ↑(p.inv_fun ⟨m.val, h⟩)) (λ (h : ¬m.val < n), m))
         m) =
    m

[Johan Commelin]

Does dsimp, split_ifs work?

[Johan Commelin]

Or do you need to funext first? No, doesn't look like that.

[Kris Brown]

That did do something! Off the top of my head, not sure what dite is or how to eliminate.

1 goal
n : ℕ,
p : perm (fin n),
m : fin (n + 2),
h : m.val < n
⊢ dite
      ((dite (m.val < n) (λ (h : m.val < n), ↑↑(⇑(equiv.symm p) ⟨m.val, h⟩)) (λ (h : ¬m.val < n), m)).val <
         n)
      (λ
       (h_1 :
         (dite (m.val < n) (λ (h : m.val < n), ↑↑(⇑(equiv.symm p) ⟨m.val, h⟩))
              (λ (h : ¬m.val < n), m)).val <
           n), ↑↑(⇑p ⟨↑↑(⇑(equiv.symm p) ⟨m.val, h⟩).val, _⟩))
      (λ
       (h_1 :
         ¬(dite (m.val < n) (λ (h : m.val < n), ↑↑(⇑(equiv.symm p) ⟨m.val, h⟩))
                (λ (h : ¬m.val < n), m)).val <
             n), ↑↑(⇑(equiv.symm p) ⟨m.val, h⟩)) =
    m

I'm trying to avoid simp as a beginner though to avoid relying on magic - unless there is a way to inspect which sequence of tactics simp came up with to prove the goal? (that's a different question that's been on my mind)

[Johan Commelin]

squeeze_simp

[Bryan Gin-ge Chen]

There's also set_option trace.simplify.rewrite true. See the simp tutorial here: https://leanprover-community.github.io/extras/simp.html

We should probably add this info to the simp docstring.

[Reid Barton]

if h: m.val < n then p.to_fun ⟨m.val, h⟩ else m is
dite (m.val < n) (\lam h, ...) (\lam h, ...).

[Kris Brown]

Thanks! Though I wasn't able to find a squeeze_dsimp version . And set_option trace.simplify.rewrite true gives me info underneath split_ifs but not dsimp.

[Kris Brown]

(I'm happy to use dsimp here, though). A follow up is how to eliminate dite b x y when I have a term h: b or h: ¬b

[Johan Commelin]

rw dif_pos h or rw dif_neg h