Library ZFwf

Require Export basic.
Require Import ZF.

Theory about well-founded sets

Section WellFoundedSets.

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.
red; intros.
apply H0; intros.
red in H.
apply H; trivial.
Qed.

Lemma isWf_inv : ∀ a b,
  isWf a -> b ∈ a -> isWf b.
intros a b H; revert b.
red in H; apply H; intros.
apply isWf_intro; eauto.
Qed.

Lemma isWf_ext : ∀ x x', x == x' -> isWf x -> isWf x'.
intros.
apply isWf_intro; intros.
rewrite <- H in H1.
apply isWf_inv with x; trivial.
Qed.

Global Instance isWf_morph : Proper (eq_set ==> iff) isWf.
apply morph_impl_iff1; auto with *.
do 4 red; intros.
apply isWf_ext with x; auto.
Qed.

Lemma isWf_acc x : isWf x <-> Acc in_set x.
split; intros.
 apply H; intros; constructor; auto.

 elim H; intros; apply isWf_intro; auto.
Qed.

Lemma isWf_ind :
  ∀ P : set -> Prop,
  (∀ a, isWf a -> (∀ b, b ∈ a -> P b)-> P a) ->
  ∀ x, isWf x -> P x.
intros.
cut (isWf x /\ P x).
 destruct 1; trivial.
apply H0; intros.
assert (isWf a).
 apply isWf_intro; intros; apply H1; trivial.
split; trivial.
apply H; intros; trivial.
apply H1; trivial.
Qed.

The class of well-founded sets form a model of IZF+foundation axiom

Lemma isWf_zero: isWf empty.
apply isWf_intro; intros.
apply empty_ax in H; contradiction.
Qed.

Lemma isWf_pair : ∀ x y,
  isWf x -> isWf y -> isWf (pair x y).
intros.
apply isWf_intro; intros.
elim pair_elim with (1:=H1); intros.
 rewrite H2; trivial.
 rewrite H2; trivial.
Qed.

Lemma isWf_power : ∀ x, isWf x -> isWf (power x).
intros.
apply isWf_intro; intros.
apply isWf_intro; intros.
apply isWf_inv with x; trivial.
apply power_elim with a; trivial.
Qed.

Lemma isWf_union : ∀ x, isWf x -> isWf (union x).
intros.
apply isWf_intro; intros.
elim union_elim with (1:=H0); intros.
apply isWf_inv with x0; trivial.
apply isWf_inv with x; trivial.
Qed.

Lemma isWf_incl x y : isWf x -> y ⊆ x -> isWf y.
intros.
apply isWf_intro; intros.
apply isWf_inv with x; auto.
Qed.

Lemma isWf_subset : ∀ x P, isWf x -> isWf (subset x P).
intros.
apply isWf_incl with x; trivial.
red; intros.
apply subset_elim1 in H0; trivial.
Qed.

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).
intros.
apply isWf_intro; intros.
elim repl_elim with (1:=H) (2:=H1); intros; eauto.
Qed.

Lemma isWf_inter2 : ∀ x y, isWf x -> isWf y -> isWf (x ∩ y).
unfold inter2; intros.
unfold inter.
apply isWf_subset.
apply isWf_union.
apply isWf_pair; trivial.
Qed.

A well-founded set does not belong to itself.
Lemma isWf_antirefl : ∀ x, isWf x -> ~ x ∈ x.
intros.
elim H using isWf_ind; clear x H; intros.
red; intros.
apply H0 with a; trivial.
Qed.

Defining well-founded sets without resorting to higher-order

Transitive closure

Definition tr x p :=
  x ∈ p /\
  (∀ a b, a ∈ b -> b ∈ p -> a ∈ p).

Instance tr_morph : Proper (eq_set ==> eq_set ==> iff) tr.
unfold tr.
apply morph_impl_iff2; auto with *.
do 4 red; intros.
destruct H1; split; intros.
 rewrite <- H; rewrite <- H0; trivial.

 rewrite <- H0 in H4|-*; eauto.
