Skip to content

Instantly share code, notes, and snippets.

@srbmiy srbmiy/ssrzfc002.v
Created Dec 23, 2014

Embed
What would you like to do?
順序対の定義と性質
(*--- Kuratowski's Definition of ordered-pairs ---*)
Definition ordered_pair (x y : SET) : SET :=
{ {{x}} , { x , y } }.
Notation "\( x , y \)" := (ordered_pair x y) (at level 35).
Lemma 補題_Singletonのequality : forall (x y z : SET), {{x}} = {y, z} -> x = y.
Proof.
move=> y x z; move.
case=> Hsingleton.
assert ( x ∈ {x, z} ) as Hxinx.
apply (PairingAxiom x z x); left; reflexivity.
assert ( x ∈ {{y}} ) as Hyinx.
rewrite -> Hsingleton; exact.
assert (y = x \/ y = x) as Htmp.
apply (PairingAxiom y y x).
exact.
destruct Htmp.
exact.
exact.
Qed.
Lemma 補題_非順序対は交換可能 : forall (x y : SET), {x , y} = {y , x}.
Proof.
move=> x y.
rewrite <- (Extensionality ({x , y}) ({y , x})).
move=> z.
move; split.
move=> Hleft.
apply (PairingAxiom y x z).
assert ((x = z) \/ (y = z)).
apply (PairingAxiom x y z); exact.
destruct H.
move: H; auto.
move: H; auto.
move=> Hleft.
apply (PairingAxiom x y z).
assert ((y = z) \/ (x = z)).
apply (PairingAxiom y x z); exact.
destruct H.
move: H; auto.
move: H; auto.
Qed.
Lemma 補題_順序対のequality : forall (x0 x1 y0 y1 : SET), (x0 = x1) /\ (y0 = y1) <-> ( \( x0, y0 \) = \(x1 , y1\) ).
Proof.
move => x y z w.
(* 片方ずつ示すこととします *)
assert ((x = y) /\ (z = w) -> \(x, z\) = \(y, w\)) as Hright.
case=> Hxy Hzw.
rewrite <- Hxy; rewrite <- Hzw; exact.
(* もう片方の難しい方を示す *)
assert ( \(x, z\) = \(y, w\) -> (x=y)/\(z=w) ) as Hleft.
case=> Hpair. (* 仮定の導入 *)
(* Proof x=y Start. *)
assert (x = y) as Hxy.
assert ({{x}} ∈ \(x, z \)) as Hx.
apply (PairingAxiom ({{x}}) ({x , z})).
left; exact.
assert ({{x}} ∈ \(y, w\)) as Hxinyw.
rewrite <- Hpair; assumption.
assert (({{y}} = {{x}}) \/ ({y,w} = {{x}})) as Hdicotomy.
apply (PairingAxiom ({{y}}) ({y,w}) ({{x}})); assumption.
destruct Hdicotomy. (* Dicotomiyの場合分け. *)
(* どちらの場合でも x=y でて来るはず *)
assert (y= x) as Hxeqy.
apply (補題_Singletonのequality y x x); exact.
rewrite -> Hxeqy; reflexivity.
assert ({{x}} = {y, w}) as Hprev.
rewrite <- H; reflexivity.
apply (補題_Singletonのequality x y w); exact.
(* Proof x=y End. *)
(* Proof z=w Start. Simply a symmetric argument. *)
assert (z = w) as Hzw.
assert ({x , z} ∈ \(x, z \)) as Hxz.
apply (PairingAxiom ({{x}}) ({x,z}) ({x , z})).
right; exact.
assert ({x , z} ∈ \(y, w \)) as Hxzinyw.
rewrite <- Hpair; assumption.
assert ({{y}} = ({x ,z}) \/ ({y , w} = {x , z})) as Hdicotomy.
apply (PairingAxiom ({{y}}) ({y , w}) ({x , z})); assumption.
destruct Hdicotomy. (* Dicotomiyの場合分け. *)
(* どちらの場合でも z=w でて来るはず *)
(*apply (補題_Singletonのequality y x z); exact.*)
assert ({{y}} = {z,x} ) as HH.
rewrite -> (補題_非順序対は交換可能 z x); exact.
assert (y = z) as Hyz.
apply (補題_Singletonのequality y z x); exact.
assert (x = z) as Hxeqz.
rewrite <- Hyz; exact.
assert ({y, w} ∈ \(x , z \)) as Hyw.
assert ({y, w} ∈ \(y , w \)).
apply (PairingAxiom ({{y}}) ({y , w}) ({y , w})); right; reflexivity.
rewrite -> Hpair; exact.
assert ({y , w} = {{x}}).
assert (({{x}} = {y , w}) \/ ({x , z} = {y , w})).
apply (PairingAxiom ({{x}}) ({x , z}) ({y , w})); exact.
case: H0; auto.
rewrite <- Hxeqz; auto.
assert ({{x}} = {y, w}) as Hprev.
auto.
move: Hprev.
rewrite <- Hxeqz.
rewrite <- Hxy.
move=> Hprev.
assert (w ∈ {x , w}).
apply (PairingAxiom x w w); right; reflexivity.
move: H1.
rewrite <- Hprev.
move=> Hprev2.
assert (x = w \/ x = w).
apply (PairingAxiom x x w); exact.
case H1; exact.
assert (x = w \/ x <> w) as EMxz.
Hypothesis EM : forall p : Prop, p \/ ~p.
apply (EM (x = w)).
case: EMxz.
move=> Hxeqw.
assert ({{x}} = {x , z}).
rewrite <- H.
rewrite <- Hxy.
rewrite <- Hxeqw; reflexivity.
assert ({{x}} = {z , x}).
rewrite -> (補題_非順序対は交換可能 z x); exact.
assert (x = z).
apply (補題_Singletonのequality x z x); exact.
rewrite <- H2; exact.
move=> Hxneqw.
assert (w ∈ {x , z}).
assert (w ∈ {y , w}).
apply (PairingAxiom y w w); right; reflexivity.
rewrite <- H; exact.
assert ((x = w) \/ (z = w)).
apply (PairingAxiom x z w); exact.
case: H1.
move=> H2.
contradiction.
trivial.
move: Hxy Hzw; auto.
move.
auto.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.