Zulip Chat Archive

Stream: new members

Topic: dec_trivial fails


view this post on Zulip Kenny Lau (Oct 30 2018 at 20:52):

import data.rat

def rat.sqrt (q : ) :  :=
rat.mk (nat.sqrt $ int.to_nat q.num) (nat.sqrt q.denom)

example : rat.sqrt 2 = 1 := dec_trivial -- fails

#eval rat.sqrt 2 -- 1

view this post on Zulip Kenny Lau (Oct 30 2018 at 20:52):

Why does dec_trivial fail?

view this post on Zulip Kenny Lau (Oct 30 2018 at 20:55):

@Chris Hughes

view this post on Zulip Kenny Lau (Oct 30 2018 at 21:09):

example : nat.sqrt (int.to_nat 2) = 1 := dec_trivial -- fails
example : nat.sqrt 1 = 1 := dec_trivial -- fails
example : rat.mk 1 1 = 1 := dec_trivial -- succeeds

view this post on Zulip Kenny Lau (Oct 30 2018 at 21:10):

ok so the problem boils down to this

view this post on Zulip Kenny Lau (Oct 30 2018 at 21:10):

import data.nat.sqrt

example : nat.sqrt 1 = 1 := dec_trivial -- fails

view this post on Zulip Scott Olson (Oct 30 2018 at 21:15):

Looks like it goes nat.sqrt -> nat.size -> nat.binary_rec and binary_rec reduces very slowly, so dec_trivial gives up

view this post on Zulip Kevin Buzzard (Oct 30 2018 at 21:16):

From data.nat.sqrt:

def sqrt (n : ) :  :=
match size n with
| 0      := 0
| succ s := sqrt_aux (shiftl 1 (bit0 (div2 s))) 0 n
end
import data.nat.sqrt

open nat

#eval size (1 : ) -- 1
#check size (1 : ) -- ℕ

example : nat.sqrt 1 = 1 := dec_trivial -- fails

example : sqrt_aux (shiftl 1 (bit0 (div2 0))) 0 1 = 1 := dec_trivial -- works?

view this post on Zulip Kevin Buzzard (Oct 30 2018 at 21:17):

Yes Scott has seen the right path -- example : size 1 = 1 := dec_trivial fails

view this post on Zulip Scott Olson (Oct 30 2018 at 21:19):

I get failure for the sqrt_aux line

view this post on Zulip Kevin Buzzard (Oct 30 2018 at 21:19):

Did you open nat?

view this post on Zulip Scott Olson (Oct 30 2018 at 21:19):

Yes

view this post on Zulip Kenny Lau (Oct 30 2018 at 21:21):

hmm

view this post on Zulip Kenny Lau (Oct 30 2018 at 21:21):

this is troublesome

view this post on Zulip Kenny Lau (Oct 30 2018 at 21:21):

because we can't change nat.binary_rec

view this post on Zulip Kenny Lau (Oct 30 2018 at 21:21):

well maybe we can write nat.binary_rec' just like we do other functions

view this post on Zulip Kevin Buzzard (Oct 30 2018 at 21:25):

example : binary_rec 0 (λ_ _, succ) 1 = 1 := begin
  unfold binary_rec,
  split_ifs,
    cases h,
  refl,
end

Maybe you can add some sort of decidability instance for size?

view this post on Zulip Kevin Buzzard (Oct 30 2018 at 21:27):

I don't think you need to go down as far as binary_rec.

view this post on Zulip Kenny Lau (Oct 30 2018 at 21:28):

I don't see how we can just add decidability instance.

view this post on Zulip Kevin Buzzard (Oct 30 2018 at 21:28):

You know more about decidability than me.

view this post on Zulip Kevin Buzzard (Oct 30 2018 at 21:28):

decidable (size a = b)?

view this post on Zulip Kenny Lau (Oct 30 2018 at 21:28):

that wouldn't be useful

view this post on Zulip Kenny Lau (Oct 30 2018 at 21:29):

because I can have another function that calls size

view this post on Zulip Kevin Buzzard (Oct 30 2018 at 21:29):

Or "computability" or something? I have no idea how these things work.

view this post on Zulip Kenny Lau (Oct 30 2018 at 21:29):

I don't see any other solution than rewriting some functions in the chain, but maybe @Mario Carneiro would have some idea

view this post on Zulip Kevin Buzzard (Oct 30 2018 at 21:30):

So what's going on here? You need to make sure that the...kernel? VM? can compute size a?

view this post on Zulip Kevin Buzzard (Oct 30 2018 at 21:31):

I don't really understand how a = b can fail to be proved by dec_trivial (if a and b are explicit computable nats). Equality on nat is decidable, so whatever runs dec_trivial just has to work out what a and b are and then check that they're equal.

view this post on Zulip Kevin Buzzard (Oct 30 2018 at 21:32):

and any nat in Lean is reducible to succ succ ... succ zero

view this post on Zulip Kevin Buzzard (Oct 30 2018 at 21:37):

Aah I understand more about the problem now. #reduce size 1 is a deterministic timeout.

view this post on Zulip Kevin Buzzard (Oct 30 2018 at 21:37):

and then a segfault ;-)

view this post on Zulip Kevin Buzzard (Oct 30 2018 at 21:39):

[ten seconds later]

view this post on Zulip Scott Olson (Oct 30 2018 at 21:41):

Yeah, my understanding is dec_trivial should never fail on closed terms, but it gives up when reduction takes too long

view this post on Zulip Kevin Buzzard (Oct 30 2018 at 21:43):

open nat

example : binary_rec 0 (λ_ _, succ) 1 = 1 :=
begin
  unfold binary_rec,
  exact dec_trivial
end -- works

example : binary_rec 0 (λ_ _, succ) 1 = 1 :=
begin
  exact dec_trivial
end -- fails

view this post on Zulip Scott Olson (Oct 30 2018 at 21:47):

That does seem a bit... artificial. I wish I knew more about how the reductions worked

view this post on Zulip Scott Olson (Oct 30 2018 at 21:48):

But I can confirm #reduce binary_rec 0 (λ_ _, succ) 1 times out but #reduce on the goal after unfold binary_rec (copy/pasted out with set_option pp.proofs true and set_option pp.implicit true) does give you 1

view this post on Zulip Mario Carneiro (Oct 30 2018 at 23:20):

This is because proofs are irreducible by default. I think there is an option for this, I forget the name

view this post on Zulip Mario Carneiro (Oct 30 2018 at 23:21):

It is almost never necessary to reduce a proof during evaluation, but well founded definitions require recursion on proofs of wellfoundedness

view this post on Zulip Kenny Lau (Oct 30 2018 at 23:26):

then what should we do?

view this post on Zulip Mario Carneiro (Oct 30 2018 at 23:54):

give up? This definition is not intended for kernel reduction

view this post on Zulip Mario Carneiro (Oct 30 2018 at 23:56):

If you need to calculate these things, you can either use the definition, or if we need larger scale computation we can add another norm_num add-on for this (I really need to make it extensible via annotation...)


Last updated: May 13 2021 at 06:15 UTC