LambdaProj.Definitions

Require Export Infrastructure.

Syntax


Inductive ty : Set :=
  | Ty_Top : ty
  | Ty_Arrow : ty -> ty -> ty
  | Ty_RNil : ty
  | Ty_RCons : string -> ty -> ty -> ty.

Declare Custom Entry stlc_ty.
Notation "<{{ T }}>" := T (T custom stlc_ty at level 99).
Notation "( T )" := T (in custom stlc_ty, T at level 99).
Notation "T" := T (in custom stlc_ty at level 0, T constr at level 0).
Notation "'Top'" := (Ty_Top) (in custom stlc_ty at level 0).
Notation "S -> T" := (Ty_Arrow S T) (in custom stlc_ty at level 50, right associativity).
Notation "'nil'" := (Ty_RNil) (in custom stlc_ty).
Notation " l ':' T '::' Tr" := (Ty_RCons l T Tr) (in custom stlc_ty at level 3, right associativity).

Inductive tm : Set :=
  | tm_var : string -> tm
  | tm_app : tm -> tm -> tm
  | tm_abs : string -> ty -> tm -> tm
  | tm_rproj : tm -> string -> tm
  | tm_rnil : tm
  | tm_rcons : string -> tm -> tm -> tm.

Declare Custom Entry stlc.
Notation "<{ t }>" := t (t custom stlc at level 99).
Notation "( t )" := t (in custom stlc, t at level 99).
Notation "t" := t (in custom stlc at level 0, t constr at level 0).
Notation "t1 t2" := (tm_app t1 t2) (in custom stlc at level 1, left associativity).
Notation "\ x : T , t" :=
  (tm_abs x T t) (in custom stlc at level 90,
                     x at level 99,
                     T custom stlc_ty at level 99,
                     t custom stlc at level 99,
                     left associativity).
Notation "r --> l" := (tm_rproj r l) (in custom stlc at level 0).
Notation "'nil'" := (tm_rnil) (in custom stlc).
Notation " l '=' t '::' tr" := (tm_rcons l t tr) (in custom stlc at level 3, right associativity).
Coercion tm_var : string >-> tm.

Well-Formedness


Inductive record_ty : ty -> Prop :=
  | RTnil :
      record_ty <{{ nil }}>
  | RTcons : forall l T Tr,
      record_ty <{{ l : T :: Tr }}>.

Inductive record_tm : tm -> Prop :=
  | rtnil :
      record_tm <{ nil }>
  | rtcons : forall l t tr,
      record_tm <{ l = t :: tr }>.

Inductive well_formed_ty : ty -> Prop :=
  | wfTop :
      well_formed_ty <{{ Top }}>
  | wfArrow : forall T1 T2,
      well_formed_ty T1 ->
      well_formed_ty T2 ->
      well_formed_ty <{{ T1 -> T2 }}>
  | wfRNil :
      well_formed_ty <{{ nil }}>
  | wfRCons : forall l T Tr,
      well_formed_ty T ->
      well_formed_ty Tr ->
      record_ty Tr ->
      well_formed_ty <{{ l : T :: Tr }}>.

#[export] Hint Constructors record_ty record_tm well_formed_ty : core.

Substitution


Reserved Notation "t '[' x ':=' s ']'" (in custom stlc at level 20, x constr).
Fixpoint subst (x:string) (s:tm) (t:tm) : tm :=
  match t with
  | tm_var y =>
      if eqb x y then s else t
  | <{ \y:T, t1 }> =>
      if eqb x y then t else <{ \y:T, t1 [x:=s] }>
  | <{ t1 t2 }> =>
      <{ (t1 [x:=s]) (t2 [x:=s]) }>
  | <{ t1 --> l }> =>
      <{ (t1 [x:=s]) --> l }>
  | <{ nil }> =>
      <{ nil }>
  | <{ l = t1 :: tr }> =>
      <{ l = t1 [x:=s] :: (tr [x:=s]) }>
  end
where "t '[' x ':=' s ']'" := (subst x s t) (in custom stlc).

Reduction


Inductive value : tm -> Prop :=
  | v_abs : forall x T t,
      value <{ \x:T, t }>
  | v_rnil :
      value <{ nil }>
  | v_rcons : forall l v vr,
      value v ->
      value vr ->
      value <{ l = v :: vr }>.

#[export] Hint Constructors value : core.

Fixpoint Tlookup (l:string) (Tr:ty) : option ty :=
  match Tr with
  | <{{ l' : T :: Tr' }}> =>
      if eqb l l' then Some T else Tlookup l Tr'
  | _ => None
  end.

Fixpoint tlookup (l:string) (tr:tm) : option tm :=
  match tr with
  | <{ l' = t :: tr' }> =>
      if eqb l l' then Some t else tlookup l tr'
  | _ => None
  end.

