## Stream: general

### Topic: squeeze_simp and simp only disagreeing

#### Yakov Pechersky (Sep 10 2020 at 03:43):

Is there something I don't understand about simplifying in a dite conditional? Why do the first two examples work, but the third one doesn't?

import data.fin

variables {n : ℕ}

open fin

@[simp] lemma succ_above_lt_iff (p : fin (n + 1)) (i : fin n) : p.succ_above i < p ↔ i.cast_succ < p :=
begin
refine iff.intro _ _,
{ intro h,
cases succ_above_lt_ge p i with H H,
{ exact H },
{ rw succ_above_above _ _ H at h,
exact lt_trans (cast_succ_lt_succ i) h } },
{ intro h,
rw succ_above_below _ _ h,
exact h }
end

example (p : fin (n + 1)) (i : fin n) :
p.pred_above (p.succ_above i) (succ_above_ne _ _) = i :=
begin
rw pred_above,
simp, -- it's able to simp in the dite condition
/-
n : ℕ,
p : fin (n + 1),
i : fin n
⊢ dite (i.cast_succ < p) (λ (h : i.cast_succ < p), (p.succ_above i).cast_lt _)
(λ (h : ¬i.cast_succ < p), (p.succ_above i).pred _) =
i
-/
sorry
end

example (p : fin (n + 1)) (i : fin n) :
p.pred_above (p.succ_above i) (succ_above_ne _ _) = i :=
begin
rw pred_above,
squeeze_simp, -- still able to simp in the dite condition, suggests succ_above_lt_iff
sorry
end

example (p : fin (n + 1)) (i : fin n) :
p.pred_above (p.succ_above i) (succ_above_ne _ _) = i :=
begin
rw pred_above,
simp only [succ_above_lt_iff], -- simplify tactic failed to simplify
sorry
end


#### Johan Commelin (Sep 10 2020 at 05:13):

Yes, this is really annoying. I don't understand the details, but it's a known issue. And I think people have ideas on how to improve this.

Last updated: May 14 2021 at 04:22 UTC