This Kata is part of a collection of supplementary exercises for Programming Language Foundations.

Subtyping Mutable References

The key definitions, concepts and notations presented in this Kata are adapted from the Software Foundations series, an excellent resource for learning Coq.

Prerequisites

You should have at least read and understood the content presented in the following chapters of Programming Language Foundations:

• Subtyping (Sub)
• Typing Mutable References (References)

Task

The calculus we shall consider in this Kata is the simply typed lambda calculus extended with subtyping and mutable references. Your task is to prove the progress and preservation theorems for this calculus.

A brief description of each component of our calculus as well as more detailed explanations on the nonstandard sections have been included as comments within the Preloaded section which is displayed in full below for your reference.

Preloaded.v

(* Preloaded.v

   The key definitions and notations presented in this file are
   adapted from the Software Foundations series, an excellent
   resource for learning Coq:
   https://softwarefoundations.cis.upenn.edu/current/index.html

   The copyright notice of the series is reproduced below as
   follows:

   Copyright (c) 2019

   Permission is hereby granted, free of charge, to any person obtaining a copy
   of this software and associated documentation files (the "Software"), to deal
   in the Software without restriction, including without limitation the rights
   to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
   copies of the Software, and to permit persons to whom the Software is
   furnished to do so, subject to the following conditions:

   The above copyright notice and this permission notice shall be included in
   all copies or substantial portions of the Software.

   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
   OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
   THE SOFTWARE. *)

