pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Revising for next lecture

Browse source
This commit is contained in:
Adam Chlipala 2021-04-18 16:23:25 -04:00
parent 796fc8d64c
commit b549b15af7
2 changed files with 8 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
DeepAndShallowEmbeddings.v
View file

@ -14,8 +14,8 @@ Notation "m $! k" := (match m $? k with Some n => n | None => O end) (at level 3
Definition heap := fmap nat nat. Definition heap := fmap nat nat.
Definition assertion := heap -> Prop. Definition assertion := heap -> Prop.
Hint Extern 1 (_ <= _) => linear_arithmetic : core. Local Hint Extern 1 (_ <= _) => linear_arithmetic : core.
Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core. Local Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
Example h0 : heap := $0 $+ (0, 2) $+ (1, 1) $+ (2, 8) $+ (3, 6). Example h0 : heap := $0 $+ (0, 2) $+ (1, 1) $+ (2, 8) $+ (3, 6).
@ -494,6 +494,7 @@ Module Deep.
eauto. eauto.
Qed. Qed.
End Deep. End Deep.
(* We use Coq's *extraction* feature to produce OCaml versions of our deeply (* We use Coq's *extraction* feature to produce OCaml versions of our deeply
* embedded programs. Then we can run them using OCaml intepreters, which are * embedded programs. Then we can run them using OCaml intepreters, which are
* able to take advantage of the side effects built into OCaml, as a * able to take advantage of the side effects built into OCaml, as a
@ -839,6 +840,7 @@ End Deeper.
Extraction "Deeper.ml" Deeper.index_of. Extraction "Deeper.ml" Deeper.index_of.
(** * Adding the possibility of program failure *) (** * Adding the possibility of program failure *)
(* Let's model another effect that can be implemented using native OCaml (* Let's model another effect that can be implemented using native OCaml
@ -1270,7 +1272,7 @@ Module DeeperWithFail.
apply IHls; linear_arithmetic. apply IHls; linear_arithmetic.
Qed. Qed.
Hint Resolve le_max : core. Local Hint Resolve le_max : core.
(* Finally, a short proof of [array_max], appealing mostly to the generic (* Finally, a short proof of [array_max], appealing mostly to the generic
* proof of [heapfold] *) * proof of [heapfold] *)

6
DeepAndShallowEmbeddings_template.v
View file

@ -9,8 +9,8 @@ Notation "m $! k" := (match m $? k with Some n => n | None => O end) (at level 3
Definition heap := fmap nat nat. Definition heap := fmap nat nat.
Definition assertion := heap -> Prop. Definition assertion := heap -> Prop.
Hint Extern 1 (_ <= _) => linear_arithmetic : core. Local Hint Extern 1 (_ <= _) => linear_arithmetic : core.
Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core. Local Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
Example h0 : heap := $0 $+ (0, 2) $+ (1, 1) $+ (2, 8) $+ (3, 6). Example h0 : heap := $0 $+ (0, 2) $+ (1, 1) $+ (2, 8) $+ (3, 6).
@ -1085,7 +1085,7 @@ Module DeeperWithFail.
apply IHls; linear_arithmetic. apply IHls; linear_arithmetic.
Qed. Qed.
Hint Resolve le_max : core. Local Hint Resolve le_max : core.
Theorem array_max_ok : forall ls : list nat, Theorem array_max_ok : forall ls : list nat,
{{ h ~> forall i, i < length ls -> h $! i = nth_default 0 ls i}} {{ h ~> forall i, i < length ls -> h $! i = nth_default 0 ls i}}