CoqEx11-12.v

(* Q11 *)
Require Import Arith.

Fixpoint sum_odd(n:nat) : nat :=
  match n with
  | O => O
  | S m => 1 + m + m + sum_odd m
end.

Goal forall n, sum_odd n = n * n.
Proof.
  induction n.
    (* case n = O *)
    simpl.
    reflexivity.
    (* induction step *)
    simpl.
    apply f_equal.
    rewrite IHn.
    rewrite <- plus_assoc.
    replace (n + n * n) with (n * S n).
    reflexivity.
    rewrite <- NPeano.Nat.add_1_r. 
    rewrite mult_plus_distr_l.
    rewrite mult_1_r.
    rewrite plus_comm.
    reflexivity.
  Qed.

(* Q12 *)
Require Import Lists.List.

Fixpoint sum (xs : list nat) : nat := 
  match xs with
  | nil => 0
  | x :: xs => x + sum xs
end.

Theorem Pigeon_Hole_Principle :
  forall (xs : list nat), length xs < sum xs ->
    (exists x, 1 < x /\ In x xs).
  Proof.
  induction xs.
  (* case xs = nil *)
    simpl.
    intro.
    apply False_ind. 
    apply lt_n_0 in H.
    apply H.
  (* induction step *)
    simpl.
    intro.
    (* a <= 1 or 1 < a *)
    destruct (le_or_lt a 1).
      (* case a <= 1 *)
      assert (length xs < sum xs).
      assert (a + sum xs <= 1 + sum xs).
      apply plus_le_compat_r.
      apply H0.
      assert (S (length xs) < 1 + sum xs).
      apply lt_le_trans with (m := a + sum xs).
      apply H.
      apply H1.
      apply lt_S_n.
      replace (S (sum xs)) with (1 + sum xs).
      apply H2.
      rewrite NPeano.Nat.add_1_l.
      reflexivity.
      assert (exists x : nat, 1 < x /\ In x xs).
      apply IHxs.
      apply H1.
      destruct H2.
      destruct H2.
      exists x.
      split.
      apply H2.
      right.
      apply H3.
      (* case 1 < a *)
      exists a.
      split.
      apply H0.
      left.
      reflexivity.
  Qed.