Formalisation of "Axiomatic Set Theory in Type Theory" by Gert Smolka
• Version: 16 May 2015
• Author: Dominik Kirst, Saarland University
• This file shows how the general linearity proof for towers is instantiated
• Acknowlegments: This instantiation is based on the library of the general proof given by Gert Smolka, Steven SchÃ¤fer and Christian Doczkal (https://www.ps.uni-saarland.de/extras/itp15/)

Require Import sets GeneralTower Classical.

# Instantiation of Linearity Proof

1. We assume an increasing function f and define the Tower of f inductively

Definition increasing f :=
forall x, x <<= f x.

Variable f: set -> set.
Variable FI: increasing f.

Inductive Tower: set -> Prop :=
| TU x: subsc x Tower -> Tower (union x)
| TS x: Tower x -> Tower (f x).

2. To define a join operator for classes over sets (= realizable union), we have to assume an empty set and define the general description operator.

Axiom empty: set.
Axiom Empty: ~ inhab empty.

Lemma ninhab_union x:
~ inhab x -> union x = empty.
Proof.
intros H. apply sub_anti; intros y Y.
- apply Union in Y as [z[Z _]]. contradict H. now exists z.
- exfalso. apply Empty. now exists y.
Qed.

Definition des p :=
union (rep (sing empty) (fun y => p)).

Lemma des_correct p x:
unique p x -> p (des p).
Proof.
intros [P1 P2]. cutrewrite (des p = x); trivial.
apply sub_anti; intros y Y.
- apply Union in Y as [z[Z1 Z2]]. apply Rep in Z1 as [u[U1 U2]].
cutrewrite (x = z); trivial. apply P2. apply U2.
- apply Union. exists x. split; trivial. apply Rep.
exists empty. split; firstorder using el_sing.
Qed.

Lemma des_unique p x:
unique p x -> x = des p.
Proof.
intros H. apply H. apply (des_correct H).
Qed.

3. Since the realizes predicate acts uniquely on sets, we can derive the wished join operator.

Lemma realizes_unique M x:
realizes x M -> unique (fun x => realizes x M) x.
Proof.
intros XM. split; trivial. intros y YM. apply Ext. firstorder.
Qed.

Definition join M :=
union (des (fun x => realizes x M)).

Lemma join_union x:
join (class x) = union x.
Proof.
unfold join. rewrite <- des_unique with (x:=x); trivial. firstorder using Ext.
Qed.

4. Altogether, the type of sets with the inclusion ordering implements the abstract definition of a complete partial order.

Definition sets: CompletePartialOrder.CompletePartialOrder.
exists set realizable sub join; auto using sub_anti.
intros M y [x X]. apply realizes_unique in X. split; intros H.
- apply union_incl. rewrite <- (des_unique X). firstorder.
- unfold join in H. rewrite <- (des_unique X) in H.
destruct (union_incl y x) as [I _]. firstorder.
Defined.

5. Finally, since our predicate Tower corresponds to Reach, the predicate that describes transfinite reachability in the library, we can easily instantiate the linearity proof for towers.

Lemma tower_reach x:
Tower x -> Reach (T:=sets) f empty x.
Proof.
induction 1 as [x H IH|x H IH].
- destruct (classic (inhab x)) as [NE|E].
+ rewrite <- (join_union x). constructor; firstorder.
+ rewrite (ninhab_union E). constructor.
- now constructor.
Qed.

Lemma linearity x y:
Tower x -> Tower y -> x <<= y \/ y <<= x.
Proof.
intros TX TY. apply (@linearity sets f FI) with (c:=empty).
- intros p q PQ [z Z]. exists (sep z p). apply sep_realizes. firstorder.
- now apply tower_reach.
- now apply tower_reach.
Qed.