Skip to content

Instantly share code, notes, and snippets.

@autotaker
Created April 27, 2014 13:42
Show Gist options
  • Save autotaker/11345941 to your computer and use it in GitHub Desktop.
Save autotaker/11345941 to your computer and use it in GitHub Desktop.
(* 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment