Require Import List Min Arith Div2.

Notation "n .+1" := (S n)(at level 2, left associativity, format "n .+1"): nat_scope.

(* Minus *)

Lemma minus_match k1 k2: match k2 - k1 with O => k2 <= k1 | S _ => k1 < k2 end.
Proof.
(* Goal: match Init.Nat.sub k2 k1 with | O => le k2 k1 | S n => lt k1 k2 end *)
generalize k2; clear k2.
(* Goal: forall k2 : nat, match Init.Nat.sub k2 k1 with | O => le k2 k1 | S n => lt k1 k2 end *)
induction k1 as [| k1 IH]; intros [| k2]; simpl; auto with arith.
(* Goal: match Init.Nat.sub k2 k1 with | O => le (S k2) (S k1) | S n => lt (S k1) (S k2) end *)
generalize (IH k2); case minus; auto with arith.
Qed.


(* The exponential function *)

Section Exp.

Fixpoint exp (n m: nat) {struct m} : nat := 
  match m with O => 1 | 1 => n | (S m1) => n * exp n m1 end.

Lemma exp0 n: exp n 0 = 1.
Proof. auto. Qed.

Lemma expS n m: exp n (S m) = n * exp n m.
Proof. 
(* Goal: @eq nat (exp n O) (S O) *)
destruct m; simpl; auto; rewrite <- mult_n_Sm; rewrite <- mult_n_O; auto.
Qed.

End Exp.

(* Some iterators on list *)

Section Fold2.

Variable A B C: Type.
Variable f: A -> B -> C -> C.

Definition dhead a (l : list A) :=
  match l with nil => a | b :: _ => b end.

Fixpoint fold2 (l1: list A) (l2: list B) (c: C) {struct l1}: C :=
  match l1, l2 with
    a::l3, b::l4 => fold2 l3 l4 (f a b c)
  | _, _ => c
  end.

Variable g: A -> B -> C.

Fixpoint map2 (l1: list A) (l2: list B) {struct l1}: list C :=
  match l1, l2 with
    a::l3, b::l4 => (g a b)::map2 l3 l4
  | _, _ => nil
  end.

Lemma map2_length l1 l2:
  length (map2 l1 l2) = min (length l1) (length l2).
Proof.
(* Goal: @eq nat (@length C (map2 l1 l2)) (Nat.min (@length A l1) (@length B l2)) *)
generalize l2; clear l2.
(* Goal: @eq nat (exp n O) (S O) *)
induction l1 as [| a1 l1 IH]; intros [| a2 l2]; simpl; auto.
Qed.


Fixpoint dmap2 (a : A) (l1: list A) (l2: list B) {struct l2}: list C :=
  match l1, l2 with
    a1::l3, b1 :: l4 => g a1 b1 :: dmap2 a l3 l4
  |    nil, b1 :: l4 =>  g a b1 :: dmap2 a nil l4
  | _, _ => nil
  end.

End Fold2.
Arguments dhead[A].
Arguments fold2[A B C].
Arguments map2[A B C].
Arguments dmap2[A B C].

Section Perm.

Variable A: Type.

Inductive perm: list A -> list A -> Prop :=
  perm_id: forall l, perm l l
| perm_swap: forall a b l,  perm (a::b::l) (b::a::l)
| perm_skip: forall a l1 l2,  perm l1 l2 -> perm (a::l1) (a::l2)
| perm_trans: forall l1 l2 l3, perm l1 l2 -> perm l2 l3 -> perm l1 l3.

Lemma perm_sym l1 l2: perm l1 l2 -> perm l2 l1.
Proof.
(* Goal: @eq nat (exp n O) (S O) *)
intros HH; elim HH; simpl; auto.
(* Goal: @eq nat (exp n O) (S O) *)
intros; apply perm_id; auto.
(* Goal: forall (a b : A) (l : list A), perm (@cons A b (@cons A a l)) (@cons A a (@cons A b l)) *)
(* Goal: forall (a : A) (l1 l2 : list A) (_ : perm l1 l2) (_ : perm l2 l1), perm (@cons A a l2) (@cons A a l1) *)
(* Goal: forall (l1 l2 l3 : list A) (_ : perm l1 l2) (_ : perm l2 l1) (_ : perm l2 l3) (_ : perm l3 l2), perm l3 l1 *)
intros; apply perm_swap.
(* Goal: @eq nat (exp n O) (S O) *)
intros; apply perm_skip; auto.
intros l3 l4 l5 H1 H2 H3 H4; 
(* Goal: @eq nat (exp n O) (S O) *)
  apply perm_trans with (1 := H4); auto.
Qed.


Lemma perm_cons_app a l1 l2: perm ((a:: l1) ++ l2) (l1 ++ (a:: l2)).
Proof.
(* Goal: @eq nat (exp n O) (S O) *)
generalize l2; clear l2; induction l1 as [| b l1 IH]; auto.
(* Goal: forall l2 : list A, perm (@app A (@cons A a (@nil A)) l2) (@app A (@nil A) (@cons A a l2)) *)
(* Goal: forall l2 : list A, perm (@app A (@cons A a (@cons A b l1)) l2) (@app A (@cons A b l1) (@cons A a l2)) *)
intros l2; apply perm_id.
(* Goal: forall l2 : list A, perm (@app A (@cons A a (@cons A b l1)) l2) (@app A (@cons A b l1) (@cons A a l2)) *)
intros l2; apply perm_trans with (1 := perm_swap a b (l1 ++ l2)).
(* Goal: @eq nat (exp n O) (S O) *)
simpl; apply perm_skip; auto.
(* Goal: perm (@cons A a (@app A l1 l2)) (@app A l1 (@cons A a l2)) *)
apply (IH l2).
Qed.

