Require Export Classical.
Require Export Epsilon.
Require Export FunctionalExtensionality.
Require Export ProofIrrelevance.
Axiom prop_extensionality : (∀ P Q:Prop, (P ↔ Q) → P = Q).
Require Export ZFMType.
Module ZFAcz : ZF.
Inductive Acz : Type :=
Asup : ∀ A:Type, (A → Acz) → Acz.
(*** Following Werner 97 ***)
Fixpoint Aeq (X Y:Acz) : Prop :=
match X,Y with
| Asup A f,Asup B g ⇒
(∀ a, ∃ b, Aeq (f a) (g b))
∧ (∀ b, ∃ a, Aeq (f a) (g b))
end.
Lemma Aeq_ref (X:Acz) : Aeq X X.
Lemma Aeq_sym (X Y:Acz) : Aeq X Y → Aeq Y X.
Lemma Aeq_tra (X Y Z:Acz) : Aeq X Y → Aeq Y Z → Aeq X Z.
Definition Ain (X Y:Acz) : Prop :=
match Y with
| Asup B g ⇒ ∃ b, Aeq X (g b)
end.
Lemma Ain_Asup A f (a:A) : Ain (f a) (Asup A f).
Lemma Ain_mor (X1 X2 Y1 Y2:Acz) : Aeq X1 X2 → Aeq Y1 Y2 → Ain X1 Y1 → Ain X2 Y2.
Definition ASubq (X Y:Acz) : Prop :=
∀ z, Ain z X → Ain z Y.
Lemma Aeq_ext (X Y:Acz) : ASubq X Y → ASubq Y X → Aeq X Y.
Lemma Ain_ind : ∀ (P:Acz → Prop), (∀ X Y, Aeq X Y → P Y → P X) → (∀ X, (∀ x, Ain x X → P x) → P X) → ∀ X, P X.
Definition AEmpty : Acz := Asup False (fun a ⇒ match a with end).
Definition AEps : (Acz → Prop) → Acz := epsilon (inhabits AEmpty).
Lemma AEpsR (P:Acz → Prop) : (∃ x:Acz, P x) → P (AEps P).
Lemma AEps_ext (P Q:Acz → Prop) : (∀ x, P x ↔ Q x) → AEps P = AEps Q.
Definition N (X:Acz) : Acz := AEps (Aeq X).
Lemma Aeq_N (X:Acz) : Aeq X (N X).
Lemma N_idem (X:Acz) : N (N X) = N X.
Lemma Aeq_N_eq (X Y:Acz) : Aeq X Y → N X = N Y.
Lemma N_eq_Aeq (X Y:Acz) : N X = N Y → Aeq X Y.
Definition set : Type := sig (fun X ⇒ N X = X).
Definition NS (X:Acz) : set := exist (fun X ⇒ N X = X) (N X) (N_idem X).
Lemma Aeq_p1_NS (X:Acz) : Aeq X (proj1_sig (NS X)).
Definition IN : set → set → Prop := fun X Y ⇒ Ain (proj1_sig X) (proj1_sig Y).
Lemma Ain_IN_p1 (X Y:set) : Ain (proj1_sig X) (proj1_sig Y) → IN X Y.
Lemma Ain_IN_NS (X Y:Acz) : Ain X Y → IN (NS X) (NS Y).
Lemma Ain_IN_p1_NS X Y : Ain (proj1_sig X) Y → IN X (NS Y).
Lemma Ain_IN_NS_p1 X Y : Ain X (proj1_sig Y) → IN (NS X) Y.
Lemma IN_Ain_p1 (X Y:set) : IN X Y → Ain (proj1_sig X) (proj1_sig Y).
Lemma IN_Ain_NS (X Y:Acz) : IN (NS X) (NS Y) → Ain X Y.
Lemma IN_Ain_p1_NS X Y : IN X (NS Y) → Ain (proj1_sig X) Y.
Lemma IN_Ain_NS_p1 X Y : IN (NS X) Y → Ain X (proj1_sig Y).
Definition nIN (x y:set) : Prop := ¬IN x y.
Infix "∈" := IN (at level 70).
Infix "∉" := nIN (at level 70).
Definition Subq (X Y:set) : Prop := ∀ z, z ∈ X → z ∈ Y.
Infix "⊆" := Subq (at level 70).
(*** subset_eq_compat from ProofIrrelevanceFacts doesn't work here because Acz is a Type, not a Set. I copied the proof from there changing Set to Type. ***)
Lemma subset_eq_compat_Type :
∀ (U:Type) (P:U→Prop) (x y:U) (p:P x) (q:P y),
x = y → exist P x p = exist P y q.
Lemma NS_p1_eq X : NS (proj1_sig X) = X.
Lemma Aeq_p1_NS_eq (X:set) (Y:Acz) : Aeq (proj1_sig X) Y → X = NS Y.
Lemma Aeq_p1_eq : ∀ X Y:set, Aeq (proj1_sig X) (proj1_sig Y) → X = Y.
(***
intros X H1 Y H2 H3. simpl in H3. apply subset_eq_compat_Type.
rewrite <- H1. rewrite <- H2. now apply Aeq_N_eq.
Qed.
***)
(*** Extensionality ***)
Lemma set_ext : ∀ X Y, X ⊆ Y → Y ⊆ X → X = Y.
(*** Epsilon Induction (Foundation) ***)
Lemma eps_ind : ∀ (P:set → Prop), (∀ X, (∀ x, x ∈ X → P x) → P X) → ∀ X, P X.
(*** Empty ***)
Definition empty : set := NS AEmpty.
Notation "∅" := empty.
Lemma emptyE : ∀ (x:set), x ∉ ∅.
(*** Unordered Pairs ***)
Definition upair (x y : set) : set := NS (Asup bool (fun a ⇒ if a then proj1_sig x else proj1_sig y)).
Notation "{ x , y }" := (upair x y).
Lemma upairAx : ∀ (x y z:set), z ∈ {x,y} ↔ z = x ∨ z = y.
(*** Unions -- a little tricky to get one of the matches to type check ***)
Definition union (x:set) :=
NS (match (proj1_sig x) with
| Asup A f ⇒
Asup (sigT (fun a:A ⇒ match (f a) with Asup B g ⇒ B end))
(fun ab ⇒ match ab with existT a b ⇒ match (f a) as z return (match z with Asup B g ⇒ B end) → Acz with Asup B g ⇒ g end b end) end).
Notation "⋃" := union (at level 40).
Axiom unionAx : ∀ (x z:set), z ∈ ⋃ x ↔ ∃ y, y ∈ x ∧ z ∈ y.
(*** Replacement (for functions) ***)
Definition repl (X:set) (f:set → set) : set :=
NS (match (proj1_sig X) with Asup B g ⇒ Asup B (fun b ⇒ proj1_sig (f (NS (g b)))) end).
Notation "{ f | x ⋳ X }" := (repl X (fun x:set ⇒ f)).
Lemma replAx : ∀ X f z, z ∈ {f x|x ⋳ X} ↔ ∃ x, x ∈ X ∧ z = f x.
(*** Separation ***)
Definition sep (X:set) (P:set → Prop) : set :=
NS (match (proj1_sig X) with Asup A f ⇒ Asup (sig (fun x:A ⇒ P (NS (f x)))) (fun xp ⇒ match xp with exist x p ⇒ f x end) end).
Notation "{ x ⋳ X | P }" := (sep X (fun x:set ⇒ P)).
Lemma sepAx : ∀ X P z, z ∈ {x ⋳ X|P x} ↔ z ∈ X ∧ P z.
(*** Power Sets -- definition of Werner 97, using sep and impredicativity ***)
(*** Coq gives a universe inconsistency for this definition following Werner 97, although impredicativity should mean it's allowed. ***)
(***
Definition power (X:set) : set :=
NS (Asup (set -> Prop) (fun P => proj1_sig (sep X P))).
***)
Definition power (X:set) : set :=
NS (match proj1_sig X with Asup A f ⇒ Asup (A → Prop) (fun P ⇒ Asup (sig P) (fun xp ⇒ match xp with exist x p ⇒ f x end)) end).
Notation "℘" := power.
Lemma powerAx : ∀ (X:set), ∀ Y:set, Y ⊆ X ↔ Y ∈ ℘ X.
(*** singleton definition ***)
Definition sing : set → set := fun x ⇒ {x,x}.
(*** binunion definition ***)
Definition binunion (X Y:set) := ⋃ {X,Y}.
(*** infinity ***)
Fixpoint finord (n:nat) : set :=
match n with
| O ⇒ empty
| S n' ⇒ binunion (finord n') (sing (finord n'))
end.
Definition omega : set := NS (Asup nat (fun n ⇒ proj1_sig (finord n))).
Lemma infinity : ∃ X:set, ∅ ∈ X ∧ (∀ x, x ∈ X → binunion x (sing x) ∈ X).
End ZFAcz.
Require Export Epsilon.
Require Export FunctionalExtensionality.
Require Export ProofIrrelevance.
Axiom prop_extensionality : (∀ P Q:Prop, (P ↔ Q) → P = Q).
Require Export ZFMType.
Module ZFAcz : ZF.
Inductive Acz : Type :=
Asup : ∀ A:Type, (A → Acz) → Acz.
(*** Following Werner 97 ***)
Fixpoint Aeq (X Y:Acz) : Prop :=
match X,Y with
| Asup A f,Asup B g ⇒
(∀ a, ∃ b, Aeq (f a) (g b))
∧ (∀ b, ∃ a, Aeq (f a) (g b))
end.
Lemma Aeq_ref (X:Acz) : Aeq X X.
Lemma Aeq_sym (X Y:Acz) : Aeq X Y → Aeq Y X.
Lemma Aeq_tra (X Y Z:Acz) : Aeq X Y → Aeq Y Z → Aeq X Z.
Definition Ain (X Y:Acz) : Prop :=
match Y with
| Asup B g ⇒ ∃ b, Aeq X (g b)
end.
Lemma Ain_Asup A f (a:A) : Ain (f a) (Asup A f).
Lemma Ain_mor (X1 X2 Y1 Y2:Acz) : Aeq X1 X2 → Aeq Y1 Y2 → Ain X1 Y1 → Ain X2 Y2.
Definition ASubq (X Y:Acz) : Prop :=
∀ z, Ain z X → Ain z Y.
Lemma Aeq_ext (X Y:Acz) : ASubq X Y → ASubq Y X → Aeq X Y.
Lemma Ain_ind : ∀ (P:Acz → Prop), (∀ X Y, Aeq X Y → P Y → P X) → (∀ X, (∀ x, Ain x X → P x) → P X) → ∀ X, P X.
Definition AEmpty : Acz := Asup False (fun a ⇒ match a with end).
Definition AEps : (Acz → Prop) → Acz := epsilon (inhabits AEmpty).
Lemma AEpsR (P:Acz → Prop) : (∃ x:Acz, P x) → P (AEps P).
Lemma AEps_ext (P Q:Acz → Prop) : (∀ x, P x ↔ Q x) → AEps P = AEps Q.
Definition N (X:Acz) : Acz := AEps (Aeq X).
Lemma Aeq_N (X:Acz) : Aeq X (N X).
Lemma N_idem (X:Acz) : N (N X) = N X.
Lemma Aeq_N_eq (X Y:Acz) : Aeq X Y → N X = N Y.
Lemma N_eq_Aeq (X Y:Acz) : N X = N Y → Aeq X Y.
Definition set : Type := sig (fun X ⇒ N X = X).
Definition NS (X:Acz) : set := exist (fun X ⇒ N X = X) (N X) (N_idem X).
Lemma Aeq_p1_NS (X:Acz) : Aeq X (proj1_sig (NS X)).
Definition IN : set → set → Prop := fun X Y ⇒ Ain (proj1_sig X) (proj1_sig Y).
Lemma Ain_IN_p1 (X Y:set) : Ain (proj1_sig X) (proj1_sig Y) → IN X Y.
Lemma Ain_IN_NS (X Y:Acz) : Ain X Y → IN (NS X) (NS Y).
Lemma Ain_IN_p1_NS X Y : Ain (proj1_sig X) Y → IN X (NS Y).
Lemma Ain_IN_NS_p1 X Y : Ain X (proj1_sig Y) → IN (NS X) Y.
Lemma IN_Ain_p1 (X Y:set) : IN X Y → Ain (proj1_sig X) (proj1_sig Y).
Lemma IN_Ain_NS (X Y:Acz) : IN (NS X) (NS Y) → Ain X Y.
Lemma IN_Ain_p1_NS X Y : IN X (NS Y) → Ain (proj1_sig X) Y.
Lemma IN_Ain_NS_p1 X Y : IN (NS X) Y → Ain X (proj1_sig Y).
Definition nIN (x y:set) : Prop := ¬IN x y.
Infix "∈" := IN (at level 70).
Infix "∉" := nIN (at level 70).
Definition Subq (X Y:set) : Prop := ∀ z, z ∈ X → z ∈ Y.
Infix "⊆" := Subq (at level 70).
(*** subset_eq_compat from ProofIrrelevanceFacts doesn't work here because Acz is a Type, not a Set. I copied the proof from there changing Set to Type. ***)
Lemma subset_eq_compat_Type :
∀ (U:Type) (P:U→Prop) (x y:U) (p:P x) (q:P y),
x = y → exist P x p = exist P y q.
Lemma NS_p1_eq X : NS (proj1_sig X) = X.
Lemma Aeq_p1_NS_eq (X:set) (Y:Acz) : Aeq (proj1_sig X) Y → X = NS Y.
Lemma Aeq_p1_eq : ∀ X Y:set, Aeq (proj1_sig X) (proj1_sig Y) → X = Y.
(***
intros X H1 Y H2 H3. simpl in H3. apply subset_eq_compat_Type.
rewrite <- H1. rewrite <- H2. now apply Aeq_N_eq.
Qed.
***)
(*** Extensionality ***)
Lemma set_ext : ∀ X Y, X ⊆ Y → Y ⊆ X → X = Y.
(*** Epsilon Induction (Foundation) ***)
Lemma eps_ind : ∀ (P:set → Prop), (∀ X, (∀ x, x ∈ X → P x) → P X) → ∀ X, P X.
(*** Empty ***)
Definition empty : set := NS AEmpty.
Notation "∅" := empty.
Lemma emptyE : ∀ (x:set), x ∉ ∅.
(*** Unordered Pairs ***)
Definition upair (x y : set) : set := NS (Asup bool (fun a ⇒ if a then proj1_sig x else proj1_sig y)).
Notation "{ x , y }" := (upair x y).
Lemma upairAx : ∀ (x y z:set), z ∈ {x,y} ↔ z = x ∨ z = y.
(*** Unions -- a little tricky to get one of the matches to type check ***)
Definition union (x:set) :=
NS (match (proj1_sig x) with
| Asup A f ⇒
Asup (sigT (fun a:A ⇒ match (f a) with Asup B g ⇒ B end))
(fun ab ⇒ match ab with existT a b ⇒ match (f a) as z return (match z with Asup B g ⇒ B end) → Acz with Asup B g ⇒ g end b end) end).
Notation "⋃" := union (at level 40).
Axiom unionAx : ∀ (x z:set), z ∈ ⋃ x ↔ ∃ y, y ∈ x ∧ z ∈ y.
(*** Replacement (for functions) ***)
Definition repl (X:set) (f:set → set) : set :=
NS (match (proj1_sig X) with Asup B g ⇒ Asup B (fun b ⇒ proj1_sig (f (NS (g b)))) end).
Notation "{ f | x ⋳ X }" := (repl X (fun x:set ⇒ f)).
Lemma replAx : ∀ X f z, z ∈ {f x|x ⋳ X} ↔ ∃ x, x ∈ X ∧ z = f x.
(*** Separation ***)
Definition sep (X:set) (P:set → Prop) : set :=
NS (match (proj1_sig X) with Asup A f ⇒ Asup (sig (fun x:A ⇒ P (NS (f x)))) (fun xp ⇒ match xp with exist x p ⇒ f x end) end).
Notation "{ x ⋳ X | P }" := (sep X (fun x:set ⇒ P)).
Lemma sepAx : ∀ X P z, z ∈ {x ⋳ X|P x} ↔ z ∈ X ∧ P z.
(*** Power Sets -- definition of Werner 97, using sep and impredicativity ***)
(*** Coq gives a universe inconsistency for this definition following Werner 97, although impredicativity should mean it's allowed. ***)
(***
Definition power (X:set) : set :=
NS (Asup (set -> Prop) (fun P => proj1_sig (sep X P))).
***)
Definition power (X:set) : set :=
NS (match proj1_sig X with Asup A f ⇒ Asup (A → Prop) (fun P ⇒ Asup (sig P) (fun xp ⇒ match xp with exist x p ⇒ f x end)) end).
Notation "℘" := power.
Lemma powerAx : ∀ (X:set), ∀ Y:set, Y ⊆ X ↔ Y ∈ ℘ X.
(*** singleton definition ***)
Definition sing : set → set := fun x ⇒ {x,x}.
(*** binunion definition ***)
Definition binunion (X Y:set) := ⋃ {X,Y}.
(*** infinity ***)
Fixpoint finord (n:nat) : set :=
match n with
| O ⇒ empty
| S n' ⇒ binunion (finord n') (sing (finord n'))
end.
Definition omega : set := NS (Asup nat (fun n ⇒ proj1_sig (finord n))).
Lemma infinity : ∃ X:set, ∅ ∈ X ∧ (∀ x, x ∈ X → binunion x (sing x) ∈ X).
End ZFAcz.