task11.v

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.
  intros.
  induction n.
  simpl.
  reflexivity.
  simpl.
  rewrite IHn.
  rewrite (mult_succ_r n n).
  rewrite (plus_comm (n*n) n).
  rewrite (plus_assoc n n (n*n)).
  reflexivity.
Qed.

task12.v

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.
  intros.
  induction xs.
  simpl in H.
  apply (Lt.lt_n_O 0) in H.
  apply False_ind.
  apply H.
  simpl in H.
  simpl.
  assert( 1 < a \/ 1 = a \/ 0 = a ).
  rewrite <- (or_assoc (1<a) (1=a) (0=a)).
  rewrite <- (Lt.le_lt_or_eq_iff 1 a).
  replace ( 1 <= a ) with ( 0 < a ).
  apply (Lt.le_lt_or_eq 0).
  apply (Le.le_0_n a).
  auto.
  case H0.
  exists a.
  split.
  apply H1.
  left.
  reflexivity.
  intros.
  case H1.
  intros.
  replace a with 1 in H.
  assert (length xs < sum xs ).
  apply (Plus.plus_lt_reg_l (length xs) (sum xs) 1 ).
  apply H.
  apply IHxs in H3.
  destruct H3.
  exists x.
  destruct H3.
  split.
  apply H3.
  right.
  apply H4.
  intros.
  replace a with 0 in H.
  simpl in H.
  assert ( length xs < sum xs ).
  apply (Plus.plus_lt_reg_l (length xs) (sum xs) 1 ).
  simpl.
  apply (Lt.lt_S (S(length xs)) (sum xs) ).
  apply H.
  apply IHxs in H3.
  destruct H3.
  exists x.
  destruct H3.
  split.
  apply H3.
  right.
  apply H4.
Qed.