timeout with split_ifs

Stream: general

[Kenny Lau]

import data.fin

variable {n : ℕ}

def fin.fall : Π i : fin (n+1), i.1 < n → fin n :=
λ i h, ⟨i.1, h⟩

def fin.descend (pivot : fin (n+1)) : Π i : fin (n+1), i ≠ pivot → fin n :=
λ i H, if h : i.1 < pivot.1
  then i.fall (lt_of_lt_of_le h $ nat.le_of_lt_succ pivot.2)
  else i.pred (λ H1, H $ by subst H1;
    replace h := nat.eq_zero_of_le_zero (le_of_not_gt h);
    from fin.eq_of_veq h.symm)

def fin.ascend (pivot : fin (n+1)) : Π i : fin n, fin (n+1) :=
λ i, if i.1 < pivot.1 then i.raise else i.succ

@[simp] lemma fin.descend_ascend (pivot : fin (n+1))
  (i : fin n) (H : pivot.ascend i ≠ pivot) :
  pivot.descend (pivot.ascend i) H = i :=
begin
  unfold fin.descend fin.ascend,
  split_ifs -- (deterministic) timeout
end

[Kenny Lau]

I've used split_ifs quite a lot but it just happens to timeout here

[Kevin Buzzard]

begin
  unfold fin.descend fin.ascend,
  have P := (ite (i.val < pivot.val) (fin.raise i) (fin.succ i)).val < pivot.val,
  let dP : decidable P := by apply_instance, -- fails

Is P decidable? It looks decidable to me.

[Kenny Lau]

it should be decidable

[Kenny Lau]

but Lean is not very intelligent

[Kevin Buzzard]

Is there some missing instance decidable.dite?

[Kevin Buzzard]

Is there some missing instance decidable.dite?

P is just the statement that some nat is less than some other nat, right? But example (a b : ℕ) : decidable (a < b) := by apply_instance works fine

[Kevin Buzzard]

Oh I'm being an idiot. I've used have instead of let again.

[Gabriel Ebner]

https://github.com/leanprover/mathlib/pull/224

[Kevin Buzzard]

Nice one Gabriel.

[Gabriel Ebner]

Apparently simp cannot simplify the second ite.

[Kenny Lau]

thanks