Library ObjectSN

Require Export basic.
Require Import Models.
Require Import VarMap.
Require Lambda.
Module Lc := Lambda.

Module MakeObject (M: CC_Model).
Import M.

Valuations

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

Notation val := V.map.
Notation eq_val := V.eq_map.

Definition vnil : val := V.nil props.

Module I := Lambda.I.

Pseudo-terms

Record inftrm := {
  iint : val -> X;
  iint_morph : Proper (eq_val ==> eqX) iint;
  itm : Lc.intt -> Lc.term;
  itm_morph : Proper (Lc.eq_intt ==> eq) itm;
  itm_lift : Lc.liftable itm;
  itm_subst : Lc.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) /\
     (Lc.eq_intt ==> eq)%signature (itm f) (itm g)
  | None, None => True
  | _, _ => False
  end.

Instance eq_trm_refl : Reflexive eq_trm.
Qed.

Instance eq_trm_sym : Symmetric eq_trm.
Qed.

Instance eq_trm_trans : Transitive eq_trm.
Qed.

Instance eq_trm_equiv : Equivalence eq_trm.
Qed.

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

Definition dummy_trm : Lc.term.
Defined.

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

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

Definition dummy_int : X.

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

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

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

Lemma tm_substitutive : ∀ 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 : ∀ 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 : ∀ x j t,
  tm (I.cons x j) t = Lc.subst x (tm (Lc.ilift j) t).

