## Stream: new members

### Topic: unpacking ite / dite on one side of an equation

#### Kris Brown (Jun 18 2020 at 16:30):

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)):
:=  or.elim (decidable.em (m.val < n))
(by begin
intros h, -- m.val < n, should enter the IF branch
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 (Jun 18 2020 at 16:35):

Does dsimp, split_ifs work?

#### Johan Commelin (Jun 18 2020 at 16:35):

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

#### Kris Brown (Jun 18 2020 at 16:38):

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 (Jun 18 2020 at 16:39):

squeeze_simp

#### Bryan Gin-ge Chen (Jun 18 2020 at 16:40):

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 (Jun 18 2020 at 16:42):

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 (Jun 18 2020 at 16:48):

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 (Jun 18 2020 at 16:50):

(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 (Jun 18 2020 at 16:51):

rw dif_pos h or rw dif_neg h

Last updated: May 14 2021 at 23:14 UTC