# Zulip Chat Archive

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

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

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

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

Yes

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

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