Require Export Relations Wellfounded Compare_dec.
Require Import Sat.
Require Import ZF ZFcoc.
Require Import ZFlambda.

Module CCSN.

Definition mkTY x S := couple x (iSAT S).
Definition El T := fst T.
Definition Real T := sSAT (snd T) .

Definition piSAT A (F:set->SAT) :=
  prodSAT (Real A) (interSAT (fun p:{y|y ∈ El A} => F (proj1_sig p))).

Definition sn_prod A F :=
  mkTY (cc_prod (El A) (fun x => El (F x)))
       (piSAT A (fun x => Real (F x))).

Definition sn_lam A F := cc_lam (El A) F.

Lemma sn_prod_intro : ∀ dom f F,
  ext_fun (El dom) f ->
  ext_fun (El dom) F ->
  (∀ x, x ∈ El dom -> f x ∈ El (F x)) ->
  sn_lam dom f ∈ El (sn_prod dom F).

Lemma sn_prod_elim : ∀ dom f x F,
  f ∈ El (sn_prod dom F) ->
  x ∈ El dom ->
  cc_app f x ∈ El (F x).

Lemma cc_impredicative_prod_non_empty : ∀ dom F,
  ext_fun dom F ->
  (∀ x, x ∈ dom -> F x == singl prf_trm) ->
  cc_prod dom F == singl prf_trm.

Definition sn_props :=
  mkTY (replSAT(fun A => mkTY (singl prf_trm) A)) snSAT.

Lemma prop_repl_morph :
  Proper (eqSAT ==> eq_set) (fun A => couple (singl prf_trm) (iSAT A)).
Hint Resolve prop_repl_morph.

Lemma sn_impredicative_prod : ∀ dom F,
  ext_fun (El dom) F ->
  (∀ x, x ∈ El dom -> F x ∈ El sn_props) ->
  sn_prod dom F ∈ El sn_props.

  Lemma sn_proof_of_false : prf_trm ∈ El (sn_prod sn_props (fun P => P)).

End CCSN.
Import CCSN.

Require Import Models.
Module SN_CC_Model <: CC_Model.

Definition X := set.
Definition inX x y := x ∈ El y.
Definition eqX := eq_set.
Lemma eqX_equiv : Equivalence eqX.
Lemma in_ext: Proper (eqX ==> eqX ==> iff) inX.

Definition props := sn_props.
Definition app := cc_app.
Definition lam := sn_lam.
Definition prod := sn_prod.

Notation "x ∈ y" := (inX x y).
Notation "x == y" := (eqX x y).

Definition eq_fun (x:X) (f1 f2:X->X) :=
  ∀ y1 y2, y1 ∈ x -> y1 == y2 -> f1 y1 == f2 y2.

Lemma lam_ext :
  ∀ x1 x2 f1 f2,
  x1 == x2 ->
  eq_fun x1 f1 f2 ->
  lam x1 f1 == lam x2 f2.

Lemma app_ext: Proper (eqX ==> eqX ==> eqX) app.
Lemma prod_ext :
  ∀ x1 x2 f1 f2,
  x1 == x2 ->
  eq_fun x1 f1 f2 ->
  prod x1 f1 == prod x2 f2.

Lemma prod_intro : ∀ dom f F,
  eq_fun dom f f ->
  eq_fun dom F F ->
  (∀ x, x ∈ dom -> f x ∈ F x) ->
  lam dom f ∈ prod dom F.
Lemma prod_elim : ∀ dom f x F,
  eq_fun dom F F ->
  f ∈ prod dom F ->
  x ∈ dom ->
  app f x ∈ F x.

Lemma impredicative_prod : ∀ dom F,
  eq_fun dom F F ->
  (∀ x, x ∈ dom -> F x ∈ props) ->
  prod dom F ∈ props.
Lemma beta_eq:
  ∀ dom F x,
  eq_fun dom F F ->
  x ∈ dom ->
  app (lam dom F) x == F x.

End SN_CC_Model.

Import SN_CC_Model.

