Formalisation of "Axiomatic Set Theory in Type Theory" by Gert Smolka
- Version: 16 May 2015
- Author: Dominik Kirst, Saarland University
- This file covers Sections 8 and 9 of the paper
- Acknowlegments: The linearity proof of the class Tower is a porting of the more general proof given by Gert Smolka, Steven Schäfer and Christian Doczkal (https://www.ps.uni-saarland.de/extras/itp15/)
Require Export orderings sets.
Implicit Types x y z: set.
Implicit Types p q: set -> Prop.
Implicit Types R S U V: set -> set -> Prop.
General Results of the Paper
Well-Orderings on Sets
Lemma sub_el x y:
~ (x <<= y) -> exists z, z el x /\ ~ z el y.
Proof.
intros I. indirect. apply I. intros z Z.
indirect. apply H. exists z. now split.
Qed.
Lemma sing_el x y:
x <> sing y -> inhab x -> exists z, z el x /\ y <> z.
Proof.
intros H I. destruct (classic (x <<= sing y)) as [J|J].
- apply sub_sing in J; firstorder.
- destruct (sub_el J) as [z[Z1 Z2]].
exists z. split; trivial.
intros E. subst z. apply Z2. now apply el_sing.
Qed.
Definition sur R x :=
forall y, y el x -> exists z, R z y.
Lemma rep_rep x R:
sur R x -> functional R -> functional (inv R) -> x = rep (rep x (inv R)) R.
Proof.
intros SR FR FI. apply sub_anti; intros y Y.
- apply (rep_func FR). destruct (SR y Y) as [z Z].
exists z. split; trivial. apply (rep_func FI). exists y. split; assumption.
- apply (rep_func FR) in Y as [z[Z1 Z2]].
apply (rep_func FI) in Z1 as [z'[Z1' Z2']].
now rewrite (FR z y z').
Qed.
Lemma rep_equal R S x:
R o=o S -> rep x R = rep x S.
Proof.
intros RS. apply sub_anti; intros y Y; apply Rep;
apply Rep in Y as [z[Z1 Z2]]; exists z; firstorder.
Qed.
Transitive and well-founded sets
Definition trans x :=
forall y, y el x -> y <<= x.
Inductive WF x: Prop :=
| WFI: subsc x WF -> WF x.
Lemma trans_union x:
subsc x trans -> trans (union x).
Proof.
intros H y Y. apply Union in Y as [z[Z1 Z2]].
intros u UY. apply Union. exists z.
split; trivial. now apply (H z Z1 y).
Qed.
Lemma WF_union x:
WF x -> WF (union x).
Proof.
intros WFX; constructor. intros y YU. apply Union in YU as [z[Z1 Z2]].
destruct WFX as [WFX]. destruct (WFX z Z1) as [H]. now apply H.
Qed.
Lemma WF_no_loop x:
WF x -> x el x -> False.
Proof.
induction 1 as [x H IH]. eauto.
Qed.
Properties of orderings
Definition orealizable R :=
realizable (dom R).
Definition complete R :=
~ orealizable R /\ forall x, dom R x -> realizable (Seg R x).
Facts about completeness (17)
Lemma simi_realizable_iff R S:
simi R S -> orealizable R -> orealizable S.
Proof.
intros [U UI] [x XR]. exists (rep x U). intros y; split; intros Y.
- apply Rep in Y as [z[Z1 Z2]]. apply UI. exists z. apply Z2.
- apply Rep. destruct UI as [U1[_ U2]]. destruct (U2 y Y) as [z Z].
exists z. specialize (XR z). split; firstorder.
Qed.
Lemma complete_simi R S:
worder R -> worder S -> complete R -> complete S -> simi R S.
Proof.
intros WOR WOS [RU RS] [SU SS]. exists (Canon R S).
destruct (canon_max WOR WOS) as [CS[H|H]]; split; trivial; split; trivial.
- destruct (worder_Segs WOS (simi_dom2 CS)) as [I|[x[X1 X2]]]; try apply I.
exfalso. destruct (SS x X1) as [s SH]. apply RU.
exists (sep (rep s (inv (Canon R S))) (dom R)). apply sep_realizes.
intros y Y. apply rep_func; try apply CS. destruct (H y Y) as [z Z].
exists z. split; trivial. apply SH. apply X2. now exists y.
- destruct (worder_Segs WOR (simi_dom1 CS)) as [I|[x[X1 X2]]]; try apply I.
exfalso. destruct (RS x X1) as [s SH]. apply SU.
exists (sep (rep s (Canon R S)) (dom S)). apply sep_realizes.
intros y Y. apply rep_func; try apply CS. destruct (H y Y) as [z Z].
exists z. split; trivial. apply SH. apply X2. now exists y.
Qed.
Lemma real_unreal_seg R S:
worder R -> worder S -> orealizable R -> ~ orealizable S
-> exists x, dom S x /\ simi R (res_seg S x).
Proof.
intros WOR WOS [D OR] OS. destruct (embedding WOR WOS) as [[p[P1 P2]]|[q[Q1 Q2]]].
- exfalso. apply OS. destruct P2 as [U[U1[U2 U3]]].
exists (sep (rep D U) (dom S)). apply sep_realizes.
intros x X. apply rep_func; try apply U1. destruct (U3 x X) as [y Y].
exists y. split; auto. apply OR. apply (res_sub1 (p:=p)). apply U1. now exists x.
- apply (worder_Segs WOS) in Q1 as [Q1|[x[X1 X2]]].
+ exfalso. apply OS. destruct Q2 as [U[U1[U2 U3]]].
exists (sep (rep D U) (dom S)). apply sep_realizes.
intros x X. apply rep_func; try apply U1. destruct Q1 as [_ Q1].
destruct (U3 x) as [y Y]; eauto using res_sub. exists y.
split; trivial. apply OR. apply U1. now exists x.
+ exists x. split; trivial. destruct Q2 as [U[U1[U2 U3]]]. exists U. split.
* apply (simi_rewrite U1). firstorder.
* split; trivial. intros y [z Z]. apply U3. exists z. firstorder.
Qed.
Properties of classes
Definition Inc p :=
res sub p.
Definition ctrans p :=
forall x, p x -> subsc x p.
Definition ccum p :=
forall x y, p x -> p y -> (x el y <-> x << y).
Definition cWF p :=
subcc p WF.
Definition clinear p :=
forall x y, p x -> p y -> x <<= y \/ y <<= x.
Definition wordered p :=
worder (Inc p).
Facts about the inclusion ordering (18)
Lemma inc_dom p:
dom (Inc p) === p.
Proof.
firstorder.
Qed.
Lemma inc_seg p x:
subcs (Seg (Inc p) x) (pow x).
Proof.
intros y Y. apply Power. apply Y.
Qed.
Lemma cum_seg p x:
ccum p -> subcs (Seg (Inc p) x) x.
Proof.
intros PC y Y. apply PC; firstorder.
Qed.
Lemma seg_equiv p x:
p x -> ctrans p -> ccum p -> Seg (Inc p) x === class x.
Proof.
intros PX PT PC. split.
- now apply cum_seg.
- intros y Y. specialize (PT x PX y Y). specialize (PC y x PT PX).
apply PC in Y. firstorder.
Qed.
Lemma Inc_partial p:
porder (Inc p).
Proof.
firstorder using Ext, sub_anti, sub_trans.
Qed.
Lemma Inc_linear p:
clinear p -> linear (Inc p).
Proof.
firstorder.
Qed.
Lemma Inc_seg_real p x:
realizable (Seg (Inc p) x).
Proof.
exists (sep (pow x) (Seg (Inc p) x)). apply sep_realizes. apply inc_seg.
Qed.
Lemma Inc_complete p:
~ realizable p -> complete (Inc p).
Proof.
intros H. split.
- intros [x X]. apply H. exists x. firstorder.
- intros x _. apply Inc_seg_real.
Qed.
Linear, cumulative and well-founded classes are well-ordered (20)
Lemma Inc_worder p:
clinear p -> ccum p -> cWF p -> worder (Inc p).
Proof.
intros CL PC PWF. split; auto using Inc_partial.
intros q [x QX] QP. assert (QSP: subcc q p) by firstorder.
assert (WFX: WF x) by firstorder. induction WFX as [x H IH].
destruct (classic (exists z, z el x /\ q z)) as [[z Z]|I].
- apply (IH z); apply Z.
- exists x. split; trivial. intros z Z. destruct (classic (z=x)) as [E|NE].
+ subst z. repeat split; auto.
+ repeat split; auto. destruct (CL x z) as [L|L]; auto.
exfalso. apply I. exists z. split; trivial. apply PC; auto.
Qed.
Section Tower.
Definition increasing f :=
forall x, x <<= f x.
Definition cumulative f :=
forall x, x el f x.
Definition trans_pres f :=
forall x, trans x -> trans (f x).
Definition WF_pres f :=
forall x, WF x -> WF (f x).
Variable f: set -> set.
Inductive Tower: set -> Prop :=
| TU x: subsc x Tower -> Tower (union x)
| TS x: Tower x -> Tower (f x).
Lemma tower_trans x:
trans_pres f -> Tower x -> trans x.
Proof.
intros TF TX. induction TX as [x H IH| x H IH].
- now apply trans_union.
- now apply TF.
Qed.
Lemma tower_WF:
WF_pres f -> cWF Tower.
Proof.
intros WFF x TX. induction TX as [x H IH| x H IH].
- apply WF_union. now constructor.
- now apply WFF.
Qed.
Linearity of the tower class 1. Generalised tower construction
Inductive SegB x: set -> Prop :=
| SBB: SegB x x
| SFB y: SegB x y -> SegB x (f y)
| SLB M: (forall y, y el M -> SegB x y) -> inhab M -> SegB x (union M).
| SBB: SegB x x
| SFB y: SegB x y -> SegB x (f y)
| SLB M: (forall y, y el M -> SegB x y) -> inhab M -> SegB x (union M).
2. The chain that starts on the empty set is exactly the class cum
Lemma tower_SegB x:
Tower x -> (SegB (eset x)) x.
Proof.
induction 1 as [x X IH| x X IH].
- destruct (classic (inhab x)) as [H|H].
+ constructor; trivial. intros y Y. rewrite (eset_equal (union x) y). auto.
+ apply not_inhab in H. rewrite H at 2.
rewrite union_eset_eq. rewrite (eset_equal (union x) x). constructor.
- constructor. now rewrite (eset_equal (f x) x).
Qed.
Tower x -> (SegB (eset x)) x.
Proof.
induction 1 as [x X IH| x X IH].
- destruct (classic (inhab x)) as [H|H].
+ constructor; trivial. intros y Y. rewrite (eset_equal (union x) y). auto.
+ apply not_inhab in H. rewrite H at 2.
rewrite union_eset_eq. rewrite (eset_equal (union x) x). constructor.
- constructor. now rewrite (eset_equal (f x) x).
Qed.
3. The tower construction refines set inclusion
Lemma SegB_sub x y:
increasing f -> SegB x y -> x <<= y.
Proof.
intros FI. induction 1 as [|y Y IH |M MX IH MI].
- auto.
- apply (sub_trans IH). apply FI.
- destruct MI as [m MM].
specialize (IH m MM).
intros z Z. apply Union.
exists m. split; auto.
Qed.
increasing f -> SegB x y -> x <<= y.
Proof.
intros FI. induction 1 as [|y Y IH |M MX IH MI].
- auto.
- apply (sub_trans IH). apply FI.
- destruct MI as [m MM].
specialize (IH m MM).
intros z Z. apply Union.
exists m. split; auto.
Qed.
4. Two lemmas that ease the linearity proof
Definition bounded x M :=
forall y, y el M -> exists z, z el M /\ y <<= z /\ SegB x z.
Lemma relax x M:
inhab M -> bounded x M -> SegB x (union M).
Proof.
intros H I.
pose (N := sep M (fun z => SegB x z)).
cut (union M = union N).
- intros J. rewrite J. constructor.
+ intros y Y. now apply Sep in Y as [].
+ destruct H as [m MM].
destruct (I m MM) as [z[Z1[Z2 Z3]]].
exists z. apply Sep. now split.
- apply Ext; intros y; split; intros Y.
+ apply Union in Y as [z[Z1 Z2]].
destruct (I z Z1) as [u[U1[U2 U3]]].
apply Union. exists u. split; auto.
apply Sep. now split.
+ apply Union in Y as [z[Z1 Z2]].
apply Sep in Z1 as [Z1 _].
apply Union. exists z. now split.
Qed.
Lemma step x y:
increasing f -> SegB x y -> x = y \/ SegB (f x) y.
Proof.
intros FI. induction 1 as [|y Y IH |M MX IH MI].
- now left.
- destruct IH as [IH|IH].
+ right. rewrite IH. constructor.
+ right. now constructor.
- destruct (classic (M = sing x)).
+ left. rewrite H. now rewrite union_sing_eq.
+ destruct (sing_el H MI) as [z[Z1 Z2]].
right. apply relax; try assumption.
intros y Y. destruct (IH y Y) as [I|I].
* exists z. subst y.
destruct (IH z Z1) as [J|J]; try contradiction.
repeat split; try assumption.
apply (SegB_sub FI). now apply MX.
* exists y. now repeat split.
Qed.
Lemma shift x y:
increasing f -> (SegB x y \/ SegB y x) -> (SegB (f x) y \/ SegB y (f x)).
Proof.
intros FI. intros [H|H].
- apply (step FI) in H as [H|H].
+ subst y. right. repeat constructor.
+ now left.
- right. now constructor.
Qed.
forall y, y el M -> exists z, z el M /\ y <<= z /\ SegB x z.
Lemma relax x M:
inhab M -> bounded x M -> SegB x (union M).
Proof.
intros H I.
pose (N := sep M (fun z => SegB x z)).
cut (union M = union N).
- intros J. rewrite J. constructor.
+ intros y Y. now apply Sep in Y as [].
+ destruct H as [m MM].
destruct (I m MM) as [z[Z1[Z2 Z3]]].
exists z. apply Sep. now split.
- apply Ext; intros y; split; intros Y.
+ apply Union in Y as [z[Z1 Z2]].
destruct (I z Z1) as [u[U1[U2 U3]]].
apply Union. exists u. split; auto.
apply Sep. now split.
+ apply Union in Y as [z[Z1 Z2]].
apply Sep in Z1 as [Z1 _].
apply Union. exists z. now split.
Qed.
Lemma step x y:
increasing f -> SegB x y -> x = y \/ SegB (f x) y.
Proof.
intros FI. induction 1 as [|y Y IH |M MX IH MI].
- now left.
- destruct IH as [IH|IH].
+ right. rewrite IH. constructor.
+ right. now constructor.
- destruct (classic (M = sing x)).
+ left. rewrite H. now rewrite union_sing_eq.
+ destruct (sing_el H MI) as [z[Z1 Z2]].
right. apply relax; try assumption.
intros y Y. destruct (IH y Y) as [I|I].
* exists z. subst y.
destruct (IH z Z1) as [J|J]; try contradiction.
repeat split; try assumption.
apply (SegB_sub FI). now apply MX.
* exists y. now repeat split.
Qed.
Lemma shift x y:
increasing f -> (SegB x y \/ SegB y x) -> (SegB (f x) y \/ SegB y (f x)).
Proof.
intros FI. intros [H|H].
- apply (step FI) in H as [H|H].
+ subst y. right. repeat constructor.
+ now left.
- right. now constructor.
Qed.
5. Linearity proof
Lemma SegB_linearity_aux M N:
increasing f -> (forall x, x el M -> SegB x (union N) \/ SegB (union N) x) ->
(union M <<= union N -> SegB (union M) (union N) \/ SegB (union N) (union M)) ->
SegB (union M) (union N) \/ SegB (union N) (union M).
Proof with eauto using SegB_sub.
intros FI H I.
destruct (classic (exists x, x el M /\ SegB (union N) x)) as [[x[X1 X2]]|J].
- right. apply relax... now exists x. intros y Y. destruct (H y Y)...
exists x. intuition. apply (sub_trans (y:=union N))...
- apply I. apply union_incl. intros x X. apply (SegB_sub FI).
destruct (H x X) as [|H']... exfalso...
Qed.
Theorem linearity_SegB x y z:
increasing f -> SegB x y -> SegB x z -> SegB y z \/ SegB z y.
Proof.
intros FI H. revert z. induction H as [|y Y IH |M MX IHM MI]; intros z H.
- now left.
- apply (shift FI). now apply IH.
- induction H as [|y Y IH |N NX IHN NI].
+ right. now constructor.
+ apply or_comm. apply (shift FI). apply or_comm. apply IH.
+ apply (SegB_linearity_aux FI).
* intros y Y. destruct (IHM y Y (union N)); eauto using SegB.
* intros H. apply or_comm. apply (SegB_linearity_aux FI).
{ intros y Y. destruct (IHN y Y); tauto. }
intros I. left. cutrewrite (union N = union M). constructor.
now apply sub_anti.
Qed.
Corollary tower_linear:
increasing f -> clinear Tower.
Proof.
intros FI x y TX TY. apply tower_SegB in TX. apply tower_SegB in TY.
rewrite (eset_equal x y) in TX. destruct (linearity_SegB FI TX TY) as [XY|YX].
- left. now apply SegB_sub.
- right. now apply SegB_sub.
Qed.
Lemma tower_sandwich x y:
increasing f -> Tower x -> Tower y -> x << y -> f x <<= y.
Proof.
intros FI TX TY SS. apply tower_SegB in TX. apply tower_SegB in TY.
rewrite (eset_equal x y) in TX. destruct (linearity_SegB FI TX TY) as [XY|YX].
- destruct (step FI XY) as [E|FX].
+ exfalso. now apply SS.
+ now apply (SegB_sub FI).
- exfalso. apply SS. apply sub_anti; eauto using (SegB_sub FI). apply SS.
Qed.
increasing f -> (forall x, x el M -> SegB x (union N) \/ SegB (union N) x) ->
(union M <<= union N -> SegB (union M) (union N) \/ SegB (union N) (union M)) ->
SegB (union M) (union N) \/ SegB (union N) (union M).
Proof with eauto using SegB_sub.
intros FI H I.
destruct (classic (exists x, x el M /\ SegB (union N) x)) as [[x[X1 X2]]|J].
- right. apply relax... now exists x. intros y Y. destruct (H y Y)...
exists x. intuition. apply (sub_trans (y:=union N))...
- apply I. apply union_incl. intros x X. apply (SegB_sub FI).
destruct (H x X) as [|H']... exfalso...
Qed.
Theorem linearity_SegB x y z:
increasing f -> SegB x y -> SegB x z -> SegB y z \/ SegB z y.
Proof.
intros FI H. revert z. induction H as [|y Y IH |M MX IHM MI]; intros z H.
- now left.
- apply (shift FI). now apply IH.
- induction H as [|y Y IH |N NX IHN NI].
+ right. now constructor.
+ apply or_comm. apply (shift FI). apply or_comm. apply IH.
+ apply (SegB_linearity_aux FI).
* intros y Y. destruct (IHM y Y (union N)); eauto using SegB.
* intros H. apply or_comm. apply (SegB_linearity_aux FI).
{ intros y Y. destruct (IHN y Y); tauto. }
intros I. left. cutrewrite (union N = union M). constructor.
now apply sub_anti.
Qed.
Corollary tower_linear:
increasing f -> clinear Tower.
Proof.
intros FI x y TX TY. apply tower_SegB in TX. apply tower_SegB in TY.
rewrite (eset_equal x y) in TX. destruct (linearity_SegB FI TX TY) as [XY|YX].
- left. now apply SegB_sub.
- right. now apply SegB_sub.
Qed.
Lemma tower_sandwich x y:
increasing f -> Tower x -> Tower y -> x << y -> f x <<= y.
Proof.
intros FI TX TY SS. apply tower_SegB in TX. apply tower_SegB in TY.
rewrite (eset_equal x y) in TX. destruct (linearity_SegB FI TX TY) as [XY|YX].
- destruct (step FI XY) as [E|FX].
+ exfalso. now apply SS.
+ now apply (SegB_sub FI).
- exfalso. apply SS. apply sub_anti; eauto using (SegB_sub FI). apply SS.
Qed.
Well-ordering and representation theorem of towers
Lemma tower_cumulative:
increasing f -> cumulative f -> trans_pres f -> WF_pres f -> ccum Tower.
Proof.
intros FI FC FT FWF x y TX TY. split; intros H.
- split; try now apply tower_trans. intros XY. subst y.
apply (@WF_no_loop x); auto using (tower_WF FWF TX).
- apply tower_sandwich in H; trivial. apply H. apply FC.
Qed.
Lemma tower_unrealizable:
increasing f -> cumulative f -> WF_pres f -> ~ realizable Tower.
Proof.
intros FI FC FWF [x X]. cut (union x = f (union x)).
- intros H. apply (@WF_no_loop (union x)).
+ apply tower_WF; firstorder using Tower.
+ specialize (FC (union x)). congruence.
- apply sub_anti; auto. apply union_el_incl. apply X. firstorder using Tower.
Qed.
Lemma tower_norealizable:
increasing f -> cumulative f -> WF_pres f -> ~ orealizable (Inc Tower).
Proof.
intros FI FC FW. apply Inc_complete. now apply tower_unrealizable.
Qed.
Theorem tower_worder:
increasing f -> cumulative f -> trans_pres f -> WF_pres f
-> wordered Tower /\ complete (Inc Tower).
Proof.
intros FI FC FT FWF. split.
- apply Inc_worder; auto using tower_cumulative, tower_linear, tower_WF.
- apply Inc_complete. now apply tower_unrealizable.
Qed.
Lemma tower_representation R:
increasing f -> cumulative f -> trans_pres f -> WF_pres f ->
worder R -> orealizable R -> exists! x, Tower x /\ simi R (res_seg (Inc Tower) x).
Proof.
intros FI FC FT FW WR OR.
assert (TW: wordered Tower) by now apply tower_worder.
assert (TU: ~ orealizable (Inc Tower)) by now apply tower_norealizable.
generalize (real_unreal_seg WR TW). intros H. specialize(H OR TU).
destruct H as [x[H I]]. exists x. repeat split.
- destruct H as [y H]. apply H.
- apply I.
- intros x' [X1 X2]. assert (XD: dom (Inc Tower) x') by (exists x'; firstorder).
apply (seg_equal TW H XD). apply (simi_equiv TW); eauto using seg_segs.
now apply simi_trans with (R:=R).
Qed.
End Tower.