(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Require Import IZF_logic.
Require Import IZF_base.
Require Import IZF_nat.

(*************)
(** * Zero   *)
(*************)

(** In set theory, zero is implemented as the empty set.  As a
    pointed graph, we can take any (non-empty) carrier and any
    root, with an empty edge relation: *)

Definition unit : Typ1 := forall X : Typ0, X -> X.
Definition id : unit := fun X x => x.
Definition ZERO : Rel unit := fun _ _ => bot.

Lemma ZERO_elim :
 forall (X : Typ1) (A : Rel X) (a : X), ELT X A a unit ZERO id -> bot.

Proof.
(* Goal: forall (X : Typ1) (A : Rel X) (a : X) (_ : ELT X A a unit ZERO id), bot *)
intros X A a H; apply H.
(* Goal: forall (b' : unit) (_ : ZERO b' id) (_ : EQV X A a unit ZERO b'), bot *)
intros b' H1 H2; exact H1.
Qed.

(*******************************)
(** * The successor function   *)
(*******************************)

(** In set theory, the successor of von Neumann numeral n is encoded
    as the set  n U {n}, whose existence follows from the pairing
    axiom (used twice) and the union axiom, that have been already
    derived in the files "IZF_pair.v"  and "IZF_union.v".

    However, it is simpler to give here a direct implementation of the
    successor as follows.  Formally, the successor of a given pointed
    graph (X, A, a) is represented as the pointed graph

        ((opt X), (SUCC X A a), (none X))

    whose edge relation is defined by the following three clauses:

    1. Delocate A in the new graph via (some X):

         if (A x' x), then (SUCC X A a (some X x') (some X x))

    2. Connect the image of any direct element of the old root a:X
       to the new root:

         if (A x a), then (SUCC X A a (some X x) (none X))

    3. Connect the old root to the new root:

         (SUCC X A a (some X a) (none X)).

    As usual, we use a second-order encoding to define this relation. *)

Definition SUCC (X : Typ1) (A : Rel X) (a : X) : Rel (opt X) :=
  fun z' z =>
  forall E : Prop,
  (forall x x' : X,
   eq (opt X) z (some X x) -> eq (opt X) z' (some X x') -> A x' x -> E) ->
  (forall x' : X,
   eq (opt X) z (none X) -> eq (opt X) z' (some X x') -> A x' a -> E) ->
  (eq (opt X) z (none X) -> eq (opt X) z' (some X a) -> E) -> E.

Lemma SUCC_in :
 forall (X : Typ1) (A : Rel X) (a x x' : X),
 A x' x -> SUCC X A a (some X x') (some X x).

Proof
  fun X A a x x' H E H1 _ _ =>
  H1 x x' (eq_refl (opt X) (some X x)) (eq_refl (opt X) (some X x')) H.

Lemma SUCC_rt1 :
 forall (X : Typ1) (A : Rel X) (a x' : X),
 A x' a -> SUCC X A a (some X x') (none X).

Proof
  fun X A a x' H E _ H2 _ =>
  H2 x' (eq_refl (opt X) (none X)) (eq_refl (opt X) (some X x')) H.

Lemma SUCC_rt2 :
 forall (X : Typ1) (A : Rel X) (a : X), SUCC X A a (some X a) (none X).

Proof
  fun X A a E _ _ H3 =>
  H3 (eq_refl (opt X) (none X)) (eq_refl (opt X) (some X a)).

Lemma SUCC_deloc :
 forall (X : Typ1) (A : Rel X) (a : X),
 deloc X A (opt X) (SUCC X A a) (some X).

Proof.
(* Goal: forall (X : Typ1) (A : Rel X) (a : X), deloc X A (opt X) (SUCC X A a) (some X) *)
intros X A a; unfold deloc in |- *; apply and_intro.
(* Deloc 1 *)
(* Goal: forall (x x' : X) (_ : A x' x), SUCC X A a (some X x') (some X x) *)
(* Goal: forall (x : X) (y' : opt X) (_ : SUCC X A a y' (some X x)), ex2 X (fun x' : X => A x' x) (fun x' : X => eq (opt X) y' (some X x')) *)
intros; apply SUCC_in; assumption.
(* Deloc 2 *)
(* Goal: forall (x : X) (y' : opt X) (_ : SUCC X A a y' (some X x)), ex2 X (fun x' : X => A x' x) (fun x' : X => eq (opt X) y' (some X x')) *)
intros x y' H; apply H; clear H.
(* Deloc 2, case 1 *)
(* Goal: forall (x0 x' : X) (_ : eq (opt X) (some X x) (some X x0)) (_ : eq (opt X) y' (some X x')) (_ : A x' x0), ex2 X (fun x'0 : X => A x'0 x) (fun x'0 : X => eq (opt X) y' (some X x'0)) *)
(* Goal: forall (x' : X) (_ : eq (opt X) (some X x) (none X)) (_ : eq (opt X) y' (some X x')) (_ : A x' a), ex2 X (fun x'0 : X => A x'0 x) (fun x'0 : X => eq (opt X) y' (some X x'0)) *)
(* Goal: forall (_ : eq (opt X) (some X x) (none X)) (_ : eq (opt X) y' (some X a)), ex2 X (fun x' : X => A x' x) (fun x' : X => eq (opt X) y' (some X x')) *)
intros x0 x' H1 H2 H3; apply ex2_intro with x'.
(* Goal: A x' x *)
(* Goal: eq (opt X) y' (some X x') *)
(* Goal: forall (x' : X) (_ : eq (opt X) (some X x) (none X)) (_ : eq (opt X) y' (some X x')) (_ : A x' a), ex2 X (fun x'0 : X => A x'0 x) (fun x'0 : X => eq (opt X) y' (some X x'0)) *)
(* Goal: forall (_ : eq (opt X) (some X x) (none X)) (_ : eq (opt X) y' (some X a)), ex2 X (fun x' : X => A x' x) (fun x' : X => eq (opt X) y' (some X x')) *)
apply (eq_sym _ _ _ (eq_some_some X x x0 H1)); assumption.
(* Goal: P (opt nat) OMEGA (some nat n) *)
assumption.
(* Deloc 2, case 2 (absurd) *)
(* Goal: forall (x' : X) (_ : eq (opt X) (some X x) (none X)) (_ : eq (opt X) y' (some X x')) (_ : A x' a), ex2 X (fun x'0 : X => A x'0 x) (fun x'0 : X => eq (opt X) y' (some X x'0)) *)
(* Goal: forall (_ : eq (opt X) (some X x) (none X)) (_ : eq (opt X) y' (some X a)), ex2 X (fun x' : X => A x' x) (fun x' : X => eq (opt X) y' (some X x')) *)
intros x' H1 H2 H3; apply (eq_some_none _ _ H1).
(* Deloc 2, case 3 (absurd) *)
(* Goal: forall (_ : eq (opt X) (some X x) (none X)) (_ : eq (opt X) y' (some X a)), ex2 X (fun x' : X => A x' x) (fun x' : X => eq (opt X) y' (some X x')) *)
intros H1 H2; apply (eq_some_none _ _ H1).
Qed.

Lemma SUCC_eqv :
 forall (X : Typ1) (A : Rel X) (a x : X),
 EQV X A x (opt X) (SUCC X A a) (some X x).

Proof.
(* Goal: forall (X : Typ1) (A : Rel X) (a x : X), EQV X A x (opt X) (SUCC X A a) (some X x) *)
intros X A a x; apply EQV_deloc; apply SUCC_deloc.
Qed.

Lemma SUCC_intro1 :
 forall (X : Typ1) (A : Rel X) (a : X) (Y : Typ1) (B : Rel Y) (b : Y),
 ELT Y B b X A a -> ELT Y B b (opt X) (SUCC X A a) (none X).

Proof.
(* Goal: forall (X : Typ1) (A : Rel X) (a : X) (Y : Typ1) (B : Rel Y) (b : Y) (_ : ELT Y B b X A a), ELT Y B b (opt X) (SUCC X A a) (none X) *)
intros X A a Y B b H; apply H; clear H; intros a' H1 H2.
(* Goal: P (opt nat) OMEGA (some nat n) *)
apply ELT_intro with (some X a'). apply SUCC_rt1; assumption.
(* Goal: P (opt nat) OMEGA (some nat n) *)
apply EQV_trans with X A a'. assumption. apply SUCC_eqv.
Qed.

Lemma SUCC_intro2 :
 forall (X : Typ1) (A : Rel X) (a : X),
 ELT X A a (opt X) (SUCC X A a) (none X).

Proof.
(* Goal: forall (X : Typ1) (A : Rel X) (a : X), ELT X A a (opt X) (SUCC X A a) (none X) *)
intros X A a; apply ELT_intro with (some X a).
(* Goal: EQV X A a (opt X) (SUCC X A a) (some X a) *)
apply SUCC_rt2. apply SUCC_eqv.
Qed.

Lemma SUCC_elim :
 forall (X : Typ1) (A : Rel X) (a : X) (Y : Typ1) (B : Rel Y) (b : Y),
 ELT Y B b (opt X) (SUCC X A a) (none X) ->
 or (ELT Y B b X A a) (EQV Y B b X A a).

Proof.
(* Goal: forall (X : Typ1) (A : Rel X) (a : X) (Y : Typ1) (B : Rel Y) (b : Y) (_ : ELT Y B b (opt X) (SUCC X A a) (none X)), or (ELT Y B b X A a) (EQV Y B b X A a) *)
intros X A a Y B b H; apply H; clear H.
(* Goal: forall (b' : opt X) (_ : SUCC X A a b' (none X)) (_ : EQV Y B b (opt X) (SUCC X A a) b'), or (ELT Y B b X A a) (EQV Y B b X A a) *)
intros z' H H1; apply H; clear H.
(* Case 1 (absurd) *)
(* Goal: forall (x x' : X) (_ : eq (opt X) (none X) (some X x)) (_ : eq (opt X) z' (some X x')) (_ : A x' x), or (ELT Y B b X A a) (EQV Y B b X A a) *)
(* Goal: forall (x' : X) (_ : eq (opt X) (none X) (none X)) (_ : eq (opt X) z' (some X x')) (_ : A x' a), or (ELT Y B b X A a) (EQV Y B b X A a) *)
(* Goal: forall (_ : eq (opt X) (none X) (none X)) (_ : eq (opt X) z' (some X a)), or (ELT Y B b X A a) (EQV Y B b X A a) *)
intros x x' H2 H3 H4; apply (eq_none_some _ _ H2).
(* Case 2 *)
(* Goal: forall (x' : X) (_ : eq (opt X) (none X) (none X)) (_ : eq (opt X) z' (some X x')) (_ : A x' a), or (ELT Y B b X A a) (EQV Y B b X A a) *)
(* Goal: forall (_ : eq (opt X) (none X) (none X)) (_ : eq (opt X) z' (some X a)), or (ELT Y B b X A a) (EQV Y B b X A a) *)
intros x' H2 H3 H4; apply or_inl; apply ELT_intro with x'.
(* Goal: P (opt nat) OMEGA (some nat n) *)
assumption.
(* Goal: EQV Y B b X A x' *)
(* Goal: forall (_ : eq (opt X) (none X) (none X)) (_ : eq (opt X) z' (some X a)), or (ELT Y B b X A a) (EQV Y B b X A a) *)
apply EQV_trans with (opt X) (SUCC X A a) (some X x').
(* Goal: P (opt nat) OMEGA (some nat n) *)
apply H3; assumption. apply EQV_sym; apply SUCC_eqv.
(* Case 3 *)
(* Goal: forall (_ : eq (opt X) (none X) (none X)) (_ : eq (opt X) z' (some X a)), or (ELT Y B b X A a) (EQV Y B b X A a) *)
intros H2 H3; apply or_inr.
(* Goal: EQV Y B b X A a *)
apply EQV_trans with (opt X) (SUCC X A a) (some X a).
(* Goal: P (opt nat) OMEGA (some nat n) *)
apply H3; assumption. apply EQV_sym; apply SUCC_eqv.
Qed.

Lemma successor :
 forall (X : Typ1) (A : Rel X) (a : X) (Y : Typ1) (B : Rel Y) (b : Y),
 iff (ELT Y B b (opt X) (SUCC X A a) (none X))
   (or (ELT Y B b X A a) (EQV Y B b X A a)).

Proof.
(* Goal: forall (X : Typ1) (A : Rel X) (a : X) (Y : Typ1) (B : Rel Y) (b : Y), iff (ELT Y B b (opt X) (SUCC X A a) (none X)) (or (ELT Y B b X A a) (EQV Y B b X A a)) *)
intros X A a Y B b; unfold iff in |- *.
(* Goal: and (forall _ : ELT Y B b (opt X) (SUCC X A a) (none X), or (ELT Y B b X A a) (EQV Y B b X A a)) (forall _ : or (ELT Y B b X A a) (EQV Y B b X A a), ELT Y B b (opt X) (SUCC X A a) (none X)) *)
apply and_intro; intro H.
(* Direct implication (elim) *)
(* Goal: P (opt nat) OMEGA (some nat n) *)
apply SUCC_elim; assumption.
(* Converse implication (intro1,2) *)
(* Goal: ELT Y B b (opt X) (SUCC X A a) (none X) *)
apply H; clear H; intro H.
(* Goal: P (opt nat) OMEGA (some nat n) *)
apply SUCC_intro1; assumption.
(* Goal: ELT Y B b (opt X) (SUCC X A a) (none X) *)
apply ELT_compat_l with X A a.
(* Goal: P (opt nat) OMEGA (some nat n) *)
assumption. apply SUCC_intro2.
Qed.

Lemma SUCC_compat :
 forall (X : Typ1) (A : Rel X) (a : X) (Y : Typ1) (B : Rel Y) (b : Y),
 EQV X A a Y B b ->
 EQV (opt X) (SUCC X A a) (none X) (opt Y) (SUCC Y B b) (none Y).

Proof.
cut
 (forall (X : Typ1) (A : Rel X) (a : X) (Y : Typ1) (B : Rel Y) (b : Y),
  EQV X A a Y B b ->
  SUB (opt X) (SUCC X A a) (none X) (opt Y) (SUCC Y B b) (none Y)).
(* Goal: forall (_ : forall (X : Typ1) (A : Rel X) (a : X) (Y : Typ1) (B : Rel Y) (b : Y) (_ : EQV X A a Y B b), SUB (opt X) (SUCC X A a) (none X) (opt Y) (SUCC Y B b) (none Y)) (X : Typ1) (A : Rel X) (a : X) (Y : Typ1) (B : Rel Y) (b : Y) (_ : EQV X A a Y B b), EQV (opt X) (SUCC X A a) (none X) (opt Y) (SUCC Y B b) (none Y) *)
(* Goal: forall (X : Typ1) (A : Rel X) (a : X) (Y : Typ1) (B : Rel Y) (b : Y) (_ : EQV X A a Y B b), SUB (opt X) (SUCC X A a) (none X) (opt Y) (SUCC Y B b) (none Y) *)
intros H X A a Y B b H1; apply extensionality.
(* Goal: P (opt nat) OMEGA (some nat n) *)
apply H; assumption. apply H; apply EQV_sym; assumption.
(* Goal: forall (X : Typ1) (A : Rel X) (a : X) (Y : Typ1) (B : Rel Y) (b : Y) (_ : EQV X A a Y B b), SUB (opt X) (SUCC X A a) (none X) (opt Y) (SUCC Y B b) (none Y) *)
unfold SUB in |- *; intros X A a Y B b H Z C c H1.
(* Goal: ELT Z C c (opt Y) (SUCC Y B b) (none Y) *)
apply (SUCC_elim X A a Z C c H1); clear H1; intro H1.
(* Goal: P (opt nat) OMEGA (some nat n) *)
apply SUCC_intro1; apply ELT_compat_r with X A a; assumption.
(* Goal: ELT Z C c (opt Y) (SUCC Y B b) (none Y) *)
apply ELT_compat_l with Y B b.
(* Goal: P (opt nat) OMEGA (some nat n) *)
apply EQV_trans with X A a; assumption.
(* Goal: ELT (opt nat) OMEGA (some nat n) (opt (opt nat)) (SUCC (opt nat) OMEGA (some nat n)) (none (opt nat)) *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (some nat (S n)) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), ELT X A a (opt (opt nat)) (SUCC (opt nat) OMEGA (some nat n)) (none (opt nat)) *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
apply SUCC_intro2.
Qed.

(**************************************)
(** * The set of von Neuman numerals  *)
(**************************************)

(** The set omega of von Neumann numerals is represented as the
    pointed graph ((opt nat), OMEGA, (none nat)) whose edge
    relation OMEGA : (Rel (opt nat)) is defined by the following
    two clauses:

    1. Delocation of the strict ordering "lt"

         if (wf_nat n), (wf_nat m) and (lt n m),
         then (OMEGA (some nat n) (some nat m))

    2. Connecting wf_nat's to the new root:

         if (wf_nat n), then (OMEGA (some nat n) (none nat)).

    As usual, we define it via a second-order encoding: *)

Definition OMEGA : Rel (opt nat) :=
  fun z' z =>
  forall E : Prop,
  (forall n n' : nat,
   eq (opt nat) z (some nat n) ->
   eq (opt nat) z' (some nat n') -> wf_nat n -> wf_nat n' -> lt n' n -> E) ->
  (forall n' : nat,
   eq (opt nat) z (none nat) ->
   eq (opt nat) z' (some nat n') -> wf_nat n' -> E) -> E.

(** The corresponding constructors are the following: *)

Lemma OMEGA_in :
 forall n : nat,
 wf_nat n ->
 forall m : nat, wf_nat m -> lt n m -> OMEGA (some nat n) (some nat m).

Proof
  fun n Hn m Hm H E H1 _ =>
  H1 m n (eq_refl (opt nat) (some nat m)) (eq_refl (opt nat) (some nat n)) Hm
    Hn H.

Lemma OMEGA_rt : forall n : nat, wf_nat n -> OMEGA (some nat n) (none nat).

Proof
  fun n Hn E _ H2 =>
  H2 n (eq_refl (opt nat) (none nat)) (eq_refl (opt nat) (some nat n)) Hn.

(** The pointed graph ((opt nat), OMEGA, (some nat O)) is bisimilar
    to the pointed graph (unit ZERO id) that represents the empty set.
    This is done by extensionality. *)

Lemma OMEGA_ZERO : EQV (opt nat) OMEGA (some nat O) unit ZERO id.

Proof.
(* Goal: EQV (opt nat) OMEGA (some nat O) unit ZERO id *)
apply extensionality; unfold SUB in |- *; intros X A a H.
(* Direct inclusion *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
apply H; clear H; intros z H H1; apply H; clear H.
(* Case 1 (absurd) *)
(* Goal: forall (n n' : nat) (_ : eq (opt nat) (some nat O) (some nat n)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n) (_ : wf_nat n') (_ : lt n' n), ELT X A a unit ZERO id *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (some nat O) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), ELT X A a unit ZERO id *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat O) *)
intros n m H2 H3 Hn Hm H4.
(* Goal: ELT X A a unit ZERO id *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (some nat O) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), ELT X A a unit ZERO id *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat O) *)
generalize (eq_sym _ _ _ (eq_some_some _ _ _ H2)); intro H5.
(* Goal: ELT X A a unit ZERO id *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (some nat O) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), ELT X A a unit ZERO id *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat O) *)
apply (lt_n_O m (H5 (lt m) H4)).
(* Case 2 (absurd) *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (some nat O) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), ELT X A a unit ZERO id *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat O) *)
intros n H2 H3 Hn; apply (eq_some_none _ _ H2).
(* Converse inclusion *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat O) *)
apply H; clear H; intros u H H1; apply H.
Qed.

(** Inductive case: for any n:nat such that (wf_nat n), the pointed
    graph ((opt nat), OMEGA, (some nat (S n))) is bisimilar to the
    successor of the pointed graph ((opt nat), OMEGA, (some nat n)).
    Again, this is done by extensionality. *)

Lemma OMEGA_SUCC :
 forall n : nat,
 wf_nat n ->
 EQV (opt nat) OMEGA (some nat (S n)) (opt (opt nat))
   (SUCC (opt nat) OMEGA (some nat n)) (none (opt nat)).

Proof.
(* Goal: EQV (opt nat) OMEGA (some nat O) unit ZERO id *)
intros n Hn; apply extensionality; unfold SUB in |- *; intros X A a H.
(* Direct inclusion *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
apply H; clear H; intros z H H1; apply H; clear H.
(* Case 1 *)
(* Goal: forall (n0 n' : nat) (_ : eq (opt nat) (some nat n) (some nat n0)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n0) (_ : wf_nat n') (_ : lt n' n0), ELT X A a (opt nat) OMEGA (some nat (S n)) *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (some nat n) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), ELT X A a (opt nat) OMEGA (some nat (S n)) *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
intros n0 m H H2 Hn0 Hm H3.
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (some nat n) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), ELT X A a (opt nat) OMEGA (some nat (S n)) *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
generalize (eq_sym _ _ _ (eq_some_some _ _ _ H)); clear H; intro H.
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (some nat n) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), ELT X A a (opt nat) OMEGA (some nat (S n)) *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
generalize (H (lt m) H3); clear H H3 Hn0 n0; intro H3.
(* Case 1: Case disjunction on (lt m (S n)) *)
(* Goal: ELT X A a (opt (opt nat)) (SUCC (opt nat) OMEGA (some nat n)) (none (opt nat)) *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (some nat (S n)) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), ELT X A a (opt (opt nat)) (SUCC (opt nat) OMEGA (some nat n)) (none (opt nat)) *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
apply (lt_n_Sm m Hm n Hn H3); clear H3; intro H3.
(* Case 1a: (lt m n) *)
(* Goal: ELT X A a (opt (opt nat)) (SUCC (opt nat) OMEGA (some nat n)) (none (opt nat)) *)
(* Goal: ELT X A a (opt (opt nat)) (SUCC (opt nat) OMEGA (some nat n)) (none (opt nat)) *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (some nat (S n)) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), ELT X A a (opt (opt nat)) (SUCC (opt nat) OMEGA (some nat n)) (none (opt nat)) *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
apply SUCC_intro1; apply ELT_intro with (some nat m).
(* Goal: P (opt nat) OMEGA (some nat n) *)
exact (OMEGA_in m Hm n Hn H3).  apply H2; assumption.
(* Case 1b: (eq nat m n) *)
(* Goal: ELT X A a (opt (opt nat)) (SUCC (opt nat) OMEGA (some nat n)) (none (opt nat)) *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (some nat (S n)) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), ELT X A a (opt (opt nat)) (SUCC (opt nat) OMEGA (some nat n)) (none (opt nat)) *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
apply ELT_compat_l with (opt nat) OMEGA (some nat n).
(* Goal: P (opt nat) OMEGA (some nat n) *)
apply H3; apply H2; assumption.  apply SUCC_intro2.
(* Case 2 (absurd) *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (some nat n) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), ELT X A a (opt nat) OMEGA (some nat (S n)) *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
intros m H H2 Hm; apply (eq_some_none _ _ H).
(* Converse inclusion *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
apply (SUCC_elim _ _ _ _ _ _ H); clear H; intro H.
(* Case 1 *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
apply H; clear H; intros z H H1; apply H; clear H.
(* Case 1a *)
(* Goal: forall (n0 n' : nat) (_ : eq (opt nat) (some nat n) (some nat n0)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n0) (_ : wf_nat n') (_ : lt n' n0), ELT X A a (opt nat) OMEGA (some nat (S n)) *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (some nat n) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), ELT X A a (opt nat) OMEGA (some nat (S n)) *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
intros n0 m H H2 Hn0 Hm H3.
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (some nat n) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), ELT X A a (opt nat) OMEGA (some nat (S n)) *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
generalize (eq_sym _ _ _ (eq_some_some _ _ _ H)); clear H; intro H.
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (some nat n) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), ELT X A a (opt nat) OMEGA (some nat (S n)) *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
generalize (H (lt m) H3); clear H H3 Hn0 n0; intro H3.
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (some nat n) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), ELT X A a (opt nat) OMEGA (some nat (S n)) *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
apply ELT_intro with (some nat m).
(* Goal: OMEGA (some nat m) (some nat (S n)) *)
(* Goal: EQV X A a (opt nat) OMEGA (some nat m) *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (some nat n) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), ELT X A a (opt nat) OMEGA (some nat (S n)) *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
exact (OMEGA_in m Hm (S n) (wf_nat_S n Hn) (lt_S m n H3)).
(* Goal: P (opt nat) OMEGA (some nat n) *)
apply H2; assumption.
(* Case 1b (absurd) *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (some nat n) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), ELT X A a (opt nat) OMEGA (some nat (S n)) *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
intros m H H2 Hm; apply (eq_some_none _ _ H).
(* Case 2 *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
apply ELT_intro with (some nat n).
(* Goal: OMEGA (some nat n) (some nat (S n)) *)
(* Goal: EQV X A a (opt nat) OMEGA (some nat n) *)
exact (OMEGA_in n Hn (S n) (wf_nat_S n Hn) (lt_n_Sn n)).
(* Goal: P (opt nat) OMEGA (some nat n) *)
assumption.
Qed.

(** ** The axiom of infinity **)

(** The set denoted by the pointed graph ((opt nat), OMEGA, (none nat))
    contains zero (i.e. the empty set)... *)

Theorem omega_zero : ELT unit ZERO id (opt nat) OMEGA (none nat).

Proof.
(* Goal: ELT unit ZERO id (opt nat) OMEGA (none nat) *)
apply ELT_intro with (some nat O).
(* Goal: OMEGA (some nat O) (none nat) *)
(* Goal: EQV unit ZERO id (opt nat) OMEGA (some nat O) *)
exact (OMEGA_rt O wf_nat_O).
(* Goal: EQV unit ZERO id (opt nat) OMEGA (some nat O) *)
(* Goal: P unit ZERO id *)
(* Goal: forall (p : nat) (_ : wf_nat p) (_ : P (opt nat) OMEGA (some nat p)), P (opt nat) OMEGA (some nat (S p)) *)
apply EQV_sym; exact OMEGA_ZERO.
Qed.

(** ... and is closed under successor: *)

Theorem omega_succ :
 forall (X : Typ1) (A : Rel X) (a : X),
 ELT X A a (opt nat) OMEGA (none nat) ->
 ELT (opt X) (SUCC X A a) (none X) (opt nat) OMEGA (none nat).

Proof.
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
(* Goal: ELT X A a (opt nat) OMEGA (some nat (S n)) *)
intros X A a H; apply H; clear H; intros z H H1; apply H; clear H.
(* Case 1 (absurd) *)
(* Goal: forall (n n' : nat) (_ : eq (opt nat) (none nat) (some nat n)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n) (_ : wf_nat n') (_ : lt n' n), P X A a *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (none nat) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), P X A a *)
intros n m H H2 Hn Hm H3; apply (eq_none_some _ _ H).
(* Case 2 *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (none nat) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), ELT (opt X) (SUCC X A a) (none X) (opt nat) OMEGA (none nat) *)
intros n H0 H Hn; apply ELT_intro with (some nat (S n)).
(* Goal: OMEGA (some nat (S n)) (none nat) *)
(* Goal: EQV (opt X) (SUCC X A a) (none X) (opt nat) OMEGA (some nat (S n)) *)
exact (OMEGA_rt (S n) (wf_nat_S n Hn)).
apply
 EQV_trans
  with (opt (opt nat)) (SUCC (opt nat) OMEGA (some nat n)) (none (opt nat)).
(* Goal: P (opt nat) OMEGA (some nat n) *)
apply SUCC_compat; apply H; assumption.
(* Goal: P (opt nat) OMEGA (some nat n) *)
apply EQV_sym; apply OMEGA_SUCC; assumption.
Qed.

(** And we now check the induction principle on omega: *)

Require Import IZF_select.  (* For PRED and Compat *)

Theorem omega_ind
 :
 (* If P is a compatible predicate such that: *)
 forall P : PRED,
 Compat P ->
 (* 1. P holds for zero *)
 P unit ZERO id ->
 (* 2. If P holds for an element of omega, then
         P holds for the successor of this element *)
 (forall (X : Typ1) (A : Rel X) (a : X),
  ELT X A a (opt nat) OMEGA (none nat) ->
  P X A a -> P (opt X) (SUCC X A a) (none X)) ->
 (* Then: P holds for any element of omega *)
 forall (X : Typ1) (A : Rel X) (a : X),
 ELT X A a (opt nat) OMEGA (none nat) -> P X A a.

Proof.
(* Goal: forall (P : PRED) (_ : Compat P) (_ : P unit ZERO id) (_ : forall (X : Typ1) (A : Rel X) (a : X) (_ : ELT X A a (opt nat) OMEGA (none nat)) (_ : P X A a), P (opt X) (SUCC X A a) (none X)) (X : Typ1) (A : Rel X) (a : X) (_ : ELT X A a (opt nat) OMEGA (none nat)), P X A a *)
intros P HP HO HS X A a H; apply H; clear H.
(* Goal: forall (b' : opt nat) (_ : OMEGA b' (none nat)) (_ : EQV X A a (opt nat) OMEGA b'), P X A a *)
intros z H H1; apply H; clear H.
(* Case 1 (absurd) *)
(* Goal: forall (n n' : nat) (_ : eq (opt nat) (none nat) (some nat n)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n) (_ : wf_nat n') (_ : lt n' n), P X A a *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (none nat) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), P X A a *)
intros n m H H2 Hn Hm H3; apply (eq_none_some _ _ H).
(* Case 2 *)
(* Goal: forall (n' : nat) (_ : eq (opt nat) (none nat) (none nat)) (_ : eq (opt nat) z (some nat n')) (_ : wf_nat n'), P X A a *)
intros n H0 H Hn; clear H0.
(* Goal: P X A a *)
apply (HP _ _ _ _ _ _ (EQV_sym _ _ _ _ _ _ H1)).
(* Goal: P (opt nat) OMEGA z *)
apply (eq_sym _ _ _ H); clear H H1 a A X z.
(* Perform induction on n:nat *)
(* Goal: P (opt nat) OMEGA (some nat n) *)
apply (nat_ind' n Hn); clear Hn n.
(* Basic case *)
(* Goal: P (opt nat) OMEGA (some nat O) *)
(* Goal: forall (p : nat) (_ : wf_nat p) (_ : P (opt nat) OMEGA (some nat p)), P (opt nat) OMEGA (some nat (S p)) *)
apply HP with unit ZERO id.
(* Goal: P (opt nat) OMEGA (some nat n) *)
apply EQV_sym; exact OMEGA_ZERO. assumption.
(* Inductive case *)
(* Goal: forall (p : nat) (_ : wf_nat p) (_ : P (opt nat) OMEGA (some nat p)), P (opt nat) OMEGA (some nat (S p)) *)
intros n Hn Hind.
apply
 HP with (opt (opt nat)) (SUCC (opt nat) OMEGA (some nat n)) (none (opt nat)).
(* Goal: P (opt nat) OMEGA (some nat n) *)
apply EQV_sym; apply OMEGA_SUCC; assumption.
(* Goal: P (opt nat) OMEGA (some nat n) *)
apply HS. apply ELT_direct; apply OMEGA_rt; assumption.
(* Goal: P (opt nat) OMEGA (some nat n) *)
assumption.
Qed.
