Coqで鳩の巣原理の証明

1 Star2 Stars3 Stars4 Stars5 Stars (まだ評価されていません)
Loading...

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.


1 Star2 Stars3 Stars4 Stars5 Stars (まだ評価されていません)
Loading...
      この投稿は審査処理中  | 元のサイトへ