Qed.

Definition isTransClos x y :=
  tr x y /\ (∀ p, tr x p -> y ⊆ p).

Instance isTransClos_morph : Proper (eq_set ==> eq_set ==> iff) isTransClos.
apply morph_impl_iff2; auto with *.
do 5 red; intros.
destruct H1.
split; intros.
 rewrite <- H; rewrite <- H0; trivial.
 rewrite <- H in H3; rewrite <- H0; auto.
Qed.

Lemma isTransClos_fun x y y' :
  isTransClos x y ->
  isTransClos x y' -> y == y'.
unfold isTransClos; intros.
destruct H; destruct H0.
apply incl_eq; auto.
Qed.

Lemma isTransClos_intro a f :
  morph1 f ->
  (∀ b, b ∈ a -> isTransClos b (f b)) ->
  isTransClos a (singl a ∪ sup a f).
split; intros.
 split; intros.
  apply union2_intro1.
  apply singl_intro.

  apply union2_intro2.
  rewrite sup_ax; auto with *.
  apply union2_elim in H2; destruct H2.
   apply singl_elim in H2.
   rewrite H2 in H1.
   exists a0; trivial.
   apply H0; trivial.

   rewrite sup_ax in H2; auto with *.
   destruct H2.
   exists x; trivial.
   destruct H0 with (1:=H2).
   destruct H4; eauto.

 red; intros.
 destruct H1.
 apply union2_elim in H2; destruct H2.
  apply singl_elim in H2.
  rewrite H2; trivial.

  rewrite sup_ax in H2; auto with *.
  destruct H2.
  destruct H0 with (1:=H2).
  apply H6; auto.
  split; eauto.
Qed.

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.

The equivalence result
Lemma isWf_equiv x :
  isWf x <-> isWf' x.
