Playing with Fibonacci

fib.v

Fixpoint fib n :=
  match n with
  | 0 => 1
  | S n =>
    match n with
    | 0 => 1
    | S m => 
      fib n + fib m
    end
  end.

Require Import Omega.

Lemma fibPos n: fib n > 0.
Proof. induction n; cbn; try omega; destruct n; omega. Qed.

Lemma incFib n: n > 0 -> fib n < fib (S n).
Proof.
  intros; destruct n as [|n]; cbn in *; try omega.
  pose proof (fibPos n); omega.
Qed.

Require Import ssreflect.
From Coq.Arith Require Import PeanoNat.
Import Nat.

Lemma fibPow2 m: forall n, n > 0 -> n <= m -> fib n < Nat.pow 2 n.
Proof.
  induction m; intros n Hnpos Hnm; first omega.
  destruct n; cbn; first omega.
  destruct n; cbn; first omega.
  destruct n; cbn; first omega.

  (* Hacky way to refold fib's expansion to fib. *)
  remember (fib (S (S n)) + fib (S n)) as x eqn:Heqx.
  pose proof Heqx as Heqx'.
  simpl in Heqx'.
  (* ssreflect syntax to chain rewrites *)
  rewrite -Heqx' Heqx. clear Heqx Heqx' x.

  (* now, omega can do all trivial inequality manipulations, but it does no
     simplification. So first we must add all inequalities to combine to the
     context. *)

  (* The underscores turn assumptions into shelved goals *)
  epose proof incFib (S n) _ as Hinc.
  epose proof IHm (S (S n)) _ _ as Hn2.

  (* Simplify, but don't reduce fib *)
  cbn -[fib] in Hn2.
  (* Rewrite ?x + 0 -> ?x (for any x) in both Hn2 and the goal. This is also
     ssreflect syntax. *)
  rewrite !add_0_r in Hn2 |- *.

  (* (* At this point, we could finish with: *) *)
  (* Unshelve. *)
  (* all: omega. *)

  (* But let's look closer at what happens. *)

  (* Use "transitivity" (not quite), to reduce to the two inequalities used in
     https://math.stackexchange.com/a/894767/79293. Beware oemga needs no such
     crutches. *)
  apply (lt_le_trans _ (fib (S (S n)) + fib (S (S n))) _); omega.

  (* Turn shelved assumptions into goals. *)
  Unshelve.
  all: omega.
Qed.

Lemma fibPowOld m: forall n, n > 0 -> n <= m -> fib n < Nat.pow 2 n.
Proof.
  induction m; intros n Hnpos Hnm; first omega.
  destruct n; cbn; first omega.
  destruct n; cbn; first omega.
  destruct n; cbn; first omega.

  (* Hacky way to refold fib's expansion to fib. *)
  remember (fib (S (S n))) as x.
  assert (fib (S (S n)) = x) as Heqx' by auto. simpl in Heqx'.
  (* ssreflect syntax to chain rewrites *)
  rewrite Heqx' Heqx. clear Heqx Heqx' x.
  remember (fib (S n)) as x.
  assert (fib (S n) = x) as Heqx' by auto. simpl in Heqx'.
  rewrite Heqx' Heqx. clear Heqx Heqx' x.

  epose proof (IHm (S n) _ _) as Hn1.
  epose proof (IHm (S (S n)) _ _) as Hn2.
  Unshelve. all: try omega.

  SearchPattern (?a < ?b -> ?b <= ?c -> ?a < ?c).
  apply (lt_le_trans _ (2 ^ S n + 2 ^ S (S n)) _).
  - omega.
  -
    (* Optional *)
    (* repeat rewrite -> add_0_r. *)
    simpl; omega.
Qed.

What do you think about this one ? Never mind, I realized it's < rather than <=.

Require Import Psatz.
Require Import FunInd.


Fixpoint fib n :=
  match n with
  | 0 => 1
  | S n =>
    match n with
    | 0 => 1
    | S m => 
      fib n + fib m
    end
  end.

Functional Scheme fib_ind := Induction for fib Sort Prop.


Lemma powfn : forall n, fib n <= Nat.pow 2 n.
Proof.
  induction n.
  + cbn; auto.
  + cbn; destruct n.
    ++ cbn; auto.
    ++ (* don't simplify *)
      (* all I need to show that fib n <= fib (S n) *)
      assert (Ht : forall m, fib m <= fib (S m)).
      induction m.
      +++ cbn. lia. 
      +++ cbn. destruct m.
          ++++ cbn. lia.
          ++++ lia.
      +++ specialize (Ht n).
          lia.
Qed.