Lemma perm_length l1 l2: perm l1 l2 -> length l1 = length l2.
Proof.
(* Goal: @eq nat (exp n O) (S O) *)
intros HH; elim HH; simpl; auto.
(* Goal: @eq nat (exp n O) (S O) *)
intros l3 l4 l5 H1 H2 H3 H4; rewrite H2; auto.
Qed.

Lemma perm_in a l1 l2: perm l1 l2 -> In a l1 -> In a l2.
Proof.
(* Goal: forall (_ : perm l1 l2) (_ : @In A a l1), @In A a l2 *)
intros H; generalize a; elim H; clear a l1 l2 H; auto with datatypes.
(* Goal: @eq nat (exp n O) (S O) *)
simpl; intros a b l c [H1 | [H1 | H1]]; subst; auto.
(* Goal: @eq nat (exp n O) (S O) *)
simpl; intros a l1 l2 H IH c [H1 | H1]; subst; auto.
Qed.

Lemma perm_in_inv a l1: In a l1 -> exists l2, perm l1 (a:: l2).
Proof.
(* Goal: @eq nat (exp n O) (S O) *)
induction l1 as [| b l1 IH]; simpl; intros HH; case HH; auto.
(* Goal: forall _ : @eq A b a, @ex (list A) (fun l2 : list A => perm (@cons A b l1) (@cons A a l2)) *)
(* Goal: forall _ : @In A a l1, @ex (list A) (fun l2 : list A => perm (@cons A b l1) (@cons A a l2)) *)
intros HH1; subst; exists l1; apply perm_id.
(* Goal: @eq nat (exp n O) (S O) *)
intros HH1; case IH; auto.
(* Goal: forall (x : list A) (_ : perm l1 (@cons A a x)), @ex (list A) (fun l2 : list A => perm (@cons A b l1) (@cons A a l2)) *)
intros l2 Hl2; exists (b::l2).
(* Goal: perm (@cons A b l1) (@cons A a (@cons A b l2)) *)
apply perm_trans with (b::a::l2).
(* Goal: @eq nat (exp n O) (S O) *)
apply perm_skip; auto.
(* Goal: @eq nat (exp n O) (S O) *)
apply perm_swap; auto.
Qed.

Lemma perm_incl_r l1 l2 l3: perm l1 l2 -> incl l1 l3 -> incl l2 l3.
Proof.
(* Goal: forall (_ : perm l1 l2) (_ : @incl A l3 l1), @incl A l3 l2 *)
intros H; generalize l3; elim H; clear l3 l1 l2 H; auto with datatypes.
intros a b l1 l2 H x; simpl; intros [H1 | [H1 | H1]]; subst; apply H;
   auto with datatypes.
(* Goal: forall (a : A) (l1 l2 : list A) (_ : perm l1 l2) (_ : forall (l3 : list A) (_ : @incl A l1 l3), @incl A l2 l3) (l3 : list A) (_ : @incl A (@cons A a l1) l3), @incl A (@cons A a l2) l3 *)
intros a l1 l2 Hp IH l3 Hi x; simpl; intros [H1 | H1]; subst.
(* Goal: @In A x l2 *)
(* Goal: @In A x l3 *)
(* Goal: forall (x : list A) (_ : @perm A l3 (@app A l1 x)), @ex (list A) (fun l3 : list A => @perm A l2 (@app A (@cons A a l1) l3)) *)
apply Hi; auto with datatypes.
(* Goal: @In A x l3 *)
apply IH; auto with datatypes.
(* Goal: @In A x l2 *)
(* Goal: @In A x l3 *)
(* Goal: forall (x : list A) (_ : @perm A l3 (@app A l1 x)), @ex (list A) (fun l3 : list A => @perm A l2 (@app A (@cons A a l1) l3)) *)
intros y Hy; apply Hi; auto with datatypes.
Qed.

Lemma perm_incl_l l1 l2 l3: perm l1 l2 -> incl l3 l1 -> incl l3 l2.
Proof.
(* Goal: forall (_ : perm l1 l2) (_ : @incl A l3 l1), @incl A l3 l2 *)
intros H; generalize l3; elim H; clear l3 l1 l2 H; auto with datatypes.
(* Goal: forall (a b : A) (l l3 : list A) (_ : @incl A l3 (@cons A a (@cons A b l))), @incl A l3 (@cons A b (@cons A a l)) *)
(* Goal: forall (a : A) (l1 l2 : list A) (_ : perm l1 l2) (_ : forall (l3 : list A) (_ : @incl A l3 l1), @incl A l3 l2) (l3 : list A) (_ : @incl A l3 (@cons A a l1)), @incl A l3 (@cons A a l2) *)
intros a b l1 l2 H x Hx.
(* Goal: @eq nat (exp n O) (S O) *)
generalize (H _ Hx); simpl; intros [H1 | [H1 | H1]]; subst; auto.
(* Goal: forall (a : A) (l1 l2 : list A) (_ : perm l1 l2) (_ : forall (l3 : list A) (_ : @incl A l3 l1), @incl A l3 l2) (l3 : list A) (_ : @incl A l3 (@cons A a l1)), @incl A l3 (@cons A a l2) *)
intros a l1 l2 Hp IH l3 Hi x Hx.
(* Goal: @eq nat (exp n O) (S O) *)
generalize (Hi _ Hx); simpl; intros [H1 | H1]; subst; auto.
(* Goal: @eq nat (exp n O) (S O) *)
right; apply perm_in with (1 := Hp); auto.
Qed.

