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/)
Instantiation of Linearity Proof
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.
Definition des p :=
union (rep (sing empty) (fun y => p)).
Lemma des_correct p x:
unique p x -> p (des p).
Lemma des_unique p x:
unique p x -> x = des p.
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.
Definition join M :=
union (des (fun x => realizes x M)).
Lemma join_union x:
join (class x) = union x.
4. Altogether, the type of sets with the inclusion ordering
implements the abstract definition of a complete partial order.
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.