Property of substitutivity: whenever a term-denotation contains a free var, then it comes from the term-valuation (but we can't tell which var, short of using Markov rule, hence the double negation.

Lemma tm_closed : ∀ k j M,
Lc.occur k (tm j M) -> ~ ∀ n, ~ Lc.occur k (j n).

Pseudo-term constructors

Definition cst (x:X) (t:Lc.term)
  (H0 : Lc.liftable (fun _ => t)) (H1 : Lc.substitutive (fun _ => t)) : trm.
left; exists (fun _ => x) (fun _ => t); trivial.
Defined.

Definition kind : trm := None.

Definition prop : trm :=
  @cst props (Lc.K) (fun _ _ => eq_refl _) (fun _ _ _ => eq_refl _).

Definition Ref (n:nat) : trm.
left; exists (fun i => i n) (fun j => j n).
Defined.

Definition App (u v:trm) : trm.
left; exists (fun i => app (int i u) (int i v))
             (fun j => Lc.App (tm j u) (tm j v)).
Defined.

Definition CAbs t m :=
  Lc.App2 Lc.K (Lc.Abs m) t.

Definition Abs (A M:trm) : trm.
left; exists (fun i => lam (int i A) (fun x => int (V.cons x i) M))
             (fun j => CAbs (tm j A) (tm (Lc.ilift j) M)).
Defined.

Definition CProd a b :=
  Lc.App2 Lc.K a (Lc.Abs b).

Definition Prod (A B:trm) : trm.
left; exists (fun i => prod (int i A) (fun x => int (V.cons x i) B))
             (fun j => CProd (tm j A) (tm (Lc.ilift j) B)).
Defined.

Lemma intProd_eq i A B :
  int i (Prod A B) = prod (int i A) (fun x => int (V.cons x i) B).

Definition lift_rec (n m:nat) (t:trm) : trm.
destruct t as [t|]; [left|exact kind].
exists (fun i => iint t (V.lams m (V.shift n) i))
       (fun j => itm t (I.lams m (I.shift n) j)).
Defined.

Instance lift_rec_morph n k :
  Proper (eq_trm ==> eq_trm) (lift_rec n k).

Qed.

Lemma int_lift_rec_eq : ∀ 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 : ∀ k, Proper (eq_trm ==> eq_trm) (lift k).

Qed.

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

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

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

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

Definition subst_rec (arg:trm) (m:nat) (t:trm) : trm.
destruct t as [body|]; [left|right].
exists (fun i => iint body (V.lams m (V.cons (int (V.shift m i) arg)) i))
       (fun j => itm body (I.lams m (I.cons (tm (I.shift m j) arg)) j)).
Defined.

Instance subst_rec_morph :
  Proper (eq_trm ==> eq ==> eq_trm ==> eq_trm) subst_rec.

Qed.

Lemma int_subst_rec_eq : ∀ 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 : ∀ N M i,
int (V.cons (int i N) i) M == int i (subst N M).

Lemma tm_subst_rec_eq : ∀ 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 : ∀ u v j,
  tm j (subst u v) = Lc.subst (tm j u) (tm (Lc.ilift j) v).

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

Qed.

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

Qed.

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

Qed.

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

Lemma eq_trm_lift_ref_fv n k i :
  k <= i ->
  eq_trm (lift_rec n k (Ref i)) (Ref (n +i)).

Lemma red_lift_app n A B k :
  eq_trm (lift_rec n k (App A B)) (App (lift_rec n k A) (lift_rec n k B)).

Lemma red_lift_abs n A B k :
  eq_trm (lift_rec n k (Abs A B)) (Abs (lift_rec n k A) (lift_rec n (S k) B)).

Lemma red_lift_prod n A B k :
  eq_trm (lift_rec n k (Prod A B)) (Prod (lift_rec n k A) (lift_rec n (S k) B)).

Lemma red_sigma_app N A B k :
  eq_trm (subst_rec N k (App A B)) (App (subst_rec N k A) (subst_rec N k B)).

Lemma red_sigma_abs N A B k :
  eq_trm (subst_rec N k (Abs A B)) (Abs (subst_rec N k A) (subst_rec N (S k) B)).

Lemma red_sigma_prod N A B k :
  eq_trm (subst_rec N k (Prod A B)) (Prod (subst_rec N k A) (subst_rec N (S k) B)).

Lemma red_sigma_var_eq N k :
  N <> kind ->
  eq_trm (subst_rec N k (Ref k)) (lift k N).

Lemma red_sigma_var_lt N k n :
  n < k ->
  eq_trm (subst_rec N k (Ref n)) (Ref n).

Lemma red_sigma_var_gt N k n :
  k <= n ->
  eq_trm (subst_rec N k (Ref (S n))) (Ref n).

Lemma simpl_subst_lift_rec A M k :
  eq_trm M (subst_rec A k (lift_rec 1 k M)).

"Untyped" reduction: tools for proving simulation and strong normalization

Definition red_term M N :=
  ∀ j, Lc.redp (tm j M) (tm j N).

Instance red_term_morph : Proper (eq_trm ==> eq_trm ==> iff) red_term.
Qed.

Instance red_term_trans : Transitive red_term.
Qed.

Lemma red_term_app_l M M' N :
  red_term M M' ->
  red_term (App M N) (App M' N).

Lemma red_term_app_r M N N' :
  red_term N N' ->
  red_term (App M N) (App M N').

Lemma red_term_abs_l M M' N :
  red_term M M' ->
  red_term (Abs M N) (Abs M' N).

Lemma red_term_abs_r M N N' :
  red_term N N' ->
  red_term (Abs M N) (Abs M N').

Lemma red_term_prod_l M M' N :
  red_term M M' ->
  red_term (Prod M N) (Prod M' N).

Lemma red_term_prod_r M N N' :
  red_term N N' ->
  red_term (Prod M N) (Prod M N').

Lemma red_term_beta T M N :
  red_term (App (Abs T M) N) (subst N M).

"Untyped" conversion: can be used to make equality more intensional: assume we have plus and plus' that perform the addition, but with different algorithms. Then we won't have conv_term plus plus', while eq_typ e plus plus' will hold.

Definition conv_term M N :=
  ∀ j, Lc.conv (tm j M) (tm j N).

Instance conv_term_morph : Proper (eq_trm ==> eq_trm ==> iff) conv_term.
Qed.

Instance conv_term_equiv : Equivalence conv_term.
Qed.

Lemma red_conv_term M N :
  red_term M N -> conv_term M N.

Instance conv_term_app : Proper (conv_term ==>conv_term ==>conv_term) App.
Qed.

Instance conv_term_abs : Proper (conv_term ==>conv_term ==>conv_term) Abs.
Qed.

Instance conv_term_prod : Proper (conv_term ==>conv_term ==>conv_term) Prod.
Qed.

Lemma conv_term_beta T M M' N N' :
  conv_term M M' ->
  conv_term N N' ->
  conv_term (App (Abs T M) N) (subst N' M').

Lemma simul M :
  Lc.sn M ->
  ∀ j M', M = tm j M' ->
  Acc (transp _ red_term) M'.

Iterated products

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

Lemma lift_prod_list_ex n k e T :
  exists e',
  eq_trm (lift_rec n k (prod_list e T))
    (prod_list e' (lift_rec n (length e +k) T)).
Lemma subst_prod_list_ex M k e T :
  exists e',
  eq_trm (subst_rec M k (prod_list e T))
    (prod_list e' (subst_rec M (length e +k) T)).

Dealing with kind (top sorts)

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)
  end.

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

Qed.

Lemma wit_prod : ∀ x U,
  (∀ i, x ∈ int i U) ->
  ∀ e i,
  cst_fun i e x ∈ int i (prod_list e U).

Definition kind_ok T :=
  exists e, exists2 U, eq_trm T (prod_list e U) &
    exists x, ∀ i, x ∈ int i U.

Instance kind_ok_morph : Proper (eq_trm ==> iff) kind_ok.
Qed.

Lemma prop_kind_ok : kind_ok prop.

Lemma prod_kind_ok : ∀ T U,
  kind_ok U ->
  kind_ok (Prod T U).

Lemma kind_ok_witness : ∀ i T,
  kind_ok T ->
  exists x, x ∈ int i T.

Lemma kind_ok_lift M k :
  kind_ok M <-> kind_ok (lift_rec 1 k M).

End MakeObject.