Library GenModelSN

Require Import List Compare_dec.
Require Import Sat.
Require Import Models.

Module Lc := Lambda.

Module Type SN_addon (M : CC_Model).
  Import M.

  Parameter Red : X -> SAT.
  Parameter Red_morph : Proper (eqX ==> eqSAT) Red.

  Parameter Red_sort : eqSAT (Red props) snSAT.

  Parameter Red_prod : forall A B,
    eqSAT (Red (prod A B))
     (prodSAT (Red A)
        (interSAT (fun p:{y|y\in A} => Red (B (proj1_sig p))))).

  Parameter daemon : X.
  Parameter daemon_false : daemon \in prod props (fun P => P).

End SN_addon.

Module MakeModel(M : CC_Model) (SN : SN_addon M).
Import M.
Import SN.

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 :=
Notation eq_val := V.eq_map.
Instance eq_val_equiv : Equivalence eq_val.
Definition vnil : val := V.nil props.

Import V.

Module LCeq.
  Definition t := Lc.term.
  Definition eq := @Logic.eq Lc.term.
  Definition eq_equiv : Equivalence eq := eq_equivalence.
End LCeq.
Module I := VarMap.Make(LCeq).

Notation intt :=
Notation eq_intt := I.eq_map.
Instance eq_intt_equiv : Equivalence eq_intt.
Import I.

Definition ilift (j:intt) : intt :=
  fun k => match k with
  | 0 => Lc.Ref 0
  | S n => Lc.lift 1 (j n)

Instance ilift_morph : Proper (eq_intt ==> eq_intt) ilift.

Lemma ilift_lams : forall k f j,
  (forall j j', (forall a, Lc.lift 1 (j a) = j' a) ->
   forall a, Lc.lift 1 (f j a) = f j' a) ->
  eq_intt (ilift (I.lams k f j)) (I.lams (S k) f (ilift j)).

Lemma ilift_binder : forall u j k,
    (ilift (fun n => Lc.subst_rec u (j n) k))
    (fun n => Lc.subst_rec u (ilift j n) (S k)).

Lemma ilift_binder_lift : forall j k,
    (ilift (fun n => Lc.lift_rec 1 (j n) k))
    (fun n => Lc.lift_rec 1 (ilift j n) (S k)).

Definition substitutive (t:intt->Lc.term) :=
  forall u j k,
  t (fun n => Lc.subst_rec u (j n) k) = Lc.subst_rec u (t j) k.
Definition liftable (t:intt->Lc.term) :=
  forall j k,
  t (fun n => Lc.lift_rec 1 (j n) k) = Lc.lift_rec 1 (t j) k.

