Defeq involving recursors

Stream: new members

[Donald Sebastian Leung]

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)

[Kenny Lau]

what does gas stand for?

[Kenny Lau]

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

[Kenny Lau]

I think your expression is correct

[Kenny Lau]

maybe you didn't specify the types enough

[Donald Sebastian Leung]

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.

[Donald Sebastian Leung]

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.

[Kenny Lau]

I thought it was an acronym lol

[Kenny Lau]

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

[Kenny Lau]

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.

[Kenny Lau]

gas is such a Coq thing

[Donald Sebastian Leung]

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

[Andrew Ashworth]

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

[Kenny Lau]

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

[Kenny Lau]

@Donald Sebastian Leung

[Kenny Lau]

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

[Mario Carneiro]

relative to what?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kenny Lau]

hmm

[Mario Carneiro]

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

[Donald Sebastian Leung]

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!

[Kenny Lau]

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

[Kenny Lau]

I suppose this can make things faster

[Kenny Lau]

because you don’t spend time unifying with the goal

[Mario Carneiro]

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

[Mario Carneiro]

so it seems strictly worse to me

[Mario Carneiro]

you can always write a term without holes if you want

[Kenny Lau]

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

[Donald Sebastian Leung]

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?

[Kenny Lau]

yeah