(* This is a proof script formalising Section 4.3.2 of my bachelor's thesis on foundations of mathematics.
Presented as a website, you can hover the mouse over the definitions and statements to see their effects.
The commands inbetween Proof and Qed manipulate the proof state, which is also visible by hovering over theses commands. *)
(* inductive definition of trees *)
Inductive T : Type :=
sup (A : Set) (f : A -> T) : T.
(* projection functions *)
Definition pi1 s :=
match s with
sup A f => A
end.
Definition pi2 s : (pi1 s) -> T :=
match s with
sup A f => f
end.
(* recursive definition of tree equivalence *)
Fixpoint Aeq s t :=
match s, t with
| sup A f, sup B g => (forall a, exists b, Aeq (f a) (g b)) /\ (forall b, exists a, Aeq (f a) (g b))
end.
(* reflexivity *)
Lemma Aeq_ref s :
Aeq s s.
Proof.
induction s as [A f IH]. simpl. split.
- intros a. exists a. now apply IH.
- intros a. exists a. now apply IH.
Qed.
Lemma Aeq_ref' s t :
s = t -> Aeq s t.
Proof.
intros ->. apply Aeq_ref.
Qed.
(* symmetry *)
Lemma Aeq_sym s t :
Aeq s t -> Aeq t s.
Proof.
revert t. induction s as [A f IH].
intros [B g]. simpl. intros [H1 H2]. split.
- intros b. destruct (H2 b) as [a H3]. exists a. now apply IH.
- intros a. destruct (H1 a) as [b H3]. exists b. now apply IH.
Qed.
(* transitivity *)
Lemma Aeq_tra s t u :
Aeq s t -> Aeq t u -> Aeq s u.
Proof.
revert t u. induction s as [A f IH].
intros [B g] [C h]. simpl. intros [H1 H2] [H3 H4]. split.
- intros a. destruct (H1 a) as [b H5]. destruct (H3 b) as [c H6].
exists c. now apply IH with (t := (g b)).
- intros c. destruct (H4 c) as [b H5]. destruct (H2 b) as [a H6].
exists a. now apply IH with (t := (g b)).
Qed.
Hint Resolve Aeq_ref Aeq_sym Aeq_tra.
(* definition of membership *)
Definition Ain s '(sup A f) :=
exists a, Aeq s (f a).
(* definition of inclusion *)
Definition ASubq s t :=
forall u, Ain u s -> Ain u t.
(* the tree (sup A f) contains (f a) as element for all (a : A) *)
Lemma Ain_Asup A f a :
Ain (f a) (sup A f).
Proof.
simpl. exists a. now apply Aeq_ref.
Qed.
(* reformulations of the above lemma using projections *)
Lemma Ain_pi s t :
Ain s t -> exists a : (pi1 t), Aeq s (pi2 t a).
Proof.
destruct t as [A f]. intros [a H]. now exists a.
Qed.
Lemma pi_Ain (s : T) (a : pi1 s) :
Ain (pi2 s a) s.
Proof.
destruct s as [A f]; simpl in *. now exists a.
Qed.
(* extensionality *)
Lemma Aeq_ext s t :
ASubq s t -> ASubq t s -> Aeq s t.
Proof.
destruct s as [A f], t as [B g].
intros H1 H2. simpl. split.
- intros a. destruct (H1 (f a) (Ain_Asup A f a)) as [b H3]. now exists b.
- intros b. destruct (H2 (g b) (Ain_Asup B g b)) as [a H3]. exists a. now apply Aeq_sym.
Qed.
Lemma Aeq_ASubq s t :
Aeq s t -> ASubq s t.
Proof.
destruct s as [A f], t as [B g]. intros [H _] z [a Z].
destruct (H a) as [b I]. exists b. eauto.
Qed.
(* empty set *)
Definition AEmpty :=
sup False (False_rect T).
Lemma AEmptyAx s :
~ Ain s AEmpty.
Proof.
now intros [t H].
Qed.
(* pairing *)
Definition Aupair X Y :=
sup bool (fun a => if a then X else Y).
Lemma AupairAx s t u :
Ain u (Aupair s t) <-> Aeq u s \/ Aeq u t.
Proof.
split; intros H.
- destruct H as [[] H]; auto.
- destruct H as [H|H]; [now exists true | now exists false].
Qed.
(* union *)
Definition Aunion '(sup A f) :=
sup (sigT (fun (a : A) => (pi1 (f a)))) (fun p => let (a, b) := p in pi2 (f a) b).
Lemma AunionAx s u :
Ain u (Aunion s) <-> exists t, Ain t s /\ Ain u t.
Proof.
split; intros H; destruct s as [A f].
- destruct H as [[a b] H]. exists (f a). split.
+ now exists a.
+ destruct (f a) as [C h]; simpl in *. now exists b.
- destruct H as [[B g][[a Z1][b Z2]]].
apply Aeq_ASubq in Z1.
specialize (Z1 (g b) (Ain_Asup B g b)).
apply Ain_pi in Z1 as [c H].
exists (existT _ a c). eauto.
Qed.
(* natural numbers *)
Definition sigma s :=
Aunion (Aupair s (Aupair s s)).
Fixpoint sigit n :=
match n with
| O => AEmpty
| S n => sigma (sigit n)
end.
Definition Aom :=
sup nat sigit.
(* separation *)
Definition Asep (P : T -> Prop) '(sup A f) :=
sup (sig (fun a => P (f a))) (fun p => let (a, _) := p in f a).
Definition cres (P : T -> Prop) :=
forall s t, Aeq s t -> P s -> P t.
Lemma AsepAx (P : T -> Prop) s t :
cres P -> Ain t (Asep P s) <-> Ain t s /\ P t.
Proof.
intros HP. split; intros H; destruct s as [A f].
- destruct H as [[a PA]H].
split; eauto. now exists a.
- destruct H as [[a H]PY].
assert (PA : P (f a)) by now apply (HP t).
now exists (exist _ a PA).
Qed.
(* replacement *)
Definition Arepl (F : T -> T) '(sup A f) :=
sup A (fun a => F (f a)).
Definition fres (F : T -> T) :=
forall s t, Aeq s t -> Aeq (F s) (F t).
Lemma AreplAx F s u :
fres F -> Ain u (Arepl F s) <-> exists t, Ain t s /\ Aeq u (F t).
Proof.
intros HF. split; intros H; destruct s as [A f].
- destruct H as [a H]. exists (f a).
split; trivial. apply Ain_Asup.
- destruct H as [z[[a H] Z]].
exists a. apply HF in H; try now exists a.
apply (Aeq_tra _ _ _ Z). assumption.
Qed.