End Perm.

Arguments perm[A].

Section Uniq.

Variable A: Type.

Inductive uniq: list A -> Prop :=
  uniq_nil: uniq nil
| uniq_cons: forall a l, ~ In a l -> uniq l -> uniq (a::l).

Lemma uniq_perm l1 l2: perm l1 l2 -> uniq l1 -> uniq l2.
Proof.
(* Goal: @eq nat (exp n O) (S O) *)
intros H; elim H; auto.
(* Goal: forall (a b : A) (l : list A) (_ : uniq (@cons A a (@cons A b l))), uniq (@cons A b (@cons A a l)) *)
(* Goal: forall (a : A) (l1 l2 : list A) (_ : @perm A l1 l2) (_ : forall _ : uniq l1, uniq l2) (_ : uniq (@cons A a l1)), uniq (@cons A a l2) *)
intros a b l HH; inversion_clear HH as [| aa bb Hi HH1].
(* Goal: uniq (@cons A b (@cons A a l)) *)
(* Goal: forall (a : A) (l1 l2 : list A) (_ : @perm A l1 l2) (_ : forall _ : uniq l1, uniq l2) (_ : uniq (@cons A a l1)), uniq (@cons A a l2) *)
inversion_clear HH1 as [| aa bb Hi1 HH2].
(* Goal: uniq (@cons A b (@cons A a l)) *)
(* Goal: forall (a : A) (l1 l2 : list A) (_ : @perm A l1 l2) (_ : forall _ : uniq l1, uniq l2) (_ : uniq (@cons A a l1)), uniq (@cons A a l2) *)
repeat apply uniq_cons; auto with datatypes.
(* Goal: @eq nat (exp n O) (S O) *)
simpl; intros [H1 | H1]; subst; auto.
(* Goal: False *)
(* Goal: forall (a : A) (l1 l2 : list A) (_ : @perm A l1 l2) (_ : forall _ : uniq l1, uniq l2) (_ : uniq (@cons A a l1)), uniq (@cons A a l2) *)
case Hi; auto with datatypes.
(* Goal: forall (a : A) (l1 l2 : list A) (_ : @perm A l1 l2) (_ : forall _ : uniq l1, uniq l2) (_ : uniq (@cons A a l1)), uniq (@cons A a l2) *)
intros a l3 l4 H1 IH HH.
(* Goal: uniq (@cons A a l4) *)
inversion_clear HH as [| aa bb Hi HH1].
(* Goal: @eq nat (exp n O) (S O) *)
apply uniq_cons; auto.
(* Goal: @eq nat (exp n O) (S O) *)
intros HH2; case Hi; apply perm_in with (1 := perm_sym _ _ _ H1); auto.
Qed.

Lemma uniq_cons_inv a l: uniq (a::l) -> uniq l.
Proof.
(* Goal: @eq nat (exp n O) (S O) *)
intros HH; inversion HH; auto.
Qed.

Lemma uniq_app_inv_l l1 l2: uniq (l1 ++ l2) -> uniq l1.
Proof.
(* Goal: forall _ : uniq (@app A l1 l2), uniq l1 *)
generalize l1; induction l2 as [| a l2 IH]; clear l1; intros l1.
(* Goal: @eq nat (exp n O) (S O) *)
rewrite <-app_nil_end; auto.
(* Goal: forall _ : uniq (@app A l1 (@cons A a l2)), uniq l1 *)
intros HH; apply uniq_cons_inv with a.
(* Goal: uniq (@cons A a l2) *)
apply IH.
(* Goal: uniq (@app A (@cons A a l1) l2) *)
apply uniq_perm with (2 := HH).
(* Goal: @perm A (@app A l1 (@cons A a l2)) (@app A (@cons A a l1) l2) *)
apply perm_sym; apply perm_cons_app.
Qed.

Lemma uniq_app_inv_r l1 l2: uniq (l1 ++ l2) -> uniq l2.
Proof.
(* Goal: @eq nat (exp n O) (S O) *)
generalize l2; clear l2; induction l1 as [| a l1 IH]; auto.
(* Goal: forall (l2 : list A) (_ : uniq (@app A (@cons A a l1) l2)), uniq l2 *)
intros l2 Hl2. 
(* Goal: uniq l2 *)
apply uniq_cons_inv with a.
(* Goal: uniq (@cons A a l2) *)
apply IH.
(* Goal: uniq (@app A l1 (@cons A a l2)) *)
apply uniq_perm with (2 := Hl2).
(* Goal: @perm A (@app A (@cons A a l1) l2) (@app A l1 (@cons A a l2)) *)
apply perm_cons_app.
Qed.

Lemma perm_incl_inv l1 l2: 
  uniq l1 -> uniq l2 -> incl l1 l2 -> exists l3, perm l2 (l1 ++ l3).
