Zulip Chat Archive

Stream: new members

Topic: Defeq involving recursors


view this post on Zulip Donald Sebastian Leung (Apr 12 2020 at 16:02):

Suppose I have an auxiliary function for efficiently computing the nth Fibonacci number as follows:

import data.nat.parity

open nat

def fib2 (gas : ) :    ×  := nat.rec_on gas
  (λ _, (0, 1))
  (λ gas' fib2_gas' n, nat.cases_on n
    (0, 1)
    (λ _, prod.cases_on (fib2_gas' (n / 2))
      (λ a b,
        have c :  := a * (2 * b - a),
        have d :  := a * a + b * b,
        cond (even n) (c, d) (d, c + d))))

Now suppose we have natural numbers gas' and n. What would be a partially reduced expression that fib2 (succ gas') (succ n) is defeq to? In particular, I thought it would be defeq to:

prod.cases_on (fib2 gas' (succ n / 2))
  (λ a b,
    have c :  := a * (2 * b - a),
    have d :  := a * a + b * b,
    cond (even (succ n)) (c, d) (d, c + d))

but apparently not.

(I'm in the middle of a proof involving fib2 and would like to partially reduce the goal to a state where I can rewrite based on an inductive hypothesis)

view this post on Zulip Kenny Lau (Apr 12 2020 at 16:19):

what does gas stand for?

view this post on Zulip Kenny Lau (Apr 12 2020 at 16:24):

example (gas' n : ) (H : fib2 gas'.succ n.succ = (0, 0)) : false :=
begin
  change (prod.cases_on (fib2 gas' (n.succ/2)) _ :  × ) = _ at H,
/-
H :
  prod.cases_on (fib2 gas' (succ n / 2))
      (λ (a b : ℕ),
         have c : ℕ, from a * (2 * b - a),
         have d : ℕ, from a * a + b * b,
         cond (to_bool (even (succ n))) (c, d) (d, c + d)) =
    (0, 0)
-/
end

view this post on Zulip Kenny Lau (Apr 12 2020 at 16:24):

I think your expression is correct

view this post on Zulip Kenny Lau (Apr 12 2020 at 16:25):

maybe you didn't specify the types enough

view this post on Zulip Donald Sebastian Leung (Apr 13 2020 at 05:32):

Kenny Lau said:

what does gas stand for?

It's a cheap way of ensuring that a non-primitive recursive function eventually terminates, by converting a potentially non-trivial induction / recursion into induction / recursion on a natural number. IMO the concept is pretty well explained in A Step-Indexed Evaluator, you may wish to take a look there.

view this post on Zulip Donald Sebastian Leung (Apr 13 2020 at 05:33):

Kenny Lau said:

example (gas' n : ) (H : fib2 gas'.succ n.succ = (0, 0)) : false :=
begin
  change (prod.cases_on (fib2 gas' (n.succ/2)) _ :  × ) = _ at H,
/-
H :
  prod.cases_on (fib2 gas' (succ n / 2))
      (λ (a b : ℕ),
         have c : ℕ, from a * (2 * b - a),
         have d : ℕ, from a * a + b * b,
         cond (to_bool (even (succ n))) (c, d) (d, c + d)) =
    (0, 0)
-/
end

Thanks, I don't think I tried change (I was using show). I'll take another stab at it now.

view this post on Zulip Kenny Lau (Apr 13 2020 at 05:33):

I thought it was an acronym lol

view this post on Zulip Kenny Lau (Apr 13 2020 at 05:35):

oh btw you don't need gas because Lean has better recursion than Coq! :D

view this post on Zulip Kenny Lau (Apr 13 2020 at 05:35):

Chris Hughes said:

I think the #eval times are an example of why Lean is so much better than Coq. Coq can't compile well-founded recursion nicely like Lean I heard.

view this post on Zulip Kenny Lau (Apr 13 2020 at 05:35):

gas is such a Coq thing

view this post on Zulip Donald Sebastian Leung (Apr 13 2020 at 05:38):

To be fair, there's an Equations library in Coq which somewhat resembles Lean's equation compiler, but I'm not sure if there's anything it can't do that Lean's equation compiler can do (or vice versa).

view this post on Zulip Andrew Ashworth (Apr 13 2020 at 05:39):

you still might want to use gas or fuel. Sometimes you're too lazy to give a proof of well-foundedness, and if you know an upper bound for how many ops an algorithm will take, it's useful then without having to go meta

view this post on Zulip Kenny Lau (Apr 13 2020 at 05:47):

import data.nat.parity tactic

universes u

/-- fib2 n = (fib n, fib (n+1)) -/
def fib2 :    × 
| 0     := (0,1)
| (n+1) := have hwf : (n+1)/2 < n+1, from nat.div_lt_self n.succ_pos dec_trivial,
    have f :  ×  := fib2 ((n+1)/2),
    have c :  := f.1 * (2 * f.2 - f.1),
    have d :  := f.1 * f.1 + f.2 * f.2,
    cond (nat.bodd n) (c, d) (d, c + d)

#eval (list.range 10).map fib2
-- [(0, 1), (1, 1), (1, 2), (2, 3), (3, 5), (5, 8), (8, 13), (13, 21), (21, 34), (34, 55)]

view this post on Zulip Kenny Lau (Apr 13 2020 at 05:47):

@Donald Sebastian Leung

view this post on Zulip Kenny Lau (Apr 13 2020 at 05:48):

@Mario Carneiro is this O(n*log n)?

view this post on Zulip Mario Carneiro (Apr 13 2020 at 05:48):

relative to what?

view this post on Zulip Mario Carneiro (Apr 13 2020 at 05:49):

you can use n@(_+1) by the way to avoid having to say n+1 all the time

view this post on Zulip Mario Carneiro (Apr 13 2020 at 05:50):

nat.bodd is probably expensive to compute in the VM because it doesn't have a special implementation

view this post on Zulip Mario Carneiro (Apr 13 2020 at 05:51):

I think you can get an asymptotically optimal implementation if you use nat.binary_rec_on

view this post on Zulip Kenny Lau (Apr 13 2020 at 05:52):

hmm

view this post on Zulip Mario Carneiro (Apr 13 2020 at 05:54):

I really wish we had a better way to do this kind of thing where you don't have to pick between efficient in the VM and efficient in the kernel

view this post on Zulip Donald Sebastian Leung (Apr 13 2020 at 05:55):

Donald Sebastian Leung said:

Kenny Lau said:

example (gas' n : ) (H : fib2 gas'.succ n.succ = (0, 0)) : false :=
begin
  change (prod.cases_on (fib2 gas' (n.succ/2)) _ :  × ) = _ at H,
/-
H :
  prod.cases_on (fib2 gas' (succ n / 2))
      (λ (a b : ℕ),
         have c : ℕ, from a * (2 * b - a),
         have d : ℕ, from a * a + b * b,
         cond (to_bool (even (succ n))) (c, d) (d, c + d)) =
    (0, 0)
-/
end

Thanks, I don't think I tried change (I was using show). I'll take another stab at it now.

It worked! Thanks Kenny!

view this post on Zulip Kenny Lau (Apr 13 2020 at 05:58):

@Mario Carneiro I have noticed that in Coq if you use change, the expression must not contain holes that can only be filled in relative to the goal; is this better or worse?

view this post on Zulip Kenny Lau (Apr 13 2020 at 05:58):

I suppose this can make things faster

view this post on Zulip Kenny Lau (Apr 13 2020 at 05:59):

because you don’t spend time unifying with the goal

view this post on Zulip Mario Carneiro (Apr 13 2020 at 05:59):

I don't really know what else those holes would be good for

view this post on Zulip Mario Carneiro (Apr 13 2020 at 05:59):

so it seems strictly worse to me

view this post on Zulip Mario Carneiro (Apr 13 2020 at 05:59):

you can always write a term without holes if you want

view this post on Zulip Kenny Lau (Apr 13 2020 at 06:01):

@Donald Sebastian Leung what are holes in Coq used for?

view this post on Zulip Donald Sebastian Leung (Apr 13 2020 at 06:05):

For inferring implicit parameters like in Lean? BTW I don't think I have heard of the change tactic in Coq - is it the same as in Lean?

view this post on Zulip Kenny Lau (Apr 13 2020 at 06:06):

yeah


Last updated: May 14 2021 at 06:16 UTC