順序対の定義と性質

ssrzfc002.v

(*---  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.