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

Module Lam.
Section LambdaTerms.

  Variable A : set.

  Definition LAMf (X:set) :=
    prodcart (singl zero) N ∪
    prodcart (singl (succ zero)) A ∪
    (prodcart (singl (succ (succ zero))) (prodcart X X) ∪
     prodcart (singl (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 : ∀ X (P : set -> Prop),
    Proper (eq_set ==> iff) P ->
    (∀ n, n ∈ N -> P (Var n)) ->
    (∀ x, x ∈ A -> P (Cst x)) ->
    (∀ a b, a ∈ X -> b ∈ X -> P (App a b)) ->
    (∀ a, a ∈ X -> P (Abs a)) ->
    ∀ a, a ∈ LAMf X -> P a.
  Lemma Var_typ : ∀ X n,
    n ∈ N -> Var n ∈ LAMf X.

  Lemma Cst_typ : ∀ X x,
    x ∈ A -> Cst x ∈ LAMf X.

  Lemma App_typ : ∀ X a b,
    a ∈ X -> b ∈ X -> App a b ∈ LAMf X.

  Lemma Abs_typ : ∀ X a,
    a ∈ X -> Abs a ∈ LAMf X.

Require Import ZFrepl ZFfix.

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

  Lemma Lamn_incl_succ : ∀ k, Lamn k ⊆ Lamn (S k).

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

  Lemma Lamn_incl : ∀ k k', (k <= k')%nat -> Lamn k ⊆ Lamn k'.

  Definition Lambda := TI LAMf omega.

  Lemma Lambda_intro : ∀ k, Lamn k ⊆ Lambda.

  Lemma Lambda_elim : ∀ x,
    x ∈ Lambda -> exists k, x ∈ Lamn k.

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

  Lemma Lambda_fix : ∀ (P:set->Prop),
    (∀ k,
     (∀ k' x, (k' < k)%nat -> x ∈ Lamn k' -> P x) ->
     (∀ x, x ∈ Lamn k -> P x)) ->
    ∀ x, x ∈ Lambda -> P x.

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

  Lemma Lambda_eqn : Lambda == LAMf Lambda.

  Lemma Var_typ0 : ∀ n,
    n ∈ N -> Var n ∈ Lambda.

  Lemma Cst_typ0 : ∀ x,
    x ∈ A -> Cst x ∈ Lambda.

  Lemma App_typ0 : ∀ a b,
    a ∈ Lambda -> b ∈ Lambda -> App a b ∈ Lambda.

  Lemma Abs_typ0 : ∀ a,
    a ∈ Lambda -> Abs a ∈ 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 : ∀ t, iLAM t ∈ 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 : ∀ t u,
  iLAM t == iLAM u -> t=u.

Lemma interSAT_ax : ∀ A F u,
    A ->
    ((∀ 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|∀ t, sn t -> P t -> inSAT t S} => proj1_sig p).

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

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

Qed.

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

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

Lemma replSAT_ax : ∀ f z,
  Proper (eqSAT ==> eq_set) f ->
  (z ∈ replSAT f <-> exists A, z == f A).