Library GenModel

Require Import Models List.

Module MakeModel(M : CC_Model).
Import M.

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.

Module Xeq.
  Definition t := X.
  Definition eq := eqX.
  Definition eq_equiv : Equivalence eq := eqX_equiv.
End Xeq.
Require Import VarMap.
Module V := VarMap.Make(Xeq).

Notation val := V.map.
Notation eq_val := V.eq_map.
Instance eq_val_equiv : Equivalence eq_val.
Definition vnil : val := V.nil props.

Import V.


Module T.

Definition term :=
  option {f:val -> X|Proper (eq_val ==> eqX) f}.

Definition eq_term (x y:term) :=
  match x, y with
  | Some f, Some g => (eq_val ==> eqX)%signature (proj1_sig f) (proj1_sig g)
  | None, None => True
  | _, _ => False
  end.

Instance eq_term_refl : Reflexive eq_term.
Qed.

Instance eq_term_sym : Symmetric eq_term.
Qed.

Instance eq_term_trans : Transitive eq_term.
Qed.

Definition int (t:term) (i:val) : X :=
  match t with
  | Some f => proj1_sig f i
  | None => props
  end.

Instance int_morph : Proper (eq_term ==> eq_val ==> eqX) int.
Qed.

Definition el (t:term) (i:val) (x:X) :=
  match t with
  | Some f => x \in proj1_sig f i
  | None => True
  end.

Instance el_morph : Proper (eq_term ==> eq_val ==> eqX ==> iff) el.

Qed.

Definition cst (x:X) : term.
Defined.

Definition prop := cst props.

Definition kind : term := None.

Hint Unfold eq_val.

Definition Ref (n:nat) : term.
Defined.

Definition App (u v:term) : term.
Defined.

Instance App_morph : Proper (eq_term ==> eq_term ==> eq_term) App.
Qed.

Definition Abs (A M:term) : term.

Defined.

Instance Abs_morph : Proper (eq_term ==> eq_term ==> eq_term) Abs.

Qed.

Definition Prod (A B:term) : term.

Defined.

Instance Prod_morph : Proper (eq_term ==> eq_term ==> eq_term) Prod.

Qed.

Section Lift.

Definition lift_rec (n m:nat) (t:term) : term.
Defined.

Definition lift1 n := lift_rec n 1.

Lemma lift10: forall T, eq_term (lift1 0 T) T.

Lemma int_lift_rec_eq : forall n k T i,
  int (lift_rec n k T) i == int T (V.lams k (V.shift n) i).

Definition lift n := lift_rec n 0.

Instance lift_morph : forall k, Proper (eq_term ==> eq_term) (lift k).
Qed.

Lemma lift0_term : forall T, eq_term (lift 0 T) T.

Lemma simpl_int_lift : forall i n x T,
  int (lift (S n) T) (V.cons x i) == int (lift n T) i.

Lemma simpl_int_lift1 : forall i x T,
  int (lift 1 T) (V.cons x i) == int T i.

Lemma simpl_lift1 : forall i n x y T,
  int (lift1 (S n) T) (V.cons x (V.cons y i)) == int (lift1 n T) (V.cons x i).

End Lift.

Section Substitution.

Definition subst_rec (arg:term) (m:nat) (t:term) : term.
Defined.

Lemma int_subst_rec_eq : forall arg k T i,
  int (subst_rec arg k T) i == int T (V.lams k (V.cons (int arg (V.shift k i))) i).

Definition subst arg := subst_rec arg 0.

Instance subst_morph : Proper (eq_term ==> eq_term ==> eq_term) subst.
Qed.

Lemma int_subst_eq : forall N M i,
  int (subst N M) i == int M (V.cons (int N i) i).

Lemma el_subst_eq : forall N M i x,
  el (subst N M) i x <-> el M (V.cons (int N i) i) x.

End Substitution.

End T.
Import T.

Definition env := list term.

Definition val_ok (e:env) (i:val) :=
  forall n T, nth_error e n = value T -> el (lift (S n) T) i (i n).

