Library GenModelSyntax
Require Import List.
Require Import Models.
Require Import TypeJudge.
Require GenModel.
Module MakeModel (M : CC_Model).
Include GenModel.MakeModel M.
Import T.
Import Term.
Fixpoint int_trm t :=
match t with
| Srt prop => T.prop
| Srt kind => T.kind
| Ref n => T.Ref n
| App u v => T.App (int_trm u) (int_trm v)
| Abs T M => T.Abs (int_trm T) (int_trm M)
| Prod T U => T.Prod (int_trm T) (int_trm U)
end.
Definition int_env := List.map int_trm.
Lemma int_lift : forall n t,
eq_term (int_trm (lift n t)) (T.lift n (int_trm t)).
Lemma int_subst : forall u t,
eq_term (int_trm (subst u t)) (T.subst (int_trm u) (int_trm t)).
Lemma int_not_kind : forall T, T <> Srt kind -> int_trm (unmark_app T) <> T.kind.
Hint Resolve int_not_kind eq_typ_not_kind.
Lemma int_sound : forall e M M' T,
eq_typ e M M' T ->
J.typ (int_env (unmark_env e)) (int_trm (unmark_app M)) (int_trm (unmark_app T)) /\
J.eq_typ (int_env (unmark_env e)) (int_trm (unmark_app M)) (int_trm (unmark_app M')).
Load "template/Library.v".
Lemma non_provability : forall T,
(forall x, ~ el (int_trm (unmark_app T)) vnil x) ->
forall M M', ~ eq_typ nil M M' T.
End MakeModel.
Require Import Models.
Require Import TypeJudge.
Require GenModel.
Module MakeModel (M : CC_Model).
Include GenModel.MakeModel M.
Import T.
Import Term.
Fixpoint int_trm t :=
match t with
| Srt prop => T.prop
| Srt kind => T.kind
| Ref n => T.Ref n
| App u v => T.App (int_trm u) (int_trm v)
| Abs T M => T.Abs (int_trm T) (int_trm M)
| Prod T U => T.Prod (int_trm T) (int_trm U)
end.
Definition int_env := List.map int_trm.
Lemma int_lift : forall n t,
eq_term (int_trm (lift n t)) (T.lift n (int_trm t)).
Lemma int_subst : forall u t,
eq_term (int_trm (subst u t)) (T.subst (int_trm u) (int_trm t)).
Lemma int_not_kind : forall T, T <> Srt kind -> int_trm (unmark_app T) <> T.kind.
Hint Resolve int_not_kind eq_typ_not_kind.
Lemma int_sound : forall e M M' T,
eq_typ e M M' T ->
J.typ (int_env (unmark_env e)) (int_trm (unmark_app M)) (int_trm (unmark_app T)) /\
J.eq_typ (int_env (unmark_env e)) (int_trm (unmark_app M)) (int_trm (unmark_app M')).
Load "template/Library.v".
Lemma non_provability : forall T,
(forall x, ~ el (int_trm (unmark_app T)) vnil x) ->
forall M M', ~ eq_typ nil M M' T.
End MakeModel.