Library GenRealSN

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

Module Lc := Lambda.

Abstract strong mormalization model (supporting strong eliminations)

Reserved Notation "[ x , t ] \real A" (at level 60).

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

Types are equipped with a saturated set

  Parameter Real : X -> X -> SAT.
  Parameter Real_morph: Proper (eqX ==> eqX ==> eqSAT) Real.

  Parameter Real_sort : ∀ P, P ∈ props -> eqSAT (Real props P) snSAT.

  Definition piSAT A F f :=
    interSAT (fun p:{x|x ∈ A } =>
      prodSAT (Real A (proj1_sig p)) (Real (F (proj1_sig p)) (f (proj1_sig p)))).

  Parameter Real_prod : ∀ dom f F,
    eq_fun dom F F ->
    f ∈ prod dom F ->
    eqSAT (Real (prod dom F) f) (piSAT dom F (app f)).

Every proposition is inhabited

Parameter daimon : X.
Parameter daimon_false : daimon ∈ prod props (fun P => P).

End RealSN_addon.

Module MakeModel (M : CC_Model) (MM : RealSN_addon(M)).
Import M.
Import MM.

We first introduce the realizability relation, which the conjunction of the value and term interpretation requirements. [x,t] \real T reads "t is a realizer of x as a value of type T".

Notation "[ x , t ] \real A" := (x ∈ A /\ inSAT t (Real A x)).

Lemma real_daimon : ∀ x t T,
  [x ,t ] \real T -> [x ,SatSet.daimon ] \real T.

Lemma real_sn : ∀ x A t, [x ,t ] \real A -> Lc.sn t.

Lemma real_exp_K : ∀ x A u v,
  Lc.sn v ->
  [x ,u ] \real A ->
  [x ,Lc.App2 Lc.K u v ] \real A.

Lemma piSAT_intro : ∀ A B f t,
  Lc.sn t ->
  (∀ x u, x ∈ A -> inSAT u (Real A x) -> inSAT (Lc.App t u) (Real (B x) (f x))) ->
  inSAT t (piSAT A B f).

Lemma piSAT_elim : ∀ A B f x t u,
  inSAT t (piSAT A B f) ->
  x ∈ A ->
  inSAT u (Real A x) ->
  inSAT (Lc.App t u) (Real (B x) (f x)).

Lemma prod_intro_sn : ∀ dom f F m,
  eq_fun dom f f ->
  eq_fun dom F F ->
  Lc.sn m ->
  (∀ x u, [x ,u ] \real dom ->
   [f x , Lc.App m u ] \real F x) ->
  [lam dom f , m ] \real prod dom F.

Lemma prod_intro_lam : ∀ dom f F m,
  eq_fun dom f f ->
  eq_fun dom F F ->
  Lc.sn m ->
  (∀ x u, [x ,u ] \real dom ->
   [f x , Lc.subst u m ] \real F x) ->
  [lam dom f , Lc.Abs m ] \real prod dom F.

Lemma prod_elim : ∀ dom f x F t u,
  eq_fun dom F F ->
  [f ,t ] \real prod dom F ->
  [x ,u ] \real dom ->
  [app f x , Lc.App t u ] \real F x.

The abstract strong normalization proof.

Require ObjectSN.
Include ObjectSN.MakeObject(M).

Semantic typing relation.

Handles the case of kind: a type that contains all "non-empty" types and that is included in no type.

Definition in_int (i:val) (j:Lc.intt) (M T:trm) :=
  M <> None /\
  match T with

M has type kind

| None => kind_ok M /\ Lc.sn (tm j M)

T is a regular type

  | _ => [int i M , tm j M ] \real int i T
  end.

Instance in_int_morph : Proper
  (eq_val ==> pointwise_relation nat eq ==> eq_trm ==> eq_trm ==> iff)
  in_int.
Qed.

Lemma in_int_not_kind : ∀ i j M T,
  in_int i j M T ->
  T <> kind ->
  [int i M , tm j M ] \real int i T.

Lemma in_int_intro : ∀ i j M T,
  [int i M , tm j M ] \real int i T ->
  M <> kind ->
  T <> kind ->
  in_int i j M T.

Lemma in_int_var0 : ∀ i j x t T,
  [x ,t ] \real int i T ->
  T <> kind ->
  in_int (V.cons x i) (I.cons t j) (Ref 0) (lift 1 T).

Lemma in_int_varS : ∀ 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 : ∀ i j M T,
  in_int i j M T -> Lc.sn (tm j M).

Environments

Definition env := list trm.

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

