Coqで鳩の巣原理の証明

「Software Foundations」のLogic_Jで定式化された鳩の巣原理の証明。

pigeonhole_principle.v

(*  (* Logic_J.v の独自(<=)を使う場合はこの中身が必要 *)
Lemma lt_irrefl : forall n, ~ n < n.
Proof.
 induction n.
  intro. inversion H.

  intro. destruct IHn.
  apply Sn_le_Sm__n_le_m. apply H.
Qed.

Lemma lt_not_le: forall n m : nat, n < m -> ~ m <= n.
Proof.
 intros.
 induction H.
  apply lt_irrefl.

  intro. destruct IHle. inversion H0.
   apply le_S. apply le_n.

   rewrite <- H2 in H0. apply le_S. apply Sn_le_Sm__n_le_m. apply H0.
Qed. 
*)

Lemma aux1 : forall {X:Type} (x:X) xs l1 l2, (forall a, appears_in a (x :: xs ) -> appears_in a (l1++(x::l2))) -> ~repeats (x::xs) -> forall a, appears_in a xs -> appears_in a (l1++l2).
Proof.
 intros.
 destruct (appears_in_app l1 (x::l2) a (H a (ai_later a x xs H1))).
  apply app_appears_in. left. apply H2.

  apply app_appears_in. right.
  inversion H2.
   destruct H0. rewrite <- H4. apply RP_hd. apply H1.

   apply H4.
Qed.

Lemma aux2 : forall {X:Type} xs ys,
  (forall a:X, appears_in a xs -> appears_in a ys) ->
  ~ repeats xs -> length xs <= length ys.
Proof.
 intros X xs. induction xs; intros.
  apply O_le_n.  

  destruct (appears_in_app_split _ _ (H x (ai_here _ _))) as [l1].
  destruct H1 as [l2].
  rewrite H1. rewrite app_length. simpl. 
  rewrite <- plus_n_Sm. apply n_le_m__Sn_le_Sm. rewrite <- app_length.
  apply IHxs. (*ここで(l1++l2)についてIHを使う*)
   intros. rewrite H1 in H. apply (aux1 _ _ _ _ H H0). apply H2.
   
   intro. destruct H0. apply RP_tl. apply H2.
Qed.

Theorem pigeonhole_principle: forall {X:Type} (l1 l2:list X),
  excluded_middle ->
  (forall x, appears_in x l1 -> appears_in x l2) ->
  length l2 < length l1 ->
  repeats l1.
Proof.
 intros.
 Check(H (repeats l1)).
 destruct (H (repeats l1)); [assumption |]. (* 背理法 *)
 destruct (lt_not_le _ _ H1).
 apply aux2; [apply H0 | apply H2].
Qed.