Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 18 2020 at 16:35):

Does dsimp, split_ifs work?

view this post on Zulip Johan Commelin (Jun 18 2020 at 16:35):

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

view this post on Zulip 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)

view this post on Zulip Johan Commelin (Jun 18 2020 at 16:39):

squeeze_simp

view this post on Zulip 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.

view this post on Zulip 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, ...).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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