Library ZFwf
Theory about well-founded sets
Definition of well-founded sets. Could be Acc in_set...
Definition isWf x :=
∀ P : set -> Prop,
(∀ a,(∀ b, b ∈ a -> P b)-> P a) -> P x.
Lemma isWf_intro : ∀ x,
(∀ a, a ∈ x -> isWf a) -> isWf x.
Lemma isWf_inv : ∀ a b,
isWf a -> b ∈ a -> isWf b.
Lemma isWf_ext : ∀ x x', x == x' -> isWf x -> isWf x'.
Global Instance isWf_morph : Proper (eq_set ==> iff) isWf.
Qed.
Lemma isWf_acc x : isWf x <-> Acc in_set x.
Lemma isWf_ind :
∀ P : set -> Prop,
(∀ a, isWf a -> (∀ b, b ∈ a -> P b)-> P a) ->
∀ x, isWf x -> P x.
∀ P : set -> Prop,
(∀ a,(∀ b, b ∈ a -> P b)-> P a) -> P x.
Lemma isWf_intro : ∀ x,
(∀ a, a ∈ x -> isWf a) -> isWf x.
Lemma isWf_inv : ∀ a b,
isWf a -> b ∈ a -> isWf b.
Lemma isWf_ext : ∀ x x', x == x' -> isWf x -> isWf x'.
Global Instance isWf_morph : Proper (eq_set ==> iff) isWf.
Qed.
Lemma isWf_acc x : isWf x <-> Acc in_set x.
Lemma isWf_ind :
∀ P : set -> Prop,
(∀ a, isWf a -> (∀ b, b ∈ a -> P b)-> P a) ->
∀ x, isWf x -> P x.
The class of well-founded sets form a model of IZF+foundation axiom
Lemma isWf_zero: isWf empty.
Lemma isWf_pair : ∀ x y,
isWf x -> isWf y -> isWf (pair x y).
Lemma isWf_power : ∀ x, isWf x -> isWf (power x).
Lemma isWf_union : ∀ x, isWf x -> isWf (union x).
Lemma isWf_incl x y : isWf x -> y ⊆ x -> isWf y.
Lemma isWf_subset : ∀ x P, isWf x -> isWf (subset x P).
Require Import ZFrepl.
Lemma isWf_repl : ∀ x R,
repl_rel x R ->
(∀ a b, a ∈ x -> R a b -> isWf b) ->
isWf (repl x R).
Lemma isWf_inter2 : ∀ x y, isWf x -> isWf y -> isWf (x ∩ y).
A well-founded set does not belong to itself.
Definition tr x p :=
x ∈ p /\
(∀ a b, a ∈ b -> b ∈ p -> a ∈ p).
Instance tr_morph : Proper (eq_set ==> eq_set ==> iff) tr.
Qed.
Definition isTransClos x y :=
tr x y /\ (∀ p, tr x p -> y ⊆ p).
Instance isTransClos_morph : Proper (eq_set ==> eq_set ==> iff) isTransClos.
Qed.
Lemma isTransClos_fun x y y' :
isTransClos x y ->
isTransClos x y' -> y == y'.
Lemma isTransClos_intro a f :
morph1 f ->
(∀ b, b ∈ a -> isTransClos b (f b)) ->
isTransClos a (singl a ∪ sup a f).
Alternative definition, only using first-order quantification
Definition isWf' x :=
exists2 c:set, isTransClos x c &
∀ p:set,
(∀ a:set, a ⊆ c -> a ⊆ p -> a ∈ p) -> x ∈ p.
exists2 c:set, isTransClos x c &
∀ p:set,
(∀ a:set, a ⊆ c -> a ⊆ p -> a ∈ p) -> x ∈ p.
The equivalence result
Lemma isWf_equiv x :
isWf x <-> isWf' x.
Lemma isWf_clos_ex x : isWf x -> uchoice_pred (isTransClos x).
Definition trClos x := uchoice (isTransClos x).
Global Instance trClos_morph : morph1 trClos.
Qed.
Lemma trClos_intro1 x : isWf x -> x ∈ trClos x.
Lemma trClos_intro2 x y z : isWf x -> y ∈ trClos x -> z ∈ y -> z ∈ trClos x.
Lemma trClos_ind x (P:set->Prop) :
isWf x ->
(∀ x', x==x' -> P x') ->
(∀ y z, y ∈ trClos x -> P y -> z ∈ y -> P z) ->
∀ y,
y ∈ trClos x ->
P y.
Lemma isWf_trClos x : isWf x -> isWf (trClos x).
Lemma trClos_trans x y z : isWf x -> y ∈ trClos x -> z ∈ trClos y -> z ∈ trClos x.
Hint Resolve isWf_trClos trClos_intro1 trClos_intro2.
Lemma isWf_ind2 x (P : set -> Prop) :
(∀ a, a ∈ trClos x -> (∀ b, b ∈ a -> P b)-> P a) ->
isWf x -> P x.
isWf x <-> isWf' x.
Lemma isWf_clos_ex x : isWf x -> uchoice_pred (isTransClos x).
Definition trClos x := uchoice (isTransClos x).
Global Instance trClos_morph : morph1 trClos.
Qed.
Lemma trClos_intro1 x : isWf x -> x ∈ trClos x.
Lemma trClos_intro2 x y z : isWf x -> y ∈ trClos x -> z ∈ y -> z ∈ trClos x.
Lemma trClos_ind x (P:set->Prop) :
isWf x ->
(∀ x', x==x' -> P x') ->
(∀ y z, y ∈ trClos x -> P y -> z ∈ y -> P z) ->
∀ y,
y ∈ trClos x ->
P y.
Lemma isWf_trClos x : isWf x -> isWf (trClos x).
Lemma trClos_trans x y z : isWf x -> y ∈ trClos x -> z ∈ trClos y -> z ∈ trClos x.
Hint Resolve isWf_trClos trClos_intro1 trClos_intro2.
Lemma isWf_ind2 x (P : set -> Prop) :
(∀ a, a ∈ trClos x -> (∀ b, b ∈ a -> P b)-> P a) ->
isWf x -> P x.
Section TransfiniteRecursion.
Variable F : (set -> set) -> set -> set.
Hypothesis Fm : Proper ((eq_set ==> eq_set) ==> eq_set ==> eq_set) F.
Hypothesis Fext : ∀ x f f', eq_fun x f f' -> F f x == F f' x.
Require Import ZFpairs ZFrelations.
Definition isTR_rel F P :=
∀ o y,
couple o y ∈ P ->
exists2 f, (∀ n, n ∈ o -> couple n (cc_app f n) ∈ P) &
y == F (cc_app f) o.
Lemma isTR_rel_fun P P' o y y':
isWf o ->
isTR_rel F P ->
isTR_rel F P' ->
couple o y ∈ P ->
couple o y' ∈ P' ->
y == y'.
Instance isTR_rel_morph_gen :
Proper (((eq_set ==> eq_set) ==> eq_set ==> eq_set) ==> eq_set ==> iff) isTR_rel.
Qed.
Instance isTR_rel_morph : Proper (eq_set==>iff) (isTR_rel F).
Qed.
Definition TRP_rel F o P :=
isTR_rel F P /\
(exists y, couple o y ∈ P) /\
∀ P' y, isTR_rel F P' -> couple o y ∈ P' -> P ⊆ P'.
Instance TRP_rel_morph_gen :
Proper (((eq_set ==> eq_set) ==> eq_set ==> eq_set) ==> eq_set ==> eq_set ==> iff) TRP_rel.
Qed.
Instance TRP_rel_morph : Proper (eq_set==>eq_set==>iff) (TRP_rel F).
Qed.
Lemma TR_img_ex x P : isWf x ->
TRP_rel F x P ->
uchoice_pred (fun y => couple x y ∈ P).
Lemma TR_rel_ex o :
isWf o -> uchoice_pred (TRP_rel F o).
Definition WFR x := uchoice (fun y => couple x y ∈ uchoice(TRP_rel F x)).
Lemma WFR_eqn x : isWf x -> WFR x == F WFR x.
Lemma WFR_ind : ∀ x (P:set->set->Prop),
Proper (eq_set ==> eq_set ==> iff) P ->
isWf x ->
(∀ y, isWf y ->
(∀ x, x ∈ y -> P x (WFR x)) ->
P y (F WFR y)) ->
P x (WFR x).
Global Instance WFR_morph0 : morph1 WFR.
Qed.
End TransfiniteRecursion.
Global Instance WFR_morph :
Proper (((eq_set ==> eq_set) ==> eq_set ==> eq_set) ==> eq_set ==> eq_set) WFR.
Qed.
End WellFoundedSets.
Hint Resolve isWf_morph.