Zulip Chat Archive

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,
    --apply lt_add_one,
  },
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: Dec 20 2023 at 11:08 UTC