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)).
induction t; intros.
destruct s; simpl; trivial.
red; intros; reflexivity.
simpl; unfold V.lams, V.shift.
destruct (le_gt_dec k n0); simpl.
replace (k+(n+(n0-k))) with (n+n0) by omega.
red; auto.
red; auto.
simpl; red; intros.
apply M.lam_ext; intros.
rewrite H; rewrite <- IHt1.
rewrite int_lift_rec_eq.
reflexivity.
red; intros.
rewrite H; rewrite <- IHt2.
rewrite int_lift_rec_eq.
rewrite V.cons_lams; eauto with *.
rewrite H1; reflexivity.
simpl; red; intros.
do 2 rewrite <- int_lift_rec_eq.
rewrite H; rewrite IHt1; rewrite IHt2; reflexivity.
simpl; red; intros.
apply M.prod_ext; intros.
rewrite H; rewrite <- IHt1.
rewrite int_lift_rec_eq.
reflexivity.
red; intros.
rewrite H; rewrite <- IHt2.
rewrite int_lift_rec_eq.
rewrite V.cons_lams; eauto with *.
rewrite H1; reflexivity.
Qed.
Lemma int_lift : ∀ n t,
eq_term (int_trm (lift n t)) (T.lift n (int_trm t)).
intros.
unfold lift, T.lift.
symmetry; apply int_lift_rec.
Qed.
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)).
intros arg not_knd.
induction t; intros.
destruct s; simpl; trivial.
red; intros; reflexivity.
simpl subst_rec.
destruct (lt_eq_lt_dec k n) as [[fv|eqv]|bv]; simpl.
simpl; unfold V.lams, V.shift;
destruct (le_gt_dec k n); try (apply False_ind; omega; fail).
replace (n-k) with (S(pred n-k)) by omega; simpl.
replace (k+(pred n-k)) with (pred n) by omega; red; auto.
case_eq (int_trm (lift k arg)); [intros (a,am) arg_eq;simpl|intro arg_eq].
red; intros.
subst k.
unfold V.lams; simpl.
destruct (le_gt_dec n n).
2:apply False_ind; omega.
replace (n-n) with 0; auto with arith; simpl.
setoid_replace (V.shift n x) with (V.lams 0 (V.shift n) x).
2:symmetry; apply V.lams0.
rewrite <- int_lift_rec_eq.
fold (T.lift n (int_trm arg)).
rewrite <- int_lift.
rewrite arg_eq; simpl.
apply am.
exact H.
destruct arg; simpl; try discriminate.
destruct s.
elim not_knd; reflexivity.
discriminate.
simpl; unfold V.lams, V.shift;
destruct (le_gt_dec k n); try (apply False_ind; omega; fail).
red; intros; auto.
simpl; red; intros.
apply M.lam_ext.
rewrite H; rewrite <- IHt1.
rewrite int_subst_rec_eq.
reflexivity.
red; intros.
rewrite H; rewrite <- IHt2.
rewrite int_subst_rec_eq.
rewrite V.cons_lams; eauto with *.
rewrite H1; reflexivity.
simpl; red; intros.
do 2 rewrite <- int_subst_rec_eq.
rewrite H; rewrite IHt1; rewrite IHt2; reflexivity.
simpl; red; intros.
apply M.prod_ext; intros.
rewrite H; rewrite <- IHt1.
rewrite int_subst_rec_eq.
reflexivity.
red; intros.
rewrite H; rewrite <- IHt2.
rewrite int_subst_rec_eq.
rewrite V.cons_lams; eauto with *.
rewrite H1; reflexivity.
Qed.
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)).
intros.
symmetry; apply int_subst_rec; trivial.
Qed.
Lemma int_not_kind : ∀ T, T <> Srt kind -> int_trm (unmark_app T) <> T.kind.
red; intros.
apply H.
destruct T; try discriminate.
destruct s; trivial; discriminate.
destruct T1; discriminate.
Qed.
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')).
induction 1; simpl; intros.
split.
apply R.typ_prop.
apply R.refl.
split.
destruct H0.
subst t.
unfold lift; rewrite unmark_lift.
fold (lift (S v) (unmark_app x)); rewrite int_lift.
apply R.typ_var.
elim H1; simpl; auto.
apply R.refl.
destruct IHeq_typ1.
clear IHeq_typ2.
destruct IHeq_typ3.
split.
apply R.typ_abs; eauto.
apply R.eq_typ_abs; trivial.
destruct IHeq_typ1.
destruct IHeq_typ3.
split.
rewrite unmark_subst0 with (1:=H2).
rewrite int_subst; eauto.
apply R.typ_app with (int_trm (unmark_app V)); eauto.
apply R.eq_typ_app; trivial.
destruct IHeq_typ1.
destruct IHeq_typ2.
split.
apply R.typ_prod; trivial.
destruct s2; auto.
apply R.eq_typ_prod; trivial.
destruct IHeq_typ1.
destruct IHeq_typ3.
split.
rewrite unmark_subst0 with (1:=H2).
rewrite int_subst; eauto.
apply R.typ_beta; eauto.
rewrite unmark_subst0 with (1:=typ_refl2 _ _ _ _ H1).
rewrite int_subst.
apply R.eq_typ_beta; eauto.
apply typ_refl2 in H; eauto.
destruct IHeq_typ1.
destruct IHeq_typ2.
split; trivial.
apply R.typ_conv with (int_trm (unmark_app T)); eauto.
destruct IHeq_typ1.
destruct IHeq_typ2.
split; trivial.
apply typ_refl2 in H0.
apply R.typ_conv with (int_trm (unmark_app T')); eauto.
apply R.sym; trivial.
Qed.
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.
red in |- *; intros.
apply int_sound in H0.
destruct H0 as (H0,_).
red in H0.
apply H with (int (int_trm (unmark_app M)) vnil).
apply H0.
red; intros.
destruct n; discriminate.
Qed.
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_rec : ∀ n t k,
eq_term (T.lift_rec n k (int_trm t)) (int_trm (Term.lift_rec n t k)).
induction t; intros.
destruct s; simpl; trivial.
red; intros; reflexivity.
simpl; unfold V.lams, V.shift.
destruct (le_gt_dec k n0); simpl.
replace (k+(n+(n0-k))) with (n+n0) by omega.
red; auto.
red; auto.
simpl; red; intros.
apply M.lam_ext; intros.
rewrite H; rewrite <- IHt1.
rewrite int_lift_rec_eq.
reflexivity.
red; intros.
rewrite H; rewrite <- IHt2.
rewrite int_lift_rec_eq.
rewrite V.cons_lams; eauto with *.
rewrite H1; reflexivity.
simpl; red; intros.
do 2 rewrite <- int_lift_rec_eq.
rewrite H; rewrite IHt1; rewrite IHt2; reflexivity.
simpl; red; intros.
apply M.prod_ext; intros.
rewrite H; rewrite <- IHt1.
rewrite int_lift_rec_eq.
reflexivity.
red; intros.
rewrite H; rewrite <- IHt2.
rewrite int_lift_rec_eq.
rewrite V.cons_lams; eauto with *.
rewrite H1; reflexivity.
Qed.
Lemma int_lift : ∀ n t,
eq_term (int_trm (lift n t)) (T.lift n (int_trm t)).
intros.
unfold lift, T.lift.
symmetry; apply int_lift_rec.
Qed.
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)).
intros arg not_knd.
induction t; intros.
destruct s; simpl; trivial.
red; intros; reflexivity.
simpl subst_rec.
destruct (lt_eq_lt_dec k n) as [[fv|eqv]|bv]; simpl.
simpl; unfold V.lams, V.shift;
destruct (le_gt_dec k n); try (apply False_ind; omega; fail).
replace (n-k) with (S(pred n-k)) by omega; simpl.
replace (k+(pred n-k)) with (pred n) by omega; red; auto.
case_eq (int_trm (lift k arg)); [intros (a,am) arg_eq;simpl|intro arg_eq].
red; intros.
subst k.
unfold V.lams; simpl.
destruct (le_gt_dec n n).
2:apply False_ind; omega.
replace (n-n) with 0; auto with arith; simpl.
setoid_replace (V.shift n x) with (V.lams 0 (V.shift n) x).
2:symmetry; apply V.lams0.
rewrite <- int_lift_rec_eq.
fold (T.lift n (int_trm arg)).
rewrite <- int_lift.
rewrite arg_eq; simpl.
apply am.
exact H.
destruct arg; simpl; try discriminate.
destruct s.
elim not_knd; reflexivity.
discriminate.
simpl; unfold V.lams, V.shift;
destruct (le_gt_dec k n); try (apply False_ind; omega; fail).
red; intros; auto.
simpl; red; intros.
apply M.lam_ext.
rewrite H; rewrite <- IHt1.
rewrite int_subst_rec_eq.
reflexivity.
red; intros.
rewrite H; rewrite <- IHt2.
rewrite int_subst_rec_eq.
rewrite V.cons_lams; eauto with *.
rewrite H1; reflexivity.
simpl; red; intros.
do 2 rewrite <- int_subst_rec_eq.
rewrite H; rewrite IHt1; rewrite IHt2; reflexivity.
simpl; red; intros.
apply M.prod_ext; intros.
rewrite H; rewrite <- IHt1.
rewrite int_subst_rec_eq.
reflexivity.
red; intros.
rewrite H; rewrite <- IHt2.
rewrite int_subst_rec_eq.
rewrite V.cons_lams; eauto with *.
rewrite H1; reflexivity.
Qed.
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)).
intros.
symmetry; apply int_subst_rec; trivial.
Qed.
Lemma int_not_kind : ∀ T, T <> Srt kind -> int_trm (unmark_app T) <> T.kind.
red; intros.
apply H.
destruct T; try discriminate.
destruct s; trivial; discriminate.
destruct T1; discriminate.
Qed.
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')).
induction 1; simpl; intros.
split.
apply R.typ_prop.
apply R.refl.
split.
destruct H0.
subst t.
unfold lift; rewrite unmark_lift.
fold (lift (S v) (unmark_app x)); rewrite int_lift.
apply R.typ_var.
elim H1; simpl; auto.
apply R.refl.
destruct IHeq_typ1.
clear IHeq_typ2.
destruct IHeq_typ3.
split.
apply R.typ_abs; eauto.
apply R.eq_typ_abs; trivial.
destruct IHeq_typ1.
destruct IHeq_typ3.
split.
rewrite unmark_subst0 with (1:=H2).
rewrite int_subst; eauto.
apply R.typ_app with (int_trm (unmark_app V)); eauto.
apply R.eq_typ_app; trivial.
destruct IHeq_typ1.
destruct IHeq_typ2.
split.
apply R.typ_prod; trivial.
destruct s2; auto.
apply R.eq_typ_prod; trivial.
destruct IHeq_typ1.
destruct IHeq_typ3.
split.
rewrite unmark_subst0 with (1:=H2).
rewrite int_subst; eauto.
apply R.typ_beta; eauto.
rewrite unmark_subst0 with (1:=typ_refl2 _ _ _ _ H1).
rewrite int_subst.
apply R.eq_typ_beta; eauto.
apply typ_refl2 in H; eauto.
destruct IHeq_typ1.
destruct IHeq_typ2.
split; trivial.
apply R.typ_conv with (int_trm (unmark_app T)); eauto.
destruct IHeq_typ1.
destruct IHeq_typ2.
split; trivial.
apply typ_refl2 in H0.
apply R.typ_conv with (int_trm (unmark_app T')); eauto.
apply R.sym; trivial.
Qed.
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.
red in |- *; intros.
apply int_sound in H0.
destruct H0 as (H0,_).
red in H0.
apply H with (int (int_trm (unmark_app M)) vnil).
apply H0.
red; intros.
destruct n; discriminate.
Qed.
End MakeModel.