Require Import Arith.

(**** Exercice 1 *)
Definition div2_spec : 
  forall n, {m : nat & sum (n = m + m) (n = S m + m)}.
Proof.
apply nat_rect.
  exists 0; left; trivial.
intros n hin.
case hin; intros k hk; destruct hk as [e | o].
  exists k; right; rewrite e; trivial.
exists (S k); left; rewrite o; trivial.
Defined.

Definition div2 (n : nat) := projT1 (div2_spec n).

Eval compute in (div2 4).
Eval compute in (div2 7).

Lemma twotimesdiv2 : forall n, 
  n = (div2 n) + (div2 n) \/ n = S (div2 n) + (div2 n).
Proof.
intro n; unfold div2.
case (div2_spec n); intros m hm; simpl.
destruct hm as [e | o]; [left | right]; trivial.
Qed.

(**** Exercice 2 *)
Definition sub_spec : forall n m, {d : nat & sum (n = m + d) (m = n + d)}.
Proof.
intro n; pattern n.
apply nat_rect; clear n.
  intro m; exists m; right; trivial.
intros n ihn [|m].
  exists (S n); left; trivial.
destruct (ihn m) as [c ec].
exists c; destruct ec as [ec | ec]; [left | right]; rewrite ec; trivial.
Defined.

Definition sub (n m : nat) := projT1 (sub_spec n m).

Eval compute in (sub 5 3).

Definition le n m := {d : nat & m = n + d}.

Lemma le_refl : forall n, le n n.
Proof.
intro n; unfold le.
exists 0; rewrite <- plus_n_O; trivial.
Qed.

Lemma le_sym : forall n m, le n m -> le m n -> n = m.
unfold le; intro n; pattern n; apply nat_rect; clear n.
intros [|m]; simpl; intros [d1 e1 [d2 e2]]; trivial; discriminate.
intros a ha [|b]; simpl; intros [d1 e1] [d2 e2].
   discriminate.
apply (f_equal S).
apply ha.
  exists d1; auto.
exists d2; auto.
Qed.

Lemma le_trans : forall n m p, le n m -> le m p -> le n p.
unfold le; intros n; elim n; clear n; [intros m p | intros n m p].
   intros _ _; exists p; trivial.
intros q [d1 e1] [d2 e2].
exists (d1 + d2).
rewrite e2; rewrite e1; simpl.
rewrite plus_assoc.
trivial.
Qed.

Definition lt n m :=  {d : nat & m = n + (S d)}.


Definition lt_le_dec : forall n m, (lt n m) + (le m n).
Proof.
intro n; elim n.
  intros [|m]; simpl; [right; apply le_refl | left].
  exists m; trivial.
clear n; intros n hin [|m].
  right; exists (S n); trivial.
destruct (hin m) as [ [d e] | [d e]]; [left | right];
   exists d; rewrite e; auto.
Defined.
  
Definition eq_lt_dec : forall n m, le n m -> (n = m) + (lt n m).  
Proof.
intros n m [[|d] e]; [left | right]; rewrite e; trivial.
  exists d; trivial.
Defined.
  
Lemma lt_dec : forall n m, (lt n m) + (n = m) + (lt m n).
Proof.
intros n m; destruct (lt_le_dec n m) as [h1 | h1].
  left; left; trivial.
destruct (eq_lt_dec m n h1) as [h2 | h2].
  left; right; rewrite h2; trivial.
right; trivial.
Defined.

Lemma eq_dec : forall n m : nat, {b : bool & b = true <-> n = m}.
Proof.
intro n; elim n; clear n.
  intros [|m]; [exists true | exists false]; split; intro h; trivial; discriminate.
intros n ihn [|m].
  exists false; split; intro h; discriminate.
destruct (ihn m) as [b [hb1 hb2]]; exists b.
split; intro h3.
  rewrite hb1; trivial.
apply hb2; auto.
Qed.


(*** Exercice 3 *)
Set Implicit Arguments.

Section ListDefinitions.

Variables A : Type.
(* Des listes polymorphes *)
Inductive list : Type :=
|nil : list
|cons : A -> list -> list.

(* Une fonction append naive *)
Fixpoint append (l1 l2 : list){struct l1} : list :=
  match l1 with
    |nil => l2
    |cons a tl => cons a (append tl l2)
  end.

