How do I prove that two Fibonacci implementations are equal in Coq?

Question

I've two Fibonacci implementations, seen below, that I want to prove are functionally equivalent.

I've already proved properties about natural numbers, but this exercise requires another approach that I cannot figure out.

The textbook I'm using have introduced the following syntax of Coq, so it should be possible to prove equality using this notation:

<definition> ::= <keyword> <identifier> : <statement> <proof>

<keyword> ::= Proposition | Lemma | Theorem | Corollary

<statement> ::= {<quantifier>,}* <expression>

<quantifier> ::= forall {<identifier>}+ : <type>
               | forall {({<identifier>}+ : <type>)}+

<proof> ::= Proof. {<tactic>.}* <end-of-proof>

<end-of-proof> ::= Qed. | Admitted. | Abort.

Here are the two implementations:

Fixpoint fib_v1 (n : nat) : nat :=
  match n with
  | 0 => O
  | S n' => match n' with
            | O => 1
            | S n'' => (fib_v1 n') + (fib_v1 n'')
            end
  end.

Fixpoint visit_fib_v2 (n a1 a2 : nat) : nat :=
  match n with
  | 0 => a1
  | S n' => visit_fib_v2 n' a2 (a1 + a2)
  end.

It is pretty obvious that these functions compute the same value for the base case n = 0, but the induction case is much harder?

I've tried proving the following Lemma, but I'm stuck in induction case:

Lemma about_visit_fib_v2 :
  forall i j : nat,
    visit_fib_v2 i (fib_v1 (S j)) ((fib_v1 j) + (fib_v1 (S j))) = (fib_v1 (add_v1 i (S j))).
Proof.
  induction i as [| i' IHi'].

  intro j.
  rewrite -> (unfold_visit_fib_v2_0 (fib_v1 (S j)) ((fib_v1 j) + (fib_v1 (S j)))).
  rewrite -> (add_v1_0_n (S j)).
  reflexivity.

  intro j.
  rewrite -> (unfold_visit_fib_v2_S i' (fib_v1 (S j)) ((fib_v1 j) + (fib_v1 (S j)))).

 Admitted.

Where:

Fixpoint add_v1 (i j : nat) : nat :=
  match i with
  | O => j
  | S i' => S (add_v1 i' j)
  end.

Notice in your grammar you reference an undefined production ``. Do you know anything about any of the tactics? This proof isn't going to be obvious in Coq if you haven't written a proof yet at all… — Daniel Lyons, Nov 13 '16 at 07:28
The definition of `+` in the standard library is the same as `add_v1`. — Anton Trunov, Nov 15 '16 at 17:16

Anton Trunov · Accepted Answer · 2017-01-03T17:04:35.550

4

A note of warning: in what follows I'll to try to show the main idea of such a proof, so I'm not going to stick to some subset of Coq and I won't do arithmetic manually. Instead I'll use some proof automation, viz. the ring tactic. However, feel free to ask additional questions, so you could convert the proof to somewhat that would suit your purposes.

I think it's easier to start with some generalization:

Require Import Arith.    (* for `ring` tactic *)

Lemma fib_v1_eq_fib2_generalized n : forall a0 a1,
  visit_fib_v2 (S n) a0 a1 = a0 * fib_v1 n + a1 * fib_v1 (S n).
Proof.
  induction n; intros a0 a1.
  - simpl; ring.
  - change (visit_fib_v2 (S (S n)) a0 a1) with
           (visit_fib_v2 (S n) a1 (a0 + a1)).
    rewrite IHn. simpl; ring.
Qed.

If using ring doesn't suit your needs, you can perform multiple rewrite steps using the lemmas of the Arith module.

Now, let's get to our goal:

Definition fib_v2 n := visit_fib_v2 n 0 1.

Lemma fib_v1_eq_fib2 n :
  fib_v1 n = fib_v2 n.
Proof.
  destruct n.
  - reflexivity.
  - unfold fib_v2. rewrite fib_v1_eq_fib2_generalized.
    ring.
Qed.

edited Jan 03 '17 at 17:04

answered Nov 13 '16 at 09:44

Anton Trunov

15,074
2
23
43

Would it be possible to give a basic proof using only simple operations like "rewrite" and "apply"? My own idea is the following helper lemma: "forall i j : nat, visit_fib_v2 i (fib_v1 j) (fib_v1 (S j)) = (fib_v1 i + j).", but I'm stuck :-( – Shuzheng Nov 15 '16 at 14:05
See [this gist](https://gist.github.com/anton-trunov/84b63d4ca28c2698ed87b5c680974506) -- you need only `intros`, `rewrite`, `reflexivity`, maybe `apply` and several helper lemmas (which do the job of `simpl`). – Anton Trunov Nov 15 '16 at 15:02
Thank you, Anton! Would you also give a hint on how to prove my "about_visit_fib_v2", which I've added to my question. I'm stuck in the induction case. If I could make this Lemma work, I've done my own proof! – Shuzheng Nov 15 '16 at 16:51
I think the lemma is harder to prove, since it involves some less trivial properties of the Fibonacci numbers. – Anton Trunov Nov 15 '16 at 17:17
Thanks for your support @AntonTrunov. Finally, let me ask: Are the also predefined Coq procedures for proving things like "S n = n + 1"? Here I want to transform either "S n" to "n + 1" or vice versa, but I've no idea on how to do this. I usually states these facts as "Admitted." for my wrappers procedures around "+". – Shuzheng Nov 16 '16 at 08:23
See [this](http://stackoverflow.com/q/40614082/2747511) question and the link in a comment under it. You can also use `Search` to find the lemmas that can help you. Just remember to `Require Import Arith.` before searching. – Anton Trunov Nov 16 '16 at 09:07

score 4 · Answer 2 · edited May 23 '17 at 12:26

4

@larsr's answer inspired this alternative answer.

First of all, let's define fib_v2:

Require Import Coq.Arith.Arith. 

Definition fib_v2 n := visit_fib_v2 n 0 1.

Then, we are going to need a lemma, which is the same as fib_v2_lemma in @larsr's answer. I'm including it here for consistency and to show an alternative proof.

Lemma visit_fib_v2_main_property n: forall a0 a1,
  visit_fib_v2 (S (S n)) a0 a1 =
  visit_fib_v2 (S n) a0 a1 + visit_fib_v2 n a0 a1.
Proof.
  induction n; intros a0 a1; auto with arith.
  change (visit_fib_v2 (S (S (S n))) a0 a1) with
         (visit_fib_v2 (S (S n)) a1 (a0 + a1)).
  apply IHn.
Qed.

As suggested in the comments by larsr, the visit_fib_v2_main_property lemma can be also proved by the following impressive one-liner:

now induction n; firstorder.

Because of the nature of the numbers in the Fibonacci series it's very convenient to define an alternative induction principle:

Lemma pair_induction (P : nat -> Prop) :
  P 0 ->
  P 1 ->
  (forall n, P n -> P (S n) -> P (S (S n))) ->
  forall n, P n.
Proof.
  intros H0 H1 Hstep n.
  enough (P n /\ P (S n)) by tauto.
  induction n; intuition.
Qed.

The pair_induction principle basically says that if we can prove some property P for 0 and 1 and if for every natural number k > 1, we can prove P k holds under the assumption that P (k - 1) and P (k - 2) hold, then we can prove forall n, P n.

Using our custom induction principle, we get the proof as follows:

Lemma fib_v1_eq_fib2 n :
  fib_v1 n = fib_v2 n.
Proof.
  induction n using pair_induction.
  - reflexivity.
  - reflexivity.
  - unfold fib_v2.
    rewrite visit_fib_v2_main_property.
    simpl; auto.
Qed.

edited May 23 '17 at 12:26

Community

1
1

answered Nov 14 '16 at 18:08

Anton Trunov

15,074
2
23
43

I _knew_ that lemma should have a shorter proof! :-) Very nice! – larsr Nov 14 '16 at 18:22
1

The proof of the lemma went through with `now induction n; firstorder.`! – larsr Nov 14 '16 at 18:32
That's really cool! I incorporated your code into the answer. Kudos! :) – Anton Trunov Nov 14 '16 at 18:46
1

I recommend using `enough` instead of the (old-fashioned) `cut`. Plus, in this particular case, you could replace the `cut` and its proof by `enough (P n /\ P (S n)) by tauto.` – Zimm i48 Nov 15 '16 at 12:21
@Zimmi48 Updated, thanks! Incidentally, maximal automation wasn't a goal here. I tried to show as many tactics (manual and automatic) as I could come up with, hence `exact` and a couple of `reflexivity`. My personal vanilla Coq choice would be [this](http://stackoverflow.com/a/40572481/2747511) answer with a bit more automation, and maybe `ring` instead of `lia`. – Anton Trunov Nov 15 '16 at 14:04
1

Right. Well, here is a much less automated version (explicit destruct via an intro-pattern and manual use of `exact`): `enough (P n /\ P (S n)) as (H,_) by exact H.` In any case, I find this style (using `enough` instead of `cut` and `by` when its proof is simple enough) to be much more readable. – Zimm i48 Nov 15 '16 at 14:11
@Zimmi48 Elegant! Is there a way to make `H` fresh, but keep everything concise? E.g. sometimes I'd like not to keep track of names in the context. In other words, is it possible to make `H` locally bound in the `enough` command without overcomplicating things? – Anton Trunov Nov 15 '16 at 14:20
1

You could also do this: `enough (P n /\ P (S n)) as (?,_) by assumption.` but I don't think that it is what you are asking. You can also use the `?H` intro pattern to generate a fresh name but it is not better as `?` as you won't know for sure what it is. – Zimm i48 Nov 15 '16 at 14:28
@Zimmi48 It's pretty close actually, at least it allows not to think about naming :) I thought of using `?`, but didn't find anything like `by exact ?`. – Anton Trunov Nov 15 '16 at 14:30
Let us [continue this discussion in chat](http://chat.stackoverflow.com/rooms/128176/discussion-between-zimm-i48-and-anton-trunov). – Zimm i48 Nov 15 '16 at 14:32

larsr · Answer 3 · 2016-11-14T17:53:38.810

Anton's proof is very beautiful, and better than mine, but it might be useful, anyway.

Instead of coming up with the generalisation lemma, I strengthened the induction hypothesis.

Say the original goal is Q n. I then changed the goal with

cut (Q n /\ Q (S n))

from

Q n

to

 Q n /\ Q (S n)

This new goal trivially implies the original goal, but with it the induction hypothesis becomes stronger, so it becomes possible to rewrite more.

IHn : Q n /\ Q (S n)
=========================
Q (S n) /\ Q (S (S n))

This idea is explained in Software Foundations in the chapter where one does proofs over even numbers.

Because the propostion often is very long, I made an Ltac tactic that names the long and messy term.

Ltac nameit Q :=
  match goal with [ _:_ |- ?P ?n] => let X := fresh Q in remember P as X end.

Require Import Ring Arith.

(Btw, I renamed vistit_fib_v2 to fib_v2.) I needed a lemma about one step of fib_v2.

Lemma fib_v2_lemma: forall n a b, fib_v2 (S (S n)) a b = fib_v2 (S n) a b + fib_v2 n a b.
  intro n.
  pattern n.
  nameit Q.
  cut (Q n /\ Q (S n)).
  tauto.                             (* Q n /\ Q (S n) -> Q n *)

  induction n.
  split; subst; simpl; intros; ring. (* Q 0 /\ Q 1  *)
  split; try tauto.                  (* Q (S n)     *)

  subst Q.                           (* Q (S (S n)) *)
  destruct IHn as [H1 H2].
  assert (L1: forall n a b, fib_v2 (S n) a b = fib_v2 n b (a+b)) by reflexivity.
  congruence.
Qed.

The congruence tactic handles goals that follow from a bunch of A = B assumptions and rewriting.

Proving the theorem is very similar.

Theorem fib_v1_fib_v2 : forall n, fib_v1 n = fib_v2 n 0 1.
  intro n.
  pattern n.
  nameit Q.
  cut (Q n /\ Q (S n)).
  tauto.                             (* Q n /\ Q (S n) -> Q n *)

  induction n.
  split; subst; simpl; intros; ring. (* Q 0 /\ Q 1  *)
  split; try tauto.                  (* Q (S n)     *)

  subst Q.                           (* Q (S (S n)) *)
  destruct IHn as [H1 H2].
  assert (fib_v1 (S (S n)) = fib_v1 (S n) + fib_v1 n) by reflexivity.
  assert (fib_v2 (S (S n)) 0 1 = fib_v2 (S n) 0 1 + fib_v2 n 0 1) by
      (pose fib_v2_lemma; congruence).
  congruence.
Qed.

All the boiler plate code could be put in a tactic, but I didn't want to go crazy with the Ltac, since that was not what the question was about.

larsr · Answer 4 · 2016-11-14T18:18:51.257

2

This proof script only shows the proof structure. It could be useful to explain the idea of the proof.

Require Import Ring Arith Psatz.  (* Psatz required by firstorder *)

Theorem fibfib: forall n, fib_v2 n 0 1 = fib_v1 n.
Proof with (intros; simpl in *; ring || firstorder).
  assert (H: forall n a0 a1, fib_v2 (S n) a0 a1 = a0 * (fib_v1 n) + a1 * (fib_v1 (S n))).
  { induction n... rewrite IHn; destruct n... }
  destruct n; try rewrite H...
Qed.

edited Nov 14 '16 at 18:18

answered Nov 14 '16 at 18:10

larsr

5,447
19
38

I must have made some copy/paste error (I also got the error). Hope it works now! – larsr Nov 14 '16 at 18:19

Anton Trunov · Answer 5 · 2016-11-17T13:50:22.830

There is a very powerful library -- math-comp written in the Ssreflect formal proof language that is in its turn based on Coq. In this answer I present a version that uses its facilities. It's just a simplified piece of this development. All credit goes to the original author.

Let's do some imports and the definitions of our two functions, math-comp (ssreflect) style:

From mathcomp
Require Import ssreflect ssrnat ssrfun eqtype ssrbool.

Fixpoint fib_rec (n : nat) {struct n} : nat :=
  if n is n1.+1 then
    if n1 is n2.+1 then fib_rec n1 + fib_rec n2
    else 1
  else 0.

Fixpoint fib_iter (a b n : nat) {struct n} : nat :=
  if n is n1.+1 then
    if n1 is n2.+1
      then fib_iter b (b + a) n1
      else b
    else a.

A helper lemma expressing the basic property of Fibonacci numbers:

Lemma fib_iter_property : forall n a b,
  fib_iter a b n.+2 = fib_iter a b n.+1 + fib_iter a b n.
Proof.
case=>//; elim => [//|n IHn] a b; apply: IHn.
Qed.

Now, let's tackle equivalence of the two implementations. The main idea here, that distinguish the following proof from the other proofs has been presented as of time of this writing, is that we perform kind of complete induction, using elim: n {-2}n (leqnn n). This gives us the following (strong) induction hypothesis:

IHn : forall n0 : nat, n0 <= n -> fib_rec n0 = fib_iter 0 1 n0

Here is the main lemma and its proof:

Lemma fib_rec_eq_fib_iter : fib_rec =1 fib_iter 0 1.
Proof.
move=>n; elim: n {-2}n (leqnn n)=> [n|n IHn].
  by rewrite leqn0; move/eqP=>->.
case=>//; case=>// n0; rewrite ltnS=> ltn0n.
rewrite fib_iter_property.
by rewrite <- (IHn _ ltn0n), <- (IHn _ (ltnW ltn0n)).
Qed.

score 0 · Answer 6 · edited May 23 '17 at 10:30

Here is yet another answer, similar to the one using mathcomp, but this one uses "vanilla" Coq.

First of all, we need some imports, additional definitions, and a couple of helper lemmas:

Require Import Coq.Arith.Arith.

Definition fib_v2 n := visit_fib_v2 n 0 1.

Lemma visit_fib_v2_property n: forall a0 a1,
  visit_fib_v2 (S (S n)) a0 a1 =
  visit_fib_v2 (S n) a0 a1 + visit_fib_v2 n a0 a1.
Proof. now induction n; firstorder. Qed.

Lemma fib_v2_property n:
  fib_v2 (S (S n)) = fib_v2 (S n) + fib_v2 n.
Proof. apply visit_fib_v2_property. Qed.

To prove the main lemma we are going to use the standard well-founded induction lt_wf_ind principle for natural numbers with the < relation (a.k.a. complete induction):

This time we need to prove only one subgoal, since the n = 0 case for complete induction is always vacuously true. Our induction hypothesis, unsurprisingly, looks like this:

IH : forall m : nat, m < n -> fib_v1 m = fib_v2 m

Here is the proof:

Lemma fib_v1_eq_fib2 n :
  fib_v1 n = fib_v2 n.
Proof.
  pattern n; apply lt_wf_ind; clear n; intros n IH.
  do 2 (destruct n; trivial).
  rewrite fib_v2_property.
  rewrite <- !IH; auto.
Qed.

How do I prove that two Fibonacci implementations are equal in Coq?

6 Answers6

Linked