Library SN_CC

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



Module CCSN.

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

Definition piSAT A (F:set->SAT) :=
  prodSAT (Red A) (interSAT (fun p:{y|y \in 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 => Red (F x))).

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

Lemma sn_prod_intro : forall dom f F,
  ext_fun (El dom) f ->
  ext_fun (El dom) F ->
  (forall x, x \in El dom -> f x \in El (F x)) ->
  sn_lam dom f \in El (sn_prod dom F).

Lemma sn_prod_elim : forall dom f x F,
  f \in El (sn_prod dom F) ->
  x \in El dom ->
  cc_app f x \in El (F x).

Lemma cc_impredicative_prod_non_empty : forall dom F,
  ext_fun dom F ->
  (forall x, x \in 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 : forall dom F,
  ext_fun (El dom) F ->
  (forall x, x \in El dom -> F x \in El sn_props) ->
  sn_prod dom F \in El sn_props.

  Lemma sn_proof_of_false : prf_trm \in 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 \in 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 \in y" := (inX x y) (at level 60).
Notation "x == y" := (eqX x y) (at level 70).

Definition eq_fun (x:X) (f1 f2:X->X) :=
  forall y1 y2, y1 \in x -> y1 == y2 -> f1 y1 == f2 y2.

Lemma lam_ext :
  forall 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 :
  forall x1 x2 f1 f2,
  x1 == x2 ->
  eq_fun x1 f1 f2 ->
  prod x1 f1 == prod x2 f2.

Lemma prod_intro : forall dom f F,
  eq_fun dom f f ->
  eq_fun dom F F ->
  (forall x, x \in dom -> f x \in F x) ->
  lam dom f \in prod dom F.
Lemma prod_elim : forall dom f x F,
  eq_fun dom F F ->
  f \in prod dom F ->
  x \in dom ->
  app f x \in F x.

Lemma impredicative_prod : forall dom F,
  eq_fun dom F F ->
  (forall x, x \in dom -> F x \in props) ->
  prod dom F \in props.
Lemma beta_eq:
  forall dom F x,
  eq_fun dom F F ->
  x \in dom ->
  app (lam dom F) x == F x.

End SN_CC_Model.

Import SN_CC_Model.


Module SN_CC_addon.

  Definition Red : X -> SAT := Red.

  Lemma Red_morph : Proper (eqX ==> eqSAT) Red.

  Lemma Red_sort : eqSAT (Red props) snSAT.

  Lemma Red_prod : forall A B,
    eqSAT (Red (prod A B))
     (prodSAT (Red A)
        (interSAT (fun p:{y|y\in A} => Red (B (proj1_sig p))))).

  Definition daemon := empty.

  Lemma daemon_false : daemon \in prod props (fun P => P).
End SN_CC_addon.


Require GenModelSN TypeJudge.

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

Module SN := GenModelSN.MakeModel SN_CC_Model SN_CC_addon.

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 : forall n t k,
  eq_trm (lift_rec n k (int_trm t)) (int_trm (Tm.lift_rec n t k)).

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

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

Lemma int_subst : forall 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 : forall T, T <> Tm.Srt Tm.kind -> interp T <> kind.

End LiftAndSubstEquiv.

Hint Resolve int_not_kind Ty.eq_typ_not_kind.


Lemma int_sound : forall 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 : forall e, Ty.wf e -> SN.wf (int_env e).

Lemma interp_sound : forall 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).


Hint Resolve Lc.redp_app_r Lc.redp_app_l Lc.redp_abs
  Lc.redp_lift_rec.

Lemma tm_red1 : forall x y,
  Tm.red1 x y -> ~ Tm.mem_sort Tm.kind x ->
  forall j, Lc.redp (SN.tm j (int_trm x)) (SN.tm j (int_trm y)).

Lemma clos_trans_transp : forall A R x y,
  clos_trans A R x y ->
  clos_trans A (transp _ R) y x.

Lemma sn_tm : forall t j,
  ~ Tm.mem_sort Tm.kind t -> Lc.sn (SN.tm j (int_trm t)) -> Tm.sn t.

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

Print Assumptions strong_normalization.