LambdaProj.Definitions
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.
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.
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).
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').
Definition normal_form (t : tm) : Prop :=
~ exists t', t --> t'.
Definition stuck (t : tm) : Prop :=
normal_form t /\ ~ value t.
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.
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.