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