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 (

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.

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.

Definition sets: CompletePartialOrder.CompletePartialOrder.

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.

Lemma linearity x y:
  Tower x -> Tower y -> x <<= y \/ y <<= x.