Proof.
(* Goal: forall (_ : uniq l1) (_ : uniq l2) (_ : @incl A l1 l2), @ex (list A) (fun l3 : list A => @perm A l2 (@app A l1 l3)) *)
generalize l2; clear l2; induction l1 as [| a l1 IH]; intros l2.
(* Goal: forall (_ : uniq (@nil A)) (_ : uniq l2) (_ : @incl A (@nil A) l2), @ex (list A) (fun l3 : list A => @perm A l2 (@app A (@nil A) l3)) *)
(* Goal: forall (_ : uniq (@cons A a l1)) (_ : uniq l2) (_ : @incl A (@cons A a l1) l2), @ex (list A) (fun l3 : list A => @perm A l2 (@app A (@cons A a l1) l3)) *)
intros; exists l2; apply perm_id.
(* Goal: forall (_ : uniq (@cons A a l1)) (_ : uniq l2) (_ : @incl A (@cons A a l1) l2), @ex (list A) (fun l3 : list A => @perm A l2 (@app A (@cons A a l1) l3)) *)
intros Hu1 Hu2 Hi.
(* Goal: @ex (list A) (fun l3 : list A => @perm A l2 (@app A (@cons A a l1) l3)) *)
assert (H1: In a l2).
(* Goal: @In A x l2 *)
(* Goal: @In A x l3 *)
(* Goal: forall (x : list A) (_ : @perm A l3 (@app A l1 x)), @ex (list A) (fun l3 : list A => @perm A l2 (@app A (@cons A a l1) l3)) *)
apply Hi; auto with datatypes.
(* Goal: @ex (list A) (fun l3 : list A => @perm A l2 (@app A (@cons A a l1) l3)) *)
case perm_in_inv with (1 := H1).
(* Goal: forall (x : list A) (_ : @perm A l2 (@cons A a x)), @ex (list A) (fun l3 : list A => @perm A l2 (@app A (@cons A a l1) l3)) *)
intros l3 Hl3.
(* Goal: @eq nat (exp n O) (S O) *)
case (IH l3); auto.
(* Goal: @eq nat (exp n O) (S O) *)
apply uniq_cons_inv with a; auto.
(* Goal: @eq nat (exp n O) (S O) *)
apply uniq_cons_inv with a; auto.
(* Goal: @eq nat (exp n O) (S O) *)
apply uniq_perm with (1 := Hl3); auto.
(* Goal: @incl A l1 l3 *)
(* Goal: forall (x : list A) (_ : @perm A l3 (@app A l1 x)), @ex (list A) (fun l3 : list A => @perm A l2 (@app A (@cons A a l1) l3)) *)
intros x Hx.
(* Goal: @In A x l3 *)
(* Goal: forall (x : list A) (_ : @perm A l3 (@app A l1 x)), @ex (list A) (fun l3 : list A => @perm A l2 (@app A (@cons A a l1) l3)) *)
assert (H2: In x (a::l3)).
(* Goal: @In A x (@cons A a l3) *)
(* Goal: @In A x l3 *)
(* Goal: forall (x : list A) (_ : @perm A l3 (@app A l1 x)), @ex (list A) (fun l3 : list A => @perm A l2 (@app A (@cons A a l1) l3)) *)
apply perm_in with (1 := Hl3).
(* Goal: @In A x l2 *)
(* Goal: @In A x l3 *)
(* Goal: forall (x : list A) (_ : @perm A l3 (@app A l1 x)), @ex (list A) (fun l3 : list A => @perm A l2 (@app A (@cons A a l1) l3)) *)
apply Hi; auto with datatypes.
(* Goal: @eq nat (exp n O) (S O) *)
simpl in H2; case H2; intros HH; subst; auto.
(* Goal: @In A x l3 *)
(* Goal: forall (x : list A) (_ : @perm A l3 (@app A l1 x)), @ex (list A) (fun l3 : list A => @perm A l2 (@app A (@cons A a l1) l3)) *)
inversion_clear Hu1 as [| aa bb HH1 HH2].
(* Goal: @eq nat (exp n O) (S O) *)
case HH1; auto.
(* Goal: forall (x : list A) (_ : @perm A l3 (@app A l1 x)), @ex (list A) (fun l3 : list A => @perm A l2 (@app A (@cons A a l1) l3)) *)
intros l4 Hl4.
(* Goal: @ex (list A) (fun l3 : list A => @perm A l2 (@app A (@cons A a l1) l3)) *)
exists l4.
(* Goal: @perm A l2 (@app A (@cons A a l1) l4) *)
apply perm_trans with (1 := Hl3).
(* Goal: @eq nat (exp n O) (S O) *)
simpl; apply perm_skip; auto.
Qed.

End Uniq.

Lemma list_split (A: Type) n1 n2 (l: list A):
 length l = n1 + n2 ->
   exists l1, exists l2, l = l1 ++ l2 /\ length l1 = n1 /\ length l2 = n2.
