## Stream: new members

### Topic: timeout from nat.div_lt_self

#### Kendall Frey (Jul 17 2020 at 00:22):

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,
},
end

def logish := well_founded.fix is_well_order.wf logish_rec

#reduce logish 1 -- (deterministic) timeout


#### Jalex Stark (Jul 17 2020 at 00:24):

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

#### Kendall Frey (Jul 17 2020 at 00:25):

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

#### Jalex Stark (Jul 17 2020 at 00:25):

see e.g. this for a smaller example

#reduce 100 * 555
#eval 100 * 555


#### Jalex Stark (Jul 17 2020 at 00:26):

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

#### Jalex Stark (Jul 17 2020 at 00:26):

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

#### Kendall Frey (Jul 17 2020 at 00:26):

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

#### Kendall Frey (Jul 17 2020 at 00:27):

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

#### Kendall Frey (Jul 17 2020 at 00:28):

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

#### Kendall Frey (Jul 17 2020 at 00:32):

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 (Jul 17 2020 at 00:36):

can you prove logish 2 = 2 at all?

#### Kendall Frey (Jul 17 2020 at 00:44):

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

#### Kendall Frey (Jul 17 2020 at 00:45):

I got logish 1 = 1 though.

#### Bryan Gin-ge Chen (Jul 17 2020 at 00:45):

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

#### Kendall Frey (Jul 17 2020 at 00:47):

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

#### Mario Carneiro (Jul 17 2020 at 01:50):

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 (Jul 17 2020 at 01:53):

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 (Jul 17 2020 at 03:08):

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

Last updated: May 14 2021 at 03:27 UTC