## Stream: general

### Topic: timeout with split_ifs

#### Kenny Lau (Jul 28 2018 at 07:02):

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 (Jul 28 2018 at 07:02):

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

#### Kevin Buzzard (Jul 28 2018 at 07:34):

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 (Jul 28 2018 at 07:34):

it should be decidable

#### Kenny Lau (Jul 28 2018 at 07:34):

but Lean is not very intelligent

#### Kevin Buzzard (Jul 28 2018 at 07:35):

Is there some missing instance decidable.dite?

#### Kevin Buzzard (Jul 28 2018 at 07:54):

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 (Jul 28 2018 at 08:00):

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

#### Gabriel Ebner (Jul 28 2018 at 08:15):

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

#### Kevin Buzzard (Jul 28 2018 at 08:15):

Nice one Gabriel.

#### Gabriel Ebner (Jul 28 2018 at 08:16):

Apparently simp cannot simplify the second ite.

#### Kenny Lau (Jul 28 2018 at 08:17):

thanks

Last updated: Dec 20 2023 at 11:08 UTC