Library GenModel
Require Import Models List.
Module MakeModel(M : CC_Model).
Import M.
Lemma eq_fun_sym : forall x f1 f2, eq_fun x f1 f2 -> eq_fun x f2 f1.
Lemma eq_fun_trans : forall x f1 f2 f3,
eq_fun x f1 f2 -> eq_fun x f2 f3 -> eq_fun x f1 f3.
Module Xeq.
Definition t := X.
Definition eq := eqX.
Definition eq_equiv : Equivalence eq := eqX_equiv.
End Xeq.
Require Import VarMap.
Module V := VarMap.Make(Xeq).
Notation val := V.map.
Notation eq_val := V.eq_map.
Instance eq_val_equiv : Equivalence eq_val.
Definition vnil : val := V.nil props.
Import V.
Module T.
Definition term :=
option {f:val -> X|Proper (eq_val ==> eqX) f}.
Definition eq_term (x y:term) :=
match x, y with
| Some f, Some g => (eq_val ==> eqX)%signature (proj1_sig f) (proj1_sig g)
| None, None => True
| _, _ => False
end.
Instance eq_term_refl : Reflexive eq_term.
Qed.
Instance eq_term_sym : Symmetric eq_term.
Qed.
Instance eq_term_trans : Transitive eq_term.
Qed.
Definition int (t:term) (i:val) : X :=
match t with
| Some f => proj1_sig f i
| None => props
end.
Instance int_morph : Proper (eq_term ==> eq_val ==> eqX) int.
Qed.
Definition el (t:term) (i:val) (x:X) :=
match t with
| Some f => x \in proj1_sig f i
| None => True
end.
Instance el_morph : Proper (eq_term ==> eq_val ==> eqX ==> iff) el.
Qed.
Definition cst (x:X) : term.
Defined.
Definition prop := cst props.
Definition kind : term := None.
Hint Unfold eq_val.
Definition Ref (n:nat) : term.
Defined.
Definition App (u v:term) : term.
Defined.
Instance App_morph : Proper (eq_term ==> eq_term ==> eq_term) App.
Qed.
Definition Abs (A M:term) : term.
Defined.
Instance Abs_morph : Proper (eq_term ==> eq_term ==> eq_term) Abs.
Qed.
Definition Prod (A B:term) : term.
Defined.
Instance Prod_morph : Proper (eq_term ==> eq_term ==> eq_term) Prod.
Qed.
Section Lift.
Definition lift_rec (n m:nat) (t:term) : term.
Defined.
Definition lift1 n := lift_rec n 1.
Lemma lift10: forall T, eq_term (lift1 0 T) T.
Lemma int_lift_rec_eq : forall n k T i,
int (lift_rec n k T) i == int T (V.lams k (V.shift n) i).
Definition lift n := lift_rec n 0.
Instance lift_morph : forall k, Proper (eq_term ==> eq_term) (lift k).
Qed.
Lemma lift0_term : forall T, eq_term (lift 0 T) T.
Lemma simpl_int_lift : forall i n x T,
int (lift (S n) T) (V.cons x i) == int (lift n T) i.
Lemma simpl_int_lift1 : forall i x T,
int (lift 1 T) (V.cons x i) == int T i.
Lemma simpl_lift1 : forall i n x y T,
int (lift1 (S n) T) (V.cons x (V.cons y i)) == int (lift1 n T) (V.cons x i).
End Lift.
Section Substitution.
Definition subst_rec (arg:term) (m:nat) (t:term) : term.
Defined.
Lemma int_subst_rec_eq : forall arg k T i,
int (subst_rec arg k T) i == int T (V.lams k (V.cons (int arg (V.shift k i))) i).
Definition subst arg := subst_rec arg 0.
Instance subst_morph : Proper (eq_term ==> eq_term ==> eq_term) subst.
Qed.
Lemma int_subst_eq : forall N M i,
int (subst N M) i == int M (V.cons (int N i) i).
Lemma el_subst_eq : forall N M i x,
el (subst N M) i x <-> el M (V.cons (int N i) i) x.
End Substitution.
End T.
Import T.
Definition env := list term.
Definition val_ok (e:env) (i:val) :=
forall n T, nth_error e n = value T -> el (lift (S n) T) i (i n).
Lemma vcons_add_var0 : forall e T i x,
val_ok e i -> el T i x -> val_ok (T::e) (V.cons x i).
Lemma vcons_add_var : forall e T i x,
val_ok e i -> x \in int T i -> val_ok (T::e) (V.cons x i).
Lemma add_var_eq_fun : forall T U U' i,
(forall x, el T i x -> int U (V.cons x i) == int U' (V.cons x i)) ->
eq_fun (int T i)
(fun x => int U (V.cons x i))
(fun x => int U' (V.cons x i)).
Module J.
Definition typ (e:env) (M T:term) :=
forall i, val_ok e i -> el T i (int M i).
Definition eq_typ (e:env) (M M':term) :=
forall i, val_ok e i -> int M i == int M' i.
Definition sub_typ (e:env) (M M':term) :=
forall i x, val_ok e i -> x \in int M i -> x\in int M' i.
Instance typ_morph : forall e, Proper (eq_term ==> eq_term ==> iff) (typ e).
Qed.
Instance eq_typ_morph : forall e, Proper (eq_term ==> eq_term ==> iff) (eq_typ e).
Qed.
Instance sub_typ_morph : forall e, Proper (eq_term ==> eq_term ==> iff) (sub_typ e).
Qed.
End J.
Import J.
Module R.
Lemma refl : forall e M, eq_typ e M M.
Lemma sym : forall e M M', eq_typ e M M' -> eq_typ e M' M.
Lemma trans : forall e M M' M'', eq_typ e M M' -> eq_typ e M' M'' -> eq_typ e M M''.
Instance eq_typ_equiv : forall e, Equivalence (eq_typ e).
Qed.
Lemma eq_typ_app : forall 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 : forall e T T' M M',
eq_typ e T T' ->
eq_typ (T::e) M M' ->
eq_typ e (Abs T M) (Abs T' M').
Lemma eq_typ_prod : forall e T T' U U',
eq_typ e T T' ->
eq_typ (T::e) U U' ->
eq_typ e (Prod T U) (Prod T' U').
Lemma eq_typ_beta : forall 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 : forall e, typ e prop kind.
Lemma typ_var : forall e n T,
nth_error e n = value T -> typ e (Ref n) (lift (S n) T).
Lemma typ_app : forall e u v V Ur,
typ e v V ->
typ e u (Prod V Ur) ->
V <> kind ->
typ e (App u v) (subst v Ur).
Lemma typ_abs : forall e T M U,
typ (T :: e) M U ->
U <> kind ->
typ e (Abs T M) (Prod T U).
Lemma typ_beta : forall e T M N U,
typ e N T ->
typ (T::e) M U ->
T <> kind ->
U <> kind ->
typ e (App (Abs T M) N) (subst N U).
Lemma typ_prod : forall e T U s2,
s2 = kind \/ s2 = prop ->
typ (T :: e) U s2 ->
typ e (Prod T U) s2.
Lemma typ_conv : forall e M T T',
typ e M T ->
eq_typ e T T' ->
T <> kind ->
typ e M T'.
Lemma sub_refl : forall e M M',
eq_typ e M M' -> sub_typ e M M'.
Lemma sub_trans : forall e M1 M2 M3,
sub_typ e M1 M2 -> sub_typ e M2 M3 -> sub_typ e M1 M3.
Lemma typ_subsumption : forall e M T T',
typ e M T ->
sub_typ e T T' ->
T <> kind ->
typ e M T'.
End R.
End MakeModel.