## Stream: new members

### Topic: dec_trivial fails

#### 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


#### Kenny Lau (Oct 30 2018 at 20:52):

Why does dec_trivial fail?

@Chris Hughes

#### 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


#### Kenny Lau (Oct 30 2018 at 21:10):

ok so the problem boils down to this

#### Kenny Lau (Oct 30 2018 at 21:10):

import data.nat.sqrt

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


#### 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

#### 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?


#### Kevin Buzzard (Oct 30 2018 at 21:17):

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

#### Scott Olson (Oct 30 2018 at 21:19):

I get failure for the sqrt_aux line

#### Kevin Buzzard (Oct 30 2018 at 21:19):

Did you open nat?

Yes

hmm

#### Kenny Lau (Oct 30 2018 at 21:21):

this is troublesome

#### Kenny Lau (Oct 30 2018 at 21:21):

because we can't change nat.binary_rec

#### Kenny Lau (Oct 30 2018 at 21:21):

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

#### 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?

#### Kevin Buzzard (Oct 30 2018 at 21:27):

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

#### Kenny Lau (Oct 30 2018 at 21:28):

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

#### Kevin Buzzard (Oct 30 2018 at 21:28):

You know more about decidability than me.

#### Kevin Buzzard (Oct 30 2018 at 21:28):

decidable (size a = b)?

#### Kenny Lau (Oct 30 2018 at 21:28):

that wouldn't be useful

#### Kenny Lau (Oct 30 2018 at 21:29):

because I can have another function that calls size

#### Kevin Buzzard (Oct 30 2018 at 21:29):

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

#### 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

#### 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?

#### 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.

#### Kevin Buzzard (Oct 30 2018 at 21:32):

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

#### Kevin Buzzard (Oct 30 2018 at 21:37):

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

#### Kevin Buzzard (Oct 30 2018 at 21:37):

and then a segfault ;-)

#### Kevin Buzzard (Oct 30 2018 at 21:39):

[ten seconds later]

#### 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

#### 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


#### Scott Olson (Oct 30 2018 at 21:47):

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

#### 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

#### 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

#### 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

#### Kenny Lau (Oct 30 2018 at 23:26):

then what should we do?

#### Mario Carneiro (Oct 30 2018 at 23:54):

give up? This definition is not intended for kernel reduction

#### 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