Proof.
(* Goal: forall _ : @eq nat (@length A l) (Init.Nat.add n1 n2), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (and (@eq nat (@length A l1) n1) (@eq nat (@length A l2) n2)))) *)
generalize n2 l; clear n2 l; induction n1 as [| n1 IH].
(* Goal: @eq nat (exp n O) (S O) *)
intros n2 l Hl; exists nil; exists l; auto.
(* Goal: forall (n2 : nat) (l : list A) (_ : @eq nat (@length A l) (Init.Nat.add (S n1) n2)), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (and (@eq nat (@length A l1) (S n1)) (@eq nat (@length A l2) n2)))) *)
intros n2 [| a l] H; try discriminate.
(* Goal: @eq nat (exp n O) (S O) *)
case (IH n2 l); auto.
(* Goal: forall (x : list A) (_ : @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A x l2)) (and (@eq nat (@length A x) n1) (@eq nat (@length A l2) n2)))), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@app A l1 l2)) (and (@eq nat (@length A l1) (S n1)) (@eq nat (@length A l2) n2)))) *)
intros l1 (l2, (H1, (H2, H3))).
(* Goal: @eq nat (exp n O) (S O) *)
exists (a::l1); exists l2; repeat split; subst; simpl; auto.
Qed.

Lemma length_split (A B: Type) (a b: A) (lk: list B) l1 l2:
 length lk = length ((a:: l1) ++ b :: l2)%list ->
 exists k1, exists k2, exists lk1, exists lk2,
 lk = ((k1::lk1) ++ k2::lk2)%list /\ length lk1 = length l1 /\ length lk2 = length l2.
Proof.
(* Goal: forall _ : @eq nat (@length B lk) (@length A (@app A (@cons A a l1) (@cons A b l2))), @ex B (fun k1 : B => @ex B (fun k2 : B => @ex (list B) (fun lk1 : list B => @ex (list B) (fun lk2 : list B => and (@eq (list B) lk (@app B (@cons B k1 lk1) (@cons B k2 lk2))) (and (@eq nat (@length B lk1) (@length A l1)) (@eq nat (@length B lk2) (@length A l2))))))) *)
destruct lk as [| a1 lk].
(* Goal: forall _ : @eq nat (@length B (@nil B)) (@length A (@app A (@cons A a l1) (@cons A b l2))), @ex B (fun k1 : B => @ex B (fun k2 : B => @ex (list B) (fun lk1 : list B => @ex (list B) (fun lk2 : list B => and (@eq (list B) (@nil B) (@app B (@cons B k1 lk1) (@cons B k2 lk2))) (and (@eq nat (@length B lk1) (@length A l1)) (@eq nat (@length B lk2) (@length A l2))))))) *)
(* Goal: forall _ : @eq nat (@length B (@cons B a1 lk)) (@length A (@app A (@cons A a l1) (@cons A b l2))), @ex B (fun k1 : B => @ex B (fun k2 : B => @ex (list B) (fun lk1 : list B => @ex (list B) (fun lk2 : list B => and (@eq (list B) (@cons B a1 lk) (@app B (@cons B k1 lk1) (@cons B k2 lk2))) (and (@eq nat (@length B lk1) (@length A l1)) (@eq nat (@length B lk2) (@length A l2))))))) *)
intros; discriminate.
(* Goal: forall _ : @eq nat (@length B (@cons B a2 lk)) (@length A (@app A (@cons A b1 l1) (@cons A b l2))), @ex B (fun k2 : B => @ex (list B) (fun lk1 : list B => @ex (list B) (fun lk2 : list B => and (@eq (list B) (@cons B a2 lk) (@app B lk1 (@cons B k2 lk2))) (and (@eq nat (@length B lk1) (@length A (@cons A b1 l1))) (@eq nat (@length B lk2) (@length A l2)))))) *)
(* Goal: @ex B (fun k1 : B => @ex B (fun k2 : B => @ex (list B) (fun lk1 : list B => @ex (list B) (fun lk2 : list B => and (@eq (list B) (@cons B a1 lk) (@cons B k1 (@app B lk1 (@cons B k2 lk2)))) (and (@eq nat (@length B lk1) (@length A l1)) (@eq nat (@length B lk2) (@length A l2))))))) *)
simpl; intros HH; injection HH; clear HH; intros HH.
assert (H1:  exists k2, exists lk1, exists lk2,
 lk = (lk1 ++ k2::lk2)%list /\ length lk1 = length l1 /\ length lk2 = length l2).
generalize l1 HH; clear HH; induction lk as [| a2 lk IH]; clear l1;
  intros [| b1 l1]; try (intros; discriminate).
