pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-09-19 19:57:13 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Proofreading DeepAndShallowEmbeddings

Browse source
This commit is contained in:
Adam Chlipala 2018-04-22 14:07:01 -04:00
parent d5c7b9d7ce
commit 7c06dc3541
2 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
DeepAndShallowEmbeddings.v
View file

@ -22,9 +22,9 @@ Example h0 : heap := $0 $+ (0, 2) $+ (1, 1) $+ (2, 8) $+ (3, 6).
Hint Rewrite max_l max_r using linear_arithmetic. Hint Rewrite max_l max_r using linear_arithmetic.
Ltac simp := repeat (simplify; subst; propositional; Ltac simp := repeat (simplify; subst; propositional;
try match goal with try match goal with
| [ H : ex _ |- _ ] => invert H | [ H : ex _ |- _ ] => invert H
end); try linear_arithmetic. end); try linear_arithmetic.
(** * Basic concepts of shallow, deep, and mixed embeddings *) (** * Basic concepts of shallow, deep, and mixed embeddings *)
@ -510,7 +510,7 @@ End Deep.
Module Deeper. Module Deeper.
(* All programs in the last embedding must terminate, but let's add loops with (* All programs in the last embedding must terminate, but let's add loops with
* the potential to run forever, which takes us beyond what is representable * the potential to run forever, which takes us beyond what is representable
* in the shallow embedding, since Gallina enforces terminating of all * in the shallow embedding, since Gallina enforces termination for all
* programs. *) * programs. *)
(* We use this type to represent the outcome of a single loop iteration. (* We use this type to represent the outcome of a single loop iteration.

6
DeepAndShallowEmbeddings_template.v
View file

@ -17,9 +17,9 @@ Example h0 : heap := $0 $+ (0, 2) $+ (1, 1) $+ (2, 8) $+ (3, 6).
Hint Rewrite max_l max_r using linear_arithmetic. Hint Rewrite max_l max_r using linear_arithmetic.
Ltac simp := repeat (simplify; subst; propositional; Ltac simp := repeat (simplify; subst; propositional;
try match goal with try match goal with
| [ H : ex _ |- _ ] => invert H | [ H : ex _ |- _ ] => invert H
end); try linear_arithmetic. end); try linear_arithmetic.
(** * Basic concepts of shallow, deep, and mixed embeddings *) (** * Basic concepts of shallow, deep, and mixed embeddings *)