COQ example

Require Import Arith.

Fixpoint fib (n : nat) :=

match n with

0 => 1

|  1 => 1

|  S (S p as x) => fib x + fib p

end.

Fixpoint fib_t (fibn fibsn p :nat) :=

match p with

0 => fibn

| S k => fib_t fibsn (fibsn + fibn) k

end.

Lemma mylemma : forall n p, fib_t (fib n) (fib (S n)) p = fib (n + p).

Proof.

intros n.

intros p.

revert n.

induction p.

simpl.

intros n.

replace (n + 0) with n by ring.

reflexivity.

intros n’.

replace (n’ + S p) with (S (n’ + p)) by ring.

replace (fib_t (fib n’) (fib (S n’)) (S p)) with (fib_t (fib (S n’)) (fib (S (S n’))) p).

rewrite IHp.

replace (S n’ + p) with (S (n’ + p)) by ring.

reflexivity.

simpl.

reflexivity.

Qed.