(* Preliminaries (mostly taken from "Total and Partial Maps
   (Maps)" of "Logical Foundations") *)

From Coq Require Import Strings.String.

From Coq Require Import Lists.List.

Definition eqb_string (x y : string) : bool :=
  if string_dec x y then true else false.

Definition total_map (A : Type) := string -> A.

Definition t_empty {A : Type} (v : A) : total_map A :=
  (fun _ => v).

Definition t_update {A : Type} (m : total_map A)
                    (x : string) (v : A) :=
  fun x' => if eqb_string x x' then v else m x'.

Notation "'_' '!->' v" := (t_empty v)
  (at level 100, right associativity).

Notation "x '!->' v ';' m" := (t_update m x v)
                              (at level 100, v at next level, right associativity).

Definition partial_map (A : Type) := total_map (option A).

Definition empty {A : Type} : partial_map A :=
  t_empty None.

Definition update {A : Type} (m : partial_map A)
           (x : string) (v : A) :=
  (x !-> Some v ; m).

Notation "x '|->' v ';' m" := (update m x v)
  (at level 100, v at next level, right associativity).

Notation "x '|->' v" := (update empty x v)
  (at level 100).

(* Types in our STLC with subtyping and references *)

(* These are just a combination of those found in "Subtyping
   (Sub)" and "Typing Mutable References (References)" of
   "Programming Language Foundations" with the exception of
   two new type constructors: [RRef] and [WRef] representing
   "read-only reference" and "write-only reference"
   respectively *)

Inductive ty : Type :=
  | Top : ty
  | Bool : ty
  | Nat : ty
  | Arrow : ty -> ty -> ty
  | Unit : ty
  | Ref : ty -> ty
  | RRef : ty -> ty
  | WRef : ty -> ty.

(* Terms in our STLC with subtyping and references *)

(* Again, these are just a combination of the terms you've
   seen before - in fact, there are no new terms to be
   introduced since [ref] and [loc] themselves can be treated
   as read-only or write-only references depending on the
   context

   We also remove [test0] from the natural numbers since
   booleans already provide the [test] conditional *)

Inductive tm : Type :=
  (* Pure STLC *)
  | var : string -> tm
  | app : tm -> tm -> tm
  | abs : string -> ty -> tm -> tm
  (* Booleans *)
  | tru : tm
  | fls : tm
  | test : tm -> tm -> tm -> tm
  (* Natural numbers *)
  | const : nat -> tm
  | scc : tm -> tm
  | prd : tm -> tm
  | mlt : tm -> tm -> tm
  (* Unit *)
  | unit : tm
  (* References *)
  | ref : tm -> tm
  | deref : tm -> tm
  | assign : tm -> tm -> tm
  | loc : nat -> tm.

(* Substitution in our STLC with subtyping and references *)

(* These are the same as in what you've seen before *)

Fixpoint subst (x : string) (s : tm) (t : tm) : tm :=
  match t with
  | var x' =>
      if eqb_string x x' then s else t
  | app t1 t2 =>
      app (subst x s t1) (subst x s t2)
  | abs x' T t1 =>
      if eqb_string x x' then t else abs x' T (subst x s t1)
  | tru =>
      tru
  | fls =>
      fls
  | test t1 t2 t3 =>
      test (subst x s t1) (subst x s t2) (subst x s t3)
  | const n =>
      t
  | scc t1 =>
      scc (subst x s t1)
  | prd t1 =>
      prd (subst x s t1)
  | mlt t1 t2 =>
      mlt (subst x s t1) (subst x s t2)
  | unit =>
      t
  | ref t1 =>
      ref (subst x s t1)
  | deref t1 =>
      deref (subst x s t1)
  | assign t1 t2 =>
      assign (subst x s t1) (subst x s t2)
  | loc _ =>
      t
  end.

Notation "'[' x ':=' s ']' t" := (subst x s t) (at level 20).

(* Values in our STLC with subtyping and references *)

(* As you'd expect, the values in our STLC with subtyping
   and references is just a combination of those in "Sub"
   and "References" *)

Inductive value : tm -> Prop :=
  | v_abs : forall x T t,
      value (abs x T t)
  | v_true :
      value tru
  | v_false :
      value fls
  | v_nat : forall n,
      value (const n)
  | v_unit :
      value unit
  | v_loc : forall l,
      value (loc l).

(* Stores and store typings in our STLC with subtyping and
   references *)

(* These are the same as what you've seen in "References" *)

Definition store := list tm.

Definition store_lookup (n:nat) (st:store) :=
  nth n st unit.

Fixpoint replace {A:Type} (n:nat) (x:A) (l:list A) : list A :=
  match l with
  | nil => nil
  | h :: t =>
    match n with
    | O => x :: t
    | S n' => h :: replace n' x t
    end
  end.

Definition store_ty := list ty.

Definition store_Tlookup (n:nat) (ST:store_ty) :=
  nth n ST Unit.

(* Reduction in our STLC with subtyping and references *)

(* The rules are just a combination of those found in "Sub"
   and "References" except the rules for booleans in "Sub"
   are modified to take the store into account as well *)

Reserved Notation "t1 '/' st1 '-->' t2 '/' st2"
  (at level 40, st1 at level 39, t2 at level 39).

Import ListNotations.

Inductive step : tm * store -> tm * store -> Prop :=
  | ST_AppAbs : forall x T t12 v2 st,
         value v2 ->
         app (abs x T t12) v2 / st --> [x:=v2]t12 / st
  | ST_App1 : forall t1 t1' t2 st st',
         t1 / st --> t1' / st' ->
         app t1 t2 / st --> app t1' t2 / st'
  | ST_App2 : forall v1 t2 t2' st st',
         value v1 ->
         t2 / st --> t2' / st' ->
         app v1 t2 / st --> app v1 t2'/ st'
  | ST_TestTrue : forall t2 t3 st,
         test tru t2 t3 / st --> t2 / st
  | ST_TestFalse : forall t2 t3 st,
         test fls t2 t3 / st --> t3 / st
  | ST_Test : forall t1 t1' t2 t3 st st',
         t1 / st --> t1' / st' ->
         test t1 t2 t3 / st --> test t1' t2 t3 / st'
  | ST_SuccNat : forall n st,
         scc (const n) / st --> const (S n) / st
  | ST_Succ : forall t1 t1' st st',
         t1 / st --> t1' / st' ->
         scc t1 / st --> scc t1' / st'
  | ST_PredNat : forall n st,
         prd (const n) / st --> const (pred n) / st
  | ST_Pred : forall t1 t1' st st',
         t1 / st --> t1' / st' ->
         prd t1 / st --> prd t1' / st'
  | ST_MultNats : forall n1 n2 st,
         mlt (const n1) (const n2) / st --> const (mult n1 n2) / st
  | ST_Mult1 : forall t1 t2 t1' st st',
         t1 / st --> t1' / st' ->
         mlt t1 t2 / st --> mlt t1' t2 / st'
  | ST_Mult2 : forall v1 t2 t2' st st',
         value v1 ->
         t2 / st --> t2' / st' ->
         mlt v1 t2 / st --> mlt v1 t2' / st'
  | ST_RefValue : forall v1 st,
         value v1 ->
         ref v1 / st --> loc (length st) / (st ++ v1::nil)
  | ST_Ref : forall t1 t1' st st',
         t1 / st --> t1' / st' ->
         ref t1 / st --> ref t1' / st'
  | ST_DerefLoc : forall st l,
         l < length st ->
         deref (loc l) / st --> store_lookup l st / st
  | ST_Deref : forall t1 t1' st st',
         t1 / st --> t1' / st' ->
         deref t1 / st --> deref t1' / st'
  | ST_Assign : forall v2 l st,
         value v2 ->
         l < length st ->
         assign (loc l) v2 / st --> unit / replace l v2 st
  | ST_Assign1 : forall t1 t1' t2 st st',
         t1 / st --> t1' / st' ->
         assign t1 t2 / st --> assign t1' t2 / st'
  | ST_Assign2 : forall v1 t2 t2' st st',
         value v1 ->
         t2 / st --> t2' / st' ->
         assign v1 t2 / st --> assign v1 t2' / st'


  where "t1 '/' st1 '-->' t2 '/' st2" := (step (t1,st1) (t2,st2)).

(* Subtyping in our STLC with subtyping and references *)

(* You will have seen most of the subtyping rules before
   except the ones involving (read-write) references,
   read-only and write-only references.

   First of all, we have that a read-write reference to [T]
   is a subtype of both a read-only reference to [T] and a
   write-only reference to [T] by the subtyping rules
   [S_Ref_RRef] and [S_Ref_WRef], respectively.

                    --------------- (S_Ref_RRef)
                    Ref T <: RRef T

                    --------------- (S_Ref_WRef)
                    Ref T <: WRef T

   These two subtyping rules should be obvious considering
   that the subtyping relation can be interpreted as "is at
   least as good as".

   The subtyping rule for read-only references should also
   be obvious: [RRef] is _covariant_ in its argument as you
   might expect.

                         S <: T
                    ---------------- (S_RRef)
                    RRef S <: RRef T

   The interesting case here is the subtyping rule for
   write-only references: it turns out that, in order to
   achieve type-safety, [WRef] should actually by
   _contravariant_ in its argument.

                         T <: S
                    ---------------- (S_WRef)
                    WRef S <: WRef T

   Why might that be? An intuitive explanation of this
   considers the range of operations that are possible on a
   [WRef S] and a [WRef T], assuming [T <: S]:

   - An element of type [T] can be safely written to both a
     [WRef S] and a [WRef T] since in the former case, the
     element of type [T] is also an element of type [S] (by
     the rule of subsumption) and it is trivial in the latter
     case
   - However, an arbitrary element of type [S] (which _may_
     or _may not_ be an element of type [T]) cannot be safely
     written to a write-only reference expecting an element
     of type [T]

   In that sense, a [WRef S] is "at least as good as" a
   [WRef T] precisely when [T <: S].

   As for read-write references, since adding a similar
   subtyping rule would require that it be both covariant
   and contravariant in its argument (which is obviously
   impossible), we simply leave it _invariant_ in its
   argument, i.e. no subtyping rule telling us the subtyping
   relation between [Ref S] and [Ref T] when [S <: T]. *)

Reserved Notation "T '<:' U" (at level 40).

Inductive subtype : ty -> ty -> Prop :=
  | S_Refl : forall T,
      T <: T
  | S_Trans : forall S U T,
      S <: U ->
      U <: T ->
      S <: T
  | S_Top : forall S,
      S <: Top
  | S_Arrow : forall S1 S2 T1 T2,
      T1 <: S1 ->
      S2 <: T2 ->
      (Arrow S1 S2) <: (Arrow T1 T2)
  | S_Ref_RRef : forall T,
      Ref T <: RRef T
  | S_Ref_WRef : forall T,
      Ref T <: WRef T
  | S_RRef : forall S T,
      S <: T ->
      RRef S <: RRef T
  | S_WRef : forall S T,
      T <: S ->
      WRef S <: WRef T

where "T '<:' U" := (subtype T U).

(* Typing in our STLC with subtyping and references *)

(* Our typing relation combines that from "Sub" and
   "References" except we modify [T_Deref] and [T_Assign]
   to expect [RRef]s and [WRef]s respectively - the rule of
   subsumption [T_Sub] automatically allows us to perform
   both reads ([deref]) and writes ([assign]) on ordinary
   (read-write) references *)

Definition context := partial_map ty.

Reserved Notation "Gamma ';' ST '|-' t '\in' T" (at level 40).

Inductive has_type : context -> store_ty -> tm -> ty -> Prop :=
  | T_Var : forall Gamma ST x T,
      Gamma x = Some T ->
      Gamma; ST |- (var x) \in T
  | T_Abs : forall Gamma ST x T11 T12 t12,
      (update Gamma x T11); ST |- t12 \in T12 ->
      Gamma; ST |- (abs x T11 t12) \in (Arrow T11 T12)
  | T_App : forall T1 T2 Gamma ST t1 t2,
      Gamma; ST |- t1 \in (Arrow T1 T2) ->
      Gamma; ST |- t2 \in T1 ->
      Gamma; ST |- (app t1 t2) \in T2
  | T_Tru : forall Gamma ST,
      Gamma; ST |- tru \in Bool
  | T_Fls : forall Gamma ST,
      Gamma; ST |- fls \in Bool
  | T_Test : forall Gamma ST t1 t2 t3 T,
      Gamma; ST |- t1 \in Bool ->
      Gamma; ST |- t2 \in T ->
      Gamma; ST |- t3 \in T ->
      Gamma; ST |- test t1 t2 t3 \in T
  | T_Nat : forall Gamma ST n,
      Gamma; ST |- (const n) \in Nat
  | T_Succ : forall Gamma ST t1,
      Gamma; ST |- t1 \in Nat ->
      Gamma; ST |- (scc t1) \in Nat
  | T_Pred : forall Gamma ST t1,
      Gamma; ST |- t1 \in Nat ->
      Gamma; ST |- (prd t1) \in Nat
  | T_Mult : forall Gamma ST t1 t2,
      Gamma; ST |- t1 \in Nat ->
      Gamma; ST |- t2 \in Nat ->
      Gamma; ST |- (mlt t1 t2) \in Nat
  | T_Unit : forall Gamma ST,
      Gamma; ST |- unit \in Unit
  | T_Loc : forall Gamma ST l,
      l < length ST ->
      Gamma; ST |- (loc l) \in (Ref (store_Tlookup l ST))
  | T_Ref : forall Gamma ST t1 T1,
      Gamma; ST |- t1 \in T1 ->
      Gamma; ST |- (ref t1) \in (Ref T1)
  | T_Deref : forall Gamma ST t1 T11,
      Gamma; ST |- t1 \in (RRef T11) ->
      Gamma; ST |- (deref t1) \in T11
  | T_Assign : forall Gamma ST t1 t2 T11,
      Gamma; ST |- t1 \in (WRef T11) ->
      Gamma; ST |- t2 \in T11 ->
      Gamma; ST |- (assign t1 t2) \in Unit
  | T_Sub : forall Gamma ST t S T,
      Gamma; ST |- t \in S ->
      S <: T ->
      Gamma; ST |- t \in T

where "Gamma ';' ST '|-' t '\in' T" := (has_type Gamma ST t T).

(* Store typings for our STLC with subtyping and references *)

(* These are identical to those found in "References" *)

Definition store_well_typed (ST:store_ty) (st:store) :=
  length ST = length st /\
  (forall l, l < length st ->
     empty; ST |- (store_lookup l st) \in (store_Tlookup l ST)).

Inductive extends : store_ty -> store_ty -> Prop :=
  | extends_nil : forall ST',
      extends ST' nil
  | extends_cons : forall x ST' ST,
      extends ST' ST ->
      extends (x::ST') (x::ST).