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_rec : ∀ n t k,
  eq_term (T.lift_rec n k (int_trm t)) (int_trm (Term.lift_rec n t k)).

Lemma int_lift : ∀ n t,
  eq_term (int_trm (lift n t)) (T.lift n (int_trm t)).

Lemma int_subst_rec : ∀ arg,
  int_trm arg <> T.kind ->
  ∀ t k,
  eq_term (T.subst_rec (int_trm arg) k (int_trm t)) (int_trm (subst_rec arg t k)).

Lemma int_subst : ∀ u t,
  int_trm u <> T.kind ->
  eq_term (int_trm (subst u t)) (T.subst (int_trm u) (int_trm t)).

Lemma int_not_kind : ∀ T, T <> Srt kind -> int_trm (unmark_app T) <> T.kind.

Hint Resolve int_not_kind eq_typ_not_kind.

Lemma int_sound : ∀ 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 : ∀ T,
    (∀ x, ~ el (int_trm (unmark_app T)) vnil x) ->
    ∀ M M', ~ eq_typ nil M M' T.

End MakeModel.