Lemma vcons_add_var0 : forall e T i x,
  val_ok e i -> el T i x -> val_ok (T::e) (V.cons x i).

Lemma vcons_add_var : forall e T i x,
  val_ok e i -> x \in int T i -> val_ok (T::e) (V.cons x i).

Lemma add_var_eq_fun : forall T U U' i,
  (forall x, el T i x -> int U (V.cons x i) == int U' (V.cons x i)) ->
  eq_fun (int T i)
    (fun x => int U (V.cons x i))
    (fun x => int U' (V.cons x i)).

Module J.
Definition typ (e:env) (M T:term) :=
  forall i, val_ok e i -> el T i (int M i).
Definition eq_typ (e:env) (M M':term) :=
  forall i, val_ok e i -> int M i == int M' i.
Definition sub_typ (e:env) (M M':term) :=
  forall i x, val_ok e i -> x \in int M i -> x\in int M' i.

Instance typ_morph : forall e, Proper (eq_term ==> eq_term ==> iff) (typ e).
Qed.

Instance eq_typ_morph : forall e, Proper (eq_term ==> eq_term ==> iff) (eq_typ e).
Qed.

Instance sub_typ_morph : forall e, Proper (eq_term ==> eq_term ==> iff) (sub_typ e).
Qed.

End J.
Import J.

Module R.

Lemma refl : forall e M, eq_typ e M M.

Lemma sym : forall e M M', eq_typ e M M' -> eq_typ e M' M.

Lemma trans : forall e M M' M'', eq_typ e M M' -> eq_typ e M' M'' -> eq_typ e M M''.

Instance eq_typ_equiv : forall e, Equivalence (eq_typ e).
Qed.

Lemma eq_typ_app : forall e M M' N N',
  eq_typ e M M' ->
  eq_typ e N N' ->
  eq_typ e (App M N) (App M' N').

Lemma eq_typ_abs : forall e T T' M M',
  eq_typ e T T' ->
  eq_typ (T::e) M M' ->
  eq_typ e (Abs T M) (Abs T' M').

Lemma eq_typ_prod : forall e T T' U U',
  eq_typ e T T' ->
  eq_typ (T::e) U U' ->
  eq_typ e (Prod T U) (Prod T' U').

Lemma eq_typ_beta : forall e T M M' N N',
  eq_typ (T::e) M M' ->
  eq_typ e N N' ->
  typ e N T ->
  T <> kind ->
  eq_typ e (App (Abs T M) N) (subst N' M').

Lemma typ_prop : forall e, typ e prop kind.

Lemma typ_var : forall e n T,
  nth_error e n = value T -> typ e (Ref n) (lift (S n) T).

Lemma typ_app : forall e u v V Ur,
  typ e v V ->
  typ e u (Prod V Ur) ->
  V <> kind ->
  typ e (App u v) (subst v Ur).

Lemma typ_abs : forall e T M U,
  typ (T :: e) M U ->
  U <> kind ->
  typ e (Abs T M) (Prod T U).

Lemma typ_beta : forall e T M N U,
  typ e N T ->
  typ (T::e) M U ->
  T <> kind ->
  U <> kind ->
  typ e (App (Abs T M) N) (subst N U).

Lemma typ_prod : forall e T U s2,
  s2 = kind \/ s2 = prop ->
  typ (T :: e) U s2 ->
  typ e (Prod T U) s2.

Lemma typ_conv : forall e M T T',
  typ e M T ->
  eq_typ e T T' ->
  T <> kind ->
  typ e M T'.

Lemma sub_refl : forall e M M',
  eq_typ e M M' -> sub_typ e M M'.

Lemma sub_trans : forall e M1 M2 M3,
  sub_typ e M1 M2 -> sub_typ e M2 M3 -> sub_typ e M1 M3.

Lemma typ_subsumption : forall e M T T',
  typ e M T ->
  sub_typ e T T' ->
  T <> kind ->
  typ e M T'.

End R.

End MakeModel.