(* Following Aczel 78 and Werner 97 we construct an intensional type of sets *)
Inductive Acz : Type :=
Asup : forall A : Type, (A -> Acz) -> Acz.
Arguments Asup _ _ : clear implicits.
Definition pi1 s :=
match s with
Asup A f => A
end.
Definition pi2 s : (pi1 s) -> Acz :=
match s with
Asup A f => f
end.
Arguments pi2 _ : clear implicits.
Fixpoint Aeq s t :=
match s, t with
| Asup A f, Asup B g =>
(forall a, exists b, Aeq (f a) (g b))
/\ (forall b, exists a, Aeq (f a) (g b))
end.
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.
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.
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.
Instance aeq_equiv :
Equivalence Aeq.
Proof.
constructor; eauto.
Qed.
Definition Ain s '(Asup A f) :=
exists a, Aeq s (f a).
Definition ASubq s t :=
forall u, Ain u s -> Ain u t.
Lemma Ain_Asup A f a :
Ain (f a) (Asup A f).
Proof.
simpl. exists a. now apply Aeq_ref.
Qed.
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 : Acz) (a : pi1 s) :
Ain (pi2 s a) s.
Proof.
destruct s as [A f]; simpl in *. now exists a.
Qed.
Lemma Ain_mor s s' t t' :
Aeq s s' -> Aeq t t' -> Ain s t -> Ain s' t'.
Proof.
intros H1 H2 H3.
destruct t as [B1 g1]. simpl in H3. destruct H3 as [b1 H3].
destruct t' as [B2 g2]. simpl. simpl in H2. destruct H2 as [H2 _].
destruct (H2 b1) as [b2 H4]. exists b2.
rewrite <- H4. now rewrite <- H1.
Qed.
Instance Ain_proper :
Proper (Aeq ==> Aeq ==> iff) Ain.
Proof.
intros s s' H1 t t' H2. split; intros H.
- now apply (Ain_mor H1 H2).
- apply Aeq_sym in H1. apply Aeq_sym in H2.
now apply (Ain_mor H1 H2).
Qed.
Instance ASubq_proper :
Proper (Aeq ==> Aeq ==> iff) ASubq.
Proof.
intros s s' H1 t t' H2. split; intros H.
- intros u. rewrite <- H1, <- H2. apply H.
- intros u. rewrite H1, H2. apply H.
Qed.
Definition AEmpty :=
Asup False (fun a => match a with end).
Definition Aupair X Y :=
Asup bool (fun a => if a then X else Y).
Definition Aunion '(Asup A f) :=
Asup (sigT (fun (a : A) => (pi1 (f a)))) (fun p => let (a, b) := p in pi2 (f a) b).
Definition Apower '(Asup A f) :=
Asup (A -> Prop) (fun P => Asup (sig P) (fun p => let (a, _) := p in f a)).
Definition Asep (P : Acz -> Prop) '(Asup A f) :=
Asup (sig (fun a => P (f a))) (fun p => let (a, _) := p in f a).
Definition Arepl (F : Acz -> Acz) '(Asup A f) :=
Asup A (fun a => F (f a)).
Definition AczSS :=
@Build_SetStruct Acz Ain.
Definition AczZS :=
@Build_ZStruct AczSS AEmpty Aupair Aunion Apower Asep.
Instance ACZ' : ZFStruct' :=
@Build_ZFStruct' AczZS Arepl.
(* Equivalent but distinct trees exist *)
Definition sing1 :=
Asup nat (fun n => AEmpty).
Definition sing2 :=
Asup bool (fun b => AEmpty).
Lemma sing_Aeq :
Aeq sing1 sing2.
Proof.
split; intros _.
- exists false. apply Aeq_ref.
- exists O. apply Aeq_ref.
Qed.
Lemma Asup_inj A f B g :
Asup A f = Asup B g -> A = B.
Proof.
intros H. change (match (Asup A f) with (Asup A' f') => A' = B end).
rewrite H. reflexivity.
Qed.
Lemma nat_bool :
nat <> bool.
Proof.
intros H. cut (exists b1 b2 b3 : bool, b1 <> b2 /\ b2 <> b3 /\ b1 <> b3).
- intros [[][[][[][H1[H2 H3]]]]]; congruence.
- rewrite <- H. exists O, 1, 2. repeat split; auto.
Qed.
Lemma sing_neq :
sing1 <> sing2.
Proof.
intros H % Asup_inj. now apply nat_bool.
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 f a)) as [b H3]. now exists b.
- intros b. destruct (H2 (g b) (Ain_Asup g b)) as [a H3]. now exists a.
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.
Lemma Aeq_equiv s t :
s == t <-> Aeq s t.
Proof.
split; intros H.
- apply Aeq_ext; apply H.
- split; now apply Aeq_ASubq.
Qed.
(* Foundation *)
Lemma AWF_Aeq s t :
Aeq s t -> WF s -> WF t.
Proof.
revert t. induction s as [A f IH].
intros [B g] H1 H2. constructor.
intros u [b H3]. destruct H1 as [_ H1].
destruct (H1 b) as [a H4]. apply (IH a).
- now rewrite H4.
- apply H2. apply Ain_Asup.
Qed.
Lemma Ain_AWF s :
WF s.
Proof.
induction s as [A f IH].
constructor. intros t [a H].
symmetry in H. apply (AWF_Aeq H), IH.
Qed.
(* Empty *)
Lemma AEmptyAx s :
~ Ain s AEmpty.
Proof.
now intros [t H].
Qed.
(* Unordered Pairs *)
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.
Lemma Aupair_mor s s' t t' u :
Aeq s s' -> Aeq t t' -> Ain u (Aupair s t) -> Ain u (Aupair s' t').
Proof.
intros H1 H2 H. apply AupairAx.
rewrite <- H1, <- H2. now apply AupairAx in H.
Qed.
Instance Aupair_proper :
Proper (Aeq ==> Aeq ==> Aeq) Aupair.
Proof.
intros s s' H1 t t' H2. apply Aeq_ext; intros z H.
- now apply (Aupair_mor H1 H2).
- symmetry in H1, H2. now apply (Aupair_mor H1 H2).
Qed.
(* Union *)
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 g b)).
apply Ain_pi in Z1 as [c H].
exists (existT _ a c). eauto.
Qed.
Lemma Aunion_mor s s' u :
Aeq s s' -> Ain u (Aunion s) -> Ain u (Aunion s').
Proof.
intros H1 H2. apply AunionAx in H2 as [t H2].
rewrite H1 in H2. apply AunionAx. now exists t.
Qed.
Instance Aunion_proper :
Proper (Aeq ==> Aeq) Aunion.
Proof.
intros s s' H1. apply Aeq_ext; intros z H.
- now apply (Aunion_mor H1).
- symmetry in H1. now apply (Aunion_mor H1).
Qed.
(* Power *)
Lemma ApowerAx s t :
Ain t (Apower s) <-> ASubq t s.
Proof.
split; intros H; destruct s as [A f].
- destruct H as [P H].
intros u Z. apply Aeq_ASubq in H.
destruct (H u Z) as [[a PA] I]. now exists a.
- exists (fun a => Ain (f a) t). apply Aeq_ext; intros z Z.
+ destruct t as [B g], Z as [b H1].
destruct (H (g b) (Ain_Asup g b)) as [a J].
assert (H2: Ain (f a) (Asup B g)) by (exists b; auto).
exists (exist _ a H2). eauto.
+ destruct Z as [[a YA] H1 % Aeq_sym].
now apply (Ain_mor H1 (t:=t)).
Qed.
Lemma Apower_mor s s' t :
Aeq s s' -> Ain t (Apower s) -> Ain t (Apower s').
Proof.
intros H1 H2. apply ApowerAx.
rewrite <- H1. now apply ApowerAx.
Qed.
Instance Apower_proper :
Proper (Aeq ==> Aeq) Apower.
Proof.
intros s s' H1. apply Aeq_ext; intros z H.
- now apply (Apower_mor H1).
- symmetry in H1. now apply (Apower_mor H1).
Qed.
(* Separation *)
Lemma AsepAx (P : Acz -> Prop) s t :
cres Aeq 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.
Lemma Asep_mor (P P' : Acz -> Prop) s s' t :
cres Aeq P -> cres Aeq P' -> (forall s, P s <-> P' s)
-> Aeq s s' -> Ain t (Asep P s) -> Ain t (Asep P' s').
Proof.
intros H1 H2 H3 H4 H5. apply AsepAx; trivial.
rewrite <- H3, <- H4. apply AsepAx; trivial.
Qed.
Lemma Asep_proper' (P P' : Acz -> Prop) s s' :
cres Aeq P -> cres Aeq P' -> (forall s, P s <-> P' s)
-> Aeq s s' -> Aeq (Asep P s) (Asep P' s').
Proof.
intros H1 H2 H3 H4. apply Aeq_ext; intros z Z.
- apply (Asep_mor H1 H2 H3 H4); assumption.
- apply (@Asep_mor P' P s' s); firstorder.
Qed.
Lemma Asep_proper (P : Acz -> Prop) s s' :
cres Aeq P -> Aeq s s' -> Aeq (Asep P s) (Asep P s').
Proof.
intros H1 H2. apply (@Asep_proper' P P); firstorder.
Qed.
(* Functional Replacement *)
Lemma AreplAx F s u :
fres Aeq 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.
now rewrite Z, H.
Qed.
Lemma Arepl_mor (F F' : Acz -> Acz) s s' u :
fres Aeq F -> fres Aeq F' -> (forall s, Aeq (F s) (F' s))
-> Aeq s s' -> Ain u (Arepl F s) -> Ain u (Arepl F' s').
Proof.
intros H1 H2 H3 H4 H5. apply AreplAx; trivial.
apply AreplAx in H5 as [y H]; trivial.
exists y. now rewrite <- H3, <- H4.
Qed.
Lemma Arepl_proper' (F F' : Acz -> Acz) s s' :
fres Aeq F -> fres Aeq F' -> (forall s, Aeq (F s) (F' s))
-> Aeq s s' -> Aeq (Arepl F s) (Arepl F' s').
Proof.
intros H1 H2 H3 H4. apply Aeq_ext; intros z Z.
- apply (Arepl_mor H1 H2 H3 H4); assumption.
- apply (@Arepl_mor F' F s' s); auto.
Qed.
Lemma Arepl_proper (F : Acz -> Acz) s s' :
fres Aeq F -> Aeq s s' -> Aeq (Arepl F s) (Arepl F s').
Proof.
intros H1 H2. now apply Arepl_proper'.
Qed.
(* The main result is that the tree model satisfies intensional ZF' with infinity *)
Lemma fres_equiv F :
fres equiv F -> fres Aeq F.
Proof.
intros H s s'. rewrite <- !Aeq_equiv. apply H.
Qed.
Lemma cres_equiv P :
cres equiv P -> cres Aeq P.
Proof.
intros H s s'. rewrite <- Aeq_equiv. apply H.
Qed.
Lemma Acz_ZS :
@iZS ACZ'.
Proof.
split.
- now intros s s' t -> % Aeq_equiv.
- apply AEmptyAx.
- intros s t u. repeat rewrite Aeq_equiv. apply AupairAx.
- apply AunionAx.
- apply ApowerAx.
- intros P s t PR % cres_equiv. now apply AsepAx.
Qed.
Instance Acz_ZF' :
@iZF' ACZ'.
Proof.
split.
- split; [apply Acz_ZS | apply Ain_AWF].
- intros F x z FR. rewrite AreplAx.
+ split; intros [t[T1 T2]]; exists t.
* now rewrite Aeq_equiv.
* now rewrite <- Aeq_equiv.
+ now apply fres_equiv.
Qed.
Definition Aom :=
Asup nat (fun n => powit n).
Lemma Aom_spec :
agree finpow Aom.
Proof.
intros s. split; intros H.
- destruct H as [n H % Aeq_equiv]. now exists n.
- destruct H as [n H]. exists n. now apply Aeq_equiv.
Qed.
Fact Acz_Inf :
Inf ACZ'.
Proof.
exists Aom. apply Aom_spec.
Qed.