coq_practice_3_(11~14).v

Require Import Arith.
Require Import Arith Ring.

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.
  trivial.

  simpl.
  rewrite IHn.
  ring.
Qed.

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.
  contradict H.
  simpl.
  apply lt_n_O.
(*式変形の簡単のため*)
  assert (forall p : nat,p + sum xs = sum ( p :: xs)).
    simpl.
    trivial.
  assert (forall p : nat,1 + length xs = length ( p :: xs)).
    intros.
    simpl.
    trivial.
(*case .. a==0*)
  case_eq a.
  intro.
  rewrite H2 in H.
    
  assert ((length (0 :: xs) < sum (0 :: xs)) -> length xs < sum xs).
    intros.
    apply NPeano.Nat.le_lt_add_lt with 0 1.
    apply le_0_n.
    rewrite plus_comm.
    rewrite H1 with 0.
    rewrite plus_comm.
    rewrite H0 with 0.
    apply H.


  apply H3 in H.
  apply IHxs in H.
  destruct H.
  exists x.
  split.
  destruct H.
  apply H.
  destruct H.
  simpl.
  right.
  apply H4.

  intros.
(*n=0 すなわちa=1*)
  case_eq n.
  intros.
  rewrite  H3 in H2.
  rewrite H2 in H.
  rewrite <- H0 in H.
  rewrite <- H1 in H.
  apply plus_lt_reg_l in H.
  apply IHxs in H.
  destruct H.
  exists x.
  destruct H.
  split.
  apply H.
  simpl.
  right.
  apply H4.
(*a>1*)
  intros.
  rewrite H3 in H2.
  exists a.
  split.
  rewrite H2.
  rewrite <- NPeano.Nat.add_1_l.
  apply plus_lt_compat_l.
  apply lt_0_Sn.
  simpl.
  left.
  rewrite  H2.
  trivial.
Qed.



Theorem FF: ~exists f, forall n, f (f n) = S n.
Proof.
  intro.
  destruct H.
  remember (x O).

  assert (forall p,(x p)= n + p).
    intros.
    induction p.
    rewrite Heqn.
    trivial.
    rewrite <- H at 1.
    rewrite H.
    rewrite <- plus_n_Sm.
    apply NPeano.Nat.succ_inj_wd .
    apply IHp.
  
  assert (x n = S O).
    rewrite Heqn.
    apply H.

  contradict H1.
  rewrite H0.
(*この後はもう少し簡単に書けそう*)
  induction n.
  trivial.
  simpl.
  unfold not.
  assert (forall a,S a = 1 -> a = 0).
    intros.
    apply NPeano.Nat.succ_inj_wd.
    trivial.
    intro.
  apply H1 in H2.
  rewrite <- plus_n_Sm in H2.
  apply NPeano.Nat.eq_sym_iff in H2.
  contradict H2.
  apply O_S.

Qed.



Inductive pos : Set :=
  | SO : pos
  | S : pos -> pos.

Fixpoint plus(n m:pos) : pos :=  
  match n with
  | SO => S m
  | S p => S (plus p m)
  end.

Infix "+" := plus.

Theorem plus_assoc : forall n m p, n + (m + p) = (n + m) + p.
Proof.
  intros.
  induction n.
  simpl.
  trivial.
  simpl.
  rewrite <- IHn.
  trivial.
Qed.