# 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).