Library ZFind_wd

A theory of dependent inductive families (here W-types) as a subset of a W-type

Require Import ZF ZFpairs ZFrelations ZFord ZFstable ZFind_w ZFfixfun.

Section DependentW.

Parameters of W-types

Variable A : set.
Variable B : set -> set.
Hypothesis Bext : ext_fun A B.

Index type

Variable Arg : set.

Constraints on the subterms

Hypothesis f : set -> set -> set.
Hypothesis fm : morph2 f.
Hypothesis ftyp : ∀ x i,
x ∈ A -> i ∈ B x -> f x i ∈ Arg.

Instance introduced by the constructors

Hypothesis g : set -> set -> Prop.
Hypothesis gm : Proper (eq_set ==>eq_set ==>iff) g.

The intended type operator:

Inductive Wd : Arg->Type := C (x:A) (_:∀ i:B x, Wd(f x i)) : Wd(g x). is encoded as [Inductive Wd' (a:Arg) : Type := C' (x:A) (_:g x=a) (_:∀ i:B x, Wd(f x i)).

Definition W_Fd (X:set->set) (a:set) :=
  sigma (subset A (fun x => g x a)) (fun x => cc_prod (B x) (fun i => X (f x i))).

Instance W_Fd_morph :
  Proper ((eq_set ==> eq_set ) ==> eq_set ==> eq_set) W_Fd.
do 3 red; intros.
apply sigma_ext; intros.
apply subset_morph; auto with *.
red; intros.
rewrite H0; reflexivity.

apply subset_elim1 in H1.
apply cc_prod_ext; auto with *.
red; intros.
apply H.
apply fm; auto.
Qed.

Lemma W_Fd_mono : mono_fam Arg W_Fd.
do 2 red; intros.
apply sigma_mono.
do 2 red; intros.
apply subset_elim1 in H3.
apply cc_prod_ext; auto with *.
red; intros.
apply H; apply fm; auto.

do 2 red; intros.
apply subset_elim1 in H3.
apply cc_prod_ext; auto with *.
red; intros.
apply H0; apply fm; auto.

red; intros.
rewrite subset_ax in H3|-*; destruct H3 as (?,(z',?,?)).
split; trivial.
exists z'; trivial.

intros.
apply subset_elim1 in H3.
apply cc_prod_covariant; auto with *.
  do 2 red; intros.
  apply H0; apply fm; auto with *.

  intros.
  rewrite <- H4; apply H1; auto.
Qed.
Hint Resolve W_Fd_mono.

Lemma W_Fd_incl_W_F X Y :
  ext_fun Arg X ->
  (∀ a, a ∈ Arg -> X a ⊆ Y) ->
  ∀ a, a ∈ Arg -> W_Fd X a ⊆ W_F A B Y.
intros.
apply sigma_mono.
do 2 red; intros.
apply subset_elim1 in H2.
apply cc_prod_ext; auto with *.
red; intros.
apply H; auto.
apply fm; trivial.

do 2 red; intros; apply cc_arr_morph; auto with *.

red; intros.
apply subset_elim1 in H2; trivial.

intros.
apply subset_elim1 in H2.
unfold cc_arr; apply cc_prod_covariant; auto with *.
Qed.

Predicate characterizing the elements of the W-type that respect the index constraints

Inductive instance a w : Prop :=
  | I_node :
      fst w ∈ A ->
      g (fst w) a ->
      (∀ i, i ∈ B (fst w) -> instance (f (fst w) i) (cc_app (snd w) i)) ->
      instance a w.

Instance inst_m : Proper (eq_set ==> eq_set ==> iff) instance.
apply morph_impl_iff2; auto with *.
do 4 red; intros.
revert y H y0 H0.
induction H1; constructor; intros.
rewrite <- H4; trivial.

rewrite <- H3; rewrite <- H4; trivial.

apply H2 with i.
  rewrite (Bext _ _ H (fst_morph _ _ H4)); trivial.

  rewrite H4; reflexivity.

  rewrite H4; reflexivity.
Qed.

Lemma inst_inv o :
  isOrd o ->
  ∀ a, a ∈ Arg ->
  subset (TI (W_F A B) o) (instance a) == TIF Arg W_Fd o a.
induction 1 using isOrd_ind; intros.
rewrite TIF_eq; auto with *.
apply eq_set_ax; intros z.
rewrite subset_ax.
rewrite TI_eq; auto with *.
2:apply W_F_morph; trivial.
rewrite sup_ax.
rewrite sup_ax.
  split; intros.
   destruct H3 as ((o',?,?),(z',?,?)).
   exists o'; trivial.
   apply W_F_elim in H4; trivial.
   destruct H4 as (?,(?,?)).
   rewrite H8.
   apply couple_intro_sigma.
    do 2 red; intros.
    apply subset_elim1 in H9.
    apply cc_prod_ext; auto with *.
    red; intros; apply TIF_morph; auto with *.
    apply fm; trivial.

    destruct H6 as (?,?,_).
    rewrite <- H5 in H9.
    apply subset_intro; trivial.

    apply cc_prod_intro; intros.
     do 2 red; intros; apply cc_app_morph; auto with *.

     do 2 red; intros.
     apply TIF_morph; auto with *.
     apply fm; auto with *.

     rewrite <- H1; auto.
     apply subset_intro; auto.
     rewrite <- H5 in H6.
     destruct H6 as (_,_,?); auto.

   destruct H3 as (o',?,?).
   split.
    exists o'; trivial.
    revert H4; apply W_Fd_incl_W_F; trivial.
     do 2 red; intros; apply TIF_morph; auto with *.

     intros.
     rewrite <- H1; auto.
     red; intros.
     apply subset_elim1 in H5; trivial.

     exists z; auto with *.
     assert (fst z ∈ A).
      apply fst_typ_sigma in H4.
      apply subset_elim1 in H4; trivial.
     constructor; intros; trivial.
      apply fst_typ_sigma in H4.
      rewrite subset_ax in H4.
      destruct H4 as (?,(x',?,?)).
      rewrite H6; trivial.

      apply snd_typ_sigma with (y:=fst z) in H4; auto with *.
       apply cc_prod_elim with (2:=H6) in H4.
       rewrite <- H1 in H4; auto.
       rewrite subset_ax in H4; destruct H4 as (_,(w',?,?)).
       rewrite H4; trivial.

       do 2 red; intros.
       apply subset_elim1 in H7.
       apply cc_prod_ext; auto.
       red; intros; apply TIF_morph; auto with *.
       apply fm; auto.

  do 2 red; intros.
  apply W_Fd_morph; auto with *.
  red; intros; apply TIF_morph; auto.

do 2 red; intros.
apply W_F_morph; auto with *.
apply TI_morph; auto.
Qed.

Fixpoint of the W_Fd operator

Definition Wd := TIF Arg W_Fd (W_ord A B).

Lemma Wd_eqn : ∀ a, a ∈ Arg -> Wd a == W_Fd Wd a.
intros.
apply incl_eq.
unfold Wd; rewrite <- TIF_mono_succ; auto with *.
apply TIF_incl; auto with *.
  apply isOrd_succ.
  apply W_o_o; trivial.

  apply lt_osucc; apply W_o_o; trivial.

apply W_o_o; trivial.

red; intros.
unfold Wd; rewrite <- inst_inv; trivial.
2:apply W_o_o; trivial.
apply subset_intro.
  change (z ∈ W A B).
  rewrite W_eqn; trivial.
  revert H0; apply W_Fd_incl_W_F; intros; auto.
   do 2 red; intros.
   apply TIF_morph; auto with *.

   red; intros.
   unfold Wd in H1.
   rewrite <- inst_inv in H1; auto.
   2:apply W_o_o; trivial.
   apply subset_elim1 in H1; trivial.

  unfold Wd in H0; rewrite <- TIF_mono_succ in H0; auto.
   rewrite <- inst_inv in H0; auto.
   2:apply isOrd_succ; apply W_o_o; trivial.
   rewrite subset_ax in H0; destruct H0 as (_,(?,?,?)).
   rewrite H0; trivial.

   apply W_Fd_morph.

   apply W_o_o; trivial.
Qed.

End DependentW.