Tenho duas implementações de Fibonacci, vistas abaixo, que quero provar que são funcionalmente equivalentes.

Eu já provei propriedades sobre números naturais, mas este exercício requer outra abordagem que não consigo descobrir.

O livro que estou usando introduziu a seguinte sintaxe do Coq, portanto, deve ser possível provar a igualdade usando esta notação:

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

Aqui estão as duas implementações:

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.

É bastante óbvio que essas funções calculam o mesmo valor para o caso basen = 0, mas o caso de indução é muito mais difícil?

Eu tentei provar o seguinte lema, mas estou preso no caso de indução:

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.

Onde:

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