Library GenModelSN
Require Import List Compare_dec.
Require Import Sat.
Require Import Models.
Require ObjectSN.
Module Lc := Lambda.
Require Import Sat.
Require Import Models.
Require ObjectSN.
Module Lc := Lambda.
Types are equipped with a saturated set
Parameter Real : X -> SAT.
Parameter Real_morph : Proper (eqX ==> eqSAT) Real.
Parameter Real_sort : eqSAT (Real props) snSAT.
Parameter Real_prod : ∀ A B,
eqSAT (Real (prod A B))
(prodSAT (Real A)
(interSAT (fun p:{y|y∈ A} => Real (B (proj1_sig p))))).
Parameter Real_morph : Proper (eqX ==> eqSAT) Real.
Parameter Real_sort : eqSAT (Real props) snSAT.
Parameter Real_prod : ∀ A B,
eqSAT (Real (prod A B))
(prodSAT (Real A)
(interSAT (fun p:{y|y∈ A} => Real (B (proj1_sig p))))).
Every proposition is inhabited
We use the generic model construction based on the
abstract model
Semantic typing relation
Definition in_int (i:val) (j:Lc.intt) (M T:trm) :=
M <> kind /\
match T with
| None => kind_ok M /\ Lc.sn (tm j M)
| _ => int i M ∈ int i T /\ inSAT (tm j M) (Real (int i T))
end.
Instance in_int_morph : Proper
(eq_val ==> pointwise_relation nat (@eq Lc.term) ==> eq_trm ==> eq_trm ==> iff)
in_int.
Qed.
Lemma in_int_not_kind : ∀ i j M T,
in_int i j M T ->
T <> kind ->
int i M ∈ int i T /\
inSAT (tm j M) (Real (int i T)).
Lemma in_int_intro : ∀ i j M T,
int i M ∈ int i T ->
inSAT (tm j M) (Real (int i T)) ->
M <> kind ->
T <> kind ->
in_int i j M T.
Lemma in_int_var0 : ∀ i j x t T,
x ∈ int i T ->
inSAT t (Real (int i T)) ->
T <> kind ->
in_int (V.cons x i) (I.cons t j) (Ref 0) (lift 1 T).
Lemma in_int_varS : ∀ i j x t n T,
in_int i j (Ref n) (lift (S n) T) ->
in_int (V.cons x i) (I.cons t j) (Ref (S n)) (lift (S (S n)) T).
Lemma in_int_sn : ∀ i j M T,
in_int i j M T -> Lc.sn (tm j M).
M <> kind /\
match T with
| None => kind_ok M /\ Lc.sn (tm j M)
| _ => int i M ∈ int i T /\ inSAT (tm j M) (Real (int i T))
end.
Instance in_int_morph : Proper
(eq_val ==> pointwise_relation nat (@eq Lc.term) ==> eq_trm ==> eq_trm ==> iff)
in_int.
Qed.
Lemma in_int_not_kind : ∀ i j M T,
in_int i j M T ->
T <> kind ->
int i M ∈ int i T /\
inSAT (tm j M) (Real (int i T)).
Lemma in_int_intro : ∀ i j M T,
int i M ∈ int i T ->
inSAT (tm j M) (Real (int i T)) ->
M <> kind ->
T <> kind ->
in_int i j M T.
Lemma in_int_var0 : ∀ i j x t T,
x ∈ int i T ->
inSAT t (Real (int i T)) ->
T <> kind ->
in_int (V.cons x i) (I.cons t j) (Ref 0) (lift 1 T).
Lemma in_int_varS : ∀ i j x t n T,
in_int i j (Ref n) (lift (S n) T) ->
in_int (V.cons x i) (I.cons t j) (Ref (S n)) (lift (S (S n)) T).
Lemma in_int_sn : ∀ i j M T,
in_int i j M T -> Lc.sn (tm j M).
Definition env := list trm.
Definition val_ok (e:env) (i:val) (j:Lc.intt) :=
∀ n T, nth_error e n = value T ->
in_int i j (Ref n) (lift (S n) T).
Lemma vcons_add_var : ∀ e T i j x t,
val_ok e i j ->
x ∈ int i T ->
inSAT t (Real (int i T)) ->
T <> kind ->
val_ok (T::e) (V.cons x i) (I.cons t j).
Lemma add_var_eq_fun : ∀ T U U' i,
(∀ x, x ∈ int i T -> int (V.cons x i) U == int (V.cons x i) U') ->
eq_fun (int i T)
(fun x => int (V.cons x i) U)
(fun x => int (V.cons x i) U').
Lemma vcons_add_var0 : ∀ e T i j x,
val_ok e i j ->
x ∈ int i T ->
T <> kind ->
val_ok (T::e) (V.cons x i) (I.cons SatSet.daimon j).
Definition val_ok (e:env) (i:val) (j:Lc.intt) :=
∀ n T, nth_error e n = value T ->
in_int i j (Ref n) (lift (S n) T).
Lemma vcons_add_var : ∀ e T i j x t,
val_ok e i j ->
x ∈ int i T ->
inSAT t (Real (int i T)) ->
T <> kind ->
val_ok (T::e) (V.cons x i) (I.cons t j).
Lemma add_var_eq_fun : ∀ T U U' i,
(∀ x, x ∈ int i T -> int (V.cons x i) U == int (V.cons x i) U') ->
eq_fun (int i T)
(fun x => int (V.cons x i) U)
(fun x => int (V.cons x i) U').
Lemma vcons_add_var0 : ∀ e T i j x,
val_ok e i j ->
x ∈ int i T ->
T <> kind ->
val_ok (T::e) (V.cons x i) (I.cons SatSet.daimon j).
Definition wf (e:env) :=
exists i, exists j, val_ok e i j.
Definition typ (e:env) (M T:trm) :=
∀ i j, val_ok e i j -> in_int i j M T.
Definition eq_typ (e:env) (M M':trm) :=
∀ i j, val_ok e i j -> int i M == int i M'.
Instance typ_morph : ∀ e, Proper (eq_trm ==> eq_trm ==> iff) (typ e).
Qed.
Instance eq_typ_morph : ∀ e, Proper (eq_trm ==> eq_trm ==> iff) (eq_typ e).
Qed.
exists i, exists j, val_ok e i j.
Definition typ (e:env) (M T:trm) :=
∀ i j, val_ok e i j -> in_int i j M T.
Definition eq_typ (e:env) (M M':trm) :=
∀ i j, val_ok e i j -> int i M == int i M'.
Instance typ_morph : ∀ e, Proper (eq_trm ==> eq_trm ==> iff) (typ e).
Qed.
Instance eq_typ_morph : ∀ e, Proper (eq_trm ==> eq_trm ==> iff) (eq_typ e).
Qed.
Lemma model_strong_normalization e M T :
wf e ->
typ e M T ->
Acc (transp _ red_term) M.
Definition typs e T :=
typ e T kind \/ typ e T prop.
Lemma typs_not_kind : ∀ e T, wf e -> typs e T -> T <> kind.
Lemma typs_kind_ok : ∀ e T i j,
typs e T ->
val_ok e i j ->
exists x, x ∈ int i T.
Lemma refl : ∀ e M, eq_typ e M M.
Lemma sym : ∀ e M M', eq_typ e M M' -> eq_typ e M' M.
Lemma trans : ∀ e M M' M'', eq_typ e M M' -> eq_typ e M' M'' -> eq_typ e M M''.
Instance eq_typ_setoid : ∀ e, Equivalence (eq_typ e).
Qed.
Lemma eq_typ_app : ∀ e M M' N N',
eq_typ e M M' ->
eq_typ e N N' ->
eq_typ e (App M N) (App M' N').
Lemma eq_typ_abs : ∀ e T T' M M',
eq_typ e T T' ->
eq_typ (T::e) M M' ->
T <> kind ->
eq_typ e (Abs T M) (Abs T' M').
Lemma eq_typ_prod : ∀ e T T' U U',
eq_typ e T T' ->
eq_typ (T::e) U U' ->
T <> kind ->
eq_typ e (Prod T U) (Prod T' U').
Lemma eq_typ_beta : ∀ e T M M' N N',
eq_typ (T::e) M M' ->
eq_typ e N N' ->
typ e N T ->
T <> kind ->
eq_typ e (App (Abs T M) N) (subst N' M').
Lemma typ_prop : ∀ e, typ e prop kind.
Lemma typ_var : ∀ e n T,
nth_error e n = value T -> typ e (Ref n) (lift (S n) T).
Lemma typ_app : ∀ e u v V Ur,
typ e v V ->
typ e u (Prod V Ur) ->
V <> kind ->
Ur <> kind ->
typ e (App u v) (subst v Ur).
Lemma typ_abs : ∀ e T M U,
typs e T ->
typ (T :: e) M U ->
U <> kind ->
typ e (Abs T M) (Prod T U).
Lemma typ_beta : ∀ e T M N U,
typs e T ->
typ (T::e) M U ->
typ e N T ->
T <> kind ->
U <> kind ->
typ e (App (Abs T M) N) (subst N U).
Lemma typ_prod : ∀ e T U s2,
s2 = kind \/ s2 = prop ->
typs e T ->
typ (T :: e) U s2 ->
typ e (Prod T U) s2.
Lemma typ_conv : ∀ e M T T',
typ e M T ->
eq_typ e T T' ->
T <> kind ->
T' <> kind ->
typ e M T'.
End MakeModel.