timeout from nat.div_lt_self

Stream: new members

[Kendall Frey]

Can anyone explain why this times out? Using #eval instead of #reduce works just fine.

def logish_rec : Π (n : ℕ), (Π (m : ℕ), m < n → ℕ) → ℕ :=
begin
  intros n logish,
  cases n,
  {
    exact 0,
  },
  refine logish (n.succ / 2) _ + 1,
  apply nat.div_lt_self, -- The problem is related to this somehow
  {
    sorry,
    --apply nat.succ_pos,
  },
  {
    sorry,
    --apply lt_add_one,
  },
end

def logish := well_founded.fix is_well_order.wf logish_rec

#reduce logish 1 -- (deterministic) timeout

[Jalex Stark]

to an approximation, reduce only uses definitional equality to the computation, but eval replaces some of that with smart algorithms

[Kendall Frey]

yeah, though I expected logish 1 to be definitionally equal to 1 with no problems.

[Jalex Stark]

see e.g. this for a smaller example

#reduce 100 * 555
#eval 100 * 555

[Jalex Stark]

oh i didn't really read what you wrote at all; let me try to give a more relevant answer

[Jalex Stark]

i'm not sure what you expect reduce to do with those sorries

[Kendall Frey]

It's not the sorries that are the problem, I only put them there to rule out problems related to those lemmas

[Kendall Frey]

Replacing nat.div_lt_self with sorry eliminates the timeout, which is why it must be something to do with that lemma

[Kendall Frey]

(although it still doesn't reduce all the way to 1)

[Kendall Frey]

I first started investigating this when I had a goal of the form 1 ≤ logish 2, and change 1 ≤ 2 failed, even though (in my mind) logish 2 seems definitionally equal to 2

[Jalex Stark]

can you prove logish 2 = 2 at all?

[Kendall Frey]

I don't know how, but I suppose it must be possible.

[Kendall Frey]

I got logish 1 = 1 though.

[Bryan Gin-ge Chen]

If you can't prove it by rfl then they're not defeq according to Lean.

[Kendall Frey]

Good point. I had to rw well_founded.fix_eq to prove logish 1 = 1

[Mario Carneiro]

Lean's implemented defeq differs from the theoretical version when it comes to well founded recursion. We try not to unfold proofs because they haven't been written with that in mind (and it's also kind of useless), but acc.rec iota reduction requires it

[Mario Carneiro]

I think I investigated a problem similar to this a while ago and found that propext was being used somewhere in a proof in order to use rw on an iff. This axiom blocked the reduction of the proof to rfl even though you can prove it by a suitable sequence like rfl.trans $ rfl.trans rfl with carefully chosen intermediate terms

[Bryan Gin-ge Chen]

I starred that post since it was so cool! https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/noob.20question%28s%29/near/196855763