Reserved Notation "t '-->' t'" (at level 40).
Inductive step : tm -> tm -> Prop :=
  | ST_AppAbs : forall x T2 t1 v2,
      value v2 ->
      <{ (\x:T2, t1) v2 }> --> <{ t1 [x:=v2] }>
  | ST_App1 : forall t1 t1' t2,
      t1 --> t1' ->
      <{ t1 t2 }> --> <{ t1' t2 }>
  | ST_App2 : forall v1 t2 t2',
      value v1 ->
      t2 --> t2' ->
      <{ v1 t2 }> --> <{ v1 t2' }>
  | ST_Proj1 : forall t1 t1' l,
      t1 --> t1' ->
      <{ t1 --> l }> --> <{ t1' --> l }>
  | ST_ProjRcd : forall tr l v,
      value tr ->
      tlookup l tr = Some v ->
      <{ tr --> l }> --> v
  | ST_Rcd_Head : forall l t t' tr,
      t --> t' ->
      <{ l = t :: tr }> --> <{ l = t' :: tr }>
  | ST_Rcd_Tail : forall l v tr tr',
      value v ->
      tr --> tr' ->
      <{ l = v :: tr }> --> <{ l = v :: tr' }>
where "t '-->' t'" := (step t t').

#[export] Hint Constructors step : core.

Reserved Notation "t '-->*' t'" (at level 40).
Inductive multistep : tm -> tm -> Prop :=
  | Multi_refl : forall (t : tm),
      t -->* t
  | Multi_step : forall (t1 t2 t3 : tm),
      t1 --> t2 ->
      t2 -->* t3 ->
      t1 -->* t3
where "t '-->*' t'" := (multistep t t').

Normal Forms


Definition normal_form (t : tm) : Prop :=
  ~ exists t', t --> t'.

Definition stuck (t : tm) : Prop :=
  normal_form t /\ ~ value t.

Subtyping


Reserved Notation "S '<:' T" (at level 40).
Inductive subtype : ty -> ty -> Prop :=
  | S_Refl : forall T,
      well_formed_ty T ->
      T <: T
  | S_Trans : forall R S T,
      R <: S ->
      S <: T ->
      R <: T
  | S_Top : forall S,
      well_formed_ty S ->
      S <: <{{ Top }}>
  | S_Arrow : forall S1 S2 T1 T2,
      T1 <: S1 ->
      S2 <: T2 ->
      <{{ S1 -> S2 }}> <: <{{ T1 -> T2 }}>
  | S_RcdWidth : forall l T Tr,
      well_formed_ty <{{ l : T :: Tr }}> ->
      <{{ l : T :: Tr }}> <: <{{ nil }}>
  | S_RcdDepth : forall l S Sr T Tr,
      S <: T ->
      Sr <: Tr ->
      record_ty Sr ->
      record_ty Tr ->
      <{{ l : S :: Sr }}> <: <{{ l : T :: Tr }}>
  | S_RcdPerm : forall l1 l2 T1 T2 Tr,
      well_formed_ty <{{ l1 : T1 :: l2 : T2 :: Tr }}> ->
      l1 <> l2 ->
      <{{ l1 : T1 :: l2 : T2 :: Tr }}> <: <{{ l2 : T2 :: l1 : T1 :: Tr }}>
where "S '<:' T" := (subtype S T).

#[export] Hint Constructors subtype : core.

Typing


Definition environment := string -> option ty.

Reserved Notation "Gamma '|-' t ':' T" (at level 40, t custom stlc at level 99, T custom stlc_ty at level 0).
Inductive has_type : environment -> tm -> ty -> Prop :=
  | T_Var : forall Gamma (x : string) T,
      Gamma x = Some T ->
      well_formed_ty T ->
      Gamma |- x : T
  | T_Abs : forall Gamma x T11 T12 t12,
      well_formed_ty T11 ->
      (x |-> T11; Gamma) |- t12 : T12 ->
      Gamma |- (\x:T11, t12) : (T11 -> T12)
  | T_App : forall T1 T2 Gamma t1 t2,
      Gamma |- t1 : (T1 -> T2) ->
      Gamma |- t2 : T1 ->
      Gamma |- t1 t2 : T2
  | T_Proj : forall Gamma l t R T,
      Gamma |- t : R ->
      Tlookup l R = Some T ->
      Gamma |- t --> l : T
  | T_Sub : forall Gamma t S T,
      Gamma |- t : S ->
      S <: T ->
      Gamma |- t : T
  | T_RNil : forall Gamma,
      Gamma |- nil : nil
  | T_RCons : forall Gamma l t T tr Tr,
      Gamma |- t : T ->
      Gamma |- tr : Tr ->
      record_ty Tr ->
      record_tm tr ->
      Gamma |- (l = t :: tr) : (l : T :: Tr)
where "Gamma '|-' t ':' T" := (has_type Gamma t T).

#[export] Hint Constructors has_type : core.