(* Goal: forall _ : @eq nat (@length B (@cons B a2 lk)) (@length A (@app A (@cons A b1 l1) (@cons A b l2))), @ex B (fun k2 : B => @ex (list B) (fun lk1 : list B => @ex (list B) (fun lk2 : list B => and (@eq (list B) (@cons B a2 lk) (@app B lk1 (@cons B k2 lk2))) (and (@eq nat (@length B lk1) (@length A (@cons A b1 l1))) (@eq nat (@length B lk2) (@length A l2)))))) *)
(* Goal: @ex B (fun k1 : B => @ex B (fun k2 : B => @ex (list B) (fun lk1 : list B => @ex (list B) (fun lk2 : list B => and (@eq (list B) (@cons B a1 lk) (@cons B k1 (@app B lk1 (@cons B k2 lk2)))) (and (@eq nat (@length B lk1) (@length A l1)) (@eq nat (@length B lk2) (@length A l2))))))) *)
simpl; intros HH; injection HH; clear HH; intros HH.
(* Goal: @eq nat (exp n O) (S O) *)
exists a2; exists (@nil _); exists lk; repeat split; auto.
(* Goal: forall _ : @eq nat (@length B (@cons B a2 lk)) (@length A (@app A (@cons A b1 l1) (@cons A b l2))), @ex B (fun k2 : B => @ex (list B) (fun lk1 : list B => @ex (list B) (fun lk2 : list B => and (@eq (list B) (@cons B a2 lk) (@app B lk1 (@cons B k2 lk2))) (and (@eq nat (@length B lk1) (@length A (@cons A b1 l1))) (@eq nat (@length B lk2) (@length A l2)))))) *)
(* Goal: @ex B (fun k1 : B => @ex B (fun k2 : B => @ex (list B) (fun lk1 : list B => @ex (list B) (fun lk2 : list B => and (@eq (list B) (@cons B a1 lk) (@cons B k1 (@app B lk1 (@cons B k2 lk2)))) (and (@eq nat (@length B lk1) (@length A l1)) (@eq nat (@length B lk2) (@length A l2))))))) *)
simpl; intros HH; injection HH; clear HH; intros HH.
(* Goal: @eq nat (exp n O) (S O) *)
case (IH _ HH); auto.
(* Goal: forall (x : B) (_ : @ex (list B) (fun lk1 : list B => @ex (list B) (fun lk2 : list B => and (@eq (list B) lk (@app B lk1 (@cons B x lk2))) (and (@eq nat (@length B lk1) (@length A l1)) (@eq nat (@length B lk2) (@length A l2)))))), @ex B (fun k2 : B => @ex (list B) (fun lk1 : list B => @ex (list B) (fun lk2 : list B => and (@eq (list B) (@cons B a2 lk) (@app B lk1 (@cons B k2 lk2))) (and (@eq nat (@length B lk1) (S (@length A l1))) (@eq nat (@length B lk2) (@length A l2)))))) *)
(* Goal: @ex B (fun k1 : B => @ex B (fun k2 : B => @ex (list B) (fun lk1 : list B => @ex (list B) (fun lk2 : list B => and (@eq (list B) (@cons B a1 lk) (@cons B k1 (@app B lk1 (@cons B k2 lk2)))) (and (@eq nat (@length B lk1) (@length A l1)) (@eq nat (@length B lk2) (@length A l2))))))) *)
intros k1 (lk1, (lk2, (H1lk1, (H2lk1, H3lk1)))).
(* Goal: @eq nat (exp n O) (S O) *)
exists k1; exists (a2::lk1); exists lk2; simpl; repeat split; auto.
(* Goal: @eq nat (exp n O) (S O) *)
rewrite H1lk1; auto.
(* Goal: @ex B (fun k1 : B => @ex B (fun k2 : B => @ex (list B) (fun lk1 : list B => @ex (list B) (fun lk2 : list B => and (@eq (list B) (@cons B a1 lk) (@cons B k1 (@app B lk1 (@cons B k2 lk2)))) (and (@eq nat (@length B lk1) (@length A l1)) (@eq nat (@length B lk2) (@length A l2))))))) *)
case H1; intros k2 (lk1, (lk2, (H1lk, (H2lk, H3lk)))).
(* Goal: @eq nat (exp n O) (S O) *)
exists a1; exists k2; exists lk1; exists lk2; repeat split; auto.
(* Goal: @eq nat (exp n O) (S O) *)
rewrite H1lk; auto.
Qed.

Lemma list_app_inj (A: Type) (l1 l2 l3 l4: list A):
 length l1 = length l3 -> l1 ++ l2 = l3 ++ l4 -> l1 = l3 /\ l2 = l4.
Proof.
(* Goal: forall (_ : @eq nat (@length A l1) (@length A l3)) (_ : @eq (list A) (@app A l1 l2) (@app A l3 l4)), and (@eq (list A) l1 l3) (@eq (list A) l2 l4) *)
generalize l2 l3 l4; clear l2 l3 l4; induction l1 as [| x1 l1 IH].
(* Goal: @eq nat (exp n O) (S O) *)
intros  l2 [| x3 l3] l4 H1 H2; try discriminate; auto.
(* Goal: forall (l2 l3 l4 : list A) (_ : @eq nat (@length A (@cons A x1 l1)) (@length A l3)) (_ : @eq (list A) (@app A (@cons A x1 l1) l2) (@app A l3 l4)), and (@eq (list A) (@cons A x1 l1) l3) (@eq (list A) l2 l4) *)
intros l2 [| x3 l3] l4 H1 H2; try discriminate.
(* Goal: @eq nat (exp n O) (S O) *)
injection H2; intros; subst; auto.
(* Goal: @eq nat (exp n O) (S O) *)
case (IH l2 l3 l4); auto; intros; subst; auto.
Qed.

Lemma list_case (A:Type) (l: list A): l = nil \/ l <> nil.
(* Goal: @eq nat (exp n O) (S O) *)
destruct l as [|a l]; simpl; auto.
(* Goal: or (@eq (list A) (@cons A a l) (@nil A)) (not (@eq (list A) (@cons A a l) (@nil A))) *)
right; intros HH; discriminate.
Qed.

Lemma list_dec (A: Type) (P: A -> Prop) l:
 (forall x, P x \/ ~ P x) -> (forall x, In x l -> P x) \/ (exists x, In x l /\ ~ P x).
