Как мне доказать, что две реализации Фибоначчи равны в Coq?
У меня есть две реализации Фибоначчи, показанные ниже, которые я хочу доказать функционально эквивалентными.
Я уже доказал свойства натуральных чисел, но это упражнение требует другого подхода, который я не могу понять.
Учебник, который я использую, ввел следующий синтаксис Coq, поэтому должна быть возможность доказать равенство с помощью этой записи:
<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.
Вот две реализации:
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.
Совершенно очевидно, что эти функции вычисляют одно и то же значение для базового случая.n = 0
, а вот с индукцией дела обстоят намного сложнее?
Я пытался доказать следующую лемму, но я застрял в индукционном случае:
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.
Куда:
Fixpoint add_v1 (i j : nat) : nat :=
match i with
| O => j
| S i' => S (add_v1 i' j)
end.