Library ModelECC
Require Import IntMap.
Require Import TypeECC.
Require Import Models.
Require Import Max.
Module MakeModel (M : ECC_Model).
Import M M.CC.
Lemma in_reg_r : forall x y y',
x \in y ->
y == y' ->
x \in y'.
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.
Fixpoint int (i:nat->X) (t:term) {struct t} : X :=
match t with
Srt (kind n) => u_card n
| Srt prop => props
| Ref n => i n
| App u v => app (int i u) (int i v)
| Abs A M => lam (int i A) (fun x => int (cons_map x i) M)
| Prod A B => prod (int i A) (fun x => int (cons_map x i) B)
end.
Definition In_int (i:nat->X) (M T:term) : Prop :=
int i M \in int i T.
Definition eq_int (i1 i2:nat->X) := forall i, i1 i == i2 i.
Instance eq_int_equiv : Equivalence eq_int.
Qed.
Require Import Setoid.
Instance int_morph : Proper (eq_int ==> @eq _ ==> eqX) int.
Qed.
Lemma int_lift :
forall n t k i,
int i (lift_rec n t k) == int (del_map n k i) t.
Lemma int_subst :
forall n t k i,
int i (subst_rec n t k) ==
int (ins_map k (int (del_map k O i) n) i) t.
Lemma int_subst0 :
forall n t i, int i (subst n t) == int (cons_map (int i n) i) t.
Definition int_env (e:env) (i:nat->X) : Prop :=
forall t n, item_lift t e n -> i n \in int i t.
Lemma int_env_cons :
forall e i T x,
int_env e i ->
x \in int i T ->
int_env (cons T e) (cons_map x i).
Definition judge e t T : Prop :=
forall i, int_env e i -> In_int i t T.
Definition eq_judge e T U : Prop :=
forall i, int_env e i -> int i T == int i U.
Lemma eq_judge_trans : forall e T U V,
eq_judge e T U -> eq_judge e U V -> eq_judge e T V.
Lemma judge_prop : forall e, judge e (Srt prop) (Srt (kind 0)).
Lemma judge_kind : forall e n, judge e (Srt (kind n)) (Srt (kind (S n))).
Lemma judge_var : forall e n t, item_lift t e n -> judge e (Ref n) t.
Lemma judge_abs : forall e T M U s1 s2,
judge e T (Srt s1) ->
judge (T :: e) U (Srt s2) ->
judge (T :: e) M U ->
judge e (Abs T M) (Prod T U).
Lemma judge_app : forall e u v V Ur,
judge e v V ->
judge e u (Prod V Ur) ->
judge e (App u v) (subst v Ur).
Lemma u_card_incl_le : forall n m x, le n m -> x \in u_card n -> x \in u_card m.
Lemma judge_prod : forall e T U s1 s2 s3,
judge e T (Srt s1) ->
judge (T :: e) U (Srt s2) ->
ecc_prod s1 s2 s3 = true ->
judge e (Prod T U) (Srt s3).
Lemma judge_beta : forall e T M N U,
judge e N T ->
judge (T::e) M U ->
judge e (App (Abs T M) N) (subst N U).
Lemma eq_judge_beta : forall e T M N,
judge e N T ->
eq_judge e (App (Abs T M) N) (subst N M).
Lemma judge_conv :
forall e M T T',
judge e M T ->
eq_judge e T T' ->
judge e M T'.
Require Import TypeJudgeECC.
Lemma int_sound : forall e M M' T,
eq_typ e M M' T ->
judge e M T /\ eq_judge e M M'.
End MakeModel.
Require Import ZF ZFcoc ModelZF ZFecc.
Import IZF.
Module ECC <: ECC_Model.
Module CC := ModelZF.CCM.
Definition u_card := ecc.
Lemma u_card_in1 : props \in u_card 0.
Lemma u_card_in2 : forall n, u_card n \in u_card (S n).
Lemma u_card_incl : forall n x, x \in u_card n -> x \in u_card (S n).
Lemma u_card_prod : forall n X Y,
CC.eq_fun X Y Y ->
X \in u_card n ->
(forall x, x \in X -> Y x \in u_card n) ->
CC.prod X Y \in u_card n.
Lemma u_card_prod2 : forall n X Y,
CC.eq_fun X Y Y ->
X \in props ->
(forall x, x \in X -> Y x \in u_card n) ->
CC.prod X Y \in u_card n.
End ECC.