Proof.
intros Pdec.
induction l as [| a l IH].
left; intros x [].
case (Pdec a); intros H.
2: right; exists a; auto with datatypes.
case IH.
(* Goal: @eq nat (exp n O) (S O) *)
simpl; intros H1; left; intros x [Hx|Hx]; subst; auto.
intros (x,(H1x,H2x)); right; exists x; auto with datatypes.
Qed.


Arguments uniq[A].

(* Georges' trick for easy case analysis *)

Inductive eq_Spec (A: Type) (x y: A): bool -> Prop :=
 |eq_Spect:  x = y -> eq_Spec A x y true
 |eq_Specf: x <> y -> eq_Spec A x y false.

Arguments eq_Spec[A].

(** Binomial Coefficient defined using Pascal's triangle *)
Fixpoint bin (a b : nat) {struct a} : nat :=
 match a, b with
   _, O => 1
  | O, S b' => 0
  | S a', S b' => bin a' (S b') + bin a' b'
 end.

(** Basic properties of binomial coefficients *) 
Lemma bin_0: forall (n : nat),  bin n 0 = 1.
(* Goal: @eq nat (exp n O) (S O) *)
intros n; induction n; auto.
Qed.

Lemma bin_1: forall (n : nat),  bin n 1 = n.
(* Goal: @eq nat (exp n O) (S O) *)
intros; induction n as [|n IH]; simpl; auto.
(* Goal: @eq nat (exp n O) (S O) *)
rewrite bin_0, IH, Plus.plus_comm; auto.
Qed.

Lemma bin_more: forall (n m : nat), n < m ->  bin n m = 0.
(* Goal: @eq nat (exp n O) (S O) *)
intros n; induction n as [| n IH]; simpl; auto.
(* Goal: @eq nat (exp n O) (S O) *)
intros m; case m; simpl; auto.
(* Goal: @eq nat (exp n O) (S O) *)
intros H'; inversion H'; auto.
(* Goal: @eq nat (exp n O) (S O) *)
intros m; case m; simpl; auto.
(* Goal: forall _ : lt (S n) O, @eq nat (S O) O *)
(* Goal: forall (n0 : nat) (_ : lt (S n) (S n0)), @eq nat (Init.Nat.add (bin n (S n0)) (bin n n0)) O *)
intros H'0; contradict H'0; auto with arith.
(* Goal: forall (n0 : nat) (_ : lt (S n) (S n0)), @eq nat (Init.Nat.add (bin n (S n0)) (bin n n0)) O *)
intros n1 H'0; rewrite !IH; auto with arith.
Qed.
 
Lemma bin_nn: forall (n : nat),  bin n n = 1.
(* Goal: @eq nat (exp n O) (S O) *)
intros n; induction n as [| n IH]; intros; simpl; auto.
(* Goal: @eq nat (exp n O) (S O) *)
rewrite (bin_more n (S n)); auto.
Qed.
 
Lemma bin_def:
 forall (n k : nat),  bin (S n) (S k) = bin n (S k) + bin n k.
(* Goal: @eq nat (exp n O) (S O) *)
simpl; auto.
Qed.
 
Fixpoint iter {A: Type} (f: A -> A) (n: nat) (x: A) :=
  match n with 
  | O => x
  | S n1 => f (iter f n1 x)
  end.

(* A bit of ssreflect *)

Coercion b2Prop (x : bool) := x = true.

Lemma b2PropT: b2Prop true.
Proof. exact (refl_equal true). Qed.

Hint Resolve b2PropT.

Require Import Bool.

Lemma andbP b1 b2: b1 && b2 <-> b1 /\ b2.
Proof.
(* Goal: iff (b2Prop (andb b1 b2)) (and (b2Prop b1) (b2Prop b2)) *)
case b1; case b2; intuition.
Qed.

(* Some facts about div2 *)

Lemma div2_double_p n m : div2 (2 * n + m) = n + div2 m.
Proof.
(* Goal: @eq nat (exp n O) (S O) *)
induction n as [| n IH]; simpl; auto.
(* Goal: @eq nat match Init.Nat.add (Init.Nat.add n (S (Init.Nat.add n O))) m with | O => O | S n' => S (Nat.div2 n') end (S (Init.Nat.add n (Nat.div2 m))) *)
rewrite <-plus_n_Sm; simpl in IH |- *.
(* Goal: @eq nat (exp n O) (S O) *)
rewrite IH; auto.
Qed.

