Commit 79621926 authored by Robbert Krebbers's avatar Robbert Krebbers

Work on comments.

parent 8602ad8c
......@@ -64,7 +64,8 @@ Section interp_properties.
n length ρ
ty_lift n τ ρ τ (delete n ρ).
Proof.
(* We use [elim:] instead of [induction] so we can properly name hyps *)
(** We use [elim:] instead of [induction] so we can properly name the
generated variables and hypotheses. *)
revert n ρ. elim: τ; simpl; try (intros; done || f_equiv/=; by auto).
- intros x n ρ ?. repeat case_decide; simplify_eq/=; try lia.
+ by rewrite lookup_delete_lt.
......@@ -90,7 +91,8 @@ Section interp_properties.
i length ρ
ty_subst i τ' τ ρ τ (take i ρ ++ τ' ρ :: drop i ρ).
Proof.
(* We use [elim:] instead of [induction] so we can properly name hyps *)
(** We use [elim:] instead of [induction] so we can properly name the
generated variables and hypotheses. *)
revert i τ' ρ. elim: τ; simpl; try (intros; done || f_equiv/=; by auto).
- intros x i τ' ρ ?. repeat case_decide; simplify_eq/=; try lia.
+ rewrite lookup_app_l; last (rewrite take_length; lia).
......
......@@ -2,20 +2,23 @@ From iris.heap_lang Require Export adequacy.
From tutorial_popl20 Require Export fundamental.
(** * Semantic and syntactic type safety *)
(** We prove that any _closed_ expression that is semantically typed is safe,
i.e., it does not crash. Based on this theorem we then prove _syntactic type
safety_, i.e., any _closed_ syntactically well-typed program is safe. Semantic
type safety is a consequence of Iris's adequacy theorem, and syntactic type
safety is a consequence of the fundamental theorem of logical relations together
with the safety for semantic typing. *)
(** We prove *semantic type safety*, which says that any _closed_ expression
that is semantically typed is safe, i.e., it does not crash. Based on this
theorem we then prove *syntactic type safety* as a corollary, i.e., any _closed_ syntactically well-typed program is safe. Semantic type safety is a consequence
of Iris's adequacy theorem, and syntactic type safety is a consequence of the
fundamental theorem together and semantic type safety. *)
(** ** Semantic type safety *)
(** The following lemma states that given a closed program [e], heap [σ], and
(** ** Semantic type safety *)
(** Before proving semantic type safety, we first prove a stronger lemma. We
use this lemma in the file [parametricity.v] to prove parametricity properties.
This stronger lemma states that given a closed program [e], heap [σ], and a
_Coq_ predicate [φ : val → Prop], if there is a semantic type [A] such that [A]
implies [φ], and [e] is semantically typed at type [A], then we have
[adequate NotStuck e σ (λ v σ, φ v)]. The proposition
[adequate NotStuck e σ (λ v σ, φ v)] means that [e], starting in heap [σ] does
not get stuck, and if [e] reduces to a value [v], we have [φ v]. *)
[adequate NotStuck e σ (λ v σ, φ v)].
The proposition [adequate NotStuck e σ (λ v σ, φ v)] (which is defined in the
Iris library) means that [e], starting in heap [σ] does not get stuck, and if
[e] reduces to a value [v], we have [φ v]. *)
Lemma sem_gen_type_safety `{!heapPreG Σ} e σ φ :
( `{!heapG Σ}, A : sem_ty Σ, ( v, A v - ⌜φ v) ( e : A)%I)
adequate NotStuck e σ (λ v σ, φ v).
......@@ -28,9 +31,9 @@ Proof.
by iIntros; iApply HA.
Qed.
(** This lemma states that semantically typed closed programs do not get stuck.
It is a simple consequence of the lemma [sem_gen_type_safety] above. *)
Lemma sem_type_safety `{!heapPreG Σ} e σ es σ' e' :
(** The actual theorem for semantic type safety lemma states that semantically
typed closed programs do not get stuck. It is a simple consequence of the lemma [sem_gen_type_safety] above. *)
Theorem sem_type_safety `{!heapPreG Σ} e σ es σ' e' :
( `{!heapG Σ}, A, ( e : A)%I)
rtc erased_step ([e], σ) (es, σ') e' es
is_Some (to_val e') reducible e' σ'.
......@@ -41,7 +44,9 @@ Proof.
Qed.
(** ** Syntactic type safety *)
Lemma type_safety e σ es σ' e' τ :
(** Syntactic type safety is a consequence of the fundamental theorem together
and semantic type safety. *)
Corollary type_safety e σ es σ' e' τ :
( e : τ)
rtc erased_step ([e], σ) (es, σ') e' es
is_Some (to_val e') reducible e' σ'.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment