Library ZFind_nat

Require Import ZF ZFsum ZFfix ZFnats ZFrelations ZFord ZFcard ZFcont.
Require Import ZFind_basic.
Import ZFrepl.

Section Nat_theory.

Section TypeConstructor.

  Definition NATf X := sum UNIT X.

  Lemma sum_ext_natf : ∀ A, ext_fun A NATf.

  Instance NATf_mono : Proper (incl_set ==> incl_set) NATf.
Qed.
Hint Resolve NATf_mono Fmono_morph.
  Instance NATf_morph : Proper (eq_set ==> eq_set) NATf.
Qed.

Definition ZERO := inl zero.
Definition SUCC x := inr x.

  Lemma NATf_discr : ∀ n, ~ ZERO == SUCC n.

  Lemma SUCC_inj : ∀ n m, SUCC n == SUCC m -> n == m.

  Lemma ZERO_typ_gen : ∀ X, ZERO ∈ sum UNIT X.

  Lemma SUCC_typ_gen : ∀ x X, x ∈ X -> SUCC x ∈ sum UNIT X.

  Lemma NATf_case : ∀ X (P:Prop) x,
    (x == ZERO -> P) ->
    (∀ n, n ∈ X -> x == SUCC n -> P) ->
    x ∈ NATf X -> P.

  Lemma SUCC_inv_typ_gen : ∀ X x,
    SUCC x ∈ NATf X -> x ∈ X.
End TypeConstructor.

Hint Resolve NATf_mono Fmono_morph.

Section IterationNat.

  Definition NATi := TI NATf.

  Instance NATi_morph : morph1 NATi.
Qed.

  Lemma NATfun_ext : ∀ x, ext_fun x (fun n => NATf (NATi n)).
Hint Resolve NATfun_ext.

Lemma ZEROi_typ : ∀ o,
  isOrd o -> ZERO ∈ NATi (osucc o).

Lemma SUCCi_typ : ∀ o n,
  isOrd o ->
  n ∈ NATi o ->
  SUCC n ∈ NATi (osucc o).

Lemma SUCCi_inv_typ : ∀ o n,
  isOrd o ->
  SUCC n ∈ NATi (osucc o) ->
  n ∈ NATi o.

Section CaseAnalysis.

  Lemma NATi_case : ∀ (P:set->Prop) o n,
    isOrd o ->
    (∀ x x', x ∈ NATi o -> x == x' -> P x -> P x') ->
    P ZERO ->
    (∀ m o', lt o' o -> m ∈ NATi o' -> P (SUCC m)) ->
    n ∈ NATi o -> P n.

  Variable fZ : set.
  Variable fS : set -> set.

  Definition NATCASE (n:set) :=
    cond_set (n ==ZERO) fZ ∪
    cond_set (exists k,n ==SUCC k) (fS (dest_sum n)).

Instance NATCASE_m1 : morph1 fS -> morph1 NATCASE.

Qed.

Lemma NATCASE_ZERO : NATCASE ZERO == fZ.

Lemma NATCASE_SUCC : ∀ n,
  (∀ x, x == n -> fS x == fS n) ->
  NATCASE (SUCC n) == fS n.

Lemma NATCASE_mt :
  NATCASE empty == empty.

Lemma NATCASE_typ :
  ∀ (P:set->set) o,
  morph1 P ->
  morph1 fS ->
  isOrd o ->
  fZ ∈ P ZERO ->
  (∀ n, n ∈ NATi o -> fS n ∈ P (SUCC n)) ->
  ∀ n,
  n ∈ NATi (osucc o) ->
  NATCASE n ∈ P n.

End CaseAnalysis.

Lemma NATCASE_morph_gen : ∀ fZ fZ' fS fS' c c',
  c == c' ->
  fZ == fZ' ->
  (∀ x x', c == SUCC x -> x == x' -> fS x == fS' x') ->
  NATCASE fZ fS c == NATCASE fZ' fS' c'.

Instance NATCASE_morph : Proper
  (eq_set ==> (eq_set ==> eq_set ) ==> eq_set ==> eq_set) NATCASE.
Qed.

Require Import ZFfunext ZFfixrec.

Section Recursor.

  Lemma NATi_fix :
    ∀ (P:set->Prop) o,
    isOrd o ->
    (∀ i, isOrd i -> i ⊆ o ->
     (∀ i' m, lt i' i -> m ∈ NATi i' -> P m) ->
     ∀ n, n ∈ NATi i -> P n) ->
    ∀ n, n ∈ NATi o -> P n.

  Notation prod := cc_prod.

  Variable ord : set.
  Hypothesis oord : isOrd ord.

  Variable F : set -> set -> set.
  Hypothesis Fm : morph2 F.

  Variable U : set -> set -> set.
  Hypothesis Umono : ∀ o o' x x',
    isOrd o' -> o' ⊆ ord -> isOrd o -> o ⊆ o' ->
    x ∈ NATi o -> x == x' ->
    U o x ⊆ U o' x'.

  Let Ty o := prod (NATi o) (U o).
  Hypothesis Ftyp : ∀ o f, isOrd o -> o ⊆ ord ->
    f ∈ Ty o -> F o f ∈ Ty (osucc o).

  Let Q o f := ∀ x, x ∈ NATi o -> cc_app f x ∈ U o x.

  Definition NAT_ord_irrel :=
    ∀ o o' f g,
    isOrd o' -> o' ⊆ ord -> isOrd o -> o ⊆ o' ->
    f ∈ Ty o -> g ∈ Ty o' ->
    fcompat (NATi o) f g ->
    fcompat (NATi (osucc o)) (F o f) (F o' g).

  Hypothesis Firrel : NAT_ord_irrel.

  Definition NATREC := REC F.

Lemma Umorph : ∀ o o', isOrd o' -> o' ⊆ ord -> o == o' ->
    ∀ x x', x ∈ NATi o -> x == x' -> U o x == U o' x'.

Lemma Uext : ∀ o, isOrd o -> o ⊆ ord -> ext_fun (NATi o) (U o).

  Lemma NATREC_typing : ∀ o f, isOrd o -> o ⊆ ord ->
    is_cc_fun (NATi o) f -> Q o f -> f ∈ Ty o.

Lemma NATi_cont : ∀ o,
   isOrd o -> NATi o == sup o (fun o' => NATi (osucc o')).

Let Qm :
   ∀ o o',
   isOrd o ->
   o ⊆ ord ->
   o == o' -> ∀ f f', fcompat (NATi o) f f' -> Q o f -> Q o' f'.
Qed.

Let Qcont : ∀ o f : set,
isOrd o ->
o ⊆ ord ->
is_cc_fun (NATi o) f ->
(∀ o' : set, o' ∈ o -> Q (osucc o') f) -> Q o f.
Qed.

Let Qtyp : ∀ o f,
isOrd o ->
o ⊆ ord ->
is_cc_fun (NATi o) f ->
Q o f -> is_cc_fun (NATi (osucc o)) (F o f) /\ Q (osucc o) (F o f).

Qed.

  Lemma Firrel_NAT : stage_irrelevance ord NATi Q F.
Hint Resolve Firrel_NAT.

  Lemma NAT_recursor : recursor ord NATi Q F.

Hint Resolve NAT_recursor.

  Lemma NATREC_wt : NATREC ord ∈ Ty ord.

  Lemma NATREC_ord_irrel o o' x:
    isOrd o ->
    isOrd o' ->
    o ⊆ o' ->
    o' ⊆ ord ->
    x ∈ NATi o ->
    cc_app (NATREC o) x == cc_app (NATREC o') x.

  Lemma NATREC_ext G :
    is_cc_fun (NATi ord) G ->
    (∀ o', o' ∈ ord ->
     NATREC o' == cc_lam (NATi o') (cc_app G) ->
     fcompat (NATi (osucc o')) G (F o' (cc_lam (NATi o') (cc_app G)))) ->
    NATREC ord == G.

  Lemma NATREC_expand : ∀ n,
    n ∈ NATi ord -> cc_app (NATREC ord) n == cc_app (F ord (NATREC ord)) n.

  Lemma NATREC_eqn :
    NATREC ord == cc_lam (NATi ord) (cc_app (F ord (NATREC ord))).

End Recursor.

Instance NATREC_morph :
  Proper ((eq_set ==>eq_set ==>eq_set )==>eq_set ==>eq_set) NATREC.
Qed.

Section NatFixpoint.

NAT : the least fixpoint (using continuity)

  Definition NAT := NATi omega.

  Lemma NAT_continuous : ∀ F,
    ext_fun omega F ->
    NATf (sup omega F) == sup omega (fun n => NATf (F n)).

  Lemma NAT_eq : NAT == NATf NAT.

  Lemma NATi_NAT : ∀ o,
    isOrd o ->
    NATi o ⊆ NAT.

  Lemma ZERO_typ : ZERO ∈ NAT.

  Lemma SUCC_typ : ∀ n, n ∈ NAT -> SUCC n ∈ NAT.

  Lemma NAT_fix :
    ∀ (P:set->Prop),
    (∀ o, isOrd o ->
     (∀ o' m, lt o' o -> m ∈ NATi o' -> P m) ->
     ∀ n, n ∈ NATi o -> P n) ->
    ∀ n, n ∈ NAT -> P n.

  Lemma NAT_ind : ∀ (P:set->Prop),
    (∀ x x', x ∈ NAT -> x == x' -> P x -> P x') ->
    P ZERO ->
    (∀ n, n ∈ NAT -> P n -> P (SUCC n)) ->
    ∀ n, n ∈ NAT -> P n.

  Fixpoint nat2NAT (n:nat) : set :=
    match n with
    | 0 => ZERO
    | S k => SUCC (nat2NAT k)
    end.

  Lemma nat2NAT_reflect : ∀ x,
    x ∈ NAT -> exists n, x == nat2NAT n.

End NatFixpoint.

End IterationNat.

Hint Resolve NATfun_ext.

Section NatConvergence.

Convergence (using closure property of ordinal)

Require Import ZFrank.

  Variable o : set.
  Hypothesis limo : limitOrd o.
  Hypothesis diro : isDir o.

  Let oo : isOrd o.

  Let zer : ∀ x, x ∈ VN o -> zero ∈ VN o.
Qed.

  Let suc : ∀ x, x ∈ VN o -> succ x ∈ VN o.
Qed.

  Lemma NATf_size_gen :
    ∀ X, X ∈ VN o -> NATf X ∈ VN o.

  Hypothesis zer_o : zero ∈ VN o.

  Lemma NATf_size_gen_le : ∀ X,
    X ⊆ VN o -> NATf X ⊆ VN o.

End NatConvergence.

  Lemma NAT_incl_omega : NAT ⊆ VN omega.

  Lemma NAT_typ : ∀ o, isOrd o -> lt omega o -> NAT ∈ VN o.

End Nat_theory.

Hint Resolve NATf_mono Fmono_morph NATfun_ext.

Applications

Module Example.

Abel's counter-example:

Definition U o := cc_arr (cc_arr NAT (NATi (osucc o))) NAT.

Definition shift f := cc_lam NAT (fun n =>
  NATCASE ZERO (fun m => m) (cc_app f (SUCC n))).

Lemma shift_typ : ∀ o f,
  isOrd o ->
  f ∈ cc_arr NAT (NATi (osucc (osucc o))) ->
  shift f ∈ cc_arr NAT (NATi (osucc o)).

Definition loopF o loop :=
  cc_lam (NATi (osucc o)) (fun _ =>
  cc_lam (cc_arr NAT (NATi (osucc (osucc o)))) (fun f =>
  NATCASE
    ZERO
    (fun n =>
     NATCASE
       ZERO
       (fun m => cc_app (cc_app loop m) (shift f))
       n)
    (cc_app f ZERO))).

Lemma loopF_typ : ∀ o lp,
  isOrd o ->
  lp ∈ cc_arr (NATi o) (U o) ->
  loopF o lp ∈ cc_arr (NATi (osucc o)) (U (osucc o)).

Lemma sfp : ∀ o, isOrd o ->
   NAT_ord_irrel o loopF (fun o' x => U o').

End Example.