ReferencesTyping Mutable References
Require Import Coq.Arith.Arith.
Require Import Coq.omega.Omega.
Require Import Coq.Lists.List.
Import ListNotations.
Require Import Maps.
Require Import Smallstep.
Definitions
Syntax
The basic operations on references are allocation,
dereferencing, and assignment.
- To allocate a reference, we use the ref operator, providing
an initial value for the new cell. For example, ref 5
creates a new cell containing the value 5, and reduces to
a reference to that cell.
- To read the current value of this cell, we use the
dereferencing operator !; for example, !(ref 5) reduces
to 5.
- To change the value stored in a cell, we use the assignment operator. If r is a reference, r := 7 will store the value 7 in the cell referenced by r.
Types
T ::= Nat
| Unit
| T → T
| Ref T
| Unit
| T → T
| Ref T
Terms
t ::= ... Terms | ref t allocation | !t dereference | t := t assignment | l location
Inductive tm : Type :=
(* STLC with numbers: *)
| tvar : id → tm
| tapp : tm → tm → tm
| tabs : id → ty → tm → tm
| tnat : nat → tm
| tsucc : tm → tm
| tpred : tm → tm
| tmult : tm → tm → tm
| tif0 : tm → tm → tm → tm
(* New terms: *)
| tunit : tm
| tref : tm → tm
| tderef : tm → tm
| tassign : tm → tm → tm
| tloc : nat → tm.
Intuitively:
In informal examples, we'll also freely use the extensions
of the STLC developed in the MoreStlc chapter; however, to keep
the proofs small, we won't bother formalizing them again here. (It
would be easy to do so, since there are no very interesting
interactions between those features and references.)
- ref t (formally, tref t) allocates a new reference cell
with the value t and reduces to the location of the newly
allocated cell;
- !t (formally, tderef t) reduces to the contents of the
cell referenced by t;
- t_{1} := t_{2} (formally, tassign t_{1} t_{2}) assigns t_{2} to the
cell referenced by t_{1}; and
- l (formally, tloc l) is a reference to the cell at location l. We'll discuss locations later.
Typing (Preview)
Γ ⊢ t_{1} : T_{1} | (T_Ref) |
Γ ⊢ ref t_{1} : Ref T_{1} |
Γ ⊢ t_{1} : Ref T_{11} | (T_Deref) |
Γ ⊢ !t_{1} : T_{11} |
Γ ⊢ t_{1} : Ref T_{11} | |
Γ ⊢ t_{2} : T_{11} | (T_Assign) |
Γ ⊢ t_{1} := t_{2} : Unit |
Values and Substitution
Inductive value : tm → Prop :=
| v_abs : ∀x T t,
value (tabs x T t)
| v_nat : ∀n,
value (tnat n)
| v_unit :
value tunit
| v_loc : ∀l,
value (tloc l).
Hint Constructors value.
Extending substitution to handle the new syntax of terms is
straightforward.
Fixpoint subst (x:id) (s:tm) (t:tm) : tm :=
match t with
| tvar x' ⇒
if beq_id x x' then s else t
| tapp t_{1} t_{2} ⇒
tapp (subst x s t_{1}) (subst x s t_{2})
| tabs x' T t_{1} ⇒
if beq_id x x' then t else tabs x' T (subst x s t_{1})
| tnat n ⇒
t
| tsucc t_{1} ⇒
tsucc (subst x s t_{1})
| tpred t_{1} ⇒
tpred (subst x s t_{1})
| tmult t_{1} t_{2} ⇒
tmult (subst x s t_{1}) (subst x s t_{2})
| tif0 t_{1} t_{2} t_{3} ⇒
tif0 (subst x s t_{1}) (subst x s t_{2}) (subst x s t_{3})
| tunit ⇒
t
| tref t_{1} ⇒
tref (subst x s t_{1})
| tderef t_{1} ⇒
tderef (subst x s t_{1})
| tassign t_{1} t_{2} ⇒
tassign (subst x s t_{1}) (subst x s t_{2})
| tloc _ ⇒
t
end.
Notation "'[' x ':=' s ']' t" := (subst x s t) (at level 20).
Side Effects and Sequencing
r:=succ(!r); !ras an abbreviation for
(λx:Unit. !r) (r:=succ(!r)).This has the effect of reducing two expressions in order and returning the value of the second. Restricting the type of the first expression to Unit helps the typechecker to catch some silly errors by permitting us to throw away the first value only if it is really guaranteed to be trivial.
r:=succ(!r); r:=succ(!r); r:=succ(!r); r:=succ(!r); !rFormally, we introduce sequencing as a derived form tseq that expands into an abstraction and an application.
References and Aliasing
let r = ref 5 in let s = r in s := 82; (!r)+1the cell referenced by r will contain the value 82, while the result of the whole expression will be 83. The references r and s are said to be aliases for the same cell.
r := 5; r := !sassigns 5 to r and then immediately overwrites it with s's current value; this has exactly the same effect as the single assignment
r := !sunless we happen to do it in a context where r and s are aliases for the same cell!
Shared State
let c = ref 0 in let incc = λ_:Unit. (c := succ (!c); !c) in let decc = λ_:Unit. (c := pred (!c); !c) in ...
Objects
newcounter = λ_:Unit. let c = ref 0 in let incc = λ_:Unit. (c := succ (!c); !c) in let decc = λ_:Unit. (c := pred (!c); !c) in {i=incc, d=decc}
let c_{1} = newcounter unit in let c_{2} = newcounter unit in // Note that we've allocated two separate storage cells now! let r_{1} = c_{1}.i unit in let r_{2} = c_{2}.i unit in r_{2} // yields 1, not 2!
Exercise: 1 star (store_draw)
Draw (on paper) the contents of the store at the point in execution where the first two lets have finished and the third one is about to begin.(* FILL IN HERE *)
☐
References to Compound Types
equal = fix (λeq:Nat->Nat->Bool. λm:Nat. λn:Nat. if m=0 then iszero n else if n=0 then false else eq (pred m) (pred n))To build a new array, we allocate a reference cell and fill it with a function that, when given an index, always returns 0.
newarray = λ_:Unit. ref (λn:Nat.0)To look up an element of an array, we simply apply the function to the desired index.
lookup = λa:NatArray. λn:Nat. (!a) nThe interesting part of the encoding is the update function. It takes an array, an index, and a new value to be stored at that index, and does its job by creating (and storing in the reference) a new function that, when it is asked for the value at this very index, returns the new value that was given to update, while on all other indices it passes the lookup to the function that was previously stored in the reference.
update = λa:NatArray. λm:Nat. λv:Nat. let oldf = !a in a := (λn:Nat. if equal m n then v else oldf n);References to values containing other references can also be very useful, allowing us to define data structures such as mutable lists and trees.
Exercise: 2 stars, recommended (compact_update)
If we defined update more compactly like thisupdate = λa:NatArray. λm:Nat. λv:Nat. a := (λn:Nat. if equal m n then v else (!a) n)would it behave the same?
(* FILL IN HERE *)
☐
Null References
Garbage Collection
Exercise: 1 star (type_safety_violation)
Show how this can lead to a violation of type safety.(* FILL IN HERE *)
☐
Locations
Stores
We use store_lookup n st to retrieve the value of the reference
cell at location n in the store st. Note that we must give a
default value to nth in case we try looking up an index which is
too large. (In fact, we will never actually do this, but proving
that we don't will require a bit of work.)
To update the store, we use the replace function, which replaces
the contents of a cell at a particular index.
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.
As might be expected, we will also need some technical
lemmas about replace; they are straightforward to prove.
Lemma replace_nil : ∀A n (x:A),
replace n x nil = nil.
Proof.
destruct n; auto.
Qed.
destruct n; auto.
Qed.
Lemma length_replace : ∀A n x (l:list A),
length (replace n x l) = length l.
Proof with auto.
intros A n x l. generalize dependent n.
induction l; intros n.
destruct n...
destruct n...
simpl. rewrite IHl...
Qed.
intros A n x l. generalize dependent n.
induction l; intros n.
destruct n...
destruct n...
simpl. rewrite IHl...
Qed.
Lemma lookup_replace_eq : ∀l t st,
l < length st →
store_lookup l (replace l t st) = t.
Proof with auto.
intros l t st.
unfold store_lookup.
generalize dependent l.
induction st as [|t' st']; intros l Hlen.
- (* st = *)
inversion Hlen.
- (* st = t' :: st' *)
destruct l; simpl...
apply IHst'. simpl in Hlen. omega.
Qed.
intros l t st.
unfold store_lookup.
generalize dependent l.
induction st as [|t' st']; intros l Hlen.
- (* st = *)
inversion Hlen.
- (* st = t' :: st' *)
destruct l; simpl...
apply IHst'. simpl in Hlen. omega.
Qed.
Lemma lookup_replace_neq : ∀l_{1} l_{2} t st,
l_{1} ≠ l_{2} →
store_lookup l_{1} (replace l_{2} t st) = store_lookup l_{1} st.
Proof with auto.
unfold store_lookup.
induction l_{1} as [|l_{1}']; intros l_{2} t st Hneq.
- (* l_{1} = 0 *)
destruct st.
+ (* st = *) rewrite replace_nil...
+ (* st = _ :: _ *) destruct l_{2}... contradict Hneq...
- (* l_{1} = S l_{1}' *)
destruct st as [|t_{2} st_{2}].
+ (* st = *) destruct l_{2}...
+ (* st = t_{2} :: st_{2} *)
destruct l_{2}...
simpl; apply IHl1'...
Qed.
unfold store_lookup.
induction l_{1} as [|l_{1}']; intros l_{2} t st Hneq.
- (* l_{1} = 0 *)
destruct st.
+ (* st = *) rewrite replace_nil...
+ (* st = _ :: _ *) destruct l_{2}... contradict Hneq...
- (* l_{1} = S l_{1}' *)
destruct st as [|t_{2} st_{2}].
+ (* st = *) destruct l_{2}...
+ (* st = t_{2} :: st_{2} *)
destruct l_{2}...
simpl; apply IHl1'...
Qed.
Reduction
value v_{2} | (ST_AppAbs) |
(λx:T.t12) v_{2} / st ⇒ [x:=v_{2}]t_{12} / st |
t_{1} / st ⇒ t_{1}' / st' | (ST_App1) |
t_{1} t_{2} / st ⇒ t_{1}' t_{2} / st' |
value v_{1} t_{2} / st ⇒ t_{2}' / st' | (ST_App2) |
v_{1} t_{2} / st ⇒ v_{1} t_{2}' / st' |
t_{1} / st ⇒ t_{1}' / st' | (ST_Deref) |
!t_{1} / st ⇒ !t_{1}' / st' |
l < |st| | (ST_DerefLoc) |
!(loc l) / st ⇒ lookup l st / st |
t_{1} / st ⇒ t_{1}' / st' | (ST_Assign1) |
t_{1} := t_{2} / st ⇒ t_{1}' := t_{2} / st' |
t_{2} / st ⇒ t_{2}' / st' | (ST_Assign2) |
v_{1} := t_{2} / st ⇒ v_{1} := t_{2}' / st' |
l < |st| | (ST_Assign) |
loc l := v_{2} / st ⇒ unit / [l:=v_{2}]st |
t_{1} / st ⇒ t_{1}' / st' | (ST_Ref) |
ref t_{1} / st ⇒ ref t_{1}' / st' |
(ST_RefValue) | |
ref v_{1} / st ⇒ loc |st| / st,v_{1} |
Reserved Notation "t_{1} '/' st_{1} '⇒' t_{2} '/' st_{2}"
(at level 40, st_{1} at level 39, t_{2} at level 39).
Import ListNotations.
Inductive step : tm * store → tm * store → Prop :=
| ST_AppAbs : ∀x T t_{12} v_{2} st,
value v_{2} →
tapp (tabs x T t_{12}) v_{2} / st ⇒ [x:=v_{2}]t_{12} / st
| ST_App1 : ∀t_{1} t_{1}' t_{2} st st',
t_{1} / st ⇒ t_{1}' / st' →
tapp t_{1} t_{2} / st ⇒ tapp t_{1}' t_{2} / st'
| ST_App2 : ∀v_{1} t_{2} t_{2}' st st',
value v_{1} →
t_{2} / st ⇒ t_{2}' / st' →
tapp v_{1} t_{2} / st ⇒ tapp v_{1} t_{2}'/ st'
| ST_SuccNat : ∀n st,
tsucc (tnat n) / st ⇒ tnat (S n) / st
| ST_Succ : ∀t_{1} t_{1}' st st',
t_{1} / st ⇒ t_{1}' / st' →
tsucc t_{1} / st ⇒ tsucc t_{1}' / st'
| ST_PredNat : ∀n st,
tpred (tnat n) / st ⇒ tnat (pred n) / st
| ST_Pred : ∀t_{1} t_{1}' st st',
t_{1} / st ⇒ t_{1}' / st' →
tpred t_{1} / st ⇒ tpred t_{1}' / st'
| ST_MultNats : ∀n_{1} n_{2} st,
tmult (tnat n_{1}) (tnat n_{2}) / st ⇒ tnat (mult n_{1} n_{2}) / st
| ST_Mult1 : ∀t_{1} t_{2} t_{1}' st st',
t_{1} / st ⇒ t_{1}' / st' →
tmult t_{1} t_{2} / st ⇒ tmult t_{1}' t_{2} / st'
| ST_Mult2 : ∀v_{1} t_{2} t_{2}' st st',
value v_{1} →
t_{2} / st ⇒ t_{2}' / st' →
tmult v_{1} t_{2} / st ⇒ tmult v_{1} t_{2}' / st'
| ST_If_{0} : ∀t_{1} t_{1}' t_{2} t_{3} st st',
t_{1} / st ⇒ t_{1}' / st' →
tif0 t_{1} t_{2} t_{3} / st ⇒ tif0 t_{1}' t_{2} t_{3} / st'
| ST_If0_Zero : ∀t_{2} t_{3} st,
tif0 (tnat 0) t_{2} t_{3} / st ⇒ t_{2} / st
| ST_If0_Nonzero : ∀n t_{2} t_{3} st,
tif0 (tnat (S n)) t_{2} t_{3} / st ⇒ t_{3} / st
| ST_RefValue : ∀v_{1} st,
value v_{1} →
tref v_{1} / st ⇒ tloc (length st) / (st ++ v_{1}::nil)
| ST_Ref : ∀t_{1} t_{1}' st st',
t_{1} / st ⇒ t_{1}' / st' →
tref t_{1} / st ⇒ tref t_{1}' / st'
| ST_DerefLoc : ∀st l,
l < length st →
tderef (tloc l) / st ⇒ store_lookup l st / st
| ST_Deref : ∀t_{1} t_{1}' st st',
t_{1} / st ⇒ t_{1}' / st' →
tderef t_{1} / st ⇒ tderef t_{1}' / st'
| ST_Assign : ∀v_{2} l st,
value v_{2} →
l < length st →
tassign (tloc l) v_{2} / st ⇒ tunit / replace l v_{2} st
| ST_Assign1 : ∀t_{1} t_{1}' t_{2} st st',
t_{1} / st ⇒ t_{1}' / st' →
tassign t_{1} t_{2} / st ⇒ tassign t_{1}' t_{2} / st'
| ST_Assign2 : ∀v_{1} t_{2} t_{2}' st st',
value v_{1} →
t_{2} / st ⇒ t_{2}' / st' →
tassign v_{1} t_{2} / st ⇒ tassign v_{1} t_{2}' / st'
where "t_{1} '/' st_{1} '⇒' t_{2} '/' st_{2}" := (step (t_{1},st_{1}) (t_{2},st_{2})).
One slightly ugly point should be noted here: In the ST_RefValue
rule, we extend the state by writing st ++ v_{1}::nil rather than
the more natural st ++ [v_{1}]. The reason for this is that the
notation we've defined for substitution uses square brackets,
which clash with the standard library's notation for lists.
Hint Constructors step.
Definition multistep := (multi step).
Notation "t_{1} '/' st '⇒*' t_{2} '/' st'" :=
(multistep (t_{1},st) (t_{2},st'))
(at level 40, st at level 39, t_{2} at level 39).
Typing
Store typings
Γ ⊢ lookup l st : T_{1} | |
Γ ⊢ loc l : Ref T_{1} |
Gamma; st ⊢ lookup l st : T_{1} | |
Gamma; st ⊢ loc l : Ref T_{1} |
[\x:Nat. (!(loc 1)) x, λx:Nat. (!(loc 0)) x]
Exercise: 2 stars (cyclic_store)
Can you find a term whose reduction will create this particular cyclic store? ☐
The store_Tlookup function retrieves the type at a particular
index.
Suppose we are given a store typing ST describing the store
st in which some term t will be reduced. Then we can use
ST to calculate the type of the result of t without ever
looking directly at st. For example, if ST is [Unit,
Unit→Unit], then we can immediately infer that !(loc 1) has
type Unit→Unit. More generally, the typing rule for locations
can be reformulated in terms of store typings like this:
That is, as long as l is a valid location, we can compute the
type of l just by looking it up in ST. Typing is again a
four-place relation, but it is parameterized on a store typing
rather than a concrete store. The rest of the typing rules are
analogously augmented with store typings.
l < |ST| | |
Gamma; ST ⊢ loc l : Ref (lookup l ST) |
The Typing Relation
l < |ST| | (T_Loc) |
Gamma; ST ⊢ loc l : Ref (lookup l ST) |
Gamma; ST ⊢ t_{1} : T_{1} | (T_Ref) |
Gamma; ST ⊢ ref t_{1} : Ref T_{1} |
Gamma; ST ⊢ t_{1} : Ref T_{11} | (T_Deref) |
Gamma; ST ⊢ !t_{1} : T_{11} |
Gamma; ST ⊢ t_{1} : Ref T_{11} | |
Gamma; ST ⊢ t_{2} : T_{11} | (T_Assign) |
Gamma; ST ⊢ t_{1} := t_{2} : Unit |
Reserved Notation "Gamma ';' ST '⊢' t '∈' T" (at level 40).
Inductive has_type : context → store_ty → tm → ty → Prop :=
| T_Var : ∀Γ ST x T,
Γ x = Some T →
Γ; ST ⊢ (tvar x) ∈ T
| T_Abs : ∀Γ ST x T_{11} T_{12} t_{12},
(update Γ x T_{11}); ST ⊢ t_{12} ∈ T_{12} →
Γ; ST ⊢ (tabs x T_{11} t_{12}) ∈ (TArrow T_{11} T_{12})
| T_App : ∀T_{1} T_{2} Γ ST t_{1} t_{2},
Γ; ST ⊢ t_{1} ∈ (TArrow T_{1} T_{2}) →
Γ; ST ⊢ t_{2} ∈ T_{1} →
Γ; ST ⊢ (tapp t_{1} t_{2}) ∈ T_{2}
| T_Nat : ∀Γ ST n,
Γ; ST ⊢ (tnat n) ∈ TNat
| T_Succ : ∀Γ ST t_{1},
Γ; ST ⊢ t_{1} ∈ TNat →
Γ; ST ⊢ (tsucc t_{1}) ∈ TNat
| T_Pred : ∀Γ ST t_{1},
Γ; ST ⊢ t_{1} ∈ TNat →
Γ; ST ⊢ (tpred t_{1}) ∈ TNat
| T_Mult : ∀Γ ST t_{1} t_{2},
Γ; ST ⊢ t_{1} ∈ TNat →
Γ; ST ⊢ t_{2} ∈ TNat →
Γ; ST ⊢ (tmult t_{1} t_{2}) ∈ TNat
| T_If_{0} : ∀Γ ST t_{1} t_{2} t_{3} T,
Γ; ST ⊢ t_{1} ∈ TNat →
Γ; ST ⊢ t_{2} ∈ T →
Γ; ST ⊢ t_{3} ∈ T →
Γ; ST ⊢ (tif0 t_{1} t_{2} t_{3}) ∈ T
| T_Unit : ∀Γ ST,
Γ; ST ⊢ tunit ∈ TUnit
| T_Loc : ∀Γ ST l,
l < length ST →
Γ; ST ⊢ (tloc l) ∈ (TRef (store_Tlookup l ST))
| T_Ref : ∀Γ ST t_{1} T_{1},
Γ; ST ⊢ t_{1} ∈ T_{1} →
Γ; ST ⊢ (tref t_{1}) ∈ (TRef T_{1})
| T_Deref : ∀Γ ST t_{1} T_{11},
Γ; ST ⊢ t_{1} ∈ (TRef T_{11}) →
Γ; ST ⊢ (tderef t_{1}) ∈ T_{11}
| T_Assign : ∀Γ ST t_{1} t_{2} T_{11},
Γ; ST ⊢ t_{1} ∈ (TRef T_{11}) →
Γ; ST ⊢ t_{2} ∈ T_{11} →
Γ; ST ⊢ (tassign t_{1} t_{2}) ∈ TUnit
where "Gamma ';' ST '⊢' t '∈' T" := (has_type Γ ST t T).
Hint Constructors has_type.
Of course, these typing rules will accurately predict the results
of reduction only if the concrete store used during reduction
actually conforms to the store typing that we assume for purposes
of typechecking. This proviso exactly parallels the situation
with free variables in the basic STLC: the substitution lemma
promises that, if Γ ⊢ t : T, then we can replace the free
variables in t with values of the types listed in Γ to
obtain a closed term of type T, which, by the type preservation
theorem will reduce to a final result of type T if it yields
any result at all. We will see below how to formalize an
analogous intuition for stores and store typings.
However, for purposes of typechecking the terms that programmers
actually write, we do not need to do anything tricky to guess what
store typing we should use. Concrete locations arise only in
terms that are the intermediate results of reduction; they are
not in the language that programmers write. Thus, we can simply
typecheck the programmer's terms with respect to the empty store
typing. As reduction proceeds and new locations are created, we
will always be able to see how to extend the store typing by
looking at the type of the initial values being placed in newly
allocated cells; this intuition is formalized in the statement of
the type preservation theorem below.
Properties
Well-Typed Stores
Theorem preservation_wrong1 : ∀ST T t st t' st',
empty; ST ⊢ t ∈ T →
t / st ⇒ t' / st' →
empty; ST ⊢ t' ∈ T.
Abort.
If we typecheck with respect to some set of assumptions about the
types of the values in the store and then reduce with respect to
a store that violates these assumptions, the result will be
disaster. We say that a store st is well typed with respect a
store typing ST if the term at each location l in st has the
type at location l in ST. Since only closed terms ever get
stored in locations (why?), it suffices to type them in the empty
context. The following definition of store_well_typed formalizes
this.
Definition store_well_typed (ST:store_ty) (st:store) :=
length ST = length st ∧
(∀l, l < length st →
empty; ST ⊢ (store_lookup l st) ∈ (store_Tlookup l ST)).
Informally, we will write ST ⊢ st for store_well_typed ST st.
Intuitively, a store st is consistent with a store typing
ST if every value in the store has the type predicted by the
store typing. The only subtle point is the fact that, when
typing the values in the store, we supply the very same store
typing to the typing relation. This allows us to type circular
stores like the one we saw above.
Exercise: 2 stars (store_not_unique)
Can you find a store st, and two different store typings ST_{1} and ST_{2} such that both ST_{1} ⊢ st and ST_{2} ⊢ st?(* FILL IN HERE *)
☐
We can now state something closer to the desired preservation
property:
Theorem preservation_wrong2 : ∀ST T t st t' st',
empty; ST ⊢ t ∈ T →
t / st ⇒ t' / st' →
store_well_typed ST st →
empty; ST ⊢ t' ∈ T.
Abort.
This statement is fine for all of the reduction rules except
the allocation rule ST_RefValue. The problem is that this rule
yields a store with a larger domain than the initial store, which
falsifies the conclusion of the above statement: if st' includes
a binding for a fresh location l, then l cannot be in the
domain of ST, and it will not be the case that t' (which
definitely mentions l) is typable under ST.
Extending Store Typings
Inductive extends : store_ty → store_ty → Prop :=
| extends_nil : ∀ST',
extends ST' nil
| extends_cons : ∀x ST' ST,
extends ST' ST →
extends (x::ST') (x::ST).
Hint Constructors extends.
We'll need a few technical lemmas about extended contexts.
First, looking up a type in an extended store typing yields the
same result as in the original:
Lemma extends_lookup : ∀l ST ST',
l < length ST →
extends ST' ST →
store_Tlookup l ST' = store_Tlookup l ST.
Proof with auto.
intros l ST ST' Hlen H.
generalize dependent ST'. generalize dependent l.
induction ST as [|a ST_{2}]; intros l Hlen ST' HST'.
- (* nil *) inversion Hlen.
- (* cons *) unfold store_Tlookup in *.
destruct ST'.
+ (* ST' = nil *) inversion HST'.
+ (* ST' = a' :: ST'2 *)
inversion HST'; subst.
destruct l as [|l'].
* (* l = 0 *) auto.
* (* l = S l' *) simpl. apply IHST2...
simpl in Hlen; omega.
Qed.
intros l ST ST' Hlen H.
generalize dependent ST'. generalize dependent l.
induction ST as [|a ST_{2}]; intros l Hlen ST' HST'.
- (* nil *) inversion Hlen.
- (* cons *) unfold store_Tlookup in *.
destruct ST'.
+ (* ST' = nil *) inversion HST'.
+ (* ST' = a' :: ST'2 *)
inversion HST'; subst.
destruct l as [|l'].
* (* l = 0 *) auto.
* (* l = S l' *) simpl. apply IHST2...
simpl in Hlen; omega.
Qed.
Next, if ST' extends ST, the length of ST' is at least that
of ST.
Lemma length_extends : ∀l ST ST',
l < length ST →
extends ST' ST →
l < length ST'.
Proof with eauto.
intros. generalize dependent l. induction H_{0}; intros l Hlen.
inversion Hlen.
simpl in *.
destruct l; try omega.
apply lt_n_S. apply IHextends. omega.
Qed.
intros. generalize dependent l. induction H_{0}; intros l Hlen.
inversion Hlen.
simpl in *.
destruct l; try omega.
apply lt_n_S. apply IHextends. omega.
Qed.
Finally, ST ++ T extends ST, and extends is reflexive.
Lemma extends_app : ∀ST T,
extends (ST ++ T) ST.
Proof with auto.
induction ST; intros T...
simpl...
Qed.
induction ST; intros T...
simpl...
Qed.
Lemma extends_refl : ∀ST,
extends ST ST.
Proof.
induction ST; auto.
Qed.
induction ST; auto.
Qed.
Preservation, Finally
Definition preservation_theorem := ∀ST t t' T st st',
empty; ST ⊢ t ∈ T →
store_well_typed ST st →
t / st ⇒ t' / st' →
∃ST',
(extends ST' ST ∧
empty; ST' ⊢ t' ∈ T ∧
store_well_typed ST' st').
Note that the preservation theorem merely asserts that there is
some store typing ST' extending ST (i.e., agreeing with ST
on the values of all the old locations) such that the new term
t' is well typed with respect to ST'; it does not tell us
exactly what ST' is. It is intuitively clear, of course, that
ST' is either ST or else exactly ST ++ T_{1}::nil, where
T_{1} is the type of the value v_{1} in the extended store st ++
v_{1}::nil, but stating this explicitly would complicate the statement of
the theorem without actually making it any more useful: the weaker
version above is already in the right form (because its conclusion
implies its hypothesis) to "turn the crank" repeatedly and
conclude that every sequence of reduction steps preserves
well-typedness. Combining this with the progress property, we
obtain the usual guarantee that "well-typed programs never go
wrong."
In order to prove this, we'll need a few lemmas, as usual.
Substitution Lemma
Inductive appears_free_in : id → tm → Prop :=
| afi_var : ∀x,
appears_free_in x (tvar x)
| afi_app1 : ∀x t_{1} t_{2},
appears_free_in x t_{1} → appears_free_in x (tapp t_{1} t_{2})
| afi_app2 : ∀x t_{1} t_{2},
appears_free_in x t_{2} → appears_free_in x (tapp t_{1} t_{2})
| afi_abs : ∀x y T_{11} t_{12},
y ≠ x →
appears_free_in x t_{12} →
appears_free_in x (tabs y T_{11} t_{12})
| afi_succ : ∀x t_{1},
appears_free_in x t_{1} →
appears_free_in x (tsucc t_{1})
| afi_pred : ∀x t_{1},
appears_free_in x t_{1} →
appears_free_in x (tpred t_{1})
| afi_mult1 : ∀x t_{1} t_{2},
appears_free_in x t_{1} →
appears_free_in x (tmult t_{1} t_{2})
| afi_mult2 : ∀x t_{1} t_{2},
appears_free_in x t_{2} →
appears_free_in x (tmult t_{1} t_{2})
| afi_if0_1 : ∀x t_{1} t_{2} t_{3},
appears_free_in x t_{1} →
appears_free_in x (tif0 t_{1} t_{2} t_{3})
| afi_if0_2 : ∀x t_{1} t_{2} t_{3},
appears_free_in x t_{2} →
appears_free_in x (tif0 t_{1} t_{2} t_{3})
| afi_if0_3 : ∀x t_{1} t_{2} t_{3},
appears_free_in x t_{3} →
appears_free_in x (tif0 t_{1} t_{2} t_{3})
| afi_ref : ∀x t_{1},
appears_free_in x t_{1} → appears_free_in x (tref t_{1})
| afi_deref : ∀x t_{1},
appears_free_in x t_{1} → appears_free_in x (tderef t_{1})
| afi_assign1 : ∀x t_{1} t_{2},
appears_free_in x t_{1} → appears_free_in x (tassign t_{1} t_{2})
| afi_assign2 : ∀x t_{1} t_{2},
appears_free_in x t_{2} → appears_free_in x (tassign t_{1} t_{2}).
Hint Constructors appears_free_in.
Lemma free_in_context : ∀x t T Γ ST,
appears_free_in x t →
Γ; ST ⊢ t ∈ T →
∃T', Γ x = Some T'.
Proof with eauto.
intros. generalize dependent Γ. generalize dependent T.
induction H;
intros; (try solve [ inversion H_{0}; subst; eauto ]).
- (* afi_abs *)
inversion H_{1}; subst.
apply IHappears_free_in in H_{8}.
rewrite update_neq in H_{8}; assumption.
Qed.
intros. generalize dependent Γ. generalize dependent T.
induction H;
intros; (try solve [ inversion H_{0}; subst; eauto ]).
- (* afi_abs *)
inversion H_{1}; subst.
apply IHappears_free_in in H_{8}.
rewrite update_neq in H_{8}; assumption.
Qed.
Lemma context_invariance : ∀Γ Γ' ST t T,
Γ; ST ⊢ t ∈ T →
(∀x, appears_free_in x t → Γ x = Γ' x) →
Γ'; ST ⊢ t ∈ T.
Proof with eauto.
intros.
generalize dependent Γ'.
induction H; intros...
- (* T_Var *)
apply T_Var. symmetry. rewrite ← H...
- (* T_Abs *)
apply T_Abs. apply IHhas_type; intros.
unfold update, t_update.
destruct (beq_idP x x_{0})...
- (* T_App *)
eapply T_App.
apply IHhas_type1...
apply IHhas_type2...
- (* T_Mult *)
eapply T_Mult.
apply IHhas_type1...
apply IHhas_type2...
- (* T_If_{0} *)
eapply T_If_{0}.
apply IHhas_type1...
apply IHhas_type2...
apply IHhas_type3...
- (* T_Assign *)
eapply T_Assign.
apply IHhas_type1...
apply IHhas_type2...
Qed.
intros.
generalize dependent Γ'.
induction H; intros...
- (* T_Var *)
apply T_Var. symmetry. rewrite ← H...
- (* T_Abs *)
apply T_Abs. apply IHhas_type; intros.
unfold update, t_update.
destruct (beq_idP x x_{0})...
- (* T_App *)
eapply T_App.
apply IHhas_type1...
apply IHhas_type2...
- (* T_Mult *)
eapply T_Mult.
apply IHhas_type1...
apply IHhas_type2...
- (* T_If_{0} *)
eapply T_If_{0}.
apply IHhas_type1...
apply IHhas_type2...
apply IHhas_type3...
- (* T_Assign *)
eapply T_Assign.
apply IHhas_type1...
apply IHhas_type2...
Qed.
Lemma substitution_preserves_typing : ∀Γ ST x s S t T,
empty; ST ⊢ s ∈ S →
(update Γ x S); ST ⊢ t ∈ T →
Γ; ST ⊢ ([x:=s]t) ∈ T.
Proof with eauto.
intros Γ ST x s S t T Hs Ht.
generalize dependent Γ. generalize dependent T.
induction t; intros T Γ H;
inversion H; subst; simpl...
- (* tvar *)
rename i into y.
destruct (beq_idP x y).
+ (* x = y *)
subst.
rewrite update_eq in H_{3}.
inversion H_{3}; subst.
eapply context_invariance...
intros x Hcontra.
destruct (free_in_context _ _ _ _ _ Hcontra Hs)
as [T' HT'].
inversion HT'.
+ (* x <> y *)
apply T_Var.
rewrite update_neq in H_{3}...
- (* tabs *) subst.
rename i into y.
destruct (beq_idP x y).
+ (* x = y *)
subst.
apply T_Abs. eapply context_invariance...
intros. rewrite update_shadow. reflexivity.
+ (* x <> x_{0} *)
apply T_Abs. apply IHt.
eapply context_invariance...
intros. unfold update, t_update.
destruct (beq_idP y x_{0})...
subst.
rewrite false_beq_id...
Qed.
intros Γ ST x s S t T Hs Ht.
generalize dependent Γ. generalize dependent T.
induction t; intros T Γ H;
inversion H; subst; simpl...
- (* tvar *)
rename i into y.
destruct (beq_idP x y).
+ (* x = y *)
subst.
rewrite update_eq in H_{3}.
inversion H_{3}; subst.
eapply context_invariance...
intros x Hcontra.
destruct (free_in_context _ _ _ _ _ Hcontra Hs)
as [T' HT'].
inversion HT'.
+ (* x <> y *)
apply T_Var.
rewrite update_neq in H_{3}...
- (* tabs *) subst.
rename i into y.
destruct (beq_idP x y).
+ (* x = y *)
subst.
apply T_Abs. eapply context_invariance...
intros. rewrite update_shadow. reflexivity.
+ (* x <> x_{0} *)
apply T_Abs. apply IHt.
eapply context_invariance...
intros. unfold update, t_update.
destruct (beq_idP y x_{0})...
subst.
rewrite false_beq_id...
Qed.
Assignment Preserves Store Typing
Lemma assign_pres_store_typing : ∀ST st l t,
l < length st →
store_well_typed ST st →
empty; ST ⊢ t ∈ (store_Tlookup l ST) →
store_well_typed ST (replace l t st).
Proof with auto.
intros ST st l t Hlen HST Ht.
inversion HST; subst.
split. rewrite length_replace...
intros l' Hl'.
destruct (beq_nat l' l) eqn: Heqll'.
- (* l' = l *)
apply beq_nat_true in Heqll'; subst.
rewrite lookup_replace_eq...
- (* l' <> l *)
apply beq_nat_false in Heqll'.
rewrite lookup_replace_neq...
rewrite length_replace in Hl'.
apply H_{0}...
Qed.
intros ST st l t Hlen HST Ht.
inversion HST; subst.
split. rewrite length_replace...
intros l' Hl'.
destruct (beq_nat l' l) eqn: Heqll'.
- (* l' = l *)
apply beq_nat_true in Heqll'; subst.
rewrite lookup_replace_eq...
- (* l' <> l *)
apply beq_nat_false in Heqll'.
rewrite lookup_replace_neq...
rewrite length_replace in Hl'.
apply H_{0}...
Qed.
Weakening for Stores
Lemma store_weakening : ∀Γ ST ST' t T,
extends ST' ST →
Γ; ST ⊢ t ∈ T →
Γ; ST' ⊢ t ∈ T.
Proof with eauto.
intros. induction H_{0}; eauto.
- (* T_Loc *)
erewrite ← extends_lookup...
apply T_Loc.
eapply length_extends...
Qed.
intros. induction H_{0}; eauto.
- (* T_Loc *)
erewrite ← extends_lookup...
apply T_Loc.
eapply length_extends...
Qed.
We can use the store_weakening lemma to prove that if a store is
well typed with respect to a store typing, then the store extended
with a new term t will still be well typed with respect to the
store typing extended with t's type.
Lemma store_well_typed_app : ∀ST st t_{1} T_{1},
store_well_typed ST st →
empty; ST ⊢ t_{1} ∈ T_{1} →
store_well_typed (ST ++ T_{1}::nil) (st ++ t_{1}::nil).
Proof with auto.
intros.
unfold store_well_typed in *.
inversion H as [Hlen Hmatch]; clear H.
rewrite app_length, plus_comm. simpl.
rewrite app_length, plus_comm. simpl.
split...
- (* types match. *)
intros l Hl.
unfold store_lookup, store_Tlookup.
apply le_lt_eq_dec in Hl; inversion Hl as [Hlt | Heq].
+ (* l < length st *)
apply lt_S_n in Hlt.
rewrite !app_nth1...
* apply store_weakening with ST. apply extends_app.
apply Hmatch...
* rewrite Hlen...
+ (* l = length st *)
inversion Heq.
rewrite app_nth2; try omega.
rewrite ← Hlen.
rewrite minus_diag. simpl.
apply store_weakening with ST...
{ apply extends_app. }
rewrite app_nth2; try omega.
rewrite minus_diag. simpl. trivial.
Qed.
intros.
unfold store_well_typed in *.
inversion H as [Hlen Hmatch]; clear H.
rewrite app_length, plus_comm. simpl.
rewrite app_length, plus_comm. simpl.
split...
- (* types match. *)
intros l Hl.
unfold store_lookup, store_Tlookup.
apply le_lt_eq_dec in Hl; inversion Hl as [Hlt | Heq].
+ (* l < length st *)
apply lt_S_n in Hlt.
rewrite !app_nth1...
* apply store_weakening with ST. apply extends_app.
apply Hmatch...
* rewrite Hlen...
+ (* l = length st *)
inversion Heq.
rewrite app_nth2; try omega.
rewrite ← Hlen.
rewrite minus_diag. simpl.
apply store_weakening with ST...
{ apply extends_app. }
rewrite app_nth2; try omega.
rewrite minus_diag. simpl. trivial.
Qed.
Preservation!
Lemma nth_eq_last : ∀A (l:list A) x d,
nth (length l) (l ++ x::nil) d = x.
Proof.
induction l; intros; [ auto | simpl; rewrite IHl; auto ].
Qed.
induction l; intros; [ auto | simpl; rewrite IHl; auto ].
Qed.
And here, at last, is the preservation theorem and proof:
Theorem preservation : ∀ST t t' T st st',
empty; ST ⊢ t ∈ T →
store_well_typed ST st →
t / st ⇒ t' / st' →
∃ST',
(extends ST' ST ∧
empty; ST' ⊢ t' ∈ T ∧
store_well_typed ST' st').
Proof with eauto using store_weakening, extends_refl.
remember (@empty ty) as Γ.
intros ST t t' T st st' Ht.
generalize dependent t'.
induction Ht; intros t' HST Hstep;
subst; try solve_by_invert; inversion Hstep; subst;
try (eauto using store_weakening, extends_refl).
(* T_App *)
- (* ST_AppAbs *) ∃ST.
inversion Ht_{1}; subst.
split; try split... eapply substitution_preserves_typing...
- (* ST_App1 *)
eapply IHHt1 in H_{0}...
inversion H_{0} as [ST' [Hext [Hty Hsty]]].
∃ST'...
- (* ST_App2 *)
eapply IHHt2 in H_{5}...
inversion H_{5} as [ST' [Hext [Hty Hsty]]].
∃ST'...
- (* T_Succ *)
+ (* ST_Succ *)
eapply IHHt in H_{0}...
inversion H_{0} as [ST' [Hext [Hty Hsty]]].
∃ST'...
- (* T_Pred *)
+ (* ST_Pred *)
eapply IHHt in H_{0}...
inversion H_{0} as [ST' [Hext [Hty Hsty]]].
∃ST'...
(* T_Mult *)
- (* ST_Mult1 *)
eapply IHHt1 in H_{0}...
inversion H_{0} as [ST' [Hext [Hty Hsty]]].
∃ST'...
- (* ST_Mult2 *)
eapply IHHt2 in H_{5}...
inversion H_{5} as [ST' [Hext [Hty Hsty]]].
∃ST'...
- (* T_If_{0} *)
+ (* ST_If0_1 *)
eapply IHHt1 in H_{0}...
inversion H_{0} as [ST' [Hext [Hty Hsty]]].
∃ST'... split...
(* T_Ref *)
- (* ST_RefValue *)
∃(ST ++ T_{1}::nil).
inversion HST; subst.
split.
apply extends_app.
split.
replace (TRef T_{1})
with (TRef (store_Tlookup (length st) (ST ++ T_{1}::nil))).
apply T_Loc.
rewrite ← H. rewrite app_length, plus_comm. simpl. omega.
unfold store_Tlookup. rewrite ← H. rewrite nth_eq_last.
reflexivity.
apply store_well_typed_app; assumption.
- (* ST_Ref *)
eapply IHHt in H_{0}...
inversion H_{0} as [ST' [Hext [Hty Hsty]]].
∃ST'...
(* T_Deref *)
- (* ST_DerefLoc *)
∃ST. split; try split...
inversion HST as [_ Hsty].
replace T_{11} with (store_Tlookup l ST).
apply Hsty...
inversion Ht; subst...
- (* ST_Deref *)
eapply IHHt in H_{0}...
inversion H_{0} as [ST' [Hext [Hty Hsty]]].
∃ST'...
(* T_Assign *)
- (* ST_Assign *)
∃ST. split; try split...
eapply assign_pres_store_typing...
inversion Ht_{1}; subst...
- (* ST_Assign1 *)
eapply IHHt1 in H_{0}...
inversion H_{0} as [ST' [Hext [Hty Hsty]]].
∃ST'...
- (* ST_Assign2 *)
eapply IHHt2 in H_{5}...
inversion H_{5} as [ST' [Hext [Hty Hsty]]].
∃ST'...
Qed.
remember (@empty ty) as Γ.
intros ST t t' T st st' Ht.
generalize dependent t'.
induction Ht; intros t' HST Hstep;
subst; try solve_by_invert; inversion Hstep; subst;
try (eauto using store_weakening, extends_refl).
(* T_App *)
- (* ST_AppAbs *) ∃ST.
inversion Ht_{1}; subst.
split; try split... eapply substitution_preserves_typing...
- (* ST_App1 *)
eapply IHHt1 in H_{0}...
inversion H_{0} as [ST' [Hext [Hty Hsty]]].
∃ST'...
- (* ST_App2 *)
eapply IHHt2 in H_{5}...
inversion H_{5} as [ST' [Hext [Hty Hsty]]].
∃ST'...
- (* T_Succ *)
+ (* ST_Succ *)
eapply IHHt in H_{0}...
inversion H_{0} as [ST' [Hext [Hty Hsty]]].
∃ST'...
- (* T_Pred *)
+ (* ST_Pred *)
eapply IHHt in H_{0}...
inversion H_{0} as [ST' [Hext [Hty Hsty]]].
∃ST'...
(* T_Mult *)
- (* ST_Mult1 *)
eapply IHHt1 in H_{0}...
inversion H_{0} as [ST' [Hext [Hty Hsty]]].
∃ST'...
- (* ST_Mult2 *)
eapply IHHt2 in H_{5}...
inversion H_{5} as [ST' [Hext [Hty Hsty]]].
∃ST'...
- (* T_If_{0} *)
+ (* ST_If0_1 *)
eapply IHHt1 in H_{0}...
inversion H_{0} as [ST' [Hext [Hty Hsty]]].
∃ST'... split...
(* T_Ref *)
- (* ST_RefValue *)
∃(ST ++ T_{1}::nil).
inversion HST; subst.
split.
apply extends_app.
split.
replace (TRef T_{1})
with (TRef (store_Tlookup (length st) (ST ++ T_{1}::nil))).
apply T_Loc.
rewrite ← H. rewrite app_length, plus_comm. simpl. omega.
unfold store_Tlookup. rewrite ← H. rewrite nth_eq_last.
reflexivity.
apply store_well_typed_app; assumption.
- (* ST_Ref *)
eapply IHHt in H_{0}...
inversion H_{0} as [ST' [Hext [Hty Hsty]]].
∃ST'...
(* T_Deref *)
- (* ST_DerefLoc *)
∃ST. split; try split...
inversion HST as [_ Hsty].
replace T_{11} with (store_Tlookup l ST).
apply Hsty...
inversion Ht; subst...
- (* ST_Deref *)
eapply IHHt in H_{0}...
inversion H_{0} as [ST' [Hext [Hty Hsty]]].
∃ST'...
(* T_Assign *)
- (* ST_Assign *)
∃ST. split; try split...
eapply assign_pres_store_typing...
inversion Ht_{1}; subst...
- (* ST_Assign1 *)
eapply IHHt1 in H_{0}...
inversion H_{0} as [ST' [Hext [Hty Hsty]]].
∃ST'...
- (* ST_Assign2 *)
eapply IHHt2 in H_{5}...
inversion H_{5} as [ST' [Hext [Hty Hsty]]].
∃ST'...
Qed.
Exercise: 3 stars (preservation_informal)
Write a careful informal proof of the preservation theorem, concentrating on the T_App, T_Deref, T_Assign, and T_Ref cases.☐
Progress
Theorem progress : ∀ST t T st,
empty; ST ⊢ t ∈ T →
store_well_typed ST st →
(value t ∨ ∃t', ∃st', t / st ⇒ t' / st').
Proof with eauto.
intros ST t T st Ht HST. remember (@empty ty) as Γ.
induction Ht; subst; try solve_by_invert...
- (* T_App *)
right. destruct IHHt1 as [Ht1p | Ht1p]...
+ (* t_{1} is a value *)
inversion Ht1p; subst; try solve_by_invert.
destruct IHHt2 as [Ht2p | Ht2p]...
* (* t_{2} steps *)
inversion Ht2p as [t_{2}' [st' Hstep]].
∃(tapp (tabs x T t) t_{2}'). ∃st'...
+ (* t_{1} steps *)
inversion Ht1p as [t_{1}' [st' Hstep]].
∃(tapp t_{1}' t_{2}). ∃st'...
- (* T_Succ *)
right. destruct IHHt as [Ht1p | Ht1p]...
+ (* t_{1} is a value *)
inversion Ht1p; subst; try solve [ inversion Ht ].
* (* t_{1} is a tnat *)
∃(tnat (S n)). ∃st...
+ (* t_{1} steps *)
inversion Ht1p as [t_{1}' [st' Hstep]].
∃(tsucc t_{1}'). ∃st'...
- (* T_Pred *)
right. destruct IHHt as [Ht1p | Ht1p]...
+ (* t_{1} is a value *)
inversion Ht1p; subst; try solve [inversion Ht ].
* (* t_{1} is a tnat *)
∃(tnat (pred n)). ∃st...
+ (* t_{1} steps *)
inversion Ht1p as [t_{1}' [st' Hstep]].
∃(tpred t_{1}'). ∃st'...
- (* T_Mult *)
right. destruct IHHt1 as [Ht1p | Ht1p]...
+ (* t_{1} is a value *)
inversion Ht1p; subst; try solve [inversion Ht_{1}].
destruct IHHt2 as [Ht2p | Ht2p]...
* (* t_{2} is a value *)
inversion Ht2p; subst; try solve [inversion Ht_{2}].
∃(tnat (mult n n_{0})). ∃st...
* (* t_{2} steps *)
inversion Ht2p as [t_{2}' [st' Hstep]].
∃(tmult (tnat n) t_{2}'). ∃st'...
+ (* t_{1} steps *)
inversion Ht1p as [t_{1}' [st' Hstep]].
∃(tmult t_{1}' t_{2}). ∃st'...
- (* T_If_{0} *)
right. destruct IHHt1 as [Ht1p | Ht1p]...
+ (* t_{1} is a value *)
inversion Ht1p; subst; try solve [inversion Ht_{1}].
destruct n.
* (* n = 0 *) ∃t_{2}. ∃st...
* (* n = S n' *) ∃t_{3}. ∃st...
+ (* t_{1} steps *)
inversion Ht1p as [t_{1}' [st' Hstep]].
∃(tif0 t_{1}' t_{2} t_{3}). ∃st'...
- (* T_Ref *)
right. destruct IHHt as [Ht1p | Ht1p]...
+ (* t_{1} steps *)
inversion Ht1p as [t_{1}' [st' Hstep]].
∃(tref t_{1}'). ∃st'...
- (* T_Deref *)
right. destruct IHHt as [Ht1p | Ht1p]...
+ (* t_{1} is a value *)
inversion Ht1p; subst; try solve_by_invert.
eexists. eexists. apply ST_DerefLoc...
inversion Ht; subst. inversion HST; subst.
rewrite ← H...
+ (* t_{1} steps *)
inversion Ht1p as [t_{1}' [st' Hstep]].
∃(tderef t_{1}'). ∃st'...
- (* T_Assign *)
right. destruct IHHt1 as [Ht1p|Ht1p]...
+ (* t_{1} is a value *)
destruct IHHt2 as [Ht2p|Ht2p]...
* (* t_{2} is a value *)
inversion Ht1p; subst; try solve_by_invert.
eexists. eexists. apply ST_Assign...
inversion HST; subst. inversion Ht_{1}; subst.
rewrite H in H_{5}...
* (* t_{2} steps *)
inversion Ht2p as [t_{2}' [st' Hstep]].
∃(tassign t_{1} t_{2}'). ∃st'...
+ (* t_{1} steps *)
inversion Ht1p as [t_{1}' [st' Hstep]].
∃(tassign t_{1}' t_{2}). ∃st'...
Qed.
intros ST t T st Ht HST. remember (@empty ty) as Γ.
induction Ht; subst; try solve_by_invert...
- (* T_App *)
right. destruct IHHt1 as [Ht1p | Ht1p]...
+ (* t_{1} is a value *)
inversion Ht1p; subst; try solve_by_invert.
destruct IHHt2 as [Ht2p | Ht2p]...
* (* t_{2} steps *)
inversion Ht2p as [t_{2}' [st' Hstep]].
∃(tapp (tabs x T t) t_{2}'). ∃st'...
+ (* t_{1} steps *)
inversion Ht1p as [t_{1}' [st' Hstep]].
∃(tapp t_{1}' t_{2}). ∃st'...
- (* T_Succ *)
right. destruct IHHt as [Ht1p | Ht1p]...
+ (* t_{1} is a value *)
inversion Ht1p; subst; try solve [ inversion Ht ].
* (* t_{1} is a tnat *)
∃(tnat (S n)). ∃st...
+ (* t_{1} steps *)
inversion Ht1p as [t_{1}' [st' Hstep]].
∃(tsucc t_{1}'). ∃st'...
- (* T_Pred *)
right. destruct IHHt as [Ht1p | Ht1p]...
+ (* t_{1} is a value *)
inversion Ht1p; subst; try solve [inversion Ht ].
* (* t_{1} is a tnat *)
∃(tnat (pred n)). ∃st...
+ (* t_{1} steps *)
inversion Ht1p as [t_{1}' [st' Hstep]].
∃(tpred t_{1}'). ∃st'...
- (* T_Mult *)
right. destruct IHHt1 as [Ht1p | Ht1p]...
+ (* t_{1} is a value *)
inversion Ht1p; subst; try solve [inversion Ht_{1}].
destruct IHHt2 as [Ht2p | Ht2p]...
* (* t_{2} is a value *)
inversion Ht2p; subst; try solve [inversion Ht_{2}].
∃(tnat (mult n n_{0})). ∃st...
* (* t_{2} steps *)
inversion Ht2p as [t_{2}' [st' Hstep]].
∃(tmult (tnat n) t_{2}'). ∃st'...
+ (* t_{1} steps *)
inversion Ht1p as [t_{1}' [st' Hstep]].
∃(tmult t_{1}' t_{2}). ∃st'...
- (* T_If_{0} *)
right. destruct IHHt1 as [Ht1p | Ht1p]...
+ (* t_{1} is a value *)
inversion Ht1p; subst; try solve [inversion Ht_{1}].
destruct n.
* (* n = 0 *) ∃t_{2}. ∃st...
* (* n = S n' *) ∃t_{3}. ∃st...
+ (* t_{1} steps *)
inversion Ht1p as [t_{1}' [st' Hstep]].
∃(tif0 t_{1}' t_{2} t_{3}). ∃st'...
- (* T_Ref *)
right. destruct IHHt as [Ht1p | Ht1p]...
+ (* t_{1} steps *)
inversion Ht1p as [t_{1}' [st' Hstep]].
∃(tref t_{1}'). ∃st'...
- (* T_Deref *)
right. destruct IHHt as [Ht1p | Ht1p]...
+ (* t_{1} is a value *)
inversion Ht1p; subst; try solve_by_invert.
eexists. eexists. apply ST_DerefLoc...
inversion Ht; subst. inversion HST; subst.
rewrite ← H...
+ (* t_{1} steps *)
inversion Ht1p as [t_{1}' [st' Hstep]].
∃(tderef t_{1}'). ∃st'...
- (* T_Assign *)
right. destruct IHHt1 as [Ht1p|Ht1p]...
+ (* t_{1} is a value *)
destruct IHHt2 as [Ht2p|Ht2p]...
* (* t_{2} is a value *)
inversion Ht1p; subst; try solve_by_invert.
eexists. eexists. apply ST_Assign...
inversion HST; subst. inversion Ht_{1}; subst.
rewrite H in H_{5}...
* (* t_{2} steps *)
inversion Ht2p as [t_{2}' [st' Hstep]].
∃(tassign t_{1} t_{2}'). ∃st'...
+ (* t_{1} steps *)
inversion Ht1p as [t_{1}' [st' Hstep]].
∃(tassign t_{1}' t_{2}). ∃st'...
Qed.
References and Nontermination
(λr:Ref (Unit -> Unit). r := (λx:Unit.(!r) unit); (!r) unit) (ref (λx:Unit.unit))First, ref (λx:Unit.unit) creates a reference to a cell of type Unit → Unit. We then pass this reference as the argument to a function which binds it to the name r, and assigns to it the function \x:Unit.(!r) unit — that is, the function which ignores its argument and calls the function stored in r on the argument unit; but of course, that function is itself! To start the divergent loop, we execute the function stored in the cell by evaluating (!r) unit.
Module ExampleVariables.
Definition x := Id "x".
Definition y := Id "y".
Definition r := Id "r".
Definition s := Id "s".
End ExampleVariables.
Module RefsAndNontermination.
Import ExampleVariables.
Definition loop_fun :=
tabs x TUnit (tapp (tderef (tvar r)) tunit).
Definition loop :=
tapp
(tabs r (TRef (TArrow TUnit TUnit))
(tseq (tassign (tvar r) loop_fun)
(tapp (tderef (tvar r)) tunit)))
(tref (tabs x TUnit tunit)).
This term is well typed:
Lemma loop_typeable : ∃T, empty; nil ⊢ loop ∈ T.
Proof with eauto.
eexists. unfold loop. unfold loop_fun.
eapply T_App...
eapply T_Abs...
eapply T_App...
eapply T_Abs. eapply T_App. eapply T_Deref. eapply T_Var.
unfold update, t_update. simpl. reflexivity. auto.
eapply T_Assign.
eapply T_Var. unfold update, t_update. simpl. reflexivity.
eapply T_Abs.
eapply T_App...
eapply T_Deref. eapply T_Var. reflexivity.
Qed.
eexists. unfold loop. unfold loop_fun.
eapply T_App...
eapply T_Abs...
eapply T_App...
eapply T_Abs. eapply T_App. eapply T_Deref. eapply T_Var.
unfold update, t_update. simpl. reflexivity. auto.
eapply T_Assign.
eapply T_Var. unfold update, t_update. simpl. reflexivity.
eapply T_Abs.
eapply T_App...
eapply T_Deref. eapply T_Var. reflexivity.
Qed.
To show formally that the term diverges, we first define the
step_closure of the single-step reduction relation, written
⇒+. This is just like the reflexive step closure of
single-step reduction (which we're been writing ⇒*), except
that it is not reflexive: t ⇒+ t' means that t can reach
t' by one or more steps of reduction.
Inductive step_closure {X:Type} (R: relation X) : X → X → Prop :=
| sc_one : ∀(x y : X),
R x y → step_closure R x y
| sc_step : ∀(x y z : X),
R x y →
step_closure R y z →
step_closure R x z.
Definition multistep1 := (step_closure step).
Notation "t_{1} '/' st '⇒+' t_{2} '/' st'" :=
(multistep1 (t_{1},st) (t_{2},st'))
(at level 40, st at level 39, t_{2} at level 39).
Now, we can show that the expression loop reduces to the
expression !(loc 0) unit and the size-one store
[r:=(loc 0)]loop_fun.
As a convenience, we introduce a slight variant of the normalize
tactic, called reduce, which tries solving the goal with
multi_refl at each step, instead of waiting until the goal can't
be reduced any more. Of course, the whole point is that loop
doesn't normalize, so the old normalize tactic would just go
into an infinite loop reducing it forever!
Ltac print_goal := match goal with ⊢ ?x ⇒ idtac x end.
Ltac reduce :=
repeat (print_goal; eapply multi_step ;
[ (eauto 10; fail) | (instantiate; compute)];
try solve [apply multi_refl]).
Next, we use reduce to show that loop steps to
!(loc 0) unit, starting from the empty store.
Lemma loop_steps_to_loop_fun :
loop / nil ⇒*
tapp (tderef (tloc 0)) tunit / cons ([r:=tloc 0]loop_fun) nil.
Proof.
unfold loop.
reduce.
Qed.
Finally, we show that the latter expression reduces in
two steps to itself!
Lemma loop_fun_step_self :
tapp (tderef (tloc 0)) tunit / cons ([r:=tloc 0]loop_fun) nil ⇒+
tapp (tderef (tloc 0)) tunit / cons ([r:=tloc 0]loop_fun) nil.
Proof with eauto.
unfold loop_fun; simpl.
eapply sc_step. apply ST_App1...
eapply sc_one. compute. apply ST_AppAbs...
Qed.
unfold loop_fun; simpl.
eapply sc_step. apply ST_App1...
eapply sc_one. compute. apply ST_AppAbs...
Qed.
Exercise: 4 stars (factorial_ref)
Use the above ideas to implement a factorial function in STLC with references. (There is no need to prove formally that it really behaves like the factorial. Just uncomment the example below to make sure it gives the correct result when applied to the argument 4.)Definition factorial : tm
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Lemma factorial_type : empty; nil ⊢ factorial ∈ (TArrow TNat TNat).
Proof with eauto.
(* FILL IN HERE *) Admitted.
If your definition is correct, you should be able to just
uncomment the example below; the proof should be fully
automatic using the reduce tactic.
(*
Lemma factorial_4 : exists st,
tapp factorial (tnat 4) / nil ==>* tnat 24 / st.
Proof.
eexists. unfold factorial. reduce.
Qed.
*)
☐