## Stream: new members

### Topic: Defeq involving recursors

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

#### Kenny Lau (Apr 12 2020 at 16:19):

what does gas stand for?

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


#### Kenny Lau (Apr 12 2020 at 16:24):

I think your expression is correct

#### Kenny Lau (Apr 12 2020 at 16:25):

maybe you didn't specify the types enough

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

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

#### Kenny Lau (Apr 13 2020 at 05:33):

I thought it was an acronym lol

#### Kenny Lau (Apr 13 2020 at 05:35):

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

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

#### Kenny Lau (Apr 13 2020 at 05:35):

gas is such a Coq thing

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

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

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


#### Kenny Lau (Apr 13 2020 at 05:47):

@Donald Sebastian Leung

#### Kenny Lau (Apr 13 2020 at 05:48):

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

#### Mario Carneiro (Apr 13 2020 at 05:48):

relative to what?

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

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

#### Mario Carneiro (Apr 13 2020 at 05:51):

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

hmm

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

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

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

#### Kenny Lau (Apr 13 2020 at 05:58):

I suppose this can make things faster

#### Kenny Lau (Apr 13 2020 at 05:59):

because you don’t spend time unifying with the goal

#### Mario Carneiro (Apr 13 2020 at 05:59):

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

#### Mario Carneiro (Apr 13 2020 at 05:59):

so it seems strictly worse to me

#### Mario Carneiro (Apr 13 2020 at 05:59):

you can always write a term without holes if you want

#### Kenny Lau (Apr 13 2020 at 06:01):

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

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

#### Kenny Lau (Apr 13 2020 at 06:06):

yeah

Last updated: May 14 2021 at 06:16 UTC