# Zulip Chat Archive

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

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

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) -/ endThanks, 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