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.