Module SN_CC_addon.

  Definition Real : X -> SAT := Real.

  Lemma Real_morph : Proper (eqX ==> eqSAT) Real.

  Lemma Real_sort : eqSAT (Real props) snSAT.

  Lemma Real_prod : ∀ A B,
    eqSAT (Real (prod A B))
     (prodSAT (Real A)
        (interSAT (fun p:{y|y∈ A} => Real (B (proj1_sig p))))).

  Definition daimon := empty.

  Lemma daimon_false : daimon ∈ prod props (fun P => P).
End SN_CC_addon.


Require GenModelSN.
Module SN := GenModelSN.MakeModel SN_CC_Model SN_CC_addon.

Definition cst (x:set) : SN.trm.
Defined.

Definition mkSET (x:set) := cst (mkTY x snSAT).

Lemma mkSET_kind e x :
  (exists w, in_set w x) ->
  SN.typ e (mkSET x) SN.kind.

Lemma cst_typ e x y :
  in_set x y ->
  SN.typ e (cst x) (mkSET y).

Lemma cst_typ_inv x y :
  SN.typ nil (cst x) (mkSET y) ->
  in_set x y.

Lemma cst_eq_typ e x y :
  x == y ->
  SN.eq_typ e (cst x) (cst y).

Lemma cst_eq_typ_inv x y :
  SN.eq_typ nil (cst x) (cst y) ->
  x == y.

Lemma mkSET_eq_typ e x y :
  x == y ->
  SN.eq_typ e (mkSET x) (mkSET y).

Lemma mkSET_eq_typ_inv x y :
  SN.eq_typ nil (mkSET x) (mkSET y) ->
  x == y.

Require TypeJudge.
Module Ty := TypeJudge.
Module Tm := Term.
Module Lc := Lambda.

Fixpoint int_trm t :=
  match t with
  | Tm.Srt Tm.prop => SN.prop
  | Tm.Srt Tm.kind => SN.kind
  | Tm.Ref n => SN.Ref n
  | Tm.App u v => SN.App (int_trm u) (int_trm v)
  | Tm.Abs T M => SN.Abs (int_trm T) (int_trm M)
  | Tm.Prod T U => SN.Prod (int_trm T) (int_trm U)
  end.
Definition interp t := int_trm (Ty.unmark_app t).
Definition int_env := List.map interp.

Section LiftAndSubstEquiv.

Import SN.

Lemma int_lift_rec : ∀ n t k,
  eq_trm (lift_rec n k (int_trm t)) (int_trm (Tm.lift_rec n t k)).

Lemma int_lift : ∀ n t,
  eq_trm (int_trm (Tm.lift n t)) (lift n (int_trm t)).

Lemma int_subst_rec : ∀ arg,
  int_trm arg <> kind ->
  ∀ t k,
  eq_trm (subst_rec (int_trm arg) k (int_trm t)) (int_trm (Tm.subst_rec arg t k)).

Lemma int_subst : ∀ u t,
  int_trm u <> kind ->
  eq_trm (int_trm (Tm.subst u t)) (subst (int_trm u) (int_trm t)).

Lemma int_not_kind : ∀ T, T <> Tm.Srt Tm.kind -> interp T <> kind.

End LiftAndSubstEquiv.
Lemma red1_sound : ∀ x y,
  Tm.red1 x y -> ~ Tm.mem_sort Tm.kind x ->
  SN.red_term (int_trm x) (int_trm y).

Lemma sn_sound : ∀ M,
  Acc (transp _ SN.red_term) (interp M) ->
  ~ Tm.mem_sort Tm.kind (Ty.unmark_app M) ->
  Tm.sn (Ty.unmark_app M).

Hint Resolve int_not_kind Ty.eq_typ_not_kind.

Lemma int_sound : ∀ e M M' T,
  Ty.eq_typ e M M' T ->
  SN.typ (int_env e) (interp M) (interp T) /\
  SN.eq_typ (int_env e) (interp M) (interp M').

  Lemma interp_wf : ∀ e, Ty.wf e -> SN.wf (int_env e).

Lemma interp_sound : ∀ e M M' T,
  Ty.eq_typ e M M' T ->
  SN.wf (int_env e) /\ SN.typ (int_env e) (interp M) (interp T).

Lemma strong_normalization : ∀ e M M' T,
  Ty.eq_typ e M M' T ->
  Tm.sn (Ty.unmark_app M).

Print Assumptions strong_normalization.