split; intros.
 apply H; intros.
 assert (Hm : ext_fun a (fun b => uchoice (isTransClos b))).
  do 2 red; intros.
  apply uchoice_morph_raw; red; intros.
  apply isTransClos_morph; trivial.
 assert (Hch : ∀ b, b ∈ a -> uchoice_pred (isTransClos b)).
  split; [|split; intros]; auto.
   intros.
   rewrite <- H2; trivial.

   destruct H0 with (1:=H1).
   exists x0; trivial.

   apply isTransClos_fun with b; trivial.
 exists (singl a ∪ sup a (fun b => uchoice (isTransClos b))).
  apply isTransClos_intro.
   do 2 red; intros.
   apply uchoice_morph_raw; red; intros.
   apply isTransClos_morph; trivial.

   intros.
   apply uchoice_def; auto.

  intros.
  apply H1; intros; trivial.
   red; intros; apply union2_intro2.
   rewrite sup_ax; trivial.
   exists z; trivial.
   assert (isTransClos z (uchoice (isTransClos z))).
    apply uchoice_def; auto.
   destruct H3.
   destruct H3; trivial.

   red; intros.
   destruct H0 with (1:=H2).
   apply H4; intros.
   apply H1; trivial.
   red; intros; apply union2_intro2.
   rewrite sup_ax; trivial.
   exists z; trivial.
   rewrite <- uchoice_ext with (x:=x0); auto.

 red; intros.
 destruct H as (c,?,?).
 destruct H.
 cut (x ∈ subset (power c) (fun x' => ∀ x'', x' == x'' -> P x'')).
  rewrite subset_ax; destruct 1 as (?,(x',?,?)).
  auto with *.
 apply H1; intros.
 apply subset_intro; intros.
  apply power_intro; auto.

  apply H0; intros.
  rewrite <- H5 in H6; clear x'' H5.
  generalize (H4 _ H6); rewrite subset_ax; intros (_,(b',?,?)); auto with *.
Qed.

Lemma isWf_clos_ex x : isWf x -> uchoice_pred (isTransClos x).
split;[|split]; intros.
 rewrite <- H0; trivial.

 rewrite isWf_equiv in H; destruct H; eauto.

 apply isTransClos_fun with x; trivial.
Qed.

Definition trClos x := uchoice (isTransClos x).

Global Instance trClos_morph : morph1 trClos.
do 2 red; intros; unfold trClos.
apply uchoice_morph_raw; red; intros.
apply isTransClos_morph; trivial.
Qed.

Lemma trClos_intro1 x : isWf x -> x ∈ trClos x.
intro.
specialize isWf_clos_ex with (1:=H); intro.
apply uchoice_def in H0.
destruct H0 as ((?,_),_); trivial.
Qed.

Lemma trClos_intro2 x y z : isWf x -> y ∈ trClos x -> z ∈ y -> z ∈ trClos x.
intros.
specialize isWf_clos_ex with (1:=H); intro.
apply uchoice_def in H2.
destruct H2 as ((_,?),_); eauto.
Qed.

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.
intros.
specialize isWf_clos_ex with (1:=H); intro.
apply uchoice_def in H3.
destruct H3 as (?,?).
assert (y ∈ subset (trClos x) (fun z => ∀ z', z==z' -> P z')).
 apply H4; trivial.
 split; intros.
  apply subset_intro; trivial.
  apply trClos_intro1; trivial.

  rewrite subset_ax in H6; destruct H6.
  destruct H7.
  rewrite H7 in H5,H6.
  apply subset_intro.
   apply trClos_intro2 with x0; auto.

   intros; apply H1 with x0; auto with *.
   rewrite <- H9; trivial.
rewrite subset_ax in H5; destruct H5.
destruct H6.
eauto with *.
Qed.

Lemma isWf_trClos x : isWf x -> isWf (trClos x).
intros.
apply isWf_intro; intros.
elim H0 using trClos_ind; intros; trivial.
 rewrite <- H1; trivial.

 apply isWf_inv with y; trivial.
Qed.

Lemma trClos_trans x y z : isWf x -> y ∈ trClos x -> z ∈ trClos y -> z ∈ trClos x.
intros.
revert z H1; elim H0 using trClos_ind; intros; trivial.
 rewrite H1; trivial.

 apply H2.
 assert (isWf y0).
  apply isWf_inv with (trClos x); auto.
  apply isWf_trClos; trivial.
 elim H4 using trClos_ind; intros; trivial.
  apply isWf_inv with y0; trivial.

  rewrite <- H6; apply trClos_intro2 with y0; trivial.
  apply trClos_intro1; trivial.

  apply trClos_intro2 with y1; trivial.
Qed.

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.
intros.
generalize (trClos_intro1 _ H0).
pattern x at 1 3; elim H0 using isWf_ind; intros; eauto.
Qed.

Transfinite iteration on a well-founded set (not using higher-order)

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'.
intros wfo istr istr' inP inP'; revert y y' inP inP'; elim wfo using isWf_ind; intros.
destruct istr with (1:=inP) as (f,?,?).
destruct istr' with (1:=inP') as (f',?,?).
rewrite H2; rewrite H4; apply Fext; auto.
red; intros.
rewrite <- H6; clear x' H6.
apply H0 with x; auto.
Qed.

  Instance isTR_rel_morph_gen :
    Proper (((eq_set ==> eq_set) ==> eq_set ==> eq_set) ==> eq_set ==> iff) isTR_rel.
do 3 red; intros.
unfold isTR_rel.
apply fa_morph; intro o.
apply fa_morph; intro y'.
rewrite H0.
apply fa_morph; intros ?.
apply ex2_morph; red; intros; auto with *.
 apply fa_morph; intros n.
 rewrite H0; reflexivity.

 split; intros h;rewrite h;[|symmetry]; (apply H; [apply cc_app_morph|];auto with *).
Qed.

  Instance isTR_rel_morph : Proper (eq_set==>iff) (isTR_rel F).
do 2 red; intros.
apply fa_morph; intro o.
apply fa_morph; intro y'.
rewrite H.
apply fa_morph; intros ?.
apply ex2_morph; red; intros; auto with *.
apply fa_morph; intros n.
rewrite H; reflexivity.
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.
do 4 red; intros.
unfold TRP_rel.
apply and_iff_morphism.
 apply isTR_rel_morph_gen; trivial.
apply and_iff_morphism.
 apply ex_morph; red; intros; rewrite H0; rewrite H1; reflexivity.

 apply fa_morph; intros P'.
 apply fa_morph; intros w.
 apply impl_morph.
  apply isTR_rel_morph_gen; auto with *.

  intros; rewrite H0; rewrite H1; reflexivity.
Qed.

  Instance TRP_rel_morph : Proper (eq_set==>eq_set==>iff) (TRP_rel F).
do 3 red; intros.
unfold TRP_rel.
apply and_iff_morphism.
 rewrite H0; reflexivity.
apply and_iff_morphism.
 apply ex_morph; red; intros; rewrite H; rewrite H0; reflexivity.

 apply fa_morph; intros P'.
 apply fa_morph; intros w.
 rewrite H; rewrite H0; reflexivity.
Qed.

  Lemma TR_img_ex x P : isWf x ->
    TRP_rel F x P ->
    uchoice_pred (fun y => couple x y ∈ P).
intros.
split;[|split]; intros.
 rewrite <- H1; trivial.

 destruct H0 as (_,(?,_)); trivial.

 destruct H0 as (?,(?,?)).
 apply isTR_rel_fun with (2:=H0)(3:=H0)(4:=H1)(5:=H2); trivial.
Qed.

  Lemma TR_rel_ex o :
    isWf o -> uchoice_pred (TRP_rel F o).
intro wfo; elim wfo using isWf_ind; clear o wfo; intros.
split;[|split]; intros.
 revert H2; apply TRP_rel_morph; auto with *.

 pose (P:=singl(couple a (F (fun b=> uchoice(fun y => couple b y ∈ uchoice(TRP_rel F b))) a)) ∪
          sup a (fun b => uchoice(TRP_rel F b))).
 assert (Pax:∀ z, z ∈ P <->
     z == couple a (F (fun b=> uchoice(fun y => couple b y ∈ uchoice(TRP_rel F b))) a) \/
     exists2 b, b ∈ a & z ∈ uchoice(TRP_rel F b)).
  intros; unfold P; rewrite union2_ax; apply or_iff_morphism.
   split; intros.
    apply singl_elim in H1; trivial.
    rewrite H1; apply singl_intro.

   rewrite sup_ax.
    reflexivity.

    do 2 red; intros; apply uchoice_morph_raw.
    apply TRP_rel_morph; trivial.
 assert (ychm : morph1 (fun b =>
      uchoice (fun y0 => couple b y0 ∈ uchoice (TRP_rel F b)))).
  do 2 red; intros.
  apply uchoice_morph_raw.
  red; intros.
  rewrite H1; rewrite H2; reflexivity.
 exists P.
 split;[|split]; intros.
  red; intros.
  rewrite Pax in H1; destruct H1 as [?|(b,?,?)].
   apply couple_injection in H1; destruct H1.
   exists (cc_lam o (fun b=> uchoice
            (fun y : set => couple b y ∈ uchoice(TRP_rel F b)))); intros.
    rewrite cc_beta_eq; trivial.
     rewrite Pax; right.
     rewrite H1 in H3; exists n; trivial.
     apply uchoice_def.
     apply TR_img_ex.
      apply isWf_inv with a; trivial.

      apply uchoice_def; auto.

     do 2 red; intros; apply uchoice_morph_raw; red; intros.
     rewrite H5; rewrite H6; reflexivity.

    rewrite H1; rewrite H2; apply Fext.
    red; intros.
    rewrite <- H4.
    rewrite cc_beta_eq; auto with *.

   destruct (uchoice_def _ (H0 _ H1)) as (?,trp').
   destruct H3 with (1:=H2) as (f,?,?).
   exists f; trivial; intros.
   rewrite Pax; right.
   exists b; auto.

  exists (F (fun b => uchoice (fun y => couple b y ∈ uchoice (TRP_rel F b))) a).
  rewrite Pax; left; reflexivity.

  red; intros.
  rewrite Pax in H3; destruct H3 as [?|(y',?,?)].
   destruct H1 with (1:=H2) as (f,?,?).
   rewrite H5 in H2; rewrite H3; revert H2; apply in_reg.
   apply couple_morph; auto with *.
   apply Fext; red; intros.
   apply uchoice_ext; auto.
    rewrite H6 in H2; auto.
    apply TR_img_ex.
     apply isWf_inv with a; trivial.

     apply uchoice_def; auto.

    rewrite <- H6; clear x' H6.
    specialize H0 with (1:=H2).
    apply uchoice_def in H0.
    destruct H0 as (?,((yx,?),_)).
    specialize H4 with (1:=H2).
    rewrite isTR_rel_fun with (2:=H1) (3:=H0) (4:=H4) (5:=H6); trivial.
    apply isWf_inv with a; trivial.

  specialize H0 with (1:=H3).
  apply uchoice_def in H0; destruct H0 as (?,((w,?),?)).
  assert (z == couple (fst z) (snd z)).
   assert (z ∈ subset (uchoice(TRP_rel F y')) (fun z => z == couple (fst z) (snd z))).
    apply H6 with w; trivial.
     red; intros.
     apply subset_elim1 in H7.
     destruct H0 with (1:=H7) as (f',?,?).
     exists f'; intros; trivial.
     apply subset_intro; auto.
     rewrite fst_def; rewrite snd_def; reflexivity.

     apply subset_intro; trivial.
     rewrite fst_def; rewrite snd_def; reflexivity.
   apply subset_elim2 in H7; destruct H7.
   rewrite H7; trivial.
  rewrite H7 in H4|-*.
  destruct H1 with (1:=H2) as (f0,?,_).
  specialize H8 with (1:=H3).
  apply H6 with (cc_app f0 y'); trivial.

 destruct H1 as (?,((y,?),?)).
 destruct H2 as (?,((y',?),?)).
 apply incl_eq; eauto.
Qed.

  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.
unfold WFR; intros.
specialize TR_rel_ex with (1:=H); intro.
apply uchoice_def in H0.
generalize H0; intros (?,_).
apply TR_img_ex in H0; trivial.
apply uchoice_def in H0.
destruct H1 with (1:=H0) as (f,?,?).
rewrite H3; apply Fext; red; intros.
rewrite H5 in H4|-*; clear x0 H5.
assert (isWf x') by eauto using isWf_inv.
specialize H2 with (1:=H4).
specialize TR_rel_ex with (1:=H5); intro.
apply uchoice_def in H6.
generalize H6; intros (?,_).
apply TR_img_ex in H6; trivial.
apply uchoice_def in H6.
apply isTR_rel_fun with (4:=H2) (5:=H6); trivial.
Qed.

  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).
intros x P Pm wfx Hrec.
induction wfx using isWf_ind; intros.
rewrite WFR_eqn; trivial.
apply Hrec; auto with *; intros.
Qed.

  Global Instance WFR_morph0 : morph1 WFR.
do 2 red; intros.
unfold WFR.
apply uchoice_morph_raw.
red; intros.
rewrite H; rewrite H0; reflexivity.
Qed.

End TransfiniteRecursion.

  Global Instance WFR_morph :
    Proper (((eq_set ==> eq_set) ==> eq_set ==> eq_set) ==> eq_set ==> eq_set) WFR.
do 3 red; intros.
unfold WFR.
apply uchoice_morph_raw; red; intros.
rewrite (couple_morph _ _ H0 _ _ H1).
split; apply eq_elim; [|symmetry]; apply uchoice_morph_raw; red; intros.
 apply TRP_rel_morph_gen; trivial.
 apply TRP_rel_morph_gen; trivial.
Qed.

End WellFoundedSets.

Hint Resolve isWf_morph.