Lemma div2_prop n: n + div2 (n * (n - 1)) = div2 (n.+1 * n).
Proof.
(* Goal: @eq nat (Init.Nat.add n (Nat.div2 (Init.Nat.mul n (Init.Nat.sub n (S O))))) (Nat.div2 (Init.Nat.mul (S n) n)) *)
assert (F1: forall n, (n + n * n = 2 * n + n * (n - 1))%nat).
(* Goal: @eq nat (exp n O) (S O) *)
intros [|n1]; simpl; auto.
(* Goal: @eq nat (S (Init.Nat.add n1 (S (Init.Nat.add n1 (Init.Nat.mul n1 (S n1)))))) (S (Init.Nat.add (Init.Nat.add n1 (S (Init.Nat.add n1 O))) (Init.Nat.add (Init.Nat.sub n1 O) (Init.Nat.mul n1 (Init.Nat.sub n1 O))))) *)
(* Goal: @eq nat (Init.Nat.add n (Nat.div2 (Init.Nat.mul n (Init.Nat.sub n (S O))))) (Nat.div2 (Init.Nat.mul (S n) n)) *)
rewrite <-!Minus.minus_n_O; ring.
(* Goal: @eq nat (exp n O) (S O) *)
induction n; simpl; auto.
(* Goal: @eq nat (S (Init.Nat.add n (Nat.div2 (Init.Nat.add (Init.Nat.sub n O) (Init.Nat.mul n (Init.Nat.sub n O)))))) match Init.Nat.add n (S (Init.Nat.add n (Init.Nat.mul n (S n)))) with | O => O | S n' => S (Nat.div2 n') end *)
rewrite <-plus_n_Sm.
(* Goal: @eq nat (S (Init.Nat.add n (Nat.div2 (Init.Nat.add (Init.Nat.sub n O) (Init.Nat.mul n (Init.Nat.sub n O)))))) (S (Nat.div2 (Init.Nat.add n (Init.Nat.add n (Init.Nat.mul n (S n)))))) *)
rewrite <-Minus.minus_n_O.
(* Goal: @eq nat (S (Init.Nat.add n (Nat.div2 (Init.Nat.add n (Init.Nat.mul n n))))) (S (Nat.div2 (Init.Nat.add n (Init.Nat.add n (Init.Nat.mul n (S n)))))) *)
rewrite F1, div2_double_p.
(* Goal: @eq nat (S (Init.Nat.add n (Init.Nat.add n (Nat.div2 (Init.Nat.mul n (Init.Nat.sub n (S O))))))) (S (Nat.div2 (Init.Nat.add n (Init.Nat.add n (Init.Nat.mul n (S n)))))) *)
rewrite !Plus.plus_assoc; replace (n + n) with (2 * n); try ring.
(* Goal: @eq nat (S (Nat.add (Init.Nat.mul (S (S O)) n) (Nat.div2 (Init.Nat.mul n (Init.Nat.sub n (S O)))))) (S (Nat.div2 (Nat.add (Init.Nat.mul (S (S O)) n) (Init.Nat.mul n (S n))))) *)
rewrite div2_double_p, <-(Mult.mult_comm (n.+1)), <-IHn.
(* Goal: @eq nat (S (Nat.add (Init.Nat.mul (S (S O)) n) (Nat.div2 (Init.Nat.mul n (Init.Nat.sub n (S O)))))) (S (Init.Nat.add n (Init.Nat.add n (Nat.div2 (Init.Nat.mul n (Init.Nat.sub n (S O))))))) *)
ring.
Qed.

Lemma minus_minus_le m n: n <= m -> m - (m - n) = n.
Proof.
(* Goal: forall _ : le n m, @eq nat (Init.Nat.sub m (Init.Nat.sub m n)) n *)
assert (F1: (forall n m, n <= m -> exists k, m = k + n)%nat).
(* Goal: @eq nat (exp n O) (S O) *)
intros n1 m1 H; elim H; auto.
(* Goal: @eq nat (exp n O) (S O) *)
exists 0%nat; auto.
(* Goal: @eq nat (exp n O) (S O) *)
intros m2 _ (k, Hk); rewrite Hk; exists k.+1; auto.
(* Goal: forall _ : le n m, @eq nat (Init.Nat.sub m (Init.Nat.sub m n)) n *)
intros H; case (F1 _ _ H).
(* Goal: forall (x : nat) (_ : @eq nat m (Init.Nat.add x n)), @eq nat (Init.Nat.sub m (Init.Nat.sub m n)) n *)
intros k Hk; subst.
(* Goal: @eq nat (Init.Nat.sub (Init.Nat.add k n) (Init.Nat.sub (Init.Nat.add k n) n)) n *)
rewrite (Plus.plus_comm k), Minus.minus_plus.
(* Goal: @eq nat (exp n O) (S O) *)
rewrite (Plus.plus_comm n), Minus.minus_plus; auto.
Qed.

Lemma minus0_le m n: m <= n -> m - n = 0.
Proof.
(* Goal: @eq nat (exp n O) (S O) *)
generalize n; clear n; induction m as [| m IH]; auto.
(* Goal: forall (n : nat) (_ : le (S m) n), @eq nat (Init.Nat.sub (S m) n) O *)
intros [|n]; simpl; auto with arith.
Qed.

Fixpoint eq_nat (m n: nat) :=
  match m, n with (S m), (S n) => eq_nat m n | 0, 0 => true | _, _ => false end.

Notation "m ?= n" := (eq_nat m n) (at level 70): nat_scope.

Inductive eq_nat_spec: nat -> nat -> bool -> Type := 
  eq_nat_spect: forall m, eq_nat_spec m m true
| eq_nat_specb: forall m n, m <> n -> eq_nat_spec m n false.

Lemma eq_natP m n: eq_nat_spec m n (m ?= n).
Proof.
generalize n; clear n; induction m as [| m IH]; intros [| n]; simpl;
  try constructor; try (intros; discriminate).
(case (IH n); clear m n IH); [intros m | intros m n H];
(* Goal: @eq nat (exp n O) (S O) *)
  constructor; intros H1; case H; injection H1; auto.
Qed.

Notation "x .+2" := (S (S x))  (at level 9): nat_scope.