# Zulip Chat Archive

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

Does `dsimp, split_ifs`

work?

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

~~Or do you need to ~~ No, doesn't look like that.`funext`

first?

#### 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: Dec 20 2023 at 11:08 UTC