Lemma app_nil : forall l : list, append l nil = l.
Proof.
intro l; elim l; clear l; trivial.
intros a l e; simpl; rewrite e; trivial.
Qed.

End ListDefinitions.


Fixpoint count (l : list nat)(x : nat){struct l} : nat :=
  match l with
    |nil => 0
    |cons a tl => if projT1 (eq_dec a x) then S (count tl x)
      else count tl x
  end.

Lemma count_app : forall l1 l2 n,
  count (append l1 l2) n = (count l1 n) + (count l2 n).
Proof.
intro l1; elim l1; clear l1; simpl; trivial.
intros n l2 hl1 l3 m; rewrite hl1; simpl.
destruct (eq_dec n m) as [b hb]; simpl. 
case_eq b; intro vb; auto.
Qed.


Definition perm_eq (l1 l2 : list nat) := forall n, count l1 n = count l2 n.

Lemma perm_eq_refl : forall l, perm_eq l l.
Proof.
intros l n; trivial.
Qed.

Lemma perm_eq_sym : forall l1 l2, perm_eq l1 l2 -> perm_eq l2 l1.
Proof.
intros l1 l2; unfold perm_eq; intros h n.
rewrite h; trivial.
Qed.

Lemma perm_eq_trans : forall l1 l2 l3, 
  perm_eq l1 l2 -> perm_eq l2 l3 -> perm_eq l1 l3.
Proof.
intros l1 l2 l3; unfold perm_eq; intros e1 e2 n.
rewrite e1; rewrite e2.
trivial.
Qed.

Lemma cons_perm_eq: forall l1 l2 a,
  perm_eq l1 l2 -> perm_eq (cons a l1) (cons a l2).
Proof.
intro l1; case l1; clear l1.
  intros l2 a; unfold perm_eq; simpl; intros e n; rewrite <- e; trivial.
intros a l1 hl1 [|l2].
  unfold perm_eq; simpl; intros e m; rewrite e; trivial.
unfold perm_eq; simpl; intros e p.
rewrite e; trivial.
Qed.


Lemma app_perm_eq : forall l1 l2, perm_eq (append l1 l2) (append l2 l1).
Proof.
intro l1; elim l1; clear l1.
  intros l2; unfold perm_eq; simpl; rewrite app_nil; trivial.
intros a l1 e [|b l2]; simpl.
   rewrite app_nil; exact (perm_eq_refl (cons a l1)).
intros c; simpl; rewrite e.
rewrite count_app; rewrite count_app; simpl.
destruct (eq_dec a c) as [b1 he1]; simpl.
destruct (eq_dec b c) as [b2 he2]; simpl.
case_eq b1; intro vb1; case_eq b2; intro vb2; simpl; auto.
Qed.


Inductive Color : Type := Red | Black.

Parameter col : nat -> Color.

Definition colored (c : Color) := {x : nat & col x = c}.
Definition col_list (c : Color) :=  list (colored c).
Definition Reds := col_list Red.
Definition Blacks := col_list Black.

Fixpoint R2list (l : Reds) : list nat :=
  match l with
    |nil => @nil nat
    |cons a tl => cons (projT1 a) (R2list tl)
  end.

Fixpoint B2list (l : Blacks) : list nat :=
  match l with
    |nil => @nil nat
    |cons a tl => cons (projT1 a) (B2list tl)
  end.

Definition Partition l :=
  {l12 : Reds * Blacks & let (l1, l2) := l12 in
    perm_eq l (append (R2list l1) (B2list l2))}.

Definition mkPartition : forall l, Partition l.
Proof.
intro l; elim l; clear l; unfold Partition.
  exists (@nil _ : Reds, @nil _ : Blacks); unfold perm_eq; trivial.
intros a l [t ht]; destruct t as [l1 l2].
case_eq (col a); intro ca.
  pose (red_a := existT _ a ca : colored Red).
  exists (cons red_a l1, l2); simpl.
  apply cons_perm_eq; trivial.
pose (black_a := existT _ a ca : colored Black).
exists (l1, cons black_a l2); simpl.
apply perm_eq_trans with (append (cons a (B2list l2)) (R2list l1)).
  simpl; apply cons_perm_eq.
  apply perm_eq_trans with (append (R2list l1) (B2list l2)); trivial.
  apply app_perm_eq.
apply app_perm_eq.
Qed.