Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Fengmin Zhu
Tutorial POPL20
Commits
14ee8d5f
Commit
14ee8d5f
authored
Jan 20, 2020
by
Robbert Krebbers
Browse files
More comments.
parent
c7362b6b
Changes
4
Hide whitespace changes
Inline
Side-by-side
_CoqProject
View file @
14ee8d5f
-Q solutions
tutorial_popl20
-Q solutions
solutions
# non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
-arg -w -arg -redundant-canonical-projection
# change_no_check does not exist yet in 8.9.
...
...
solutions/interp.v
View file @
14ee8d5f
...
...
@@ -3,8 +3,10 @@ From tutorial_popl20 Require Export sem_typed sem_type_formers types.
(** * Interpretation of syntactic types *)
(** We use semantic type formers to define the interpretation [⟦ τ ⟧ : sem_ty]
of syntactic types [τ : ty]. The interpretation is defined recursively on the
structure of syntactic types. *)
structure of syntactic types. To account for type variables (that appear freely
in [τ]), we need to keep track of their corresponding semantic types. We
represent these semantic types as a list, since de use De Bruijn indices for
type variables. *)
Reserved
Notation
"⟦ τ ⟧"
.
Fixpoint
interp
`
{!
heapG
Σ
}
(
τ
:
ty
)
(
ρ
:
list
(
sem_ty
Σ
))
:
sem_ty
Σ
:
=
match
τ
return
_
with
...
...
@@ -20,16 +22,10 @@ Fixpoint interp `{!heapG Σ} (τ : ty) (ρ : list (sem_ty Σ)) : sem_ty Σ :=
|
TRef
τ
=>
ref
(
⟦
τ
⟧
ρ
)
end
%
sem_ty
where
"⟦ τ ⟧"
:
=
(
interp
τ
).
Instance
:
Params
(@
interp
)
2
:
=
{}.
(** Given a syntactic typing context [Γ : gmap string ty] (a mapping from
variables [string] to syntactic types [ty]) together with a mapping
[ρ : list (sem_ty Σ)] from type variables (that appear freely in [Γ]) to
their corresponding semantic types (represented as a list, since de use De
Bruijn indices for type variables), we define a semantic typing context
[interp_env Γ ρ : gmap string (sem_ty Σ)], i.e., a mapping from variables
(strings) to semantic types. *)
(** We now lift the interpretation of types to typing contexts. This is done in
a pointwise fashion using the [<$> : (A → B) → gmap K A → gmap K B] operator. *)
Definition
interp_env
`
{!
heapG
Σ
}
(
Γ
:
gmap
string
ty
)
(
ρ
:
list
(
sem_ty
Σ
))
:
gmap
string
(
sem_ty
Σ
)
:
=
flip
interp
ρ
<$>
Γ
.
Instance
:
Params
(@
interp_env
)
3
:
=
{}.
...
...
solutions/parametricity.v
View file @
14ee8d5f
From
tutorial_popl20
Require
Export
safety
.
(** * Parametricity *)
Section
parametricity
.
Context
`
{!
heapG
Σ
}.
(** * The polymorphic identity function *)
Lemma
identity_param
`
{!
heapPreG
Σ
}
e
(
v
:
val
)
σ
w
es
σ
'
:
(
∀
`
{!
heapG
Σ
},
(
∅
⊨
e
:
∀
A
,
A
→
A
)%
I
)
→
rtc
erased_step
([
e
<
_
>
v
]%
E
,
σ
)
(
of_val
w
::
es
,
σ
'
)
→
w
=
v
.
...
...
@@ -20,6 +22,7 @@ Section parametricity.
wp_apply
(
wp_wand
with
"Hu"
).
iIntros
(
w'
)
"Hw'"
.
by
iApply
"Hw'"
.
Qed
.
(** * Exercise (empty_type_param, easy) *)
Lemma
empty_type_param
`
{!
heapPreG
Σ
}
e
(
v
:
val
)
σ
w
es
σ
'
:
(
∀
`
{!
heapG
Σ
},
(
∅
⊨
e
:
∀
A
,
A
)%
I
)
→
rtc
erased_step
([
e
<
_
>]%
E
,
σ
)
(
of_val
w
::
es
,
σ
'
)
→
...
...
@@ -38,6 +41,7 @@ Section parametricity.
iApply
(
"Hu"
$!
T
).
Qed
.
(** * Exercise (boolean_param, moderate) *)
Lemma
boolean_param
`
{!
heapPreG
Σ
}
e
(
v1
v2
:
val
)
σ
w
es
σ
'
:
(
∀
`
{!
heapG
Σ
},
(
∅
⊨
e
:
∀
A
,
A
→
A
→
A
)%
I
)
→
rtc
erased_step
([
e
<
_
>
v1
v2
]%
E
,
σ
)
(
of_val
w
::
es
,
σ
'
)
→
w
=
v1
∨
w
=
v2
.
...
...
@@ -59,6 +63,7 @@ Section parametricity.
iApply
(
"Hw''"
$!
v2
).
by
iRight
.
Qed
.
(** * Exercise (nat_param, hard) *)
Lemma
nat_param
`
{!
heapPreG
Σ
}
e
σ
w
es
σ
'
:
(
∀
`
{!
heapG
Σ
},
(
∅
⊨
e
:
∀
A
,
(
A
→
A
)
→
A
→
A
)%
I
)
→
rtc
erased_step
([
e
<
_
>
(
λ
:
"n"
,
"n"
+
#
1
)%
V
#
0
]%
E
,
σ
)
...
...
@@ -85,6 +90,7 @@ Section parametricity.
by
iExists
0
%
nat
.
Qed
.
(** * Exercise (strong_nat_param, hard) *)
Lemma
strong_nat_param
`
{!
heapPreG
Σ
}
e
σ
w
es
σ
'
(
vf
vz
:
val
)
φ
:
(
∀
`
{!
heapG
Σ
},
∃
Φ
:
sem_ty
Σ
,
(
∅
⊨
e
:
∀
A
,
(
A
→
A
)
→
A
→
A
)%
I
∧
...
...
solutions/sem_type_formers.v
View file @
14ee8d5f
...
...
@@ -92,7 +92,7 @@ Section types.
Definition
sem_ty_ref
(
A
:
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
∃
l
:
loc
,
⌜
w
=
#
l
⌝
∧
inv
(
tyN
.@
l
)
(
∃
v
,
l
↦
v
∗
A
v
))%
I
.
(** Intuitively, values of the reference type [sem_ty_ref A] should
be locations
l
that hold a value [w] in the semantic type [A] at
be locations
[l]
that hold a value [w] in the semantic type [A] at
all times. In order to express this intuition in a formal way, we
make use of two features of Iris:
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment