Zulip Chat Archive

Stream: new members

Topic: timeout from nat.div_lt_self


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kendall Frey (Jul 17 2020 at 00:25):

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

view this post on Zulip Jalex Stark (Jul 17 2020 at 00:25):

see e.g. this for a smaller example

#reduce 100 * 555
#eval 100 * 555

view this post on Zulip 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

view this post on Zulip Jalex Stark (Jul 17 2020 at 00:26):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kendall Frey (Jul 17 2020 at 00:28):

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

view this post on Zulip 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

view this post on Zulip Jalex Stark (Jul 17 2020 at 00:36):

can you prove logish 2 = 2 at all?

view this post on Zulip Kendall Frey (Jul 17 2020 at 00:44):

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

view this post on Zulip Kendall Frey (Jul 17 2020 at 00:45):

I got logish 1 = 1 though.

view this post on Zulip 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.

view this post on Zulip Kendall Frey (Jul 17 2020 at 00:47):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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