Record inftrm := {
  iint : val -> X;
  iint_morph : Proper (eq_val ==> eqX) iint;
  itm : intt -> Lc.term;
  itm_morph : Proper (eq_intt ==> @eq Lc.term) itm;
  itm_lift : liftable itm;
  itm_subst : substitutive itm

Definition trm := option inftrm.

Definition eq_trm (x y:trm) :=
  match x, y with
  | Some f, Some g =>
     (eq_val ==> eqX)%signature (iint f) (iint g) /\
     (eq_intt ==> @eq Lc.term)%signature (itm f) (itm g)
  | None, None => True
  | _, _ => False

Instance eq_trm_refl : Reflexive eq_trm.

Instance eq_trm_sym : Symmetric eq_trm.

Instance eq_trm_trans : Transitive eq_trm.

Instance eq_trm_equiv : Equivalence eq_trm.

Lemma eq_kind : forall (M:trm), M = None <-> eq_trm M None.

Definition tm (j:intt) (M:trm) :=
  match M with
  | Some f => itm f j
  | None => Lc.K

Definition int (i:val) (M:trm) :=
  match M with
  | Some f => iint f i
  | None => props

Lemma eq_trm_intro : forall T T',
  (forall i, int i T == int i T') ->
  (forall j, tm j T = tm j T') ->
  match T, T' with Some _,Some _=>True|None,None=>True|_,_=>False end ->
  eq_trm T T'.

Instance tm_morph : Proper (eq_intt ==> eq_trm ==> @eq Lc.term) tm.

Lemma tm_substitutive : forall u t j k,
  tm (fun n => Lc.subst_rec u (j n) k) t =
  Lc.subst_rec u (tm j t) k.

Lemma tm_liftable : forall j t k,
  tm (fun n => Lc.lift_rec 1 (j n) k) t = Lc.lift_rec 1 (tm j t) k.

Lemma tm_subst_cons : forall x j t,
  tm (I.cons x j) t = Lc.subst x (tm (ilift j) t).

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

Definition kind : trm := None.

Definition prop : trm.

Definition Ref (n:nat) : trm.

Definition App (u v:trm) : trm.


Definition Abs (A M:trm) : trm.


Definition Prod (A B:trm) : trm.


Definition lift_rec (n m:nat) (t:trm) : trm.


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

Definition lift n := lift_rec n 0.

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


Lemma int_lift_eq : forall i T,
  int i (lift 1 T) == int (V.shift 1 i) T.

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

Lemma tm_lift_rec_eq : forall n k T j,
  tm j (lift_rec n k T) = tm (I.lams k (I.shift n) j) T.

Lemma split_lift : forall n T,
  eq_trm (lift (S n) T) (lift 1 (lift n T)).

Definition subst_rec (arg:trm) (m:nat) (t:trm) : trm.


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

Definition subst arg := subst_rec arg 0.

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

Lemma tm_subst_rec_eq : forall arg k T j,
  tm j (subst_rec arg k T) = tm (I.lams k (I.cons (tm (I.shift k j) arg)) j) T.

Lemma tm_subst_eq : forall u v j,
  tm j (subst u v) = Lc.subst (tm j u) (tm (ilift j) v).

Instance App_morph : Proper (eq_trm ==> eq_trm ==> eq_trm) App.


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


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


Fixpoint cst_fun (i:val) (e:list trm) (x:X) : X :=
  match e with
  | List.nil => x
  | T::f => lam (int i T) (fun y => cst_fun (V.cons y i) f x)

Instance cst_morph : Proper (eq_val ==> @eq _ ==> eqX ==> eqX) cst_fun.


Fixpoint prod_list (e:list trm) (U:trm) :=
  match e with
  | List.nil => U
  | T::f => Prod T (prod_list f U)

Lemma wit_prod : forall x U,
  (forall i, x \in int i U) ->
  forall e i,
  cst_fun i e x \in int i (prod_list e U).

Definition non_empty T :=
  exists e, exists2 U, eq_trm T (prod_list e U) &
    exists x, forall i, x \in int i U.

Instance non_empty_morph : Proper (eq_trm ==> iff) non_empty.

Lemma prop_non_empty : non_empty prop.

Lemma prod_non_empty : forall T U,
  non_empty U ->
  non_empty (Prod T U).

Lemma non_empty_witness : forall i T,
  non_empty T ->
  exists x, x \in int i T.

Lemma discr_ref_prod : forall n A B,
  ~ eq_trm (Ref n) (Prod A B).

Lemma lift1var : forall n, eq_trm (lift 1 (Ref n)) (Ref (S n)).

Lemma non_empty_var_lift : forall n,
  non_empty (Ref n) -> non_empty (Ref (S n)).

Definition in_int (i:val) (j:intt) (M T:trm) :=
  M <> None /\
  match T with
  | None => non_empty M
  | _ => int i M \in int i T
  end /\
  inSAT (tm j M) (Red (int i T)).

Instance in_int_morph : Proper
  (eq_val ==> pointwise_relation nat (@eq Lc.term) ==> eq_trm ==> eq_trm ==> iff)


Lemma in_int_not_kind : forall i j M T,
  in_int i j M T ->
  T <> kind ->
  int i M \in int i T /\
  inSAT (tm j M) (Red (int i T)).

Lemma in_int_intro : forall i j M T,
  int i M \in int i T ->
  inSAT (tm j M) (Red (int i T)) ->
  M <> kind ->
  T <> kind ->
  in_int i j M T.

Lemma in_int_var0 : forall i j x t T,
  x \in int i T ->
  inSAT t (Red (int i T)) ->
  T <> kind ->
  in_int (V.cons x i) (I.cons t j) (Ref 0) (lift 1 T).

Lemma in_int_varS : forall i j x t n T,
  in_int i j (Ref n) (lift (S n) T) ->
  in_int (V.cons x i) (I.cons t j) (Ref (S n)) (lift (S (S n)) T).

Lemma in_int_sn : forall i j M T,
  in_int i j M T -> (tm j M).

Definition env := list trm.

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

Lemma vcons_add_var : forall e T i j x t,
  val_ok e i j ->
  x \in int i T ->
  inSAT t (Red (int i T)) ->
  T <> kind ->
  val_ok (T::e) (V.cons x i) (I.cons t j).

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

Lemma vcons_add_var0 : forall e T i j x,
  val_ok e i j ->
  x \in int i T ->
  T <> kind ->
  val_ok (T::e) (V.cons x i) (I.cons daimon j).

Definition wf (e:env) :=
  exists i, exists j, val_ok e i j.
Definition typ (e:env) (M T:trm) :=
  forall i j, val_ok e i j -> in_int i j M T.
Definition eq_typ (e:env) (M M':trm) :=
  forall i j, val_ok e i j -> int i M == int i M'.

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

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

Definition typs e T :=
  typ e T kind \/ typ e T prop.

Lemma typs_not_kind : forall e T, wf e -> typs e T -> T <> kind.

Lemma typs_non_empty : forall e T i j,
  typs e T ->
  val_ok e i j ->
  exists x, x \in int i T.

Lemma typ_sn : forall e M T,
  wf e -> typ e M T -> exists j, (tm j M).

Lemma wf_nil : wf List.nil.

Lemma wf_cons : forall e T,
  wf e ->
  typs e T ->
  wf (T::e).

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_setoid : forall e, Equivalence (eq_typ e).

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' ->
  T <> kind ->
  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' ->
  T <> kind ->
  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 ->
  Ur <> kind ->
  typ e (App u v) (subst v Ur).

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

Lemma typ_beta : forall e T M N U,
  typs e T ->
  typ (T::e) M U ->
  typ e N T ->
  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 ->
  typs e T ->
  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 ->
  T' <> kind ->
  typ e M T'.

End MakeModel.