Library coq4_recurrence_qqs

Require Import List.

Print list.

Fixpoint long (u : list nat) : nat :=
  match u with
  | nil ⇒ 0
  | cons x u' ⇒ S (long u')
  end.

Fixpoint long2 (u : list nat) : nat → nat :=
  fun a ⇒
    match u with
    | nil ⇒ a
    | cons x u' ⇒ long2 u' (S a)
    end.


Lemma long2_plus : ∀ u a, long2 u a = long u + a.
Proof.
  intros u a.
  revert a.
  Undo 2.
  intro u.
  induction u as [ | x u' Hu'].
  - intro a.
    cbn [long long2]. cbn. reflexivity.
  - intro a'.
    cbn [long long2]. cbn.
    Check (Hu' (S a')).
    rewrite (Hu' (S a')).
    Check plus_n_Sm.
    Check (plus_n_Sm (long u') a').
    rewrite (plus_n_Sm (long u') a').
    reflexivity.
Qed.

Theorem long2_long : ∀ u, long2 u 0 = long u.
Proof.
  intro u.
  rewrite (long2_plus u 0). rewrite <- (plus_n_O (long u)).
  reflexivity.
Qed.