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 : ∀ x y y',
  x ∈ y ->
  y == y' ->
  x ∈ y'.

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 ∈ int i T.

Definition eq_int (i1 i2:nat->X) := ∀ 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 :
  ∀ n t k i,
  int i (lift_rec n t k) == int (del_map n k i) t.

Lemma int_subst :
  ∀ 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 :
  ∀ 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 :=
  ∀ t n, item_lift t e n -> i n ∈ int i t.

Lemma int_env_cons :
  ∀ e i T x,
  int_env e i ->
  x ∈ int i T ->
  int_env (cons T e) (cons_map x i).

Definition judge e t T : Prop :=
   ∀ i, int_env e i -> In_int i t T.

Definition eq_judge e T U : Prop :=
  ∀ i, int_env e i -> int i T == int i U.

Lemma eq_judge_trans : ∀ e T U V,
  eq_judge e T U -> eq_judge e U V -> eq_judge e T V.

Lemma judge_prop : ∀ e, judge e (Srt prop) (Srt (kind 0)).

Lemma judge_kind : ∀ e n, judge e (Srt (kind n)) (Srt (kind (S n))).

Lemma judge_var : ∀ e n t, item_lift t e n -> judge e (Ref n) t.

Lemma judge_abs : ∀ 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 : ∀ 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 : ∀ n m x, le n m -> x ∈ u_card n -> x ∈ u_card m.

Lemma judge_prod : ∀ 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 : ∀ 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 : ∀ e T M N,
  judge e N T ->
  eq_judge e (App (Abs T M) N) (subst N M).

Lemma judge_conv :
  ∀ e M T T',
  judge e M T ->
  eq_judge e T T' ->
  judge e M T'.

Require Import TypeJudgeECC.

Lemma int_sound : ∀ 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.

Module ECC <: ECC_Model.

  Module CC := ModelZF.CCM.

  Definition u_card := ecc.

  Lemma u_card_in1 : props ∈ u_card 0.
  Lemma u_card_in2 : ∀ n, u_card n ∈ u_card (S n).
  Lemma u_card_incl_prop : ∀ x, x ∈ props -> x ∈ u_card 0.
  Lemma u_card_incl : ∀ n x, x ∈ u_card n -> x ∈ u_card (S n).
  Lemma u_card_prod : ∀ n X Y,
    CC.eq_fun X Y Y ->
    X ∈ u_card n ->
    (∀ x, x ∈ X -> Y x ∈ u_card n) ->
    CC.prod X Y ∈ u_card n.
End ECC.

Module ECC_Sound := MakeModel ECC.

Print Assumptions ECC_Sound.int_sound.