dec_trivial fails

Stream: new members

[Kenny Lau]

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]

Why does dec_trivial fail?

[Kenny Lau]

@Chris Hughes

[Kenny Lau]

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]

ok so the problem boils down to this

[Kenny Lau]

import data.nat.sqrt

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

[Scott Olson]

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

[Kevin Buzzard]

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]

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

[Scott Olson]

I get failure for the sqrt_aux line

[Kevin Buzzard]

Did you open nat?

[Scott Olson]

Yes

[Kenny Lau]

hmm

[Kenny Lau]

this is troublesome

[Kenny Lau]

because we can't change nat.binary_rec

[Kenny Lau]

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

[Kevin Buzzard]

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]

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

[Kenny Lau]

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

[Kevin Buzzard]

You know more about decidability than me.

[Kevin Buzzard]

decidable (size a = b)?

[Kenny Lau]

that wouldn't be useful

[Kenny Lau]

because I can have another function that calls size

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

and then a segfault ;-)

[Kevin Buzzard]

[ten seconds later]

[Scott Olson]

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

[Kevin Buzzard]

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]

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

[Scott Olson]

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]

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

[Mario Carneiro]

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

[Kenny Lau]

then what should we do?

[Mario Carneiro]

give up? This definition is not intended for kernel reduction

[Mario Carneiro]

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