Lemma vcons_add_var : ∀ e T i j x t,
  val_ok e i j ->
  [x ,t ] \real int i T ->
  T <> kind ->
  val_ok (T ::e) (V.cons x i) (I.cons t j).

Lemma vcons_add_var_daimon : ∀ e T i j x,
  val_ok e i j ->
  x ∈ int i T ->
  T <> kind ->
  val_ok (T ::e) (V.cons x i) (I.cons SatSet.daimon j).

Lemma add_var_eq_fun : ∀ T U U' i,
  (∀ x t, [x ,t ] \real 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').

Judgements

Definition wf (e:env) :=
  exists i, exists j, val_ok e i j.
Definition typ (e:env) (M T:trm) :=
  ∀ i j, val_ok e i j -> in_int i j M T.
Definition eq_typ (e:env) (M M':trm) :=
  ∀ i j, val_ok e i j -> int i M == int i M'.
Definition sub_typ (e:env) (M M':trm) :=
  ∀ i j, val_ok e i j ->
  ∀ x t, [x ,t ] \real int i M -> [x ,t ] \real int i M'.

Definition eq_typ' e M N := eq_typ e M N /\ conv_term M N.

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

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

Instance eq_typ'_morph : ∀ e, Proper (eq_trm ==> eq_trm ==> iff) (eq_typ' e).

Qed.

Instance sub_typ_morph : ∀ e, Proper (eq_trm ==> eq_trm ==> iff) (sub_typ e).

Qed.

Lemma typ_common e M T :
  match M,T with Some _,Some _=> True |_,_ => False end ->
  (∀ i j, val_ok e i j -> [int i M , tm j M ]\real int i T) ->
  typ e M T.

Well-formed types

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

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

Lemma typs_non_empty : ∀ e T i j,
  typs e T ->
  val_ok e i j ->
  exists x, [x ,SatSet.daimon ] \real int i T.

Strong normalization

Lemma typs_sn : ∀ e T i j, typs e T -> val_ok e i j -> Lc.sn (tm j T).

This lemma shows that the abstract model construction entails strong normalization. At this level, we do not have the actual syntax. However, red_term is a relation on the denotations that admits the same introduction rules as the syntactic reduction. When the syntax is introduced, it will only remain to check that the syntactic reduction implies the semantic one, which will be straightforward.

Lemma model_strong_normalization e M T :
  wf e ->
  typ e M T ->
  Acc (transp _ red_term) M.

Inference rules

Context formation rules

Lemma wf_nil : wf List.nil.

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

Extensional equality rules

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

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

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

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

Lemma eq_typ_app : ∀ 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 : ∀ 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 : ∀ 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 : ∀ 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').

Intensional equality

Instance eq_typ'_equiv : ∀ e, Equivalence (eq_typ' e).
Qed.

Lemma eq_typ'_eq_typ e M N :
  eq_typ' e M N -> eq_typ e M N.

Lemma eq_typ'_app : ∀ 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 : ∀ 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 : ∀ 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 : ∀ 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').

Typing rules

Lemma typ_prop : ∀ e, typ e prop kind.

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

Lemma typ_app : ∀ 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 prod_intro2 : ∀ dom f F t m,
  eq_fun dom f f ->
  eq_fun dom F F ->
  Lc.sn t ->
  (exists x, [x ,SatSet.daimon ] \real dom) ->
  (∀ x u, [x , u ] \real dom -> [f x , Lc.subst u m ] \real F x) ->
  [lam dom f , CAbs t m ] \real prod dom F.

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

Lemma typ_prod : ∀ 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 : ∀ e M T T',
  typ e M T ->
  eq_typ e T T' ->
  T <> kind ->
  T' <> kind ->
  typ e M T'.

Weakening

Lemma weakening : ∀ e M T A,
typ e M T ->
typ (A ::e) (lift 1 M) (lift 1 T).

Subtyping rules

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

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

Instance sub_typ_preord e : PreOrder (sub_typ e).

Qed.

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

Covariance can be derived if we have a weak eta property: any function is a lambda abstraction *with the same domain*. This is OK with set-theoretical functions (in contrast with general eta which does not hold on set-theoretical functions). This property could be added to the abstract domain.

Contravariance of product does not hold in set-theory.

Definition sub_typ_covariant
  (eta_eq : ∀ dom F f, f ∈ prod dom F -> f == lam dom (app f))
  e U1 U2 V1 V2 :
  U1 <> kind ->
  eq_typ e U1 U2 ->
  sub_typ (U1 ::e) V1 V2 ->
  sub_typ e (Prod U1 V1) (Prod U2 V2).

Qed.

End MakeModel.