Library ZFlambda

Require Import Lambda.
Require Import ZF ZFpairs ZFnats ZFord.
Import IZF.
Require Import Sat.
Require Import Setoid Compare_dec Wf_nat.


Module Lam.
Section LambdaTerms.

  Variable A : set.

  Definition LAMf (X:set) :=
    union2
     (union2
       (replf N (fun n => couple zero n))
       (replf A (fun x => couple (succ zero) x)))
     (union2
       (replf (prodcart X X) (fun p => couple (succ (succ zero)) p))
       (replf X (fun x => couple (succ (succ (succ zero))) x))).

Instance LAMf_mono : Proper (incl_set ==> incl_set) LAMf.




Qed.

Instance LAMf_morph : Proper (eq_set ==> eq_set) LAMf.

Qed.

  Definition Var n := couple zero n.
  Definition Cst x := couple (succ zero) x.
  Definition App a b := couple (succ (succ zero)) (couple a b).
  Definition Abs a := couple (succ (succ (succ zero))) a.

  Lemma LAMf_ind : forall X (P : set -> Prop),
    Proper (eq_set ==> iff) P ->
    (forall n, n \in N -> P (Var n)) ->
    (forall x, x \in A -> P (Cst x)) ->
    (forall a b, a \in X -> b \in X -> P (App a b)) ->
    (forall a, a \in X -> P (Abs a)) ->
    forall a, a \in LAMf X -> P a.

  Lemma Var_typ : forall X n,
    n \in N -> Var n \in LAMf X.

  Lemma Cst_typ : forall X x,
    x \in A -> Cst x \in LAMf X.

  Lemma App_typ : forall X a b,
    a \in X -> b \in X -> App a b \in LAMf X.

  Lemma Abs_typ : forall X a,
    a \in X -> Abs a \in LAMf X.

Require Import ZFrepl ZFfix.

  Definition Lamn n := TI LAMf (nat2ordset n).

  Lemma Lamn_incl_succ : forall k, Lamn k \incl Lamn (S k).

  Lemma Lamn_eq : forall k, Lamn (S k) == LAMf (Lamn k).

  Lemma Lamn_incl : forall k k', k <= k' -> Lamn k \incl Lamn k'.

  Definition Lambda := TI LAMf omega.

  Lemma Lambda_intro : forall k, Lamn k \incl Lambda.

  Lemma Lambda_elim : forall x,
    x \in Lambda -> exists k, x \in Lamn k.

  Lemma Lamn_case : forall k (P : set -> Prop),
    Proper (eq_set ==> iff) P ->
    (forall n, n \in N -> P (Var n)) ->
    (forall x, x \in A -> P (Cst x)) ->
    (forall a b k', k' < k -> a \in Lamn k' -> b \in Lamn k' -> P (App a b)) ->
    (forall a k', k' < k -> a \in Lamn k' -> P (Abs a)) ->
    forall a, a \in Lamn k -> P a.

  Lemma Lambda_fix : forall (P:set->Prop),
    (forall k,
     (forall k' x, k' < k -> x \in Lamn k' -> P x) ->
     (forall x, x \in Lamn k -> P x)) ->
    forall x, x \in Lambda -> P x.

  Lemma Lambda_ind : forall P : set -> Prop,
    Proper (eq_set ==> iff) P ->
    (forall n, n \in N -> P (Var n)) ->
    (forall x, x \in A -> P (Cst x)) ->
    (forall a b, a \in Lambda -> b \in Lambda -> P a -> P b -> P (App a b)) ->
    (forall a, a \in Lambda -> P a -> P (Abs a)) ->
    forall a, a \in Lambda -> P a.

  Lemma Lambda_eqn : Lambda == LAMf Lambda.

  Lemma Var_typ0 : forall n,
    n \in N -> Var n \in Lambda.

  Lemma Cst_typ0 : forall x,
    x \in A -> Cst x \in Lambda.

  Lemma App_typ0 : forall a b,
    a \in Lambda -> b \in Lambda -> App a b \in Lambda.

  Lemma Abs_typ0 : forall a,
    a \in Lambda -> Abs a \in Lambda.

End LambdaTerms.
End Lam.

Import Lam.
Import Lambda.

Definition CCLam := Lambda zero.

Fixpoint iLAM (t:term) :=
  match t with
  | Ref n => Lam.Var (nat2set n)
  | Abs M => Lam.Abs (iLAM M)
  | App u v => Lam.App (iLAM u) (iLAM v)
  end.

Lemma iLAM_typ : forall t, iLAM t \in CCLam.

Ltac inj_pre H :=
  unfold Var, Cst, Lam.App, Lam.Abs in H;
  change (succ (succ (succ zero))) with (nat2set 3) in H;
  change (succ (succ zero)) with (nat2set 2) in H;
  change (succ zero) with (nat2set 1) in H;
  change zero with (nat2set 0) in H.

Ltac inj_lam H :=
  (apply nat2set_inj in H; try discriminate H) ||
  (apply couple_injection in H;
   let H2 := fresh "H" in
   destruct H as (H,H2); inj_lam H; inj_lam H2) ||
  idtac.

Ltac injl H := inj_pre H; inj_lam H.

Lemma iLAM_inj : forall t u,
  iLAM t == iLAM u -> t=u.

Lemma interSAT_ax : forall A F u,
    A ->
    ((forall x:A, inSAT u (F x)) <->
     inSAT u (interSAT F)).

Definition iSAT S :=
  subset CCLam (fun x => exists2 t, inSAT t S & x == iLAM t).

Instance iSAT_morph : Proper (eqSAT ==> eq_set) iSAT.


Qed.

Definition complSAT (P:term->Prop) :=
  interSAT (fun p:{S|forall t, sn t -> P t -> inSAT t S} => proj1_sig p).

Definition sSAT x :=
  complSAT (fun t => iLAM t \in x).

Instance sSAT_morph : Proper (eq_set ==> eqSAT) sSAT.

Qed.

Lemma iSAT_id : forall S, eqSAT (sSAT (iSAT S)) S.

Definition replSAT F :=
  repl (power CCLam) (fun P y => y == F (sSAT P)).

Lemma replSAT_ax : forall f z,
  Proper (eqSAT ==> eq_set) f ->
  (z \in replSAT f <-> exists A, z == f A).