tobast/mpri-funcprog-project
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

merge

Browse source
This commit is contained in:
REMY Didier 2017-10-27 10:40:08 +02:00
commit c24814e9bb
54 changed files with 9603 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

125
README.md
View file

@ -1,13 +1,15 @@
# Functional programming and type systems (2017-2018)
[The official MPRI
page](https://wikimpri.dptinfo.ens-cachan.fr/doku.php?id=cours:c-2-4-2)
This page supplements
[the official page of MPRI 2-4](https://wikimpri.dptinfo.ens-cachan.fr/doku.php?id=cours:c-2-4-2).
## Location
## Location and duration
The lessons take place at University of Paris 7 - Denis Diderot,
Batiment Sophie Germain in room 2035 on Fridays at 12:45 and ends at 15:30.
There will be a break of 15' in the middle of the course.
The lectures take place at University Paris 7 - Denis Diderot,
Bâtiment Sophie Germain, in room 2035.
They are scheduled on Fridays from 12:45 to 15:30.
There is a 15-minute break in the middle of each lecture.
## Teachers
@ -20,6 +22,7 @@ There will be a break of 15' in the middle of the course.
This course presents the principles and formalisms that underlie many of
today's typed functional programming languages.
(Here are some [introductory slides](slides/fpottier-00.pdf).)
The course is made up of four parts and can be split after the first two
parts.
@ -43,8 +46,8 @@ systems. We study parametric polymorphism (as in System F and ML), data
types and type abstraction. We show syntactic type soundness (via progress
and subject reduction) by reasoning by induction on typing derivations. We
also show how to obtain semantic properties via logical relations by
reasoning by induction on the structure of types. We also introduce
subtyping and row polymorphism and illustrate typing problems induced by
reasoning by induction on the structure of types. Finally, we introduce
subtyping, row polymorphism, and illustrate the problems induced by
side effects (references) and the need for the value restriction.
The third part of the course describes more advanced features of type
@ -61,25 +64,50 @@ We also show the limits of dependently-typed functional programming.
### Functional Programming: Under the Hood
* (22/09/2017) From a small-step operational semantics...
* (29/09/2017) ... to an efficient interpreter. (2 weeks.)
* (06/10/2017) Compiling away first-class functions: closure conversion, defunctionalization.
* (13/10/2017) Compiling away the call stack: the CPS transformation.
* (20/10/2017) Equational reasoning and program optimizations.
* (22/09/2017)
Introduction ([slides 00](slides/fpottier-00.pdf)).
Syntax and operational semantics, on paper and on a machine
([slides 01a](slides/fpottier-01a.pdf))
([slides 01b](slides/fpottier-01b.pdf)).
* Newton-Raphson in OCaml ([solution](ocaml/NewtonRaphson.ml)).
* 1 is not even in Coq ([Even.v](coq/Even.v)).
* (29/09/2017)
From a small-step semantics down to an efficient verified interpreter,
in several stages
([Coq demo](coq/DemoSyntaxReduction.v))
([slides 02](slides/fpottier-02.pdf))
([OCaml code](ocaml/Lambda.ml))
([Coq repo](coq/)).
* (06/10/2017) Compiling away first-class functions:
closure conversion, defunctionalization
([slides 03](slides/fpottier-03.pdf))
([Coq repo](coq/)).
* (13/10/2017) Making the stack explicit: the CPS transformation
([slides 04](slides/fpottier-04.pdf))
([Coq repo](coq/)).
* Transforming a call-by-value interpreter
([exercise](ocaml/EvalCBVExercise.ml), [solution](ocaml/EvalCBVCPS.ml)).
* Transforming a call-by-name interpreter
([solution](ocaml/EvalCBNCPS.ml)).
* Transforming a graph traversal
([solution](ocaml/Graph.ml)).
* (20/10/2017) Equational reasoning and program optimizations
([slides 05](slides/fpottier-05.pdf))
([Coq mini-demo](coq/DemoEqReasoning.v)).
### Metatheory of Typed Programming Languages
* (15/09/2017)
[Metatheory of System F](http://gallium.inria.fr/~remy/mpri/slides1.pdf)
(See also [intro](http://gallium.inria.fr/~remy/mpri/slides8.pdf),
and chap [1](http://gallium.inria.fr/~remy/mpri/cours1.pdf)
and [2](http://gallium.inria.fr/~remy/mpri/cours2.pdf)
(See also [intro](http://gallium.inria.fr/~remy/mpri/slides8.pdf),
and chap [1](http://gallium.inria.fr/~remy/mpri/cours1.pdf)
and [2](http://gallium.inria.fr/~remy/mpri/cours2.pdf)
of [course notes](http://gallium.inria.fr/~remy/mpri/cours.pdf))
* (27/10/2017)
[ADTs, existential types, GADTs]
(http://gallium.inria.fr/~remy/mpri/slides2.pdf).
* (03/11/2017) Logical relations.
* (10/11/2017) Subtyping. Rows.
* (10/11/2017) Subtyping. Rows.
* (17/11/2017) References, Value restriction, Side effects.
### Advanced Aspects of Type Systems
@ -108,24 +136,24 @@ who split the course.
Although the course has changed, you may still have a look at previous exams
available with solutions:
- mid-term exam 2016-2017:
- mid-term exam 2016-2017:
[Record concatenation](http://gallium.inria.fr/~remy/mpri/exams/partiel-2016-2017.pdf)
- mid-term exam 2015-2016:
- mid-term exam 2015-2016:
[Type containment](http://gallium.inria.fr/~remy/mpri/exams/partiel-2015-2016.pdf)
- final exam 2014-2015: [Copatterns](http://gallium.inria.fr/~remy/mpri/exams/final-2014-2015.pdf)
- mid-term exam 2014-2015:
- mid-term exam 2014-2015:
[Information flow](http://gallium.inria.fr/~remy/mpri/exams/partiel-2014-2015.pdf)
- final exam 2013-2014:
- final exam 2013-2014:
[Operation on records](http://gallium.inria.fr/~remy/mpri/exams/final-2013-2014.pdf)
- mid-term exam 2013-2014:
- mid-term exam 2013-2014:
[Typechecking Effects](http://gallium.inria.fr/~remy/mpri/exams/partiel-2013-2014.pdf)
- final exam 2012-2013:
- final exam 2012-2013:
[Refinement types](http://gallium.inria.fr/~remy/mpri/exams/final-2012-2013.pdf)
- mid-term exam 2012-2013:
- mid-term exam 2012-2013:
[Variations on ML](http://gallium.inria.fr/~remy/mpri/exams/partiel-2012-2013.pdf)
- final exam 2011-2012:
- final exam 2011-2012:
[Intersection types](http://gallium.inria.fr/~remy/mpri/exams/final-2011-2012.pdf)
- mid-term exam 2011-2012:
- mid-term exam 2011-2012:
[Parametricity](http://gallium.inria.fr/~remy/mpri/exams/partiel-2011-2012.pdf)
- final exam 2010-2011:
[Compiling a language with subtyping](http://gallium.inria.fr/~xleroy/mpri/2-4/exam-2010-2011.pdf)
@ -135,19 +163,58 @@ available with solutions:
## Recommended software
OCaml 4.0x and Coq **8.5**.
Please install [opam](https://opam.ocaml.org/doc/Install.html) first.
Once you have installed [opam](https://opam.ocaml.org/doc/Install.html), use the following commands:
Then, install OCaml 4.0x and Coq **8.5** via the following commands:
```bash
opam init --comp=4.05 # for instance
opam repo add coq-released https://coq.inria.fr/opam/released
opam update
opam install -j4 -v coq.8.5.3
```
(Do *not* install Coq 8.6. The version of AutoSubst that I am using is
not compatible with it. If for some reason you need Coq 8.6, or have
already installed Coq 8.6, note that `opam switch` can be used to let
multiple versions of Coq coexist.)
Please also install François Pottier's
[variant](https://github.com/fpottier/autosubst)
of the
[AutoSubst](https://www.ps.uni-saarland.de/autosubst/) library:
```bash
git clone git@github.com:fpottier/autosubst.git
make -C autosubst install
```
In order to use Coq inside `emacs`,
[ProofGeneral](https://proofgeneral.github.io/)
is highly recommended.
Here is a suggested installation script:
```bash
rm -rf /tmp/PG
cd /tmp
git clone git@github.com:ProofGeneral/PG.git
cd PG
EMACS=/Applications/Aquamacs.app/Contents/MacOS/Aquamacs
if [ ! -x $EMACS ]; then
EMACS=emacs
fi
make EMACS=$EMACS compile
TARGET=/usr/local/share/emacs/site-lisp/ProofGeneral
sudo rm -rf $TARGET
sudo mv /tmp/PG $TARGET
```
Enable ProofGeneral by adding the following line to your `.emacs` file:
```elisp
(load-file "/usr/local/share/emacs/site-lisp/ProofGeneral/generic/proof-site.el")
```
If desired, ProofGeneral can be further
[customized](https://proofgeneral.github.io/doc/userman/ProofGeneral_9/).
## Bibliography
[Types and Programming Languages](https://mitpress.mit.edu/books/types-and-programming-languages),
[Types and Programming Languages](https://mitpress.mit.edu/books/types-and-programming-languages),
Benjamin C. Pierce, MIT Press, 2002.
[Advanced Topics in Types and Programming Languages](https://www.cis.upenn.edu/~bcpierce/attapl/),

7
coq/.gitignore vendored Normal file
View file

@ -0,0 +1,7 @@
*.vo
*.glob
*.v.d
.*.aux
.coq-native
_CoqProject
*~

172
coq/AutosubstExtra.v Normal file
View file

@ -0,0 +1,172 @@
Require Import Omega.
Require Import Autosubst.Autosubst.
Require Import MyTactics. (* TEMPORARY *)
(* -------------------------------------------------------------------------- *)
(* A more recognizable notation for lifting. *)
Notation lift i t := (t.[ren(+i)]).
(* -------------------------------------------------------------------------- *)
Section Extras.
Context A `{Ids A, Rename A, Subst A, SubstLemmas A}.
Lemma up_ren:
forall xi,
ren (upren xi) = up (ren xi).
Proof.
intros. autosubst.
Qed.
Lemma upn_ren:
forall i xi,
ren (iterate upren i xi) = upn i (ren xi).
Proof.
induction i; intros.
{ reflexivity. }
{ rewrite <- fold_up_upn. rewrite <- IHi. asimpl. reflexivity. }
Qed.
Lemma plus_upn: (* close to [up_liftn] *)
forall i sigma,
(+i) >>> upn i sigma = sigma >> ren (+i).
Proof.
induction i; intros.
{ rewrite iterate_0. autosubst. }
{ rewrite iterate_S. asimpl. rewrite IHi. autosubst. }
Qed.
Lemma up_sigma_up_ren:
forall t i sigma,
t.[up sigma].[up (ren (+i))] = t.[up (ren (+i))].[upn (1 + i) sigma].
Proof.
intros. asimpl. rewrite plus_upn. asimpl. reflexivity.
Qed.
Lemma upn_k_sigma_x:
forall k sigma x,
x < k ->
upn k sigma x = ids x.
Proof.
induction k; intros; asimpl.
{ omega. }
{ destruct x; asimpl.
{ eauto. }
{ rewrite IHk by omega. autosubst. }
}
Qed.
Lemma push_substitution_last:
forall t v i,
t.[v .: ren (+i)] = t.[up (ren (+i))].[v/].
Proof.
intros. autosubst.
Qed.
Lemma push_substitution_last_up_hoist:
forall t v i j,
t.[up (v .: ren (+i))].[up (ren (+j))] =
t.[up (up (ren (+j + i)))].[up (lift j v .: ids)].
Proof.
intros. autosubst.
Qed.
Lemma lift_lift:
forall i j t,
lift i (lift j t) = lift (i + j) t.
Proof.
intros. autosubst.
Qed.
Lemma lift_upn:
forall t i sigma,
(lift i t).[upn i sigma] = lift i t.[sigma].
Proof.
intros. asimpl.
erewrite plus_upn.
reflexivity.
Qed.
Lemma lift_up:
forall t sigma,
(lift 1 t).[up sigma] = lift 1 t.[sigma].
Proof.
intros. change up with (upn 1). eapply lift_upn.
Qed.
Lemma up_sigma_f:
forall (sigma : var -> A) (f : A -> A),
f (ids 0) = ids 0 ->
(forall i t, lift i (f t) = f (lift i t)) ->
up (sigma >>> f) = up sigma >>> f.
Proof.
intros. f_ext. intros [|x]; asimpl; eauto.
Qed.
Lemma upn_sigma_f:
forall (sigma : var -> A) (f : A -> A),
f (ids 0) = ids 0 ->
(forall i t, lift i (f t) = f (lift i t)) ->
forall i,
upn i (sigma >>> f) = upn i sigma >>> f.
Proof.
induction i; intros.
{ reflexivity. }
{ do 2 rewrite <- fold_up_upn. rewrite IHi. erewrite up_sigma_f by eauto. reflexivity. }
Qed.
Lemma upn_theta_sigma_ids:
forall theta sigma i,
theta >> sigma = ids ->
upn i theta >> upn i sigma = ids.
Proof.
intros theta sigma i Hid.
rewrite up_comp_n.
rewrite Hid.
rewrite up_id_n.
reflexivity.
Qed.
Lemma up_theta_sigma_ids:
forall theta sigma,
theta >> sigma = ids ->
up theta >> up sigma = ids.
Proof.
change up with (upn 1). eauto using upn_theta_sigma_ids.
Qed.
Lemma scons_scomp:
forall (T : A) Gamma theta,
T.[theta] .: (Gamma >> theta) = (T .: Gamma) >> theta.
Proof.
intros. autosubst.
Qed.
(* BUG: the two sides of this equation are distinct, yet they are
printed identically. *)
Goal
forall v f,
v .: (ids >>> f) = (v .: ids) >>> f.
Proof.
intros.
Fail reflexivity.
Abort.
End Extras.
(* This incantation means that [eauto with autosubst] can use the tactic
[autosubst] to prove an equality. *)
Hint Extern 1 (_ = _) => autosubst : autosubst.
(* This incantation means that [eauto with autosubst] can use the lemmas
whose names are listed here. This is useful when an equality involves
metavariables, so the tactic [autosubst] fails. *)
Hint Resolve scons_scomp : autosubst.
(* -------------------------------------------------------------------------- *)

329
coq/Autosubst_EOS.v Normal file
View file

@ -0,0 +1,329 @@
Require Import Omega.
Require Import Autosubst.Autosubst.
Require Import AutosubstExtra. (* just for [upn_ren] *)
Require Import MyTactics. (* TEMPORARY *)
(* This file defines the construction [eos x t], which can be understood as
an end-of-scope mark for [x] in the term [t]. *)
(* It also defines the single-variable substitution t.[u // x], which is the
substitution of [u] for [x] in [t]. *)
(* -------------------------------------------------------------------------- *)
Section EOS.
Context {A} `{Ids A, Rename A, Subst A, SubstLemmas A}.
(* The substitution [Var 0 .: Var 1 .: ... .: Var (x-1) .: Var (x+1) .: ...]
does not have [Var x] in its codomain. Thus, applying this substitution
to a term [t] can be understood as an end-of-scope construct: it means
``end the scope of [x] in [t]''. We write [eos x t] for this construct.
It is also known as [adbmal]: see Hendriks and van Oostrom,
https://doi.org/10.1007/978-3-540-45085-6_11 *)
(* There are at least two ways of defining the above substitution. One way
is to define it in terms of AutoSubst combinators: *)
Definition eos_var x : var -> var :=
(iterate upren x (+1)).
Definition eos x t :=
t.[ren (eos_var x)].
Lemma eos_eq:
forall x t,
t.[upn x (ren (+1))] = eos x t.
Proof.
intros. unfold eos, eos_var. erewrite upn_ren by tc. reflexivity.
Qed.
(* Another way is to define directly as a function of type [var -> var]. *)
Definition lift_var x : var -> var :=
fun y => if le_gt_dec x y then 1 + y else y.
(* The two definitions coincide: *)
Lemma upren_lift_var:
forall x,
upren (lift_var x) = lift_var (S x).
Proof.
intros. f_ext; intros [|y].
{ reflexivity. }
{ simpl. unfold lift_var, var. dblib_by_cases; omega. }
Qed.
Lemma eos_var_eq_lift_var:
eos_var = lift_var.
Proof.
(* An uninteresting proof. *)
f_ext; intros x.
unfold eos_var.
induction x.
{ reflexivity. }
{ rewrite iterate_S.
rewrite IHx.
rewrite upren_lift_var.
reflexivity. }
Qed.
(* -------------------------------------------------------------------------- *)
(* [eos] enjoys certain commutation laws. *)
(* Ending the scope of variable [k], then the scope of variable [s], is the
same as first ending the scope of variable [1 + s], then ending the scope
of variable [k]. This holds provided [k <= s] is true, i.e., [k] is the
most recently-introduced variable.*)
Lemma lift_var_lift_var:
forall k s,
k <= s ->
lift_var s >>> lift_var k = lift_var k >>> lift_var (S s).
Proof.
(* By case analysis. *)
intros. f_ext; intros x. asimpl.
unfold lift_var, var. dblib_by_cases; omega.
Qed.
Lemma eos_eos:
forall k s t,
k <= s ->
eos k (eos s t) = eos (1 + s) (eos k t).
Proof.
intros. unfold eos. asimpl.
rewrite eos_var_eq_lift_var.
rewrite lift_var_lift_var by eauto.
reflexivity.
Qed.
(* What about the case where [k] is the least recently-introduced variable?
It is obtained by symmetry, of course. *)
Lemma eos_eos_reversed:
forall k s t,
k >= s + 1 ->
eos k (eos s t) = eos s (eos (k - 1) t).
Proof.
intros.
replace k with (1 + (k - 1)) by omega.
rewrite <- eos_eos by omega.
replace (1 + (k - 1) - 1) with (k - 1) by omega.
reflexivity.
Qed.
(* -------------------------------------------------------------------------- *)
(* Single-variable substitutions. *)
(* [subst_var u x] is the substitution of [u] for [x]. *)
(* We give a direct definition of it as a function of type [var -> term],
defined by cases. I don't know if it could also be nicely defined in
terms of the basic combinators of de Bruijn algebra. Note that the
candidate definition [upn x (t .: ids)] is WRONG when [x > 0]. *)
Definition subst_var (u : A) (x y : var) : A :=
match lt_eq_lt_dec y x with
| inleft (left _) => ids y
| inleft (right _) => u
| inright _ => ids (y - 1)
end.
(* A nice notation: [t.[u // x]] is the substitution of [u] for [x] in [t]. *)
Notation "t .[ u // x ]" := (subst (subst_var u x) t)
(at level 2, u at level 200, left associativity,
format "t .[ u // x ]") : subst_scope.
(* The following laws serve as sanity checks: we got the definition right. *)
Lemma subst_var_miss_1:
forall x y u,
y < x ->
(ids y).[u // x] = ids y.
Proof.
intros. asimpl. unfold subst_var. dblib_by_cases. reflexivity.
Qed.
Lemma subst_var_match:
forall x u,
(ids x).[ u // x ] = u.
Proof.
intros. asimpl. unfold subst_var. dblib_by_cases. reflexivity.
Qed.
Lemma subst_var_miss_2:
forall x y u,
x < y ->
(ids y).[u // x] = ids (y - 1).
Proof.
intros. asimpl. unfold subst_var. dblib_by_cases. reflexivity.
Qed.
(* In the special case where [x] is 0, the substitution [t // 0] can also
be written [t/], which is an AutoSubst notation for [t .: ids]. *)
Lemma subst_var_0:
forall t u,
t.[u // 0] = t.[u/].
Proof.
intros. f_equal. clear t.
f_ext. intros [|x].
{ reflexivity. }
{ unfold subst_var. simpl. f_equal. omega. }
Qed.
(* -------------------------------------------------------------------------- *)
(* A cancellation law: substituting for a variable [x] that does not occur in
[t] yields just [t]. In other words, a substitution for [x] vanishes when
it reaches [eos x _]. *)
(* In informal syntax, this lemma would be written:
t[u/x] = t
under the hypothesis that x does not occur free in t.
In de Bruijn style, the statement is just as short, and does not have a
side condition. Instead, it requires an explicit [eos x _] to appear at the
root of the term to which the substitution is applied; this may require
rewriting before this lemma can be applied. *)
Lemma subst_eos:
forall x t u,
(eos x t).[u // x] = t.
Proof.
intros.
(* Again, let's simplify this first. *)
unfold eos. asimpl.
(* Aha! We can forget about [t], and focus on proving that two
substitutions are equal. To do so, it is sufficient that
their actions on a variable [y] are the same. *)
rewrite <- subst_id.
f_equal. clear t.
f_ext. intro y.
(* The proof is easy if we replace [eos_var] with [lift_var]. *)
rewrite eos_var_eq_lift_var. simpl.
unfold subst_var, lift_var. dblib_by_cases; f_equal; omega.
Qed.
(* The above property allows us to prove that [eos x _] is injective.
Indeed, it has an inverse, namely [u // x], where [u] is arbitrary. *)
Lemma eos_injective:
forall x t1 t2,
eos x t1 = eos x t2 ->
t1 = t2.
Proof.
intros.
pose (u := t1). (* dummy *)
erewrite <- (subst_eos x t1 u).
erewrite <- (subst_eos x t2 u).
congruence.
Qed.
(* -------------------------------------------------------------------------- *)
(* More commutation laws. *)
Lemma eos_subst_1:
forall k s t u,
k <= s ->
eos k (t.[u // s]) = (eos k t).[eos k u // s + 1].
Proof.
intros. unfold eos. asimpl. f_equal. clear t.
rewrite eos_var_eq_lift_var.
f_ext. intros y.
asimpl.
unfold subst_var, lift_var.
dblib_by_cases; asimpl; dblib_by_cases; solve [ eauto | f_equal; omega ].
Qed.
Lemma eos_subst_2:
forall k s t u,
s <= k ->
eos k (t.[u // s]) = (eos (k + 1) t).[eos k u // s].
Proof.
intros. unfold eos. asimpl. f_equal. clear t.
rewrite eos_var_eq_lift_var.
f_ext. intros y.
asimpl.
unfold subst_var, lift_var.
dblib_by_cases; asimpl; dblib_by_cases; solve [ eauto | f_equal; omega ].
Qed.
Lemma subst_subst:
forall t k v s w,
k <= s ->
t.[w // k].[v // s] =
t.[eos k v // 1 + s].[w.[v // s] // k].
Proof.
(* First, get rid of [t]. It is sufficient to consider the action of
these substitutions at a variable [y]. *)
intros. asimpl. f_equal. clear t. f_ext. intros y.
(* Replace [eos_var] with [lift_var], whose definition is more direct. *)
unfold eos. rewrite eos_var_eq_lift_var.
(* Then, use brute force (case analysis) to prove that the goal holds. *)
unfold subst_var. simpl.
dblib_by_cases; asimpl; dblib_by_cases;
(* This case analysis yields 5 cases, of which 4 are trivial... *)
eauto.
(* ... thus, one case remains. *)
(* Now get rid of [v]. It is again sufficient to consider the action
of these substitutions at a variable [z]. *)
replace v with v.[ids] at 1 by autosubst.
f_equal. f_ext. intros z. simpl.
(* Again, use brute force. *)
unfold lift_var. dblib_by_cases; f_equal. unfold var. omega.
(* Not really proud of this proof. *)
Qed.
Lemma pun_1:
forall t x,
(eos x t).[ ids x // x + 1 ] = t.
Proof.
(* First, get rid of [t]. It is sufficient to consider the action of
these substitutions at a variable [y]. *)
intros. unfold eos. asimpl.
replace t with t.[ids] at 2 by autosubst.
f_equal. clear t. f_ext. intros y.
(* Replace [eos_var] with [lift_var], whose definition is more direct. *)
rewrite eos_var_eq_lift_var.
(* Then, use brute force (case analysis) to prove that the goal holds. *)
simpl. unfold subst_var, lift_var. dblib_by_cases; f_equal; unfold var; omega.
Qed.
Lemma pun_2:
forall t x,
(eos (x + 1) t).[ ids x // x ] = t.
Proof.
(* First, get rid of [t]. It is sufficient to consider the action of
these substitutions at a variable [y]. *)
intros. unfold eos. asimpl.
replace t with t.[ids] at 2 by autosubst.
f_equal. clear t. f_ext. intros y.
(* Replace [eos_var] with [lift_var], whose definition is more direct. *)
rewrite eos_var_eq_lift_var.
(* Then, use brute force (case analysis) to prove that the goal holds. *)
simpl. unfold subst_var, lift_var. dblib_by_cases; f_equal; unfold var; omega.
Qed.
End EOS.
(* Any notations defined in the above section must now be repeated. *)
Notation "t .[ u // x ]" := (subst (subst_var u x) t)
(at level 2, u at level 200, left associativity,
format "t .[ u // x ]") : subst_scope.
(* The tactic [subst_var] attempts to simplify applications of [subst_var]. *)
Ltac subst_var :=
first [
rewrite subst_var_miss_1 by omega
| rewrite subst_var_match by omega
| rewrite subst_var_miss_2 by omega
].

130
coq/Autosubst_Env.v Normal file
View file

@ -0,0 +1,130 @@
Require Import List.
Require Import MyTactics. (* TEMPORARY *)
Require Import Autosubst.Autosubst.
Require Import Autosubst_EOS. (* [eos_var] *)
(* Environments are sometimes represented as finite lists. This file
provides a few notions that helps deal with this representation. *)
Section Env.
Context {A} `{Ids A, Rename A, Subst A, SubstLemmas A}.
(* -------------------------------------------------------------------------- *)
(* The function [env2subst default], where [default] is a default value,
converts an environment (a finite list) to a substitution (a total
function). *)
Definition env2subst (default : A) (e : list A) (x : var) : A :=
nth x e default.
(* -------------------------------------------------------------------------- *)
(* [env_ren_comp e xi e'] means (roughly) that the environment [e] is equal to
the composition of the renaming [xi] and the environment [e'], that is,
[e = xi >>> e']. We also explicitly require the environments [e] and [e']
to have matching lengths, up to [xi], as this is *not* a consequence of
the other premise. *)
Inductive env_ren_comp : list A -> (var -> var) -> list A -> Prop :=
| EnvRenComp:
forall e xi e',
(forall x, x < length e -> xi x < length e') ->
(forall x default, nth x e default = nth (xi x) e' default) ->
env_ren_comp e xi e'.
(* A reformulation of the second premise in the above definition. *)
Lemma env_ren_comp_eq:
forall e xi e',
(forall default, env2subst default e = xi >>> env2subst default e') <->
(forall x default, nth x e default = nth (xi x) e' default).
Proof.
unfold env2subst. split; intros h; intros.
{ change (nth x e default) with ((fun x => nth x e default) x).
rewrite h. reflexivity. }
{ f_ext; intro x. eauto. }
Qed.
(* -------------------------------------------------------------------------- *)
(* Initialization: [e = id >>> e]. *)
Lemma env_ren_comp_id:
forall e,
env_ren_comp e (fun x => x) e.
Proof.
econstructor; eauto.
Qed.
(* -------------------------------------------------------------------------- *)
(* The relation [e = xi >>> e'] can be taken under a binder, as follows. *)
Lemma env_ren_comp_up:
forall e xi e' v,
env_ren_comp e xi e' ->
env_ren_comp (v :: e) (upren xi) (v :: e').
Proof.
inversion 1; intros; subst; econstructor;
intros [|x]; intros; simpl in *; eauto with omega.
Qed.
(* -------------------------------------------------------------------------- *)
(* One element can be prepended to [e'], provided [xi] is adjusted. *)
Lemma env_ren_comp_prepend:
forall e xi e' v,
env_ren_comp e xi e' ->
env_ren_comp e (xi >>> (+1)) (v :: e').
Proof.
inversion 1; intros; subst.
econstructor; intros; simpl; eauto with omega.
Qed.
(* -------------------------------------------------------------------------- *)
(* A consequence of [env_ren_comp_id] and [env_ren_comp_prepend]. The renaming
(+1) will eat away the first entry in [v :: e]. *)
Lemma env_ren_comp_plus1:
forall e v,
env_ren_comp e (+1) (v :: e).
Proof.
econstructor; intros; simpl; eauto with omega.
Qed.
(* -------------------------------------------------------------------------- *)
(* More generally, the renaming [eos_var x], which means that [x] goes out of
scope, will eat away the entry at index [x] in [e1 ++ v :: e2]. *)
Lemma env_ren_comp_eos_var:
forall x e1 v e2,
x = length e1 ->
env_ren_comp (e1 ++ e2) (eos_var x) (e1 ++ v :: e2).
Proof.
rewrite eos_var_eq_lift_var. unfold lift_var.
econstructor; intros y; dblib_by_cases.
{ rewrite app_length in *. simpl. omega. }
{ rewrite app_length in *. simpl. omega. }
{ do 2 (rewrite app_nth2 by omega).
replace (1 + y - length e1) with (1 + (y - length e1)) by omega.
reflexivity. }
{ do 2 (rewrite app_nth1 by omega).
reflexivity. }
Qed.
(* -------------------------------------------------------------------------- *)
End Env.
Hint Resolve
env_ren_comp_id
env_ren_comp_up
env_ren_comp_prepend
env_ren_comp_plus1
env_ren_comp_eos_var
: env_ren_comp.

345
coq/Autosubst_FreeVars.v Normal file
View file

@ -0,0 +1,345 @@
Require Import Omega.
Require Import Autosubst.Autosubst.
Require Import AutosubstExtra.
Require Import Autosubst_EOS.
(* -------------------------------------------------------------------------- *)
Class IdsLemmas (term : Type) {Ids_term : Ids term} := {
(* The identity substitution is injective. *)
ids_inj:
forall x y,
ids x = ids y ->
x = y
}.
(* -------------------------------------------------------------------------- *)
Section FreeVars.
Context
{A : Type}
{Ids_A : Ids A}
{Rename_A : Rename A}
{Subst_A : Subst A}
{IdsLemmas_A : IdsLemmas A}
{SubstLemmas_A : SubstLemmas A}.
(* -------------------------------------------------------------------------- *)
(* A reformulation of [ids_inj]. *)
Lemma ids_inj_False:
forall x y,
ids x = ids y ->
x <> y ->
False.
Proof.
intros.
assert (x = y). { eauto using ids_inj. }
unfold var in *.
omega.
Qed.
(* -------------------------------------------------------------------------- *)
(* The predicate [fv k t] means that the free variables of the term [t] are
contained in the semi-open interval [0..k). *)
Definition fv k t :=
t.[upn k (ren (+1))] = t.
(* -------------------------------------------------------------------------- *)
(* The predicate [closed t] means that the term [t] is closed, that is, [t]
has no free variables. *)
Definition closed :=
fv 0.
(* -------------------------------------------------------------------------- *)
(* This technical lemma states that the renaming [+1] is injective. *)
Lemma lift_inj_ids:
forall t x,
t.[ren (+1)] = ids (S x) <-> t = ids x.
Proof.
split; intros.
{ eapply lift_inj. autosubst. }
{ subst. autosubst. }
Qed.
(* -------------------------------------------------------------------------- *)
(* This lemma characterizes the meaning of [fv k] when applied to a variable. *)
Lemma fv_ids_eq:
forall k x,
fv k (ids x) <-> x < k.
Proof.
unfold fv. induction k; intros.
(* Base case. *)
{ asimpl. split; intros; elimtype False.
{ eauto using ids_inj_False. }
{ omega. }
}
(* Step. *)
{ destruct x; asimpl.
{ split; intros. { omega. } { reflexivity. } }
{ rewrite lift_inj_ids.
rewrite <- id_subst.
rewrite IHk. omega. }
}
Qed.
(* -------------------------------------------------------------------------- *)
(* A simplification lemma. *)
Lemma fv_lift:
forall k i t,
fv (k + i) t.[ren (+i)] <-> fv k t.
Proof.
unfold fv. intros. asimpl.
rewrite Nat.add_comm.
rewrite <- upn_upn.
erewrite plus_upn by eauto.
rewrite <- subst_comp.
split; intros.
{ eauto using lift_injn. }
{ f_equal. eauto. }
Qed.
(* -------------------------------------------------------------------------- *)
(* If [t] has at most [n - 1] free variables,
and if [x] is inserted among them,
then we get [eos x t],
which has at most [n] free variables. *)
Lemma fv_eos:
forall x n t,
x < n ->
fv (n - 1) t ->
fv n (eos x t).
Proof.
unfold fv. intros x n t ? ht.
rewrite eos_eq in ht.
rewrite eos_eq.
rewrite eos_eos_reversed by omega. (* nice! *)
rewrite ht.
reflexivity.
Qed.
Lemma fv_eos_eq:
forall x n t,
x < n ->
fv n (eos x t) <->
fv (n - 1) t.
Proof.
unfold fv. intros x n t ?.
rewrite eos_eq.
rewrite eos_eq.
rewrite eos_eos_reversed by omega. (* nice! *)
split; intros h.
{ eauto using eos_injective. }
{ rewrite h. reflexivity. }
Qed.
(* -------------------------------------------------------------------------- *)
(* A substitution [sigma] is regular if and only if, for some [j], for
sufficiently large [x], [sigma x] is [x + j]. *)
Definition regular (sigma : var -> A) :=
exists i j,
ren (+i) >> sigma = ren (+j).
Lemma regular_ids:
regular ids.
Proof.
exists 0. exists 0. autosubst.
Qed.
Lemma regular_plus:
forall i,
regular (ren (+i)).
Proof.
intros. exists 0. exists i. autosubst.
Qed.
Lemma regular_upn:
forall n sigma,
regular sigma ->
regular (upn n sigma).
Proof.
intros ? ? (i&j&hsigma).
exists (n + i). eexists (n + j).
replace (ren (+(n + i))) with (ren (+i) >> ren (+n)) by autosubst.
rewrite <- scompA.
rewrite up_liftn.
rewrite scompA.
rewrite hsigma.
autosubst.
Qed.
(* -------------------------------------------------------------------------- *)
(* If the free variables of the term [t] are below [k], then [t] is unaffected
by a substitution of the form [upn k sigma]. *)
(* Unfortunately, in this file, where the definition of type [A] is unknown, I
am unable to establish this result for arbitrary substitutions [sigma]. I
am able to establish it for *regular* substitutions, where The proof is somewhat interesting, so it is given here, even
though, once the definition of the type [A] is known, a more direct proof,
without a regularity hypothesis, can usually be given. *)
(* An intermediate result states that, since [upn k (ren (+1))] does not
affect [t], then (by iteration) neither does [upn k (ren (+j))]. *)
Lemma fv_unaffected_lift:
forall j t k,
fv k t ->
t.[upn k (ren (+j))] = t.
Proof.
induction j as [| j ]; intros t k ht.
{ asimpl. rewrite up_id_n. autosubst. }
{ replace (ren (+S j)) with (ren (+1) >> ren (+j)) by autosubst.
rewrite <- up_comp_n.
replace (t.[upn k (ren (+1)) >> upn k (ren (+j))])
with (t.[upn k (ren (+1))].[upn k (ren (+j))]) by autosubst.
rewrite ht.
rewrite IHj by eauto.
eauto. }
Qed.
(* There follows that a substitution of the form [upn k sigma], where [sigma]
is regular, does not affect [t]. The proof is slightly subtle but very
short. The previous lemma is used twice. *)
Lemma fv_unaffected_regular:
forall k t sigma,
fv k t ->
regular sigma ->
t.[upn k sigma] = t.
Proof.
intros k t sigma ? (i&j&hsigma).
rewrite <- (fv_unaffected_lift i t k) at 1 by eauto.
asimpl. rewrite up_comp_n.
rewrite hsigma.
rewrite fv_unaffected_lift by eauto.
reflexivity.
Qed.
(* A corollary. *)
Lemma closed_unaffected_regular:
forall t sigma,
closed t ->
regular sigma ->
t.[sigma] = t.
Proof.
unfold closed. intros.
rewrite <- (upn0 sigma).
eauto using fv_unaffected_regular.
Qed.
(*One might also wish to prove a result along the following lines:
Goal
forall t k sigma1 sigma2,
fv k t ->
(forall x, x < k -> sigma1 x = sigma2 x) ->
t.[sigma1] = t.[sigma2].
I have not yet investigated how this could be proved. *)
(* -------------------------------------------------------------------------- *)
(* If some term [t] has free variables under [j], then it also has free
variables under [k], where [j <= k]. *)
Lemma fv_monotonic:
forall j k t,
fv j t ->
j <= k ->
fv k t.
Proof.
intros. unfold fv.
replace k with (j + (k - j)) by omega.
rewrite <- upn_upn.
eauto using fv_unaffected_regular, regular_upn, regular_plus.
Qed.
(* -------------------------------------------------------------------------- *)
(* These little lemmas may be occasionally useful. *)
Lemma use_fv_length_cons:
forall A (x : A) (xs : list A) n t,
(forall x, fv (length (x :: xs)) t) ->
n = length xs ->
fv (n + 1) t.
Proof.
intros. subst.
replace (length xs + 1) with (length (x :: xs)) by (simpl; omega).
eauto.
Qed.
Lemma prove_fv_length_cons:
forall A (x : A) (xs : list A) n t,
n = length xs ->
fv (n + 1) t ->
fv (length (x :: xs)) t.
Proof.
intros. subst.
replace (length (x :: xs)) with (length xs + 1) by (simpl; omega).
eauto.
Qed.
(* -------------------------------------------------------------------------- *)
(* [closed t] is equivalent to [t.[ren (+1)] = t]. *)
Lemma closed_eq:
forall t,
closed t <-> t.[ren (+1)] = t.
Proof.
unfold closed, fv. asimpl. tauto.
Qed.
(* -------------------------------------------------------------------------- *)
(* A variable is not closed. *)
Lemma closed_ids:
forall x,
~ closed (ids x).
Proof.
unfold closed, fv. intros. asimpl. intro.
eauto using ids_inj_False.
Qed.
End FreeVars.
(* -------------------------------------------------------------------------- *)
(* The tactic [fv] is intended to use a number of lemmas as rewriting rules.
The hint database [fv] can be extended with language-specific lemmas. *)
Hint Rewrite @fv_ids_eq @fv_lift @fv_eos_eq : fv.
Ltac fv :=
autorewrite with fv in *;
eauto with typeclass_instances.
(* -------------------------------------------------------------------------- *)
(* A hint database to prove goals of the form [~ (closed _)] or [closed _]. *)
Hint Resolve closed_ids : closed.
(* -------------------------------------------------------------------------- *)
Hint Resolve regular_ids regular_plus regular_upn : regular.

87
coq/Autosubst_IsRen.v Normal file
View file

@ -0,0 +1,87 @@
Require Import Coq.Logic.ClassicalUniqueChoice.
Require Import Autosubst.Autosubst.
Require Import AutosubstExtra.
Section Lemmas.
Context {A} `{Ids A, Rename A, Subst A, SubstLemmas A}.
(* The predicate [is_ren sigma] means that the substitution [sigma] is in fact
a renaming [ren xi]. *)
(* When stating a lemma that involves a renaming, it is preferable to use a
substitution [sigma], together with a hypothesis [is_ren sigma], rather
than request that [sigma] be of the form [ren xi]. This allows us to use
[obvious] to check that [sigma] is a renaming, whereas we would otherwise
have to manually rewrite [sigma] to the form [ren xi]. *)
Definition is_ren sigma :=
exists xi, sigma = ren xi.
(* One way of proving that [sigma] is a renaming is to prove that [sigma] maps
every variable [x] to a variable [y]. *)
Lemma prove_is_ren:
forall sigma,
(forall x y, ids x = ids y -> x = y) ->
(forall x, exists y, sigma x = ids y) ->
is_ren sigma.
Proof.
(* This proof uses the axiom of unique choice. If one is willing to use
the stronger axiom of choice, then one can remove the hypothesis that
[ids] is injective. *)
intros ? Hinj Hxy.
assert (Hxi: exists xi : var -> var, forall x, sigma x = ids (xi x)).
{ eapply unique_choice with (R := fun x y => sigma x = ids y).
intros x. destruct (Hxy x) as [ y Heqy ]. exists y.
split.
{ assumption. }
{ intros x' Heqx'. eapply Hinj. congruence. }
}
destruct Hxi as [ xi ? ].
exists xi.
f_ext; intros x. eauto.
Qed.
(* Applying [up] or [upn i] to a renaming produces a renaming. *)
Lemma up_is_ren:
forall sigma,
is_ren sigma ->
is_ren (up sigma).
Proof.
intros ? [ xi ? ]. subst. exists (upren xi).
erewrite <- up_ren by eauto with typeclass_instances. reflexivity.
Qed.
Lemma upn_is_ren:
forall sigma i,
is_ren sigma ->
is_ren (upn i sigma).
Proof.
intros ? ? [ xi ? ]. subst. exists (iterate upren i xi).
erewrite <- upn_ren by eauto with typeclass_instances. reflexivity.
Qed.
(* Composing two renamings yields a renaming. *)
Lemma comp_is_ren:
forall sigma1 sigma2,
is_ren sigma1 ->
is_ren sigma2 ->
is_ren (sigma1 >> sigma2).
Proof.
intros ? ? [ xi1 ? ] [ xi2 ? ]. subst. exists (xi1 >>> xi2). autosubst.
Qed.
Lemma is_ren_ids:
is_ren ids.
Proof.
exists id. autosubst.
Qed.
End Lemmas.
Hint Unfold is_ren : is_ren obvious.
Hint Resolve up_is_ren upn_is_ren comp_is_ren is_ren_ids : is_ren obvious.

77
coq/CPSContextSubstitution.v Normal file
View file

@ -0,0 +1,77 @@
Require Import MyTactics.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusValues.
Require Import CPSDefinition.
(* This file contains a few lemmas about [substc]. *)
(* Two successive applications of [substc] can be fused. *)
Lemma substc_substc:
forall sigma1 sigma2 c,
substc sigma2 (substc sigma1 c) = substc (sigma1 >> sigma2) c.
Proof.
intros. destruct c; autosubst.
Qed.
(* Two successive applications of [liftc] can be fused. *)
Lemma liftc_liftc:
forall i j c,
liftc i (liftc j c) = liftc (i + j) c.
Proof.
intros i j c. destruct c; autosubst.
Qed.
(* [apply] commutes with substitutions. *)
Lemma apply_substitution:
forall c sigma c' v,
substc sigma c = c' ->
(apply c v).[sigma] = apply c' v.[sigma].
Proof.
intros. subst. destruct c; autosubst.
Qed.
(* [reify] commutes with substitutions. *)
Lemma reify_substitution:
forall c sigma c',
substc sigma c = c' ->
(reify c).[sigma] = reify c'.
Proof.
intros. subst. destruct c; reflexivity.
Qed.
(* As a special case, [reify] commutes with lifting. *)
Lemma lift_reify:
forall i c,
lift i (reify c) = reify (liftc i c).
Proof.
intros. destruct c; reflexivity.
Qed.
(* [substc] is preserved by [liftc]. *)
Lemma substc_liftc_liftc:
forall i c sigma c',
substc sigma c = c' ->
substc (upn i sigma) (liftc i c) = liftc i c'.
Proof.
intros. subst. destruct c; simpl.
{ rewrite lift_upn by tc. reflexivity. }
{ asimpl. erewrite plus_upn by tc. autosubst. }
Qed.
Hint Resolve substc_liftc_liftc : obvious.
(* As is the case for terms, lifting [c] by 1, then applying a substitution
of the form [v .: ids], yields [c] again. *)
Lemma substc_liftc_single:
forall c v,
substc (v .: ids) (liftc 1 c) = c.
Proof.
intros. destruct c; autosubst.
Qed.

138
coq/CPSCorrectness.v Normal file
View file

@ -0,0 +1,138 @@
Require Import MyTactics.
Require Import Sequences.
Require Import Relations.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusValues.
Require Import LambdaCalculusReduction.
Require Import LambdaCalculusStandardization.
Require Import CPSDefinition.
Require Import CPSSpecialCases.
Require Import CPSSimulation.
(* [cbv+ . pcbv] implies [pcbv*]. *)
Lemma technical_inclusion_0:
inclusion plus_cbv_pcbv (star pcbv).
Proof.
intros t1 t2. unfold composition. intros. unpack.
eauto 6 using cbv_subset_pcbv, plus_covariant with sequences.
Qed.
(* [(cbv+ . pcbv)*] implies [pcbv*]. *)
Lemma technical_inclusion_1:
inclusion (star plus_cbv_pcbv) (star pcbv).
Proof.
eapply inclusion_transitive; [| eapply inclusion_star_star ].
eapply star_covariant_inclusion.
eapply technical_inclusion_0.
Qed.
(* A simplified simulation diagram. *)
Lemma simulation_cbv_pcbv:
forall t t',
star cbv t t' ->
star pcbv (cps t init) (cps t' init).
Proof.
intros t t' Hred.
(* According to the simulation diagram (iterated), [cps t c] reduces to
[cps v c] via a series of [cbv] and [pcbv] steps. *)
destruct (star_diamond_left _ _ _ cps_init_simulation _ _ Hred _ eq_refl)
as (?&?&?). subst.
(* Thus, [cps t c] reduces to [cps t' c] via [pcbv*]. *)
eapply technical_inclusion_1. eauto.
Qed.
(* If [t] diverges, then [cps t init] diverges, too. *)
Lemma cps_preserves_divergence:
forall t,
infseq cbv t ->
infseq cbv (cps t init).
Proof.
intros.
eapply pcbv_preserves_divergence.
eapply infseq_simulation.
{ eapply cps_init_simulation. }
{ eauto. }
{ tauto. }
Qed.
(* If [t] converges to a value [v], then [cps t init] converges to a value [w].
Furthermore, [w] reduces to [cpsv v] via a number of parallel reduction
steps. *)
Lemma cps_preserves_convergence:
forall t v,
star cbv t v ->
is_value v ->
exists w,
star cbv (cps t init) w /\
is_value w /\
star pcbv w (cpsv v).
Proof.
intros ? ? Htv Hv.
(* [cps t init] reduces to [cps v init] via [pcbv*]. *)
generalize (simulation_cbv_pcbv _ _ Htv); intro Hred.
(* [cps v init] is [cpsv v]. *)
assert (Heq: cps v init = cpsv v).
{ cps. reflexivity. }
(* Thus, [cps t init] reduces to [cpsv v] via [pcbv*]. *)
rewrite Heq in Hred.
(* Bifurcate this reduction sequence. *)
forward1 crarys_lemma9. clear Hred.
(* This gives us the value [w] that we are looking for. *)
eexists. split. eauto. split.
{ eauto using
(star_implication_reversed _ ipcbv_preserves_values_reversed)
with obvious. }
{ eauto using star_covariant, ipcbv_subset_pcbv. }
Qed.
(* If [t] is stuck, then [cps t c] is stuck. Not a really interesting
property, but we prove it, just so that no stone is left unturned. *)
Lemma cps_preserves_stuck:
forall t,
stuck t ->
forall c,
stuck (cps t c).
Proof.
induction 1; intros.
(* StuckApp *)
{ rewrite cps_app_value_value by eauto.
eapply StuckAppL.
eapply StuckApp; [ obvious | obvious |].
(* Only [Lam] is translated to [Lam]. *)
intros. destruct v1.
{ cpsv. congruence. }
{ cpsv. false. congruence. }
{ obvious. }
{ obvious. }
}
(* StuckAppL *)
{ cps. eauto. }
(* StuckAppR *)
{ rewrite cps_app_value by eauto. eauto. }
(* StuckLetL *)
{ cps. eauto. }
Qed.
(* As a corollary, the property of going wrong is preserved by the CPS
transformation. *)
Lemma cps_preserves_going_wrong:
forall t,
goes_wrong t ->
goes_wrong (cps t init).
Proof.
intros ? [ t' [ Htt' ? ]].
(* [cps t init] reduces to [cps t' init] via [pcbv*]. *)
generalize (simulation_cbv_pcbv _ _ Htt'); intro Hred.
(* Bifurcate this reduction sequence. *)
forward1 crarys_lemma9. clear Hred.
(* This gives us the stuck term we are looking for. *)
eexists. split. eauto.
eauto using cps_preserves_stuck, reverse_star_ipcbv_preserves_stuck.
Qed.

107
coq/CPSCounterExample.v Normal file
View file

@ -0,0 +1,107 @@
Require Import MyTactics.
Require Import Sequences.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusValues.
Require Import LambdaCalculusReduction.
Require Import CPSDefinition.
(* The single-step simulation lemma in Danvy and Filinski's paper states that
if [t1] reduces to [t2], then [cps t1 c] reduces (in one or more steps) to
[cps t2 c]. Although this lemma is true in the pure lambda calculus, it
fails when the calculus is extended with [Let]. This file provides two
counter-examples. *)
(* Although Danvy and Filinski's paper does not claim that this lemma holds
when the calculus is extended with [Let], it does not indicate that the
lemma fails, either. *)
(* -------------------------------------------------------------------------- *)
(* The tactic [analyze] assumes that there is a hypothesis [star cbv t1 t2].
It checks that [t1] and [t2] are distinct and, if [t1] reduces to [t'1],
updates this hypothesis to [star cbv t'1 t2]. Repeating this tactic allows
proving that [t1] does *not* reduce to [t2]. *)
Ltac analyze :=
invert_star_cbv; repeat invert_cbv; compute in *; fold cbv_mask in *;
repeat match goal with h: True |- _ => clear h end.
Transparent cps cpsv. (* required by [compute] *)
(* -------------------------------------------------------------------------- *)
(* Consider the term [t1], defined as follows. In informal syntax, [t1]
is written (\z.let w = z in w) (\x.x). *)
Definition t1 :=
App (Lam (Let (Var 0) (Var 0))) (Lam (Var 0)).
(* The term [t1] reduces to [t2], which in informal syntax is written
let w = \x.x in w. *)
Definition t2 :=
Let (Lam (Var 0)) (Var 0).
Goal
cbv t1 t2.
Proof.
unfold t1, t2. obvious.
Qed.
(* The single-step simulation diagram is violated: [cps t1 init] does
*not* reduce (in any number of steps) to [cps t2 init]. *)
Goal
~ (star cbv (cps t1 init) (cps t2 init)).
Proof.
compute; fold cbv_mask. intro.
analyze.
analyze.
(* This point is the near miss:
[cps t1 init] has now reduced to a [Let] construct, whereas
[cps t2 init] is a similar-looking [Let] construct.
Both have the same value on the left-hand side of the [Let].
But the right-hand sides of the [Let] construct differ. *)
analyze.
analyze.
analyze.
Qed.
(* Let us summarize.
The term [t1] reduces in one step to [t2] as follows:
(\z.let w = z in w) (\x.x)
->
let w = \x.x in w
The term [cps t1 init], in informal notation, is as follows:
(\z.\k.let w = z in k w)
(\x.\k. k x)
(\w.w)
This term reduces in two steps to:
let w = \x.\k. k x in
(\w.w) w
But the term [cps t2 init], in informal notation, is:
let w = \x.\k. k x in
w
This is our near miss. Both terms are [let] constructs and both have
the same left-hand side, but the right-hand sides differ by a beta-v
reduction. Thus, [cps t1 init] does not reduce *in call-by-value* to
[cps t2 init]. In order to allow [cps u1 init] to join [cps u2 init],
we must allow beta-v reductions in the right-hand side of [let]
constructs (and, it turns out, under lambda-abstractions, too.)
This is visible in the proof of the [simulation] lemma in the file
CPSSimulation: there, we use the reduction strategy [pcbv], which
allows (parallel) beta-v reductions under arbitrary contexts. *)
(* This counter-example is one of two closed counter-examples of minimal size.
It has size 4 (counting [Lam], [App], and [Let] nodes) and involves only
one [Let] construct. There are no smaller counter-examples. An exhaustive
search procedure, coded in OCaml, was used to find it. *)

446
coq/CPSDefinition.v Normal file
View file

@ -0,0 +1,446 @@
Require Import MyTactics.
Require Import FixExtra.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusValues.
(* This is a definition of the CPS transformation. *)
(* This CPS transformation is "one-pass" in the sense that it does not produce
any administrative redexes. (In other words, there is no need for a second
pass, whose purpose would be to remove administrative redexes.)
To achieve this, instead of defining [cps t k], where the continuation [k]
is a term, we define [cps t c], where the continuation [c] is either a term
(also known as an object-level continuation) or a term-with-a-hole [K]
(also known as a meta-level continuation).
This formulation of the CPS transformation is analogous to Danvy and
Filinski's higher-order formulation. Yet, it is still technically
first-order, because we represent a term-with-a-hole [K] as a term,
where the variable 0 denotes the hole. *)
(* This CPS transformation is defined by recursion on the size of terms. This
allows recursive calls of the form [cps (lift 1 t)], which would be illegal
if [cps] was defined by structural induction. Definitions by well-founded
recursion in Coq are somewhat tricky, requiring the use of the fixed point
combinator [Fix] and the tactic [refine]. For explanations, see the chapter
on general recursion in Chlipala's book at
http://adam.chlipala.net/cpdt/html/GeneralRec.html *)
(* The situation could be complicated by the fact that we wish to define two
functions simultaneously:
[cpsv v] is the translation of a value [v].
[cps t c] is the translation of a term [t] with continuation [c].
To avoid this problem, we follow Danvy and Filinski's approach, which is to
first define [cps] directly (as this does not cause much duplication), then
define [cpsv] in terms of [cps]. In the latter step, no case analysis is
required: [cpsv] is obtained by invoking [cps] with an identity meta-level
continuation.
Regardless of how [cps] and [cpsv] are defined, we prove that the they
satisfy the desired recurrence equations, so, in the end, everything is
just as if they had been defined in a mutually recursive manner. *)
(* -------------------------------------------------------------------------- *)
(* As explained above, a continuation [c] is
either [O k], where [k] is a term (in fact, a value)
(an object-level continuation)
or [M K], where [K] is term-with-a-hole
(a meta-level continuation).
A term-with-a-hole [K] is represented as a term where the variable 0 denotes
the hole (and, of course, all other variables are shifted up). *)
Inductive continuation :=
| O (k : term)
| M (K : term).
(* The term [apply c v] is the application of the continuation [c] to the
value [v]. If [c] is an object-level continuation [k] (that is, a term),
then it is just the object-level application [App k v]. If [c] is a
meta-level continuation [K], then it is the meta-level operation of filling
the hole with the value [v], which in fact is just a substitution,
[K.[v/]]. *)
Definition apply (c : continuation) (v : term) : term :=
match c with
| O k =>
App k v
| M K =>
K.[v/]
end.
(* The term [reify c] is the reification of the continuation [c] as an
object-level continuation (that is, a term). If [c] is an object-level
continuation [k], then it is just [k]. If [c] is a meta-level continuation
[K], then [reify c] is the term [\x.K x]. (This is usually known as a
two-level eta-expansion.) Because the hole is already represented by the
variable 0, filling the hole with the variable [x] is a no-op. Therefore,
it suffices to write [Lam K] to obtain the desired lambda-abstraction. *)
Definition reify (c : continuation) : term :=
match c with
| O k =>
k
| M K =>
Lam K
end.
(* The continuation [substc sigma c] is the result of applying the
substitution [sigma] to the continuation [c]. *)
Definition substc sigma (c : continuation) : continuation :=
match c with
| O k =>
O k.[sigma]
| M K =>
M K.[up sigma]
end.
(* [liftc i c] is the result of lifting the free names of the continuation [c]
up by [i]. The function [liftc] can be defined in terms of [substc]. *)
Notation liftc i c :=
(substc (ren (+i)) c).
(* -------------------------------------------------------------------------- *)
(* Here is the definition of [cps]. Because we must keep track of sizes and
prove that the recursive calls cause a decrease in the size, this
definition cannot be easily written as Coq terms. Instead, we switch to
proof mode and use the tactic [refine]. This allows us to write some of the
code, with holes [_] in it, and use proof mode to fill the holes. *)
(* [cps t c] is the CPS-translation of the term [t] with continuation [c]. *)
Definition cps : term -> continuation -> term.
Proof.
(* The definition is by well-founded recursion on the size of [t]. *)
refine (Fix smaller_wf_transparent (fun _ => continuation -> term) _).
(* We receive the arguments [t] and [c] as well as a function [cps_]
which we use for recursive calls. At every call to [cps_], there
is an obligation to prove that the size of the argument is less
than the size of [t]. *)
intros t cps_ c.
(* The definition is by cases on the term [t]. *)
destruct t as [ x | t | t1 t2 | t1 t2 ].
(* When [t] is a value, we return an application of the continuation [c]
to a value which will later be known as [cpsv t]. *)
(* Case: [Var x]. *)
{ refine (apply c (Var x)). }
(* Case: [Lam t]. *)
(* In informal notation, the term [\x.t] is transformed to an application of
[c] to [\x.\k.[cps t k]], where [k] is a fresh variable. Here, [k] is
represented by the de Bruijn index 0, and the term [t] must be lifted
because it is brought into the scope of [k]. *)
{ refine (apply c
(Lam (* x *) (Lam (* k *) (cps_ (lift 1 t) _ (O (Var 0)))))
); abstract size. }
(* Case: [App t1 t2]. *)
(* The idea is, roughly, to first obtain the value [v1] of [t1], then obtain
the value [v2] of [t2], then perform the application [v1 v2 c].
Two successive calls to [cps] are used to obtain [v1] and [v2]. In each
case, we avoid administrative redexes by using an [M] continuation.
Thus, [v1] and [v2] are represented by two holes, denoted by the
variables [Var 1] and [Var 0].
If [t1] is a value, then the first hole will be filled directly with (the
translation of) [t1]; otherwise, it will be filled with a fresh variable,
bound to the result of evaluating (the translation of) [t1]. The same
goes for [t2].
The application [v1 v2 c] does not directly make sense, since [c] is a
continuation, not a term. Instead of [c], we must use [reify c]. The
continuation [c] must turned into a term, so it can be used in this
term-level application.
A little de Bruijn wizardry is involved. The term [t2] must be lifted up
by 1 because it is brought into the scope of the first meta-level
continuation. Similarly, the first hole must be lifted by 1 because it is
brought into the scope of the second meta-level continuation: thus, it
becomes Var 1. Finally, the continuation [c] must be lifted up by [2]
because it is brought into the scope of both. Here, we have a choice
between [reify (liftc _ c)] and [lift _ (reify c)], which mean the same
thing. *)
{ refine (
cps_ t1 _ (M (
cps_ (lift 1 t2) _ (M (
App (App (Var 1) (Var 0)) (lift 2 (reify c))
))
))
);
abstract size.
}
(* Case: [Let x = t1 in t2]. *)
(* The idea is to first obtain the value [v1] of [t1]. This value is
represented by the hole [Var 0] in the [M] continuation. We bind
this value via a [Let] construct to the variable [x] (represented by the
index 0 in [t2]), then execute [t2], under the original continuation [c].
All variables in [t2] except [x] must lifted up by one because they are
brought in the scope of the meta-level continuation. The continuation [c]
must be lifted up by 2 because it is brought in the scope of the
meta-level continuation and in the scope of the [Let] construct. *)
{ refine (
cps_ t1 _ (M (
Let (Var 0) (
cps_ t2.[up (ren (+1))] _ (liftc 2 c)
)
))
);
abstract size.
}
Defined.
(* -------------------------------------------------------------------------- *)
(* The above definition can be used inside Coq to compute the image of a term
through the transformation. For instance, the image under [cps] of [\x.x]
with object-level continuation [k] (a variable) is [k (\x.\k.k x)]. *)
Goal
cps (Lam (Var 0)) (O (Var 0)) =
App (Var 0) (Lam (Lam (App (Var 0) (Var 1)))).
Proof.
compute. (* optional *)
reflexivity.
Qed.
(* The image of [(\x.x) y] with continuation [k] is [(\x.\k.k x) y k]. *)
Goal
cps (App (Lam (Var 0)) (Var 0)) (O (Var 1)) =
App (App (Lam (Lam (App (Var 0) (Var 1)))) (Var 0)) (Var 1).
Proof.
compute. (* optional *)
reflexivity.
Qed.
(* -------------------------------------------------------------------------- *)
(* The initial continuation is used when invoking [cps] at the top level. *)
(* We could use [O (Lam (Var 0))] -- that is, the identity function -- as
the initial continuation. Instead, we use [M (Var 0)], that is, the
empty context. This sometimes saves one beta-redex. *)
Definition init :=
M (Var 0).
Definition cpsinit t :=
cps t init.
(* -------------------------------------------------------------------------- *)
(* Now that [cps] is defined, we can define [cpsv] in terms of it. *)
(* We explicitly check whether [v] is a value, and if it is not, we return a
dummy closed value. [cpsv] is supposed to be applied only to values,
anyway. Using a dummy value allows us to prove that [cpsv v] is always a
value, without requiring that [v] itself be a value. *)
Definition cpsv (v : term) :=
if_value v
(cpsinit v)
(Lam (Var 0)).
(* -------------------------------------------------------------------------- *)
(* The function [cps] satisfies the expected recurrence equations. *)
(* The lemmas [cps_var] and [cps_lam] are not used outside this file, as we
use [cps_value] instead, followed with [cpsv_var] or [cpsv_lam]. *)
Lemma cps_var:
forall x c,
cps (Var x) c = apply c (Var x).
Proof.
reflexivity.
Qed.
Lemma cps_lam:
forall t c,
cps (Lam t) c =
apply c (Lam (* x *) (Lam (* k *) (cps (lift 1 t) (O (Var 0))))).
Proof.
intros. erewrite Fix_eq_simplified with (f := cps) by reflexivity.
reflexivity.
Qed.
Lemma cps_app:
forall t1 t2 c,
cps (App t1 t2) c =
cps t1 (M (
cps (lift 1 t2) (M (
App (App (Var 1) (Var 0)) (lift 2 (reify c))
))
)).
Proof.
intros. erewrite Fix_eq_simplified with (f := cps) by reflexivity.
reflexivity.
Qed.
Lemma cps_let:
forall t1 t2 c,
cps (Let t1 t2) c =
cps t1 (M (
Let (Var 0) (
cps t2.[up (ren (+1))] (liftc 2 c)
)
)).
Proof.
intros. erewrite Fix_eq_simplified with (f := cps) by reflexivity.
reflexivity.
Qed.
(* -------------------------------------------------------------------------- *)
(* The translation of values is uniform: we also have the following equation. *)
Lemma cps_value:
forall v c,
is_value v ->
cps v c = apply c (cpsv v).
Proof.
destruct v; simpl; intros; try not_a_value; unfold cpsv, cpsinit.
{ rewrite !cps_var. reflexivity. }
{ rewrite !cps_lam. reflexivity. }
Qed.
(* -------------------------------------------------------------------------- *)
(* The function [cpsv] satisfies the expected recurrence equations. *)
Lemma cpsv_var:
forall x,
cpsv (Var x) = Var x.
Proof.
reflexivity.
Qed.
Lemma cpsv_lam:
forall t,
cpsv (Lam t) = Lam (Lam (cps (lift 1 t) (O (Var 0)))).
Proof.
intros. unfold cpsv, cpsinit. rewrite cps_lam. reflexivity.
Qed.
(* If [theta] is a renaming, then [theta x] is a variable, so [cpsv (theta x)]
is [theta x], which can also be written [(Var x).[theta]]. *)
Lemma cpsv_var_theta:
forall theta x,
is_ren theta ->
cpsv (theta x) = (Var x).[theta].
Proof.
inversion 1. subst. asimpl. reflexivity.
Qed.
(* -------------------------------------------------------------------------- *)
(* The tactic [cps] applies the rewriting rules [cps_value] and [cps_app] as
many times as possible, therefore expanding applications of the function
[cps] to values and to applications. *)
Ltac cps :=
repeat first [ rewrite cps_value by obvious
| rewrite cps_app | rewrite cps_let ].
(* -------------------------------------------------------------------------- *)
(* The translation of a value is a value. *)
(* In fact, thanks to the manner in which we have defined [cpsv], the image of
every term through [cpsv] is a value. This turns out to be quite pleasant,
as it allows removing nasty side conditions in several lemmas. *)
Lemma is_value_cpsv:
forall v,
(* is_value v -> *)
is_value (cpsv v).
Proof.
intros. destruct v; simpl; tauto.
Qed.
Hint Resolve is_value_cpsv : is_value obvious.
Hint Rewrite cpsv_var cpsv_lam : cpsv.
Ltac cpsv := autorewrite with cpsv.
(* -------------------------------------------------------------------------- *)
(* As a final step, we prove an induction principle that helps work with the
functions [cpsv] and [cps]. When trying to establish a property of the
function [cps], we often need to prove this property by induction on the
size of terms. Furthermore, we usually need to state an auxiliary property
of the function [cpsv] and to prove the two statements simultaneously, by
induction on the size of terms. The following lemma is tailored for this
purpose. It proves the properties [Pcpsv] and [Pcps] simultaneously. The
manner in which the index [n] is used reflects precisely the manner in
which each function depends on the other, with or without a decrease in
[n]. The dependencies are as follows:
[cpsv] invokes [cps] with a size decrease.
[cps] invokes [cpsv] without a size decrease and
[cps] with a size decrease.
It is worth noting that this proof has nothing to do with the definitions
of [cpsv] and [cps]. It happens to reflect just the right dependencies
between them. *)
Lemma mutual_induction:
forall
(Pcpsv : term -> Prop)
(Pcps : term -> continuation -> Prop),
(forall n,
(forall t c, size t < n -> Pcps t c) ->
(forall v, size v < S n -> Pcpsv v)
) ->
(forall n,
(forall v, size v < S n -> Pcpsv v) ->
(forall t c, size t < n -> Pcps t c) ->
(forall t c, size t < S n -> Pcps t c)
) ->
(
(forall v, Pcpsv v) /\
(forall t c, Pcps t c)
).
Proof.
intros Pcpsv Pcps IHcpsv IHcps.
assert (fact:
forall n,
(forall v, size v < n -> Pcpsv v) /\
(forall t k, size t < n -> Pcps t k)
).
{ induction n; intros; split; intros;
try solve [ elimtype False; omega ];
destruct IHn as (?&?); eauto. }
split; intros; eapply fact; eauto.
Qed.
(* -------------------------------------------------------------------------- *)
(* In the proofs that follow, we never expand the definition of [cpsv] or
[cps]: we use the tactics [cpsv] and [cps] instead. We actually forbid
unfolding [cpsv] and [cps], so our proofs cannot depend on the details of
the above definitions.
In general, when working with complex objects, it is good practice anyway
to characterize an object and forget how it was defined. Here, the
functions [cpsv] and [cps] are characterized by the equations that they
satisfy; the rest does not matter.
Attempting to work with transparent [cpsv] and [cps] would be problematic
for several reasons. The tactics [simpl] and [asimpl] would sometimes
expand these functions too far. Furthermore, because we have used the term
[smaller_wf_transparent] inside the definition of [cps], expanding [cps]
definition would often give rise to uncontrollably large terms. *)
Global Opaque cps cpsv.

262
coq/CPSIndifference.v Normal file
View file

@ -0,0 +1,262 @@
Require Import MyTactics.
Require Import Sequences.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusValues.
Require Import LambdaCalculusReduction.
Require Import CPSDefinition.
(* In a CPS term (i.e., a term produced by the CPS translation), the
right-hand side of every application is a value, and the left-hand
side of every [let] construct is a value. *)
Inductive is_cps : term -> Prop :=
| IsCPSVar:
forall x,
is_cps (Var x)
| IsCPSLam:
forall t,
is_cps t ->
is_cps (Lam t)
| IsCPSApp:
forall t1 t2,
is_cps t1 ->
is_cps t2 ->
is_value t2 ->
is_cps (App t1 t2)
| IsCPSLet:
forall t1 t2,
is_cps t1 ->
is_cps t2 ->
is_value t1 ->
is_cps (Let t1 t2)
.
(* To prove that the above invariant holds, we must also define what it means
for a continuation [c] to satisfy this invariant. *)
Inductive is_cps_continuation : continuation -> Prop :=
| IsCPSO:
forall k,
is_value k ->
is_cps k ->
is_cps_continuation (O k)
| IsCPSM:
forall K,
is_cps K ->
is_cps_continuation (M K).
Local Hint Constructors is_cps is_cps_continuation.
(* [is_cps] is preserved by renamings. *)
Lemma is_cps_renaming:
forall t,
is_cps t ->
forall sigma,
is_ren sigma ->
is_cps t.[sigma].
Proof.
induction 1; intros sigma Hsigma; asimpl;
try solve [ econstructor; obvious ].
(* Var *)
{ destruct Hsigma as [ xi ? ]. subst sigma. asimpl. econstructor. }
Qed.
Local Hint Resolve is_cps_renaming.
Lemma is_cps_continuation_renaming:
forall c i,
is_cps_continuation c ->
is_cps_continuation (liftc i c).
Proof.
induction 1; simpl; econstructor; obvious.
Qed.
Local Hint Resolve is_cps_continuation_renaming.
(* [is_cps] is preserved by substitution. *)
Lemma is_cps_substitution_aux:
forall sigma,
(forall x, is_cps (sigma x)) ->
(forall x, is_cps (up sigma x)).
Proof.
intros sigma H [|x]; asimpl.
{ econstructor. }
{ eapply is_cps_renaming; obvious. }
Qed.
Lemma is_cps_substitution:
forall K,
is_cps K ->
forall sigma,
(forall x, is_cps (sigma x)) ->
is_value_subst sigma ->
is_cps K.[sigma].
Proof.
induction 1; intros; asimpl; eauto;
econstructor; eauto using is_cps_substitution_aux with obvious.
Qed.
Lemma is_cps_substitution_0:
forall K v,
is_cps K ->
is_cps v ->
is_value v ->
is_cps K.[v/].
Proof.
intros. eapply is_cps_substitution; obvious.
intros [|x]; asimpl; eauto.
Qed.
(* Inversion lemmas for [is_cps]. *)
Lemma is_cps_Lam_inversion:
forall t,
is_cps (Lam t) ->
is_cps t.
Proof.
inversion 1; eauto.
Qed.
(* A CPS term reduces in the same manner in call-by-value and in call-by-name.
Thus, the CPS transformation produces terms that are "indifferent" to which
of these two reduction strategies is chosen. *)
Lemma cps_indifference_1:
forall t1, is_cps t1 ->
forall t2, cbv t1 t2 -> cbn t1 t2.
Proof.
induction 1; intros; invert_cbv; obvious.
Qed.
Lemma cps_indifference_2:
forall t1, is_cps t1 ->
forall t2, cbn t1 t2 -> cbv t1 t2.
Proof.
induction 1; intros; invert_cbn; obvious.
Qed.
(* [is_cps] is preserved by call-by-value and call-by-name reduction. *)
Lemma is_cps_cbv:
forall t,
is_cps t ->
forall t',
cbv t t' ->
is_cps t'.
Proof.
induction 1; intros; invert_cbv;
eauto using is_cps, is_cps_substitution_0, is_cps_Lam_inversion.
Qed.
Lemma is_cps_cbn:
forall t,
is_cps t ->
forall t',
cbn t t' ->
is_cps t'.
Proof.
induction 1; intros; invert_cbn;
eauto using is_cps, is_cps_substitution_0, is_cps_Lam_inversion.
Qed.
(* A CPS term reduces in the same manner in call-by-value and in call-by-name.
The statement is here generalized to a sequence of reduction steps. *)
Lemma cps_star_indifference_1:
forall t1 t2,
star cbv t1 t2 ->
is_cps t1 ->
star cbn t1 t2.
Proof.
induction 1; intros;
eauto using cps_indifference_1, is_cps_cbv with sequences.
Qed.
Lemma cps_star_indifference_2:
forall t1 t2,
star cbn t1 t2 ->
is_cps t1 ->
star cbv t1 t2.
Proof.
induction 1; intros;
eauto using cps_indifference_2, is_cps_cbn with sequences.
Qed.
(* The main auxiliary lemmas. *)
Lemma is_cps_apply:
forall c v,
is_cps_continuation c ->
is_cps v ->
is_value v ->
is_cps (apply c v).
Proof.
inversion 1; intros; simpl; eauto using is_cps_substitution_0.
Qed.
Lemma is_cps_reify:
forall c,
is_cps_continuation c ->
is_cps (reify c).
Proof.
inversion 1; simpl; eauto.
Qed.
Lemma is_value_reify:
forall c,
is_cps_continuation c ->
is_value (reify c).
Proof.
inversion 1; simpl; eauto.
Qed.
Local Hint Resolve is_cps_apply is_cps_reify is_value_reify.
(* The main lemma. *)
Lemma cps_form:
(
forall v,
is_value v ->
is_cps (cpsv v)
) /\ (
forall t c,
is_cps_continuation c ->
is_cps (cps t c)
).
Proof.
eapply mutual_induction.
(* [cpsv] *)
{ intros n IHcps v Hvn ?.
destruct v; [ | | false; obvious | false; obvious ].
{ cpsv; eauto. }
{ cpsv; eauto 6 with size. }
}
(* [cps] *)
{ intros n IHcpsv IHcps t c Htn Hc.
value_or_app_or_let t; cps.
(* Case: [t] is a value. *)
{ obvious. }
(* Case: [t] is an application. *)
{ eapply IHcps; [ size | econstructor ].
eapply IHcps; [ size | econstructor ].
econstructor; obvious. }
(* Case: [t] is a [let] construct. *)
{ eauto 8 with obvious. }
}
Qed.
Lemma cps_form_main:
forall t,
is_cps (cpsinit t).
Proof.
simpl. intros. eapply cps_form. unfold init. obvious.
Qed.
(* One property of CPS terms that we do not prove is that all applications are
in tail position, or, in other words, that there is no need for reduction
under a context. In fact, because a CPS-translated function expects two
arguments, there *is* a need for reduction under a context, but only under
a context of depth zero or one. *)

120
coq/CPSKubstitution.v Normal file
View file

@ -0,0 +1,120 @@
Require Import MyTactics.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusValues.
Require Import CPSDefinition.
Require Import CPSContextSubstitution.
Require Import CPSRenaming.
(* The [substitution] lemma in CPSSubstitution pushes a substitution
into [cps t k]. The substitution is pushed into both [t] and [k].
Because it is pushed into [t], this substitution must be of the
form [sigma >>> cpsv], so that, once pushed into [t], it becomes
just [sigma]. *)
(* Here, we prove another substitution lemma, where the substitution
need not be of the form [sigma >>> cpsv]. It can be an arbitrary
substitution. We require [sigma] to not affect the term [t], so
[sigma] is not pushed into [t]: it is pushed into [k] only. For
this reason, we refer to this lemma as the [kubstitution] lemma.
In order to express the idea that [sigma] does not affect a term,
more precisely, we write this term under the form [t.[theta]]
and we require that [theta] and [sigma] cancel out, that is,
theta >> sigma = ids
(This condition implies [is_ren theta], that is, [theta] must be
a renaming.) Then, we are able to prove the following result:
(cps t.[theta] (O k)).[sigma] = cps t (O k.[sigma])
That is, the substitution [sigma], when pushed into [t], meets [theta]
and they cancel out. *)
(* [apply] commutes with kubstitutions. *)
Lemma apply_kubstitution:
forall c theta sigma c' v,
theta >> sigma = ids ->
substc sigma c = c' ->
(apply c v.[theta]).[sigma] = apply c' v.
Proof.
intros. subst.
destruct c; asimpl; pick @eq ltac:(fun h => rewrite h); autosubst.
Qed.
Local Hint Resolve up_theta_sigma_ids : obvious.
(* The main result: [cpsv] and [cps] commute with kubstitutions. *)
Lemma kubstitution:
(
forall v theta sigma,
theta >> sigma = ids ->
(cpsv v.[theta]).[sigma] = cpsv v
) /\ (
forall t c theta sigma c',
theta >> sigma = ids ->
substc sigma c = c' ->
(cps t.[theta] c).[sigma] = cps t c'
).
Proof.
eapply mutual_induction.
(* [cpsv] *)
{ intros n IHcps v Hvn theta sigma Hid. clear IHcps.
rewrite <- cpsv_renaming by obvious.
asimpl. rewrite Hid.
asimpl. reflexivity. }
(* [cps] *)
{ intros n IHcpsv IHcps t c Htn theta sigma c' Hid Hkubstc. clear IHcpsv.
value_or_app_or_let t; asimpl; cps.
(* Case: [t] is a value. *)
{ rewrite <- cpsv_renaming by obvious.
eauto using apply_kubstitution. }
(* Case: [t] is an application. *)
{ eapply IHcps; obvious.
simpl. f_equal.
erewrite <- lift_up by tc.
eapply IHcps; obvious.
asimpl. do 2 f_equal.
rewrite lift_reify.
eapply reify_substitution.
subst. rewrite substc_substc.
reflexivity. }
(* Case: [t] is a [let] construct. *)
{ eapply IHcps; obvious.
simpl. do 2 f_equal.
rewrite fold_up_up.
rewrite up_sigma_up_ren by tc. simpl.
eapply IHcps; obvious. }
}
Qed.
(* The projections of the above result. *)
Definition cpsv_kubstitution := proj1 kubstitution.
Definition cps_kubstitution := proj2 kubstitution.
(* A corollary where the substitution [sigma] is [v .: ids], that is, a
substitution of the value [v] for the variable 0. *)
Lemma cps_kubstitution_0:
forall t c v,
(cps (lift 1 t) c).[v/] = cps t (substc (v .: ids) c).
Proof.
intros. eapply cps_kubstitution.
{ autosubst. }
{ reflexivity. }
Qed.
(* A corollary where the substitution [sigma] is [up (v .: ids)], that is, a
substitution of the value [v] for the variable 1. *)
Lemma cps_kubstitution_1:
forall t c v,
(cps t.[up (ren (+1))] c).[up (v .: ids)] = cps t (substc (up (v .: ids)) c).
Proof.
intros. eapply cps_kubstitution.
{ autosubst. }
{ reflexivity. }
Qed.

92
coq/CPSRenaming.v Normal file
View file

@ -0,0 +1,92 @@
Require Import MyTactics.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusValues.
Require Import CPSDefinition.
Require Import CPSContextSubstitution.
(* The CPS transformation commutes with renamings, where a renaming [sigma] is
a substitution that maps variables to variables. (Note that [sigma] is not
necessarily injective.) *)
Lemma renaming:
(
forall v sigma,
is_ren sigma ->
(cpsv v).[sigma] = cpsv v.[sigma]
) /\ (
forall t c sigma c',
is_ren sigma ->
substc sigma c = c' ->
(cps t c).[sigma] = cps t.[sigma] c'
).
Proof.
eapply mutual_induction.
(* [cpsv] *)
{ intros n IHcps v Hvn sigma Hsigma.
destruct v; asimpl; cpsv; asimpl; try reflexivity.
(* [Var] *)
(* The CPS transformation maps variables to variables. *)
{ destruct Hsigma as [ xi ? ]. subst sigma. reflexivity. }
(* [Lam] *)
{ erewrite IHcps by obvious. asimpl. reflexivity. }
}
(* [cps] *)
{ intros n IHcpsv IHcps t c Htn sigma c' Hsigma Hsubstc.
(* Perform case analysis on [t]. The first two cases, [Var] and [Lam],
can be shared by treating the case where [t] is a value. *)
value_or_app_or_let t; asimpl; cps.
(* Case: [t] is a value. *)
{ erewrite apply_substitution by eauto.
rewrite IHcpsv by obvious.
reflexivity. }
(* Case: [t] is an application. *)
{ eapply IHcps; obvious.
erewrite <- lift_upn by tc.
simpl. f_equal.
eapply IHcps; obvious.
simpl.
rewrite fold_up_upn, lift_upn by tc.
do 3 f_equal.
eauto using reify_substitution. }
(* Case: [t] is a [let] construct. *)
{ eapply IHcps; obvious.
simpl. do 2 f_equal.
rewrite fold_up_up.
erewrite IHcps by first [ eapply substc_liftc_liftc; eauto | obvious ].
autosubst. }
}
Qed.
(* The projections of the above result. *)
Definition cpsv_renaming := proj1 renaming.
Definition cps_renaming := proj2 renaming.
(* A point-free reformulation of the above result: [cpsv] commutes with
an arbitrary renaming [xi]. *)
Goal
forall sigma,
is_ren sigma ->
cpsv >>> subst sigma = subst sigma >>> cpsv.
Proof.
intros. f_ext; intros t. asimpl. eauto using cpsv_renaming.
Qed.
(* Corollaries. *)
Lemma up_sigma_cpsv:
forall sigma,
up (sigma >>> cpsv) = up sigma >>> cpsv.
Proof.
eauto using up_sigma_f, cpsv_renaming with is_ren typeclass_instances.
Qed.
Lemma upn_sigma_cpsv:
forall i sigma,
upn i (sigma >>> cpsv) = upn i sigma >>> cpsv.
Proof.
eauto using upn_sigma_f, cpsv_renaming with is_ren typeclass_instances.
Qed.
Hint Resolve up_sigma_cpsv upn_sigma_cpsv : obvious.

177
coq/CPSSimulation.v Normal file
View file

@ -0,0 +1,177 @@
Require Import MyTactics.
Require Import Sequences.
Require Import Relations.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusValues.
Require Import LambdaCalculusReduction.
Require Import CPSDefinition.
Require Import CPSContextSubstitution.
Require Import CPSRenaming.
Require Import CPSSubstitution.
Require Import CPSKubstitution.
Require Import CPSSpecialCases.
(* We now prepare for the statement of the "magic step" lemma [pcbv_cps]. This
lemma states that if the continuations [c1] and [c2] are similar, then [cps
t c1] is able to reduce via [pcbv] to [cps t c2]. We use parallel reduction
[pcbv] because we must allow reduction to take place under [Lam] and in the
right-hand side of [Let]. We do not need the full power of [pcbv]: we only
reduce zero or one redexes, never more. *)
(* A simplified copy of this file, where we pretend that the [Let] construct
does not exist, can be found in [CPSSimulationWithoutLet.v]. There, there
is no need for parallel reduction; a simpler simulation diagram holds. *)
(* Similarity of continuations is defined as follows: *)
Inductive similar : continuation -> continuation -> Prop :=
| SimilarReify:
forall c,
similar (O (reify c)) c
| SimilarM:
forall K1 K2,
pcbv K1 K2 ->
similar (M K1) (M K2).
(* Similarity is preserved by lifting. *)
Lemma similar_liftc_liftc:
forall i c1 c2,
similar c1 c2 ->
similar (liftc i c1) (liftc i c2).
Proof.
induction 1; intros; simpl.
{ rewrite lift_reify. econstructor. }
{ econstructor. eapply red_subst; obvious. }
Qed.
(* The lemmas [pcbv_apply] and [pcbv_reify] are preliminaries for the
"magic step" lemma. *)
Lemma pcbv_apply:
forall c1 c2,
similar c1 c2 ->
forall v,
pcbv (apply c1 (cpsv v)) (apply c2 (cpsv v)).
Proof.
inversion 1; subst; intros; [ destruct c2 |]; simpl.
(* Case: both [c1] and [c2] are an object-level continuation [k].
No computation step is taken. *)
{ eapply red_refl; obvious. }
(* Case: [c1] is a two-level eta-expansion of [c2], which is a
meta-level continuation [K]. One beta-reduction step is taken. *)
{ eapply pcbv_RedBetaV; obvious. }
(* Case: [c1] and [c2] are similar meta-level continuations. The
required reduction steps are provided directly by the similarity
hypothesis. *)
{ eapply red_subst; obvious. }
Qed.
Lemma pcbv_reify:
forall c1 c2,
similar c1 c2 ->
pcbv (reify c1) (reify c2).
Proof.
inversion 1; subst; intros; [ destruct c2 |]; simpl.
(* Case: both [c1] and [c2] are an object-level continuation [k].
No computation step is taken. *)
{ eapply red_refl; obvious. }
(* Case: [c1] is a two-level eta-expansion of [c2], which is a
meta-level continuation [K]. No computation step is taken. *)
{ eapply red_refl; obvious. }
(* Case: [c1] and [c2] are similar meta-level continuations. The
required reduction steps are provided directly by the similarity
hypothesis, applied under a lambda-abstraction. *)
{ eapply RedLam; obvious. }
(* We could arrange to just write [obvious] in each of the above
cases and finish the entire proof in one line, but we prefer to
explicitly show what happens in each case. *)
Qed.
Local Hint Resolve red_refl : obvious.
(* The "magic step" lemma. *)
Lemma pcbv_cps:
forall t c1 c2,
similar c1 c2 ->
pcbv (cps t c1) (cps t c2).
Proof.
(* The proof is by induction on the size of [t]. *)
size_induction. intros c1 c2 Hsimilar.
value_or_app_or_let t; cps.
(* Case: [t] is a value. *)
{ eauto using pcbv_apply. }
(* Case: [t] is an application. *)
{ eapply IH; [ size | econstructor ].
eapply IH; [ size | econstructor ].
eapply RedAppLR; obvious.
eapply red_subst; obvious.
eauto using pcbv_reify. }
(* Case: [t] is a [let] construct. *)
{ eapply IH; [ size | econstructor ].
eapply RedLetLR; obvious.
eapply IH; [ size |].
eauto using similar_liftc_liftc. }
Qed.
(* The small-step simulation theorem: if [t1] reduces to [t2], then [cps t1 c]
reduces to [cps t2 c] via at least one step of [cbv], followed with one
step of [pcbv]. *)
(* Although the reduction strategies [cbv] and [pcbv] allow reduction in the
left-hand side of applications, at an arbitrary depth, in reality the CPS
transformation exploits this only at depth 0 or 1. We do not formally
establish this result (but could, if desired). *)
Notation plus_cbv_pcbv :=
(composition (plus cbv) pcbv).
Lemma cps_simulation:
forall t1 t2,
cbv t1 t2 ->
forall c,
is_value (reify c) ->
plus_cbv_pcbv
(cps t1 c)
(cps t2 c).
Proof.
induction 1; intros; subst; try solve [ tauto ].
(* Beta-reduction. *)
{ rewrite cps_app_value_value by eauto. cpsv.
(* We are looking at two beda redexes. Perform exactly two steps of [cbv]. *)
eexists. split; [ eapply plus_left; [ obvious | eapply star_step; [ obvious | eapply star_refl ]] |].
(* There remains one step of [pcbv]. *)
rewrite cps_substitution_1_O_Var_0 by eauto.
rewrite lift_up by tc.
rewrite cps_kubstitution_0. asimpl.
eapply pcbv_cps. econstructor.
}
(* Let *)
{ rewrite cps_let_value by eauto.
(* We are looking at a let-redex. Perform exactly one step of [cbv]. *)
eexists. split; [ eapply plus_left; [ obvious | eapply star_refl ] |].
(* There remains a trivial (reflexive) step of [pcbv]. *)
rewrite cps_substitution_0 by eauto.
eapply red_refl; obvious.
}
(* Reduction in the left-hand side of an application. *)
{ cps. eapply IHred. eauto. }
(* Reduction in the right-hand side of an application. *)
{ rewrite !cps_app_value by eauto. eapply IHred. tauto. }
(* Reduction in the left-hand side of [Let]. *)
{ cps. eapply IHred. tauto. }
Qed.
(* We now specialize the above result to the identity continuation and
state it as a commutative diagram. *)
Lemma cps_init_simulation:
let sim t t' := (cps t init = t') in
diamond22
cbv sim
plus_cbv_pcbv sim.
Proof.
assert (is_value (reify init)). { simpl. eauto. }
unfold diamond22. intros. subst. eauto using cps_simulation.
Qed.

137
coq/CPSSimulationWithoutLet.v Normal file
View file

@ -0,0 +1,137 @@
Require Import MyTactics.
Require Import Sequences.
Require Import Relations.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusValues.
Require Import LambdaCalculusReduction.
Require Import CPSDefinition.
Require Import CPSContextSubstitution.
Require Import CPSRenaming.
Require Import CPSSubstitution.
Require Import CPSKubstitution.
Require Import CPSSpecialCases.
(* This file is a simplified copy of [CPSSimulation]. Here, we consider how
the proof of the simulation lemma is simplified in the absence of a [Let]
construct. We simply pretend that this construct does not exist, and skip
the proof cases where it appears. *)
(* -------------------------------------------------------------------------- *)
(* The definition of similarity of continuations boils down to just one rule:
[O (reify c)] is similar to [c]. *)
Inductive similar : continuation -> continuation -> Prop :=
| SimilarReify:
forall c,
similar (O (reify c)) c.
(* -------------------------------------------------------------------------- *)
(* The lemma [pcbv_apply] is simplified: its conclusion uses [star cbv] instead
of [pcbv]. In fact, zero or one step of reduction is needed. *)
Lemma pcbv_apply:
forall c1 c2,
similar c1 c2 ->
forall v,
star cbv (apply c1 (cpsv v)) (apply c2 (cpsv v)).
Proof.
inversion 1; subst; intros; destruct c2; simpl.
(* Case: both [c1] and [c2] are an object-level continuation [k].
No computation step is taken. *)
{ eauto with sequences. }
(* Case: [c1] is a two-level eta-expansion of [c2], which is a
meta-level continuation [K]. One beta-reduction step is taken. *)
{ eauto with sequences obvious. }
Qed.
(* The lemma [pcbv_reify] is simplified: its conclusion becomes an equality. *)
Lemma pcbv_reify:
forall c1 c2,
similar c1 c2 ->
reify c1 = reify c2.
Proof.
inversion 1; subst; intros; destruct c2; simpl; reflexivity.
Qed.
(* -------------------------------------------------------------------------- *)
(* The "magic step" lemma is simplified: its conclusion uses [star cbv] instead
of [pcbv]. In fact, zero or one step of reduction is needed. The magic lies
in the case of applications, where [pcbv_reify] is used. *)
Lemma pcbv_cps:
forall t c1 c2,
similar c1 c2 ->
star cbv (cps t c1) (cps t c2).
Proof.
(* The proof does NOT require an induction. *)
intros t c1 c2 Hsimilar.
value_or_app_or_let t; cps.
(* Case: [t] is a value. *)
{ eauto using pcbv_apply. }
(* It turns out by magic that this proof case is trivial: it suffices to
take zero reduction steps. (That took me an evening to find out.) Thus,
no induction hypothesis is needed! *)
{ erewrite pcbv_reify by eauto.
eauto with sequences. }
(* Case: [t] is a [let] construct. We pretend this case is not there. *)
{ admit. }
Admitted. (* normal *)
(* -------------------------------------------------------------------------- *)
(* The small-step simulation theorem: if [t1] reduces to [t2], then [cps t1 c]
reduces to [cps t2 c] via at least one step of [cbv]. (In fact, two or three
steps are required.) *)
Lemma cps_simulation:
forall t1 t2,
cbv t1 t2 ->
forall c,
is_value (reify c) ->
plus cbv
(cps t1 c)
(cps t2 c).
Proof.
induction 1; intros; subst; try solve [ tauto ].
(* Beta-reduction. *)
{ rewrite cps_app_value_value by eauto. cpsv.
(* We are looking at two beda redexes. Perform exactly two steps of [cbv]. *)
eapply plus_left. obvious.
eapply star_step. obvious.
(* Push the inner substitution (the actual argument) into [cps]. *)
rewrite cps_substitution_1_O_Var_0 by eauto.
rewrite lift_up by tc.
(* Push the outer substitution (the continuation) into [cps]. *)
rewrite cps_kubstitution_0.
asimpl.
(* Conclude. *)
eapply pcbv_cps. econstructor.
}
(* Let. We pretend this case is not there. *)
{ admit. }
(* Reduction in the left-hand side of an application. *)
{ cps. eapply IHred. eauto. }
(* Reduction in the right-hand side of an application. *)
{ rewrite !cps_app_value by eauto. eapply IHred. tauto. }
(* Reduction in the left-hand side of [Let]. We pretend this case is not there. *)
{ admit. }
Admitted. (* normal *)
(* -------------------------------------------------------------------------- *)
(* We now specialize the above result to the identity continuation and
state it as a commutative diagram. *)
Lemma cps_init_simulation:
let sim t t' := (cps t init = t') in
diamond22
cbv sim
(plus cbv) sim.
Proof.
assert (is_value (reify init)). { simpl. eauto. }
unfold diamond22. intros. subst. eauto using cps_simulation.
Qed.

48
coq/CPSSpecialCases.v Normal file
View file

@ -0,0 +1,48 @@
Require Import MyTactics.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusValues.
Require Import CPSDefinition.
Require Import CPSContextSubstitution.
Require Import CPSKubstitution.
(* The translation of an application whose left-hand side is a value. *)
Lemma cps_app_value:
forall v1 t2 c,
is_value v1 ->
cps (App v1 t2) c =
cps t2 (M (App (App (lift 1 (cpsv v1)) (Var 0)) (lift 1 (reify c)))).
Proof.
intros. cps. simpl.
rewrite cps_kubstitution_0. asimpl.
reflexivity.
Qed.
(* The translation of a value-value application. *)
Lemma cps_app_value_value:
forall v1 v2 c,
is_value v1 ->
is_value v2 ->
cps (App v1 v2) c =
App (App (cpsv v1) (cpsv v2)) (reify c).
Proof.
intros.
rewrite cps_app_value by obvious.
rewrite cps_value by eauto. asimpl.
reflexivity.
Qed.
(* The translation of a [Let] construct whose left-hand side is a value. *)
Lemma cps_let_value:
forall v1 t2 c,
is_value v1 ->
cps (Let v1 t2) c =
Let (cpsv v1) (cps t2 (liftc 1 c)).
Proof.
intros. cps. simpl. f_equal.
eapply cps_kubstitution. (* [cps_substitution] could be used too *)
{ autosubst. }
{ rewrite substc_substc. autosubst. }
Qed.

149
coq/CPSSubstitution.v Normal file
View file

@ -0,0 +1,149 @@
Require Import MyTactics.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusValues.
Require Import CPSDefinition.
Require Import CPSContextSubstitution.
Require Import CPSRenaming.
(* The CPS transformation commutes with certain substitutions. More precisely,
it commutes with a substitution [sigma] of values for variables, up to a
transformation of the values in the codomain of [sigma].
In the case of [cpsv], we have the following diagram: applying [sigma]
first, followed with [cpsv], is the same as applying [cpsv] first, followed
with [sigma >>> cpsv].
cpsv v.[sigma] = (cpsv v).[sigma >>> cpsv]
This can also be written in point-free style, that is, without mentioning
the value [v]:
subst sigma >>> cpsv = cpsv >>> subst (sigma >>> cpsv)
As in the case of the renaming lemma (see CPSRenaming.v), this statement is
proved by induction on the size of terms, together with an analogous
statement about the function [cps]. *)
(* The proof depends on [CPSRenaming] via the lemmas [up_sigma_cpsv] and
[upn_sigma_cpsv], which are declared as hints for [obvious]. *)
Lemma substitution:
(
forall v sigma sigma',
sigma' = sigma >>> cpsv ->
is_value_subst sigma ->
(cpsv v).[sigma'] = cpsv v.[sigma]
) /\ (
forall t c sigma c' sigma',
sigma' = sigma >>> cpsv ->
is_value_subst sigma ->
substc sigma' c = c' ->
(cps t c).[sigma'] = cps t.[sigma] c'
).
Proof.
eapply mutual_induction.
(* [cpsv] *)
{ intros n IHcps v Hvn sigma sigma' Heq Hsigma. subst.
destruct v; asimpl; cpsv; asimpl; try reflexivity.
(* Lam *)
{ erewrite IHcps by obvious. asimpl. reflexivity. }
}
(* [cps] *)
{ intros n IHcpsv IHcps t c Htn sigma c' sigma' Heq Hsigma Hsubstc. subst.
value_or_app_or_let t; asimpl; cps.
(* Case: [t] is a value. *)
{ erewrite apply_substitution by eauto.
erewrite IHcpsv by obvious.
reflexivity. }
(* Case: [t] is an application. *)
{ eapply IHcps; obvious.
simpl. f_equal.
erewrite <- lift_up by tc.
eapply IHcps; obvious.
asimpl. do 2 f_equal.
rewrite lift_reify.
eapply reify_substitution.
rewrite substc_substc.
reflexivity. }
(* Case: [t] is a [let] construct. *)
{ eapply IHcps; obvious.
simpl.
rewrite fold_up_up.
do 2 f_equal.
erewrite IHcps by first [ eapply substc_liftc_liftc; eauto | obvious ].
autosubst. }
}
Qed.
(* The projections of the above result. *)
Definition cpsv_substitution := proj1 substitution.
Definition cps_substitution := proj2 substitution.
(* A point-free reformulation of the above result: [cpsv] commutes with an
arbitrary substitution [sigma], up to a transformation of the values in the
codomain of [sigma]. *)
Goal
forall sigma,
is_value_subst sigma ->
cpsv >>> subst (sigma >>> cpsv) =
subst sigma >>> cpsv.
Proof.
intros. f_ext; intros v. asimpl. eauto using cpsv_substitution.
Qed.
(* This technical lemma is used below. *)
Lemma cpsv_cons:
forall v,
cpsv v .: ids = (v .: ids) >>> cpsv.
Proof.
intros. f_ext; intros [|x]; autosubst.
Qed.
(* A corollary where the substitution [sigma] is [v .: ids], that is, a
substitution of the value [v] for the variable 0. This one is about
[cpsv]. *)
Lemma cpsv_substitution_0:
forall v w,
is_value v ->
(cpsv w).[cpsv v/] =
cpsv w.[v/].
Proof.
intros. rewrite cpsv_cons. erewrite cpsv_substitution by obvious. reflexivity.
Qed.
(* Another corollary where the substitution [sigma] is [v .: ids], that is, a
substitution of the value [v] for the variable 0. This one is about [cps]
and concerns the case where the continuation is of the form [liftc 1 c], so
it is unaffected. *)
Lemma cps_substitution_0:
forall t c v,
is_value v ->
(cps t (liftc 1 c)).[cpsv v/] =
cps t.[v/] c.
Proof.
intros. eapply cps_substitution.
{ autosubst. }
{ obvious. }
{ eauto using substc_liftc_single. }
Qed.
(* A corollary where the substitution [sigma] is [up (v .: ids)], that is, a
substitution of the value [v] for the variable 1, and the continuation is
the variable 0, so it is unaffected. *)
Lemma cps_substitution_1_O_Var_0:
forall t v,
is_value v ->
(cps t (O (Var 0))).[up (cpsv v .: ids)] =
cps t.[up (v .: ids)] (O (Var 0)).
Proof.
intros. eapply cps_substitution.
{ rewrite cpsv_cons. obvious. }
{ obvious. }
{ reflexivity. }
Qed.

349
coq/ClosureConversion.v Normal file
View file

@ -0,0 +1,349 @@
Require Import List.
Require Import MyList.
Require Import MyTactics.
Require Import Sequences.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusFreeVars.
Require Import LambdaCalculusValues.
Require Import LambdaCalculusBigStep.
Require Import MetalSyntax.
Require Import MetalBigStep.
(* This file contains a definition of closure conversion and a proof of
semantic preservation. Closure conversion is a transformation of the
lambda-calculus into a lower-level calculus, nicknamed Metal, where
lambda-abstractions must be closed. *)
(* The definition is slightly painful because we are using de Bruijn indices.
(That said, it is likely that using named variables would be painful too,
just in other ways.) One important pattern that we follow is that, as soon
as a variable [x] is no longer useful, we use [eos x _] to make it go out
of scope. Following this pattern is not just convenient -- it is actually
necessary. *)
(* The main transformation function, [cc], has type [nat -> term -> metal]. If
[t] is a source term with [n] free variables, then [cc n t] is its image
under the transformation. *)
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* The auxiliary function [cc_lam n cct] defines the transformation of
the body of a lambda-abstraction. This auxiliary function must be isolated
because it is used twice, once within [cc], and once within [cc_value]. *)
(* The parameter [n] is supposed to be the number of free variables of the
lambda-abstraction, and the parameter [cct] is the body of the transformed
lambda-abstraction. That is, [cct] is expected to be later instantiated
with [cc (n + 1) t], where [t] is the body of the source
lambda-abstraction. *)
(* The term [cc_lam n cct] has just one free variable, namely 0, which
represents the formal parameter of the transformed lambda-abstraction. This
parameter is expected to be a pair [(clo, x)], where [clo] is the closure
and [x] is the formal parameter of the source lambda-abstraction. *)
(* In nominal / informal syntax, the code would be roughly:
let (clo, x) = _ in
let x_1, ..., x_n = pi_1 clo, ..., pi_n clo in
cct
*)
(* We use meta-level [let] bindings, such as [let clo_x := 0 in ...].
These bindings generate no Metal code -- they should not be confused
with Metal [MLet] bindings. They are just a notational convenience. *)
Definition cc_lam (n : nat) (cct : metal) : metal :=
(* Let us refer to variable 0 as [clo_x]. *)
let clo_x := 0 in
(* Initially, the variable [clo_x] is bound to a pair of [clo] and [x].
Decompose this pair, then let [clo_x] go out of scope. *)
MLetPair (* clo, x *) (MVar clo_x) (
let clo_x := clo_x + 2 in
eos clo_x (
(* Two variables are now in scope, namely [clo] and [x]. *)
let clo := 1 in
let x := 0 in
(* Now, bind [n] variables, informally referred to as [x_1, ..., x_n],
to the [n] tuple projections [pi_1 clo, ..., pi_n clo]. Then, let
[clo] go out of scope, as it is no longer needed. *)
MMultiLet 0 (MProjs n (MVar clo)) (
let clo := n + clo in
let x := n + x in
eos clo (
(* We need [x] to correspond to de Bruijn index 0. Currently, this is
not the case. So, rebind a new variable to [x], and let the old [x]
go out of scope. (Yes, this is a bit subtle.) We use an explicit
[MLet] binding, but in principle, could also use a substitution. *)
MLet (MVar x) (
let x := 1 + x in
eos x (
(* We are finally ready to enter the transformed function body. *)
cct
)))))).
(* [cc] is the main transformation function. *)
Fixpoint cc (n : nat) (t : term) : metal :=
match t with
| Var x =>
(* A variable is mapped to a variable. *)
MVar x
| Lam t =>
(* A lambda-abstraction [Lam t] is mapped to a closure, that is, a tuple
whose 0-th component is a piece of code (a closed lambda-abstraction)
and whose remaining [n] components are the [n] variables numbered 0,
1, ..., n-1. *)
MTuple (
MLam (cc_lam n (cc (n + 1) t)) ::
MVars n
)
| App t1 t2 =>
(* A function application is transformed into a closure invocation. *)
(* Bind [clo] to the closure produced by the (transformed) term [t1]. *)
MLet (cc n t1) (
let clo := 0 in
(* Bind [code] to the 0-th component of this closure. *)
MLet (MProj 0 (MVar clo)) (
let clo := 1 + clo in
let code := 0 in
(* Apply the function [code] to a pair of the closure and the value
produced by the (transformed) term [t2]. Note that both [clo] and
[code] must go out of scope before referring to [t2]. This could
be done in one step by applying the renaming [(+2)], but we prefer
to explicitly use [eos] twice, for greater clarity. *)
MApp
(MVar code)
(MPair
(MVar clo)
(eos clo (eos code (cc n t2)))
)
))
| Let t1 t2 =>
(* A local definition is translated to a local definition. *)
MLet (cc n t1) (cc (n + 1) t2)
end.
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* In order to prove that the above program transformation is sound (that is,
semantics-preserving), we must relate the values computed by the source
program with the values computed by the target program. Fortunately, the
relation is simple. (It is, in fact, a function.) The image of a source
closure [Clo t e] under the translation is a closure, represented as a
tuple, whose 0-th component is a lambda-abstraction -- the translation
of [Lam t] -- and whose remaining [n] components are the translation of
the environment [e]. *)
Fixpoint cc_cvalue (cv : cvalue) : mvalue :=
match cv with
| Clo t e =>
let n := length e in
MVTuple (
MVLam (cc_lam n (cc (n + 1) t)) ::
map cc_cvalue e
)
end.
(* The translation of environments is defined pointwise. *)
Definition cc_cenv e :=
map cc_cvalue e.
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* This lemma and hint increase the power of the tactic [length]. *)
Lemma length_cc_env:
forall e,
length (cc_cenv e) = length e.
Proof.
intros. unfold cc_cenv. length.
Qed.
Hint Rewrite length_cc_env : length.
(* In this file, we allow [eauto with omega] to use the tactic [length]. *)
Local Hint Extern 1 (_ = _ :> nat) => length : omega.
Local Hint Extern 1 (lt _ _) => length : omega.
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* We now check two purely syntactic properties of the transformation. First,
if the source program [t] has [n] free variables, then the transformed
program [cc n t] has [n] free variables, too. Second, in the transformed
program, every lambda-abstraction is closed. *)
(* These proofs are "easy" and "routine", but could have been fairly lengthy
and painful if we had not set up appropriate lemmas and tactics, such as
[fv], beforehand. *)
Lemma fv_cc_lam:
forall m n t,
fv (S n) t ->
1 <= m ->
fv m (cc_lam n t).
Proof.
intros. unfold cc_lam. fv; length. repeat split;
eauto using fv_monotonic with omega.
{ eapply fv_MProjs. fv. omega. }
Qed.
Lemma fv_cc:
forall t n1 n2,
fv n2 t ->
n1 = n2 ->
fv n1 (cc n2 t).
Proof.
induction t; intros; subst; simpl; fv; unpack;
repeat rewrite Nat.add_1_r in *;
repeat split; eauto using fv_monotonic, fv_cc_lam with omega.
Qed.
(* -------------------------------------------------------------------------- *)
(* The following lemmas help reorganize our view of the environment. They are
typically used just before applying the lemma [mbigcbv_eos], that is, when
a variable [x] is about to go out of scope. We then want to organize the
environment so that it has the shape [e1 ++ mv :: e2], where the length of
[e1] is [x], so [mv] is the value that is dropped, and the environment
afterwards is [e1 ++ e2]. *)
Local Lemma access_1:
forall {A} xs (x0 x : A),
x0 :: x :: xs = (x0 :: nil) ++ x :: xs.
Proof.
reflexivity.
Qed.
Local Lemma access_2:
forall {A} xs (x0 x1 x : A),
x0 :: x1 :: x :: xs = (x0 :: x1 :: nil) ++ x :: xs.
Proof.
reflexivity.
Qed.
Local Lemma access_n_plus_1:
forall {A} xs (x : A) ys,
xs ++ x :: ys = (xs ++ x :: nil) ++ ys.
Proof.
intros. rewrite <- app_assoc. reflexivity.
Qed.
(* -------------------------------------------------------------------------- *)
(* We now establish a (forward) semantic preservation statement: if under
environment [e] the source term [t] computes the value [cv], then under
the translation of [e], the translation of [t] computes the translation
of [cv]. *)
(* The proof is fairly routine and uninteresting; it is just a matter of
checking that everything works as expected. A crucial point that helps
keep the proof manageable is that we have defined auxiliary evaluation
lemmas for tuples, projections, [MMultiLet], and so on. *)
(* Although the proof is not "hard", it would be difficult to do by hand, as
it is quite deep and one must keep track of many details, such as the shape
of the runtime environment at every program point -- that is, which de
Bruijn index is bound to which value. An off-by-one error in a de Bruijn
index, or a list that is mistakenly reversed, would be difficult to detect
in a handwritten proof. Machine assistance is valuable in this kind of
exercise. *)
Theorem semantic_preservation:
forall e t cv,
ebigcbv e t cv ->
forall n,
n = length e ->
mbigcbv (cc_cenv e) (cc n t) (cc_cvalue cv).
Proof.
induction 1; intros; simpl.
(* Case: [Var]. Nothing much to say; apply the evaluation rule and
check that its side conditions hold. *)
{ econstructor.
{ length. }
{ subst cv.
erewrite (nth_indep (cc_cenv e)) by length.
unfold cc_cenv. rewrite map_nth. eauto. }
}
(* Case: [Lam]. We have to check that a transformed lambda-abstraction
(as per [cc]) evaluates to a transformed closure (as per [cc_value]).
This is fairly easy. *)
{ subst. econstructor.
(* The code component. We must check that it is closed. *)
{ econstructor.
assert (fv (length e + 1) t).
{ eapply (use_fv_length_cons _ dummy_cvalue); eauto. }
unfold closed. fv. eauto using fv_cc_lam, fv_cc with omega. }
(* The remaining components. *)
{ eapply MBigcbvTuple.
rewrite <- length_cc_env. eauto using MBigcbvVars. }
}
(* Case: [App]. This is where most of the action takes place. We must
essentially "execute" the calling sequence and check that it works
as expected. *)
{ (* Evaluate the first [Let], which binds a variable [clo] to the closure. *)
econstructor. { eauto. }
(* Evaluate the second [Let], which projects the code out of the closure,
and binds the variable [code]. *)
econstructor.
{ econstructor; [| eauto ].
econstructor; simpl; eauto with omega. }
(* We are now looking at a function application. Evaluate in turn the function,
its actual argument, and the call itself. *)
econstructor.
(* The function. *)
{ econstructor; simpl; eauto with omega. }
(* Its argument. *)
{ econstructor.
{ econstructor; simpl; eauto with omega. }
{ (* Skip two [eos] constructs. *)
rewrite access_1. eapply mbigcbv_eos; [ simpl | length ].
eapply mbigcbv_eos with (e1 := nil); [ simpl | length ].
eauto. }
}
(* The call itself. Here, we step into a transformed lambda-abstraction, and
we begin studying how it behaves when executed. *)
unfold cc_lam at 2.
(* Evaluate [MLetPair], which binds [clo] and [x]. *)
eapply MBigcbvLetPair.
{ econstructor; simpl; eauto with omega. }
(* Skip [eos]. *)
rewrite access_2. eapply mbigcbv_eos; [ simpl | eauto ].
(* Evaluate [MMultiLet]. *)
eapply MBigcbvMultiLetProjs.
{ econstructor; simpl; eauto with omega. }
{ length. }
(* Skip [eos]. *)
rewrite access_n_plus_1. eapply mbigcbv_eos; [| length ].
rewrite app_nil_r, Nat.add_0_r.
(* Evaluate the new binding of [x]. *)
econstructor.
{ econstructor.
{ length. }
{ rewrite app_nth by (rewrite map_length; omega). simpl. eauto. }
}
(* Skip [eos]. *)
rewrite app_comm_cons. eapply mbigcbv_eos; [ rewrite app_nil_r | length ].
(* Evaluate the function body. *)
eauto with omega. }
(* Case: [Let]. Immediate. *)
{ econstructor; eauto with omega. }
Qed.

73
coq/DemoEqReasoning.v Normal file
View file

@ -0,0 +1,73 @@
Require Import List.
Section Demo.
(* -------------------------------------------------------------------------- *)
Variables A B : Type.
Variable p : B -> bool.
Variable f : A -> B.
(* The composition of [filter] and [map] can be computed by the specialized
function [filter_map]. *)
Fixpoint filter_map xs :=
match xs with
| nil =>
nil
| cons x xs =>
let y := f x in
if p y then y :: filter_map xs else filter_map xs
end.
Lemma filter_map_spec:
forall xs,
filter p (map f xs) = filter_map xs.
Proof.
induction xs as [| x xs ]; simpl.
{ reflexivity. }
{ rewrite IHxs. reflexivity. }
Qed.
(* -------------------------------------------------------------------------- *)
(* [filter] and [map] commute in a certain sense. *)
Variable q : A -> bool.
Lemma filter_map_commute:
(forall x, p (f x) = q x) ->
forall xs,
filter p (map f xs) = map f (filter q xs).
Proof.
intros h.
induction xs as [| x xs ]; simpl; intros.
(* Case: [nil]. *)
{ reflexivity. }
(* Case: [x :: xs]. *)
{ rewrite h.
rewrite IHxs.
(* Case analysis: [q x] is either true or false.
In either case, the result is immediate. *)
destruct (q x); reflexivity. }
Qed.
(* In a slightly stronger version of the lemma, the equality [p (f x) = q x]
needs to be proved only under the hypothesis that [x] is an element of the
list [xs]. *)
Lemma filter_map_commute_stronger:
forall xs,
(forall x, In x xs -> p (f x) = q x) ->
filter p (map f xs) = map f (filter q xs).
Proof.
induction xs as [| x xs ]; simpl; intro h.
{ reflexivity. }
{ (* The proof is the same as above, except the two rewriting steps have
side conditions, which are immediately proved by [eauto]. *)
rewrite h by eauto.
rewrite IHxs by eauto.
destruct (q x); reflexivity. }
Qed.
End Demo.

250
coq/DemoSyntaxReduction.v Normal file
View file

@ -0,0 +1,250 @@
Require Import Autosubst.Autosubst.
(* This file is intended as a mini-demonstration of:
1. defining the syntax of a calculus, in de Bruijn's representation;
2. equipping it with an operational semantics;
3. proving a basic lemma, e.g.,
stability of the semantics under substitution. *)
(* -------------------------------------------------------------------------- *)
(* The syntax of the lambda-calculus. *)
Inductive term :=
| Var: var -> term
| Lam: {bind term} -> term
| App: term -> term -> term
.
(* -------------------------------------------------------------------------- *)
(* The following incantations let [AutoSubst] work its magic for us.
We obtain, for free, the operations of de Bruijn algebra: application
of a substitution to a term, composition of substitutions, etc. *)
Instance Ids_term : Ids term. derive. Defined.
Instance Rename_term : Rename term. derive. Defined.
Instance Subst_term : Subst term. derive. Defined.
Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
(* -------------------------------------------------------------------------- *)
(* A demo of the tactics [autosubst] and [asimpl]. *)
Goal
forall sigma,
(Lam (App (Var 0) (Var 1))).[sigma] =
Lam (App (Var 0) (sigma 0).[ren (+1)]).
Proof.
intros.
(* The tactic [autosubst] proves this equality. *)
autosubst.
Restart.
intros.
(* If desired, we can first simplify this equality using [asimpl]. *)
asimpl.
(* [ids], the identity substitution, maps 0 to [Var 0], 1 to [Var 1],
and so on, so it is really equal to [Var] itself. As a result, the
built-in tactic [reflexivity] proves this simplified equation. *)
reflexivity.
Qed.
(* -------------------------------------------------------------------------- *)
(* More demos: let us check that the laws of substitution are satisfied. *)
Lemma subst_var:
forall x sigma,
(Var x).[sigma] = sigma x.
Proof.
autosubst.
Qed.
Lemma subst_lam:
forall t sigma,
(Lam t).[sigma] = Lam (t.[up sigma]).
Proof.
autosubst.
Qed.
Lemma subst_app:
forall t1 t2 sigma,
(App t1 t2).[sigma] = App t1.[sigma] t2.[sigma].
Proof.
autosubst.
Qed.
(* A reminder of the meaning of [up sigma]. *)
Lemma up_def:
forall sigma,
up sigma = Var 0 .: (sigma >> ren (+1)).
Proof.
intros. autosubst.
Qed.
(* -------------------------------------------------------------------------- *)
(* A small-step reduction semantics. *)
(* This is a relation between terms: hence, its type is [term -> term -> Prop].
It is inductively defined by three inference rules, as follows: *)
Inductive red : term -> term -> Prop :=
(* Beta-reduction. The use of an explicit equality hypothesis is a technical
convenience. We could instead write [red (App (Lam t1) t2) t1.[t2/]] in
the conclusion, and remove the auxiliary variable [u], but that would make
it more difficult for Coq to apply the inference rule [RedBeta]. Using an
explicit equality premise makes the rule more widely applicable. Of course
the user still has to prove (after applying the rule) that the equality
holds. *)
| RedBeta:
forall t1 t2 u,
t1.[t2/] = u ->
red (App (Lam t1) t2) u
(* Reduction in the left-hand side of an application. *)
| RedAppL:
forall t1 t2 u,
red t1 t2 ->
red (App t1 u) (App t2 u)
(* Reduction in the right-hand side of an application. *)
| RedAppR:
forall t u1 u2,
red u1 u2 ->
red (App t u1) (App t u2)
.
(* The following means that [eauto with red] is allowed to apply the above
three inference rules. *)
Hint Constructors red : red.
(* No strategy is built into this reduction relation: it is not restricted to
call-by-value or call-by-name. It is nondeterministic. Only weak reduction
is permitted here: we have not allowed reduction under a [Lam]. These choices
are arbitrary: this is just a demo anyway. *)
(* -------------------------------------------------------------------------- *)
(* This incantation means that [eauto with autosubst] can use the tactic
[autosubst] to prove an equality. It is used in the last "expert" proof
of the lemma [red_subst] below. *)
Hint Extern 1 (_ = _) => autosubst : autosubst.
(* -------------------------------------------------------------------------- *)
(* Demo: a term that reduces to itself. *)
Definition Delta :=
Lam (App (Var 0) (Var 0)).
Definition Omega :=
App Delta Delta.
Goal
red Omega Omega.
Proof.
(* Apply the beta-reduction rule.
(This forces Coq to unfold the left-hand [Omega].) *)
eapply RedBeta.
(* Check this equality. *)
asimpl. (* optional *)
reflexivity.
Qed.
(* -------------------------------------------------------------------------- *)
(* Let us prove that the semantics is stable under arbitrary substitutions. *)
Lemma red_subst:
forall t1 t2,
red t1 t2 ->
forall sigma,
red t1.[sigma] t2.[sigma].
Proof.
(* We attack a proof by induction on the derivation of [red t1 t2]. *)
induction 1; intros.
(* Case: [RedBeta]. *)
{ subst u.
eapply RedBeta.
(* Wow -- we have to prove a complicated-looking commutation property
of substitutions. Fortunately, [autosubst] is here for us! *)
autosubst. }
(* Case: [RedAppL]. The proof can be done slowly, in three steps:
1. push the substitution into [App];
2. apply the rule [RedAppL]; a simpler subgoal remains to be proved;
3. apply the induction hypothesis, which proves this subgoal. *)
{ asimpl.
eapply RedAppL.
eapply IHred. }
(* Case: [RedAppR]. The proof could be done using the same three steps
as above, but one can also let the last two steps be automatically
found by [eauto]. *)
{ asimpl. eauto using red. }
(* The proof is now finished. *)
(* For the fun of it, let us do the proof again in a more "expert" style. *)
Restart.
(* The proof is still by induction. All three cases begin in the same way,
so this common pattern can be shared, as follows. We use the semicolon
which in Ltac has special meaning: when one writes [command1; command2],
[command1] can produce multiple subgoals, and [command2] is applied to
every subgoal (in parallel). Thus, here, in each of the three cases,
we perform the sequence of commands [intros; subst; asimpl; econstructor].
The effect of [econstructor] is to apply one of [RedBeta], [RedAppL] and
[RedAppR] -- whichever is applicable. *)
induction 1; intros; subst; asimpl; econstructor.
(* Then, the three subgoals can be finished as follows: *)
{ autosubst. }
{ eauto. }
{ eauto. }
(* The proof is now finished (again). *)
(* For the fun of it, let us redo the proof in an even more expert style.
We remark that each of the three subgoals can be proved by [eauto with
autosubst], so we can write a fully shared command, where the subgoals
are no longer distinguished: *)
Restart.
induction 1; intros; subst; asimpl; econstructor; eauto with autosubst.
(* The proof is now finished (yet again). *)
(* There are several lessons that one can draw from this demo:
1. The machine helps us by keeping track of what we may assume
and what we have to prove.
2. There are several ways in which a proof can be written. In the
beginning, it is advisable to write a step-by-step, simple-minded
proof; later on, when the proof is finished and well-understood,
it can be revisited for greater compactness and sharing.
3. The proof of this lemma *can* fit in one line. On paper, one
would say that the proof is "by induction" and "immediate".
Here, we are able to be almost as concise, yet we have much
greater confidence.
4. The point of the "expert" proof is not just to make the proof
more concise: the point is also to make the proof more robust
in the face of future evolution. For instance, as an EXERCISE,
extend the calculus with pairs and projections, and see how the
proof scripts must be extended. You should find that the last
"expert" proof above requires no change at all!
*)
Qed.
(* -------------------------------------------------------------------------- *)
(* As another EXERCISE, extend the operational semantics with a rule that
allows strong reduction, that is, reduction under a lambda-abstraction.
This exercise is more difficult; do not hesitate to ask for help or hints. *)
(* Another suggested EXERCISE: define call-by-value reduction, [cbv]. Prove
that [cbv] is a subset of [red]. Prove that values do not reduce. Prove
that [cbv] is deterministic. *)

98
coq/Even.v Normal file
View file

@ -0,0 +1,98 @@
(* 22/09/2017. Someone asked during the course whether [~ (even 1)] can be
proved, and if so, how. Here are several solutions, courtesy of
Pierre-Evariste Dagand. *)
Inductive even: nat -> Prop :=
| even_O:
even 0
| even_SS:
forall n, even n -> even (S (S n)).
(* 1. The shortest proof uses the tactic [inversion] to deconstruct the
hypothesis [even 1], that is, to perform case analysis. The tactic
automatically finds that this case is impossible, so the proof is
finished. *)
Lemma even1_v1:
even 1 -> False.
Proof.
inversion 1.
(* In case you wish the see the proof term: *)
(* Show Proof. *)
Qed.
(* For most practical purposes, the above proof *script* is good enough, and
is most concise. However, those who wish to understand what they are doing
may prefer to write a proof *term* by hand, in the Calculus of Inductive
Constructions, instead of letting [inversion] construct a (possibly
needlessly complicated) proof term. *)
(* 2. Generalizing with equality. *)
Lemma even1_v2':
forall n, even n -> n = 1 -> False.
Proof.
exact (fun n t =>
match t with
| even_O =>
fun (q: 0 = 1) =>
match q with (* IMPOSSIBLE *) end
| even_SS n _ =>
fun (q : S (S n) = 1) =>
match q with (* IMPOSSIBLE *) end
end
).
Qed.
Lemma even1_v2:
even 1 -> False.
Proof.
eauto using even1_v2'.
Qed.
(* 3. Type-theoretically, through a large elimination. *)
Lemma even1_v3':
forall n,
even n ->
match n with
| 0 => True
| 1 => False
| S (S _) => True
end.
Proof.
exact (fun n t =>
match t with
| even_O => I
| even_SS _ _ => I
end
).
Qed.
Lemma even1_v3:
even 1 -> False.
Proof.
apply even1_v3'.
Qed.
(* 3'. Same technique, using a clever [match ... in ... return]. *)
Lemma even1_v4':
even 1 -> False.
Proof.
exact (fun t =>
match t in even n
return (
match n with
| 0 => True
| 1 => False
| S (S _) => True
end
(* BUG: we need the following (pointless) type annotation *)
: Prop)
with
| even_O => I
| even_SS _ _ => I
end
).
Qed.

20
coq/FixExtra.v Normal file
View file

@ -0,0 +1,20 @@
Require Import Coq.Logic.FunctionalExtensionality.
(* This is a simplified version of the lemma [Fix_eq], which is defined in
[Coq.Init.Wf]. We use functional extensionality to remove one hypothesis.
Furthermore, we introduce the auxiliary equality [f = Fix Rwf P F] so as
to avoid duplicating the (usually large) term [F] in the right-hand side
of the conclusion. *)
Lemma Fix_eq_simplified
(A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
(P : A -> Type)
(F : forall x : A, (forall y : A, R y x -> P y) -> P x)
(f : forall x, P x) :
f = Fix Rwf P F ->
forall x : A,
f x = F x (fun (y : A) (_ : R y x) => f y).
Proof.
intros. subst. eapply Fix_eq. intros. f_equal.
eauto using functional_extensionality_dep, functional_extensionality.
Qed.

532
coq/LambdaCalculusBigStep.v Normal file
View file

@ -0,0 +1,532 @@
Require Import List.
Require Import MyTactics.
Require Import Sequences.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusFreeVars.
Require Import LambdaCalculusValues.
Require Import LambdaCalculusReduction.
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* A big-step call-by-value semantics. *)
Inductive bigcbv : term -> term -> Prop :=
| BigcbvValue:
forall v,
is_value v ->
bigcbv v v
| BigcbvApp:
forall t1 t2 u1 v2 v,
bigcbv t1 (Lam u1) ->
bigcbv t2 v2 ->
bigcbv u1.[v2/] v ->
bigcbv (App t1 t2) v
| BigcbvLet:
forall t1 t2 v1 v,
bigcbv t1 v1 ->
bigcbv t2.[v1/] v ->
bigcbv (Let t1 t2) v
.
Hint Constructors bigcbv : bigcbv.
(* The tactic [invert_bigcbv] looks for a hypothesis of the form [bigcbv t v]
and inverts it. *)
Ltac invert_bigcbv :=
pick bigcbv invert;
try solve [ false; eauto 3 with obvious ].
(* -------------------------------------------------------------------------- *)
(* If [bigcbv t v] holds, then [v] must be a value. *)
Lemma bigcbv_is_value:
forall t v,
bigcbv t v ->
is_value v.
Proof.
induction 1; eauto.
Qed.
Hint Resolve bigcbv_is_value : is_value obvious.
(* -------------------------------------------------------------------------- *)
(* If [t] evaluates to [v] according to the big-step semantics,
then [t] reduces to [v] according to the small-step semantics. *)
Lemma bigcbv_star_cbv:
forall t v,
bigcbv t v ->
star cbv t v.
Proof.
(* A detailed proof: *)
induction 1.
(* BigcbvValue *)
{ eapply star_refl. }
(* BigcbvApp *)
{ eapply star_trans. obvious.
eapply star_trans. obvious.
eapply star_step. obvious.
eauto. }
(* BigcbvLet *)
{ eapply star_trans. obvious.
eapply star_step. obvious.
eauto. }
Restart.
(* A much shorter proof: *)
induction 1; eauto 6 with sequences obvious.
Qed.
(* Conversely, if [t] reduces to [v] in the small-step semantics,
then [t] evaluates to [v] in the big-step semantics. *)
Lemma cbv_bigcbv_bigcbv:
forall t1 t2,
cbv t1 t2 ->
forall v,
bigcbv t2 v ->
bigcbv t1 v.
Proof.
(* A detailed proof: *)
induction 1; intros; subst; try solve [ false; tauto ].
(* BetaV *)
{ econstructor; eauto with bigcbv. }
(* LetV *)
{ econstructor; eauto with bigcbv. }
(* AppL *)
{ invert_bigcbv. eauto with bigcbv. }
(* AppR *)
{ invert_bigcbv. eauto with bigcbv. }
(* LetL *)
{ invert_bigcbv. eauto with bigcbv. }
Restart.
(* A shorter proof: *)
induction 1; intros; subst; try solve [ false; tauto
| econstructor; eauto with bigcbv
| invert_bigcbv; eauto with bigcbv
].
Qed.
Lemma star_cbv_bigcbv:
forall t v,
star cbv t v ->
is_value v ->
bigcbv t v.
Proof.
induction 1; eauto using cbv_bigcbv_bigcbv with bigcbv.
Qed.
(* In conclusion, we have the following equivalence: *)
Lemma star_cbv_bigcbv_eq:
forall t v,
(star cbv t v /\ is_value v) <-> bigcbv t v.
Proof.
split; intros; unpack;
eauto using star_cbv_bigcbv, bigcbv_star_cbv with is_value.
Qed.
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* A big-step call-by-value semantics with explicit environments. *)
(* A closure is a pair of a term and an environment. A cvalue [cv] must be a
closure, as we have no other forms of values. An environment [e] is a list
of cvalues. *)
(* We break the mutual induction between [cvalue] and [cenv] by inlining the
definition of [cenv] into the definition of [cvalue]. *)
Inductive cvalue :=
| Clo: {bind term} -> list cvalue -> cvalue.
Definition cenv :=
list cvalue.
(* This dummy cvalue is passed below as an argument to [nth], but is really
irrelevant, as the condition [x < length e] ensures that the dummy cvalue
is never used. *)
Definition dummy_cvalue : cvalue :=
Clo (Var 0) nil.
(* The judgement [ebigcbv e t cv] means that, under the environment [e], the
term [t] evaluates to [cv]. *)
Inductive ebigcbv : cenv -> term -> cvalue -> Prop :=
| EBigcbvVar:
forall e x cv,
(* The variable [x] must be in the domain of [e]. *)
x < length e ->
(* This allows us to safely look up [e] at [x]. *)
cv = nth x e dummy_cvalue ->
ebigcbv e (Var x) cv
| EBigcbvLam:
forall e t,
(* The free variables of [t] must be less than or equal to [length e]. *)
(forall cv, fv (length (cv :: e)) t) ->
(* This allows us to build a closure that is indeed closed. *)
ebigcbv e (Lam t) (Clo t e)
| EBigcbvApp:
forall e e' t1 t2 u1 cv2 cv,
(* Evaluate [t1] to a closure, *)
ebigcbv e t1 (Clo u1 e') ->
(* evaluate [t2] to a value, *)
ebigcbv e t2 cv2 ->
(* and evaluate the function body, in a suitable environment. *)
ebigcbv (cv2 :: e') u1 cv ->
ebigcbv e (App t1 t2) cv
| EBigcbvLet:
forall e t1 t2 cv1 cv,
(* Evaluate [t1] to a value, *)
ebigcbv e t1 cv1 ->
(* and evaluate [t2] under a suitable environment. *)
ebigcbv (cv1 :: e) t2 cv ->
ebigcbv e (Let t1 t2) cv
.
Hint Constructors ebigcbv : ebigcbv.
(* -------------------------------------------------------------------------- *)
(* To explain what the above semantics means, and to prove that it is
equivalent to the big-step semantics, we first define a function that
decodes a cvalue into a value. *)
(* Ideally, the function [decode] should be defined by the equation:
decode (Clo t e) = (Lam t).[decode_cenv e]
where the auxiliary function [decode_cenv] maps [decode] over the
environment [e], and converts the result to a substitution, that
is, a function of type [term -> term]:
decode_cenv e = fun x => nth x (map decode e) (decode dummy_cvalue)
The definitions below are a bit more awkward (as Coq does not support
mutual induction very well), but mean the same thing. *)
Definition dummy_value : term :=
Lam (Var 0).
Fixpoint decode (cv : cvalue) : term :=
match cv with
| Clo t e =>
(Lam t).[fun x => nth x (map decode e) dummy_value]
end.
(* I am not even sure why this definition is accepted by Coq? *)
Definition decode_cenv e :=
fun x => nth x (map decode e) (decode dummy_cvalue).
(* The first equation in the above comment is satisfied, as shown by
the following lemma. The second equation in the above comment is
satisfied too, by definition. *)
Lemma decode_eq:
forall t e,
decode (Clo t e) = (Lam t).[decode_cenv e].
Proof.
reflexivity.
Qed.
(* This equation is useful, too. *)
Lemma decode_cenv_Var_eq:
forall x e,
(Var x).[decode_cenv e] = decode (nth x e dummy_cvalue).
Proof.
intros. asimpl. unfold decode_cenv. rewrite map_nth. eauto.
Qed.
(* The tactic [decode] rewrites using the above two equations. *)
Hint Rewrite decode_eq decode_cenv_Var_eq : decode.
Ltac decode := autorewrite with decode in *.
(* We make [decode] opaque, so its definition is not unfolded by Coq. *)
Opaque decode.
(* [decode cv] is always a value. *)
Lemma is_value_decode:
forall cv,
is_value (decode cv).
Proof.
intros. destruct cv. decode. asimpl. tauto.
Qed.
Lemma is_value_decode_cenv:
forall x e,
is_value (Var x).[decode_cenv e].
Proof.
intros. decode. eauto using is_value_decode.
Qed.
Local Hint Resolve is_value_decode is_value_decode_cenv : is_value obvious.
(* A composition of two substitutions is the same thing as one substitution. *)
Lemma decode_cenv_cons:
forall t e cv,
t.[up (decode_cenv e)].[decode cv/] = t.[decode_cenv (cv :: e)].
Proof.
intros. autosubst. (* wonderful *)
Qed.
(* The tactic [nonvalue_eq_decode] closes a subgoal when there is a hypothesis
of the form [_ = decode_cenv e x], where the left-hand side of the equation
clearly is not a value. This is a contradiction. *)
Ltac nonvalue_eq_decode :=
match goal with
| heq: _ = decode_cenv ?e ?x |- _ =>
assert (hv: is_value (decode_cenv e x)); [
solve [ obvious ]
| rewrite <- heq in hv; false; is_value ]
end.
(* -------------------------------------------------------------------------- *)
(* If [t] evaluates to [cv] under environment [e],
then, in the big-step semantics,
the term [t.[decode_cenv e]] evaluates to the value [decode cv]. *)
Lemma ebigcbv_bigcbv:
forall e t cv,
ebigcbv e t cv ->
bigcbv t.[decode_cenv e] (decode cv).
Proof.
induction 1; intros; subst.
(* EBigcbvVar *)
{ decode. econstructor. obvious. }
(* EBigcbvLam *)
{ econstructor. obvious. }
(* EBigcbvApp *)
{ decode.
asimpl. econstructor; eauto.
asimpl. eauto. }
(* EBigcbvLet *)
{ asimpl. econstructor; eauto.
asimpl. eauto. }
Qed.
(* A simplified corollary, where [t] is closed and is therefore evaluated
under the empty environment. *)
Lemma ebigcbv_bigcbv_nil:
forall t cv,
ebigcbv nil t cv ->
closed t ->
bigcbv t (decode cv).
Proof.
intros.
replace t with t.[decode_cenv nil] by eauto using closed_unaffected.
eauto using ebigcbv_bigcbv.
Qed.
(* -------------------------------------------------------------------------- *)
(* The converse statement: if in the big-step semantics, the term
[t.[decode_cenv e]] evaluates to the value [decode cv], then [t] evaluates
to [cv] under environment [e]. *)
(* This proof does not work (and, in fact, the statement is wrong). A failed
proof attempt reveals two problems... *)
Lemma bigcbv_ebigcbv_failed:
forall e t cv,
bigcbv t.[decode_cenv e] (decode cv) ->
ebigcbv e t cv.
Proof.
inversion 1; intros; subst.
(* BigcbvValue *)
{ (* [t] must be a variable or a lambda-abstraction. *)
destruct t; [ | | false; is_value | false; is_value ].
(* Case: [t] is a variable. *)
{ econstructor.
(* Here, we have two subgoals, neither of which can be proved. *)
{ (* Problem 1: we are unable to prove [x < length e]. In order
to establish such a property, we would have to express the
hypothesis that the free variables of [t] are in the domain
of the environment [e]. And, for this hypothesis to be
inductive, we have to further require every closure in
the environment [e] to satisfy a similar condition. *)
admit. }
{ (* Problem 2: we have [decode cv1 = decode cv2], and the goal
is [cv1 = cv2]. This goal cannot be proved, as the function
[decode] is not injective: multiple closures represent the
same lambda-abstraction. *)
decode.
admit. }
Abort.
(* -------------------------------------------------------------------------- *)
(* In order to fix the above failed statement, we need to express the
following well-formedness invariant: whenever a closure [Clo t e] is
constructed, the free variables of the term [t] are in the domain of the
environment [env], and, recursively, every value in [e] is well-formed. *)
Inductive wf_cvalue : cvalue -> Prop :=
| WfCvalue:
forall t e,
(forall cv, fv (length (cv :: e)) t) ->
wf_cenv e ->
wf_cvalue (Clo t e)
with wf_cenv : cenv -> Prop :=
| WfCenv:
forall e,
Forall wf_cvalue e ->
wf_cenv e.
(* The following trivial lemmas (which repeat the definition) are provided as
hints for [eauto with wf_cvalue]. *)
Lemma use_wf_cvalue_1:
forall t e cv,
wf_cvalue (Clo t e) ->
fv (length (cv :: e)) t.
Proof.
inversion 1; eauto.
Qed.
Lemma use_wf_cvalue_2:
forall t e,
wf_cvalue (Clo t e) ->
wf_cenv e.
Proof.
inversion 1; eauto.
Qed.
Lemma prove_wf_cenv_nil:
wf_cenv nil.
Proof.
econstructor. eauto.
Qed.
Lemma prove_wf_cenv_cons:
forall cv e,
wf_cvalue cv ->
wf_cenv e ->
wf_cenv (cv :: e).
Proof.
inversion 2; intros; subst.
econstructor.
econstructor; eauto.
Qed.
Hint Resolve
use_wf_cvalue_1 use_wf_cvalue_2 prove_wf_cenv_nil prove_wf_cenv_cons
: wf_cvalue.
(* The following lemma states that the invariant is preserved by [ebigcbv].
That is, if the term [t] is successfully evaluated in the well-formed
environment [e] to a cvalue [cv], then [cv] is well-formed. *)
Lemma ebigcbv_wf_cvalue:
forall e t cv,
ebigcbv e t cv ->
wf_cenv e ->
wf_cvalue cv.
Proof.
induction 1; intros; subst.
(* EBigcbvVar *)
{ pick wf_cenv invert. rewrite Forall_forall in *. eauto using nth_In. }
(* EBigcbvLam *)
{ econstructor; eauto. }
(* EBigcbvApp *)
{ eauto 6 with wf_cvalue. }
(* EBigcbvLet *)
{ eauto 6 with wf_cvalue. }
Qed.
Hint Resolve ebigcbv_wf_cvalue : wf_cvalue.
(* -------------------------------------------------------------------------- *)
(* We can now make an amended statement: if in the big-step semantics, the
term [t.[decode_cenv e]] evaluates to a value [v], if the environment [e]
is well-formed, and if the free variables of [t] are in the domain of [e],
then under environment [e] the term [t] evaluates to some cvalue [cv] such
that [decode cv] is [v]. *)
Lemma bigcbv_ebigcbv:
forall te v,
bigcbv te v ->
forall t e,
te = t.[decode_cenv e] ->
fv (length e) t ->
wf_cenv e ->
exists cv,
ebigcbv e t cv /\ decode cv = v.
Proof.
induction 1; intros; subst.
(* BigcbvValue *)
{ (* [t] must be a variable or a lambda-abstraction. *)
destruct t; [ | | false; is_value | false; is_value ]; fv.
(* Case: [t] is a variable. *)
{ eexists; split. econstructor; eauto. decode. eauto. }
(* Case: [t] is a lambda-abstraction. *)
{ eexists; split. econstructor; eauto. reflexivity. }
}
(* BigcbvApp *)
{ (* [t] must be an application. *)
destruct t;
match goal with h: _ = _ |- _ => asimpl in h end;
[ nonvalue_eq_decode | false; congruence | | false; congruence ].
fv. unpack.
(* The equality [App _ _ = App _ _] can be simplified. *)
injections. subst.
(* Exploit two of the induction hypotheses (forward). *)
edestruct IHbigcbv1; eauto. unpack. clear IHbigcbv1.
edestruct IHbigcbv2; eauto. unpack. clear IHbigcbv2.
(* If [decode cv] is [Lam _], then [cv] must be a closure. This should
be a lemma. Because (here) every cvalue is a closure, it is trivial. *)
match goal with h: decode ?cv = Lam _ |- _ =>
destruct cv as [ t' e' ];
rewrite decode_eq in h;
asimpl in h;
injections; subst
end.
(* Now, exploit the third induction hypothesis (forward). *)
edestruct IHbigcbv3; eauto using decode_cenv_cons with wf_cvalue.
unpack. clear IHbigcbv3.
(* The result follows. *)
eauto with ebigcbv.
}
(* BigcbvLet *)
{ (* [t] must be a [Let] construct. *)
destruct t;
match goal with h: _ = _ |- _ => asimpl in h end;
[ nonvalue_eq_decode | false; congruence | false; congruence | ].
fv. unpack.
injections. subst.
(* Exploit the induction hypotheses (forward). *)
edestruct IHbigcbv1; eauto. unpack. clear IHbigcbv1.
edestruct IHbigcbv2; eauto using decode_cenv_cons with wf_cvalue.
unpack. clear IHbigcbv2.
(* The result follows. *)
eauto with ebigcbv.
}
Qed.
(* A simplified corollary, where [t] is closed and is therefore evaluated
under the empty environment. *)
Lemma bigcbv_ebigcbv_nil:
forall t v,
bigcbv t v ->
closed t ->
exists cv,
ebigcbv nil t cv /\ decode cv = v.
Proof.
intros. eapply bigcbv_ebigcbv; eauto with wf_cvalue.
rewrite closed_unaffected by eauto. reflexivity.
Qed.

126
coq/LambdaCalculusFreeVars.v Normal file
View file

@ -0,0 +1,126 @@
Require Import MyTactics.
Require Import LambdaCalculusSyntax.
(* This technical lemma states that the renaming [lift 1] is injective. *)
Lemma lift_inj_Var:
forall t x,
lift 1 t = Var (S x) <-> t = Var x.
Proof.
split; intros.
{ eauto using lift_inj. }
{ subst. eauto. }
Qed.
(* -------------------------------------------------------------------------- *)
(* The predicate [fv] is characterized by the following lemmas. *)
Lemma fv_Var_eq:
forall k x,
fv k (Var x) <-> x < k.
Proof.
unfold fv. asimpl. induction k; intros.
(* Base case. *)
{ asimpl. split; intros; false.
{ unfold ids, Ids_term in *. injections. omega. }
{ omega. }
}
(* Step. *)
{ destruct x; asimpl.
{ split; intros. { omega. } { reflexivity. } }
rewrite lift_inj_Var. rewrite IHk. omega. }
Qed.
Lemma fv_Lam_eq:
forall k t,
fv k (Lam t) <-> fv (S k) t.
Proof.
unfold fv. intros. asimpl. split; intros.
{ injections. eauto. }
{ unpack. congruence. }
Qed.
Lemma fv_App_eq:
forall k t1 t2,
fv k (App t1 t2) <-> fv k t1 /\ fv k t2.
Proof.
unfold fv. intros. asimpl. split; intros.
{ injections. eauto. }
{ unpack. congruence. }
Qed.
Lemma fv_Let_eq:
forall k t1 t2,
fv k (Let t1 t2) <-> fv k t1 /\ fv (S k) t2.
Proof.
unfold fv. intros. asimpl. split; intros.
{ injections. eauto. }
{ unpack. congruence. }
Qed.
Hint Rewrite fv_Var_eq fv_Lam_eq fv_App_eq fv_Let_eq : fv.
(* -------------------------------------------------------------------------- *)
(* The following lemmas allow decomposing a closedness hypothesis.
Because [closed] is not an inductive notion, there is no lemma
for [Lam] and for the right-hand side of [Let]. *)
Lemma closed_Var:
forall x,
~ closed (Var x).
Proof.
unfold closed; intros; fv. omega.
Qed.
Lemma closed_AppL:
forall t1 t2,
closed (App t1 t2) ->
closed t1.
Proof.
unfold closed; intros; fv. tauto.
Qed.
Lemma closed_AppR:
forall t1 t2,
closed (App t1 t2) ->
closed t2.
Proof.
unfold closed; intros; fv. tauto.
Qed.
Lemma closed_LetL:
forall t1 t2,
closed (Let t1 t2) ->
closed t1.
Proof.
unfold closed; intros; fv. tauto.
Qed.
Hint Resolve closed_Var closed_AppL closed_AppR closed_LetL : closed.
(* -------------------------------------------------------------------------- *)
(* If the free variables of the term [t] are below [k], then [t] is unaffected
by a substitution of the form [upn k sigma]. *)
Lemma fv_unaffected:
forall t k sigma,
fv k t ->
t.[upn k sigma] = t.
Proof.
induction t; intros; fv; unpack; asimpl;
try solve [ eauto using upn_k_sigma_x with typeclass_instances
| f_equal; eauto ].
Qed.
(* If the term [t] is closed, then [t] is unaffected by any substitution. *)
Lemma closed_unaffected:
forall t sigma,
closed t ->
t.[sigma] = t.
Proof.
intros. eapply fv_unaffected with (k := 0). eauto.
Qed.

218
coq/LambdaCalculusInterpreter.v Normal file
View file

@ -0,0 +1,218 @@
Require Import Option.
Require Import List.
Require Import MyTactics.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusFreeVars.
Require Import LambdaCalculusBigStep.
(* We now wish to define an interpreter for the lambda-calculus. In other
words, whereas [ebigcbv] is a relation, we now wish to define a function
[interpret] whose graph is the relation [ebigcbv]. *)
(* At the moment, our lambda-calculus is pure (every value is a function)
so the interpreter cannot encounter a runtime error. *)
(* -------------------------------------------------------------------------- *)
(* We might naively wish to write the following code, which Coq rejects,
because this function is not obviously terminating. (Exercise: which
recursive call is the culprit?) Indeed, an interpreter for the untyped
lambda-calculus does not always terminate: there are lambda-terms whose
evaluation diverges. (Exercise: exhibit a term that reduces to itself
in one or more reduction steps. Prove in Coq that this is the case.) *)
Fail Fixpoint interpret (e : cenv) (t : term) : cvalue :=
match t with
| Var x =>
nth x e dummy_cvalue
(* dummy is used when x is out of range *)
| Lam t =>
Clo t e
| App t1 t2 =>
let cv1 := interpret e t1 in
let cv2 := interpret e t2 in
match cv1 with Clo u1 e' =>
interpret (cv2 :: e') u1
end
| Let t1 t2 =>
let cv1 := interpret e t1 in
interpret (cv1 :: e) t2
end.
(* -------------------------------------------------------------------------- *)
(* There are several potential solutions to the above problem. One solution
would be to write code in (some implementation of) the partiality monad.
(See Dagand's lectures.) The solution proposed here is to parameterize
the function [interpret] with a natural integer [n], which serves as an
amount of "fuel" (or "effort") that we are willing to invest before we
give up. Thus, termination becomes obvious. The downside is that the
interpreter can now fail (which means "not enough fuel"). Fortunately,
given enough fuel, every terminating term can be evaluated. *)
(* For Coq to accept the following definition, the fuel [n] must decrease at
every recursive call. We might wish to be more precise and somehow explain
that [n] needs to decrease only at the third recursive call in the case of
[App]lications. That would require defining a lexicographic ordering on the
pair [n, t], arguing that this ordering is well-founded, and defining
[interpret] by well-founded recursion. This can be done in Coq but is more
complicated, so (here) not worth the trouble. *)
Fixpoint interpret (n : nat) e t : option cvalue :=
match n with
| 0 => None (* not enough fuel *)
| S n =>
match t with
| Var x => Some (nth x e dummy_cvalue)
| Lam t => Some (Clo t e)
| App t1 t2 =>
interpret n e t1 >>= fun cv1 =>
interpret n e t2 >>= fun cv2 =>
match cv1 with Clo u1 e' =>
interpret n (cv2 :: e') u1
end
| Let t1 t2 =>
interpret n e t1 >>= fun cv1 =>
interpret n (cv1 :: e) t2
end end.
(* -------------------------------------------------------------------------- *)
(* The interpreter is correct with respect to the big-step semantics. *)
Lemma interpret_ebigcbv:
forall n e t cv,
interpret n e t = Some cv ->
fv (length e) t ->
wf_cenv e ->
ebigcbv e t cv.
Proof.
(* The definition of [interpret] is by induction on [n], so this proof
must be by induction on [n] as well. *)
induction n; destruct t; simpl; intros;
fv; unpack; injections; subst;
try solve [ congruence ].
(* Var *)
{ econstructor; eauto. }
(* Lam *)
{ econstructor; eauto. }
(* App *)
{ repeat invert_bind_Some.
(* Every cvalue is a closure. Name the components of the closure
obtained by interpreting [t1]. *)
match goal with h: interpret _ _ t1 = Some ?cv |- _ =>
destruct cv as [ t' e' ]
end.
(* The goal follows. *)
econstructor; eauto 11 with wf_cvalue. }
(* Let *)
{ invert_bind_Some.
econstructor; eauto with wf_cvalue. }
Qed.
(* A simplified corollary, where [t] is closed and is therefore evaluated
under the empty environment, and where we conclude with a [bigcbv]
judgement. *)
Lemma interpret_bigcbv_nil:
forall n t cv,
interpret n nil t = Some cv ->
closed t ->
bigcbv t (decode cv).
Proof.
eauto using ebigcbv_bigcbv_nil, interpret_ebigcbv with wf_cvalue.
Qed.
(* -------------------------------------------------------------------------- *)
(* The interpreter is monotonic with respect to the amount of fuel that is
provided: the more fuel, the better (that is, the more defined the result). *)
Lemma interpret_monotonic:
forall n1 n2 e t,
n1 <= n2 ->
less_defined (interpret n1 e t) (interpret n2 e t).
Proof.
(* This series of tactics get rid of the easy cases: *)
induction n1; destruct t; simpl; intros;
(* [less_defined None _] is always true. *)
eauto with less_defined;
(* If [S n1 <= n2], then [n2] must be a successor. *)
(destruct n2; [ omega |]); simpl;
(* [less_defined] is reflexive. *)
eauto with less_defined.
(* Two more complex cases remain, namely [App] and [Let]. Probably
the proof could be further automated, but I did not try. *)
(* App *)
{ eapply prove_less_defined_bind.
{ eauto using le_S_n. }
{ intros _ [ t' e' ]. (* destruct the closure produced by [t1] *)
eapply prove_less_defined_bind; eauto using le_S_n. }
}
(* Let *)
{ eauto 6 using le_S_n with less_defined. }
Qed.
(* A reformulation. *)
Lemma interpret_monotonic_corollary:
forall n1 n2 e t cv,
interpret n1 e t = Some cv ->
n1 <= n2 ->
interpret n2 e t = Some cv.
Proof.
generalize interpret_monotonic. unfold less_defined. eauto.
Qed.
(* -------------------------------------------------------------------------- *)
(* The interpreter is complete with respect to the big-step semantics
[ebigcbv]. That is, given enough fuel, and given a term whose value is
[cv], it will compute [cv]. *)
Lemma ebigcbv_interpret:
forall e t cv,
ebigcbv e t cv ->
exists n,
interpret n e t = Some cv.
Proof.
(* We can see, in the proof, that the necessary amount of fuel, [n], is
the height of the derivation of the judgement [ebigcbv e t cv].
Indeed, at every [App] or [Let] node, we count 1 plus the maximum
amount of fuel required by our children. *)
induction 1; intros; subst.
(* EBigcbvVar *)
{ exists 1. eauto. }
(* EBigcbvLam *)
{ exists 1. eauto. }
(* EBigcbvApp *)
{ destruct IHebigcbv1 as [ n1 ? ].
destruct IHebigcbv2 as [ n2 ? ].
destruct IHebigcbv3 as [ n3 ? ].
eexists (S (max (max n1 n2) n3)). simpl.
eauto 6 using prove_bind_Some, interpret_monotonic_corollary with omega. }
(* EBigcbvLet *)
{ destruct IHebigcbv1 as [ n1 ? ].
destruct IHebigcbv2 as [ n2 ? ].
eexists (S (max n1 n2)). simpl.
eauto using prove_bind_Some, interpret_monotonic_corollary with omega. }
Qed.
(* The interpreter is complete with respect to the big-step semantics
[bigcbv]. That is, given enough fuel, and given a term [t] whose value is
[v], it will compute a cvalue [cv] which decodes to [v]. We state this in
the case where [t] is closed and is therefore evaluated under the empty
environment. *)
Lemma bigcbv_interpret_nil:
forall t v,
bigcbv t v ->
closed t ->
exists n cv,
interpret n nil t = Some cv /\ decode cv = v.
Proof.
intros.
edestruct bigcbv_ebigcbv_nil; eauto. unpack.
edestruct ebigcbv_interpret; eauto.
Qed.

174
coq/LambdaCalculusParallelReduction.v Normal file
View file

@ -0,0 +1,174 @@
Require Import Relations.
Require Import Sequences.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusValues.
Require Import LambdaCalculusReduction.
Require Import MyTactics. (* TEMPORARY cannot be declared earlier; why? *)
(* -------------------------------------------------------------------------- *)
(* Parallel call-by-value reduction is stable by substitution. In fact,
if [t1] parallel-reduces to [t2] and [sigma1] parallel-reduces to
[sigma2], then [t1.[sigma1]] parallel-reduces to [t2.[sigma2]]. *)
Notation pcbv_subst sigma1 sigma2 :=
(forall x, pcbv (sigma1 x) (sigma2 x)).
Lemma pcbv_subst_up:
forall sigma1 sigma2,
pcbv_subst sigma1 sigma2 ->
pcbv_subst (up sigma1) (up sigma2).
Proof.
intros ? ? ? [|x]; asimpl.
{ eapply red_refl; obvious. }
{ eapply red_subst; obvious. }
Qed.
Lemma pcbv_subst_cons:
forall v1 v2 sigma1 sigma2,
pcbv v1 v2 ->
pcbv_subst sigma1 sigma2 ->
pcbv_subst (v1 .: sigma1) (v2 .: sigma2).
Proof.
intros ? ? ? ? ? ? [|x]; asimpl; eauto.
Qed.
Hint Resolve pcbv_subst_up pcbv_subst_cons : red obvious.
Lemma pcbv_parallel_subst:
forall t1 t2,
pcbv t1 t2 ->
forall sigma1 sigma2,
pcbv_subst sigma1 sigma2 ->
is_value_subst sigma1 ->
is_value_subst sigma2 ->
pcbv t1.[sigma1] t2.[sigma2].
Proof.
induction 1; try solve [ tauto ]; intros; subst.
{ rewrite subst_app, subst_lam.
eapply RedParBetaV. obvious. obvious.
{ eapply IHred1; obvious. }
{ eapply IHred2; obvious. }
autosubst. }
{ rewrite subst_let.
eapply RedParLetV. obvious. obvious.
{ eapply IHred1; obvious. }
{ eapply IHred2; obvious. }
autosubst. }
{ rewrite !subst_var. obvious. }
{ rewrite !subst_lam. eauto 6 with obvious. }
{ rewrite !subst_app. obvious. }
{ rewrite !subst_let. eauto 7 with obvious. }
Qed.
Hint Resolve pcbv_parallel_subst : red obvious.
(* -------------------------------------------------------------------------- *)
(* Parallel call-by-value reduction enjoys the diamond property. *)
(* The proof is by Takahashi's method (1995). We first define the function
[fpbcv], for "full parallel call-by-value reduction". This function
performs as much reduction as is possible in one step of [pcbv]. We prove
that this is indeed the case: if [t1] reduces to [t2] by [pcbv], then [t2]
reduces to [fpcbv t1]. The diamond property follows immediately. *)
Fixpoint fpcbv (t : term) : term :=
match t with
| Var x =>
Var x
| Lam t =>
Lam (fpcbv t)
| App (Lam t1) t2 =>
if_value t2
(fpcbv t1).[fpcbv t2/]
(App (Lam (fpcbv t1)) (fpcbv t2))
| App t1 t2 =>
App (fpcbv t1) (fpcbv t2)
| Let t1 t2 =>
if_value t1
(fpcbv t2).[fpcbv t1/]
(Let (fpcbv t1) (fpcbv t2))
end.
Ltac fpcbv :=
simpl; if_value.
Lemma pcbv_takahashi:
forall t1 t2,
pcbv t1 t2 ->
pcbv t2 (fpcbv t1).
Proof.
induction 1; try solve [ tauto ]; subst;
try solve [ fpcbv; eauto 9 with obvious ].
(* RedAppLR *)
{ destruct t1; try solve [ fpcbv; obvious ].
value_or_nonvalue u1; fpcbv; [ | obvious ].
(* [t1] is a lambda-abstraction, and [u1] is a value. We have a redex. *)
(* [pcbv (Lam _) t2] implies that [t2] is a lambda-abstraction, too. *)
match goal with h: pcbv (Lam _) ?t2 |- _ => invert h end.
(* Thus, the reduction of [t1] to [t2] is a reduction under lambda. *)
simpl in IHred1. inversion IHred1; subst.
(* The result is then... *)
obvious. }
(* RedLetLR *)
{ value_or_nonvalue t1; fpcbv; obvious. }
Qed.
Lemma diamond_pcbv:
diamond pcbv.
Proof.
intros t u1 ? u2 ?.
exists (fpcbv t).
split; eauto using pcbv_takahashi.
Qed.
Lemma diamond_star_pcbv:
diamond (star pcbv).
Proof.
eauto using diamond_pcbv, star_diamond.
Qed.
(* -------------------------------------------------------------------------- *)
(* Parallel reduction preserves the property of being stuck and the property
of being irreducible. *)
Lemma pcbv_preserves_stuck:
forall t1 t2,
pcbv t1 t2 ->
stuck t1 ->
stuck t2.
Proof.
induction 1; intros; subst; try solve [ tauto ].
(* RedParBetaV *)
{ false. eapply stuck_irred; eauto 2 with obvious. }
(* RedPatLetV *)
{ false. eapply stuck_irred; eauto 2 with obvious. }
(* RedLam *)
{ inv stuck. }
(* RedAppLR *)
{ inv stuck.
{ assert (forall t, t2 <> Lam t).
{ do 2 intro. subst.
inv red; (* invert [pcbv _ (Lam _)] *)
try solve [ false; eauto 2 with obvious | false; congruence ]. }
eauto with stuck obvious. }
{ eauto with stuck. }
{ eauto with stuck obvious. }
}
(* RedLetLR *)
{ inv stuck.
eauto with stuck. }
Qed.
Lemma pcbv_preserves_irred:
forall t1 t2,
pcbv t1 t2 ->
irred cbv t1 ->
irred cbv t2.
Proof.
intros t1 t2 ?.
rewrite !irred_cbv_characterization.
intuition eauto 2 using pcbv_preserves_stuck with obvious.
Qed.

619
coq/LambdaCalculusReduction.v Normal file
View file

@ -0,0 +1,619 @@
Require Import MyTactics.
Require Import Sequences.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusValues.
Require Import LambdaCalculusFreeVars.
(* We give a symbolic name to each reduction rule. *)
Inductive rule :=
| RuleBetaV (* reduction of a beta-v redex: (\x.t) v *)
| RuleLetV (* reduction of a let-v redex: let x = v in t *)
| RuleBeta (* reduction of a beta redex: (\x.t) u *)
| RuleLet (* reduction of a let redex: let x = u in t *)
| RuleParBetaV (* reduction of a beta-v redex and reduction in both sides *)
| RuleParLetV (* reduction of a let redex and reduction in both sides *)
| RuleVar (* no reduction *)
| RuleLam (* reduction in [Lam _] *)
| RuleAppL (* reduction in [App _ u] *)
| RuleAppVR (* reduction in [App v _], if [v] is a value *)
| RuleAppLR (* reduction in both sides of [App _ _] *)
| RuleLetL (* reduction in [Let _ u] *)
| RuleLetR (* reduction in [Let t _] *)
| RuleLetLR (* reduction in both sides of [Let _ _] *).
(* A mask is a set of rules. *)
Definition mask :=
rule -> Prop.
(* A generic small-step reduction semantics, parameterized with a mask. *)
Inductive red (mask : mask) : term -> term -> Prop :=
| RedBetaV:
forall t v u,
mask RuleBetaV ->
is_value v ->
t.[v/] = u ->
red mask (App (Lam t) v) u
| RedLetV:
forall t v u,
mask RuleLetV ->
is_value v ->
t.[v/] = u ->
red mask (Let v t) u
| RedBeta:
forall t1 t2 u,
mask RuleBeta ->
t1.[t2/] = u ->
red mask (App (Lam t1) t2) u
| RedLet:
forall t1 t2 u,
mask RuleLet ->
t2.[t1/] = u ->
red mask (Let t1 t2) u
| RedParBetaV:
forall t1 v1 t2 v2 u,
mask RuleParBetaV ->
is_value v1 ->
red mask t1 t2 ->
red mask v1 v2 ->
t2.[v2/] = u ->
red mask (App (Lam t1) v1) u
| RedParLetV:
forall t1 t2 v1 v2 u,
mask RuleParLetV ->
is_value v1 ->
red mask t1 t2 ->
red mask v1 v2 ->
t2.[v2/] = u ->
red mask (Let v1 t1) u
| RedVar:
forall x,
mask RuleVar ->
red mask (Var x) (Var x)
| RedLam:
forall t1 t2,
mask RuleLam ->
red mask t1 t2 ->
red mask (Lam t1) (Lam t2)
| RedAppL:
forall t1 t2 u,
mask RuleAppL ->
red mask t1 t2 ->
red mask (App t1 u) (App t2 u)
| RedAppVR:
forall v u1 u2,
mask RuleAppVR ->
is_value v ->
red mask u1 u2 ->
red mask (App v u1) (App v u2)
| RedAppLR:
forall t1 t2 u1 u2,
mask RuleAppLR ->
red mask t1 t2 ->
red mask u1 u2 ->
red mask (App t1 u1) (App t2 u2)
| RedLetL:
forall t1 t2 u,
mask RuleLetL ->
red mask t1 t2 ->
red mask (Let t1 u) (Let t2 u)
| RedLetR:
forall t u1 u2,
mask RuleLetR ->
red mask u1 u2 ->
red mask (Let t u1) (Let t u2)
| RedLetLR:
forall t1 t2 u1 u2,
mask RuleLetLR ->
red mask t1 t2 ->
red mask u1 u2 ->
red mask (Let t1 u1) (Let t2 u2)
.
Hint Constructors red : red obvious.
(* The following mask defines the call-by-value reduction semantics. *)
Definition cbv_mask rule :=
match rule with
| RuleBetaV (* reduction of a beta-v redex: (\x.t) v *)
| RuleLetV (* reduction of a let-v redex: let x = v in t *)
| RuleAppL (* reduction in [App _ u] *)
| RuleAppVR (* reduction in [App v _], if [v] is a value *)
| RuleLetL (* reduction in [Let _ u] *)
=> True
| _ => False
end.
Notation cbv := (red cbv_mask).
(* The following mask defines the call-by-name reduction semantics. *)
Definition cbn_mask rule :=
match rule with
| RuleBeta (* reduction of a beta redex: (\x.t) v *)
| RuleLet (* reduction of a let redex: let x = v in t *)
| RuleAppL (* reduction in [App _ u] *)
=> True
| _ => False
end.
Notation cbn := (red cbn_mask).
(* The parallel by-value reduction semantics allows beta-v reductions under
arbitrary contexts, including under lambda-abstractions. Furthermore, it
allows parallel reductions (and allows no reduction at all). *)
Definition pcbv_mask rule :=
match rule with
| RuleParBetaV (* reduction of a beta redex and reduction in both sides *)
| RuleParLetV (* reduction of a let redex and reduction in both sides *)
| RuleVar (* no reduction *)
| RuleLam (* reduction in [Lam _] *)
| RuleAppLR (* reduction in both sides of [App _ _] *)
| RuleLetLR (* reduction in both sides of [Let _ _] *)
=> True
| _ => False
end.
Notation pcbv := (red pcbv_mask).
(* The tactic [obvious] should be able to prove goals of the form
[red mask t1 t2], where [mask] is a known mask. *)
Hint Extern 1 (cbv_mask _) => (simpl; tauto) : red obvious.
Hint Extern 1 (cbn_mask _) => (simpl; tauto) : red obvious.
Hint Extern 1 (pcbv_mask _) => (simpl; tauto) : red obvious.
Goal cbv (Let (App (Lam (Var 0)) (Var 0)) (Var 0)) (Let (Var 0) (Var 0)).
Proof. obvious. Qed.
Goal cbv (Let (Var 0) (Var 0)) (Var 0).
Proof. obvious. Qed.
Goal cbn (Let (Var 0) (Var 0)) (Var 0).
Proof. obvious. Qed.
Goal
let id := Lam (Var 0) in
let t := (Let (Lam (Var 0)) (Var 0)) in
cbn (App id t) t.
Proof. simpl. obvious. Qed.
Goal pcbv (App (App (Lam (Var 0)) (Var 0)) (App (Lam (Var 0)) (Var 0)))
(App (Var 0) (Var 0)).
Proof.
eauto 8 with obvious.
Qed.
(* The tactic [step] applies to a goal of the form [star (red mask) t1 t2]. It
causes the term [t1] to take one step of reduction towards [t1'], turning
the goal into [star (red mask) t1' t2]. *)
Ltac step :=
eapply star_step; [ obvious |].
(* The tactic [finished] applies to a goal of the form [star (red mask) t1 t2].
It turns the goal into [t1 = t2]. *)
Ltac finished :=
eapply star_refl_eq.
(* The tactic [invert_cbv] inverts a hypothesis of the form [cbv t1 t2]. *)
Ltac invert_cbv :=
pick (red cbv_mask) invert;
try solve [ false; eauto 3 with obvious ].
Ltac invert_star_cbv :=
pick (star cbv) invert.
Ltac invert_cbn :=
pick (red cbn_mask) invert;
try solve [ false; eauto 3 with obvious ].
(* If the following four rules are enabled, then reduction is reflexive. *)
Lemma red_refl:
forall mask : mask,
mask RuleVar ->
mask RuleLam ->
mask RuleAppLR ->
mask RuleLetLR ->
forall t,
red mask t t.
Proof.
induction t; eauto with red.
Qed.
(* [RuleBetaV] and [RuleLetV] are special cases of [RuleParBetaV] and
[RuleParLetV], hence are admissible in parallel call-by-value reduction. *)
Lemma pcbv_RedBetaV:
forall t v u,
is_value v ->
t.[v/] = u ->
pcbv (App (Lam t) v) u.
Proof.
eauto using red_refl with obvious.
Qed.
Lemma pcbv_RedLetV:
forall t v u,
is_value v ->
t.[v/] = u ->
pcbv (Let v t) u.
Proof.
eauto using red_refl with obvious.
Qed.
(* Sequences of reduction, [star cbv], can be carried out under a context. *)
Lemma star_cbv_AppL:
forall t1 t2 u,
star cbv t1 t2 ->
star cbv (App t1 u) (App t2 u).
Proof.
induction 1; eauto with sequences obvious.
Qed.
Lemma star_pcbv_AppL:
forall t1 t2 u,
star pcbv t1 t2 ->
star pcbv (App t1 u) (App t2 u).
Proof.
induction 1; eauto using red_refl with sequences obvious.
Qed.
Lemma plus_pcbv_AppL:
forall t1 t2 u,
plus pcbv t1 t2 ->
plus pcbv (App t1 u) (App t2 u).
Proof.
induction 1.
econstructor; [ | eauto using star_pcbv_AppL ].
eapply RedAppLR; eauto using red_refl with obvious.
Qed.
Lemma star_cbv_AppR:
forall t u1 u2,
is_value t ->
star cbv u1 u2 ->
star cbv (App t u1) (App t u2).
Proof.
induction 2; eauto with sequences obvious.
Qed.
Hint Resolve star_cbv_AppL star_pcbv_AppL plus_pcbv_AppL star_cbv_AppR : red obvious.
Lemma star_cbv_AppLR:
forall t1 t2 u1 u2,
star cbv t1 t2 ->
star cbv u1 u2 ->
is_value t2 ->
star cbv (App t1 u1) (App t2 u2).
Proof.
eauto with sequences obvious.
Qed.
Lemma star_cbv_LetL:
forall t1 t2 u,
star cbv t1 t2 ->
star cbv (Let t1 u) (Let t2 u).
Proof.
induction 1; eauto with sequences obvious.
Qed.
Hint Resolve star_cbv_AppLR star_cbv_LetL : red obvious.
(* Reduction commutes with substitutions of values for variables. (This
includes renamings.) This is true of every reduction strategy, with
the proviso that if [RuleVar] is enabled, then [RuleLam], [RuleAppLR]
and [RuleLetLR] must be enabled as well, so that reduction is reflexive. *)
Lemma red_subst:
forall mask : mask,
(mask RuleVar -> mask RuleLam) ->
(mask RuleVar -> mask RuleAppLR) ->
(mask RuleVar -> mask RuleLetLR) ->
forall t1 t2,
red mask t1 t2 ->
forall sigma,
is_value_subst sigma ->
red mask t1.[sigma] t2.[sigma].
Proof.
induction 4; simpl; intros; subst;
try solve [ econstructor; solve [ eauto with is_value | autosubst ]].
(* Case: [Var] *)
{ eauto using red_refl. }
Qed.
Lemma star_red_subst:
forall mask : mask,
(mask RuleVar -> mask RuleLam) ->
(mask RuleVar -> mask RuleAppLR) ->
(mask RuleVar -> mask RuleLetLR) ->
forall t1 t2 sigma,
star (red mask) t1 t2 ->
is_value_subst sigma ->
star (red mask) t1.[sigma] t2.[sigma].
Proof.
induction 4; eauto using red_subst with sequences.
Qed.
(* Call-by-value reduction is contained in parallel call-by-value. *)
Lemma cbv_subset_pcbv:
forall t1 t2,
cbv t1 t2 ->
pcbv t1 t2.
Proof.
induction 1; try solve [ tauto ]; eauto using red_refl with red.
Qed.
(* Under call-by-value, values do not reduce. *)
Lemma values_do_not_reduce:
forall t1 t2,
cbv t1 t2 ->
~ is_value t1.
Proof.
inversion 1; is_value.
Qed.
Hint Resolve values_do_not_reduce : is_value obvious.
Hint Extern 1 (False) => (eapply values_do_not_reduce) : is_value obvious.
Lemma is_value_irred:
forall v,
is_value v ->
irred cbv v.
Proof.
intros. intro. obvious.
Qed.
Hint Resolve is_value_irred : irred obvious.
(* Under every strategy, the property of being a value is preserved by
reduction. *)
Lemma values_are_stable:
forall mask v1 v2,
red mask v1 v2 ->
is_value v1 ->
is_value v2.
Proof.
induction 1; is_value.
Qed.
Lemma nonvalues_are_stable:
forall mask v1 v2,
red mask v1 v2 ->
~ is_value v2 ->
~ is_value v1.
Proof.
induction 1; is_value.
Qed.
Hint Resolve values_are_stable nonvalues_are_stable : is_value obvious.
(* [cbv] is deterministic. *)
Lemma cbv_deterministic:
forall t t1,
cbv t t1 ->
forall t2,
cbv t t2 ->
t1 = t2.
Proof.
(* Induction over [cbv t t1]. *)
induction 1; try solve [ tauto ]; intros; subst;
(* Invert the second hypothesis, [cbv t t2]. The fact that values do not
reduce is used to eliminate some cases. *)
invert_cbv;
(* The result follows. *)
f_equal; eauto.
Qed.
(* Inversion lemmas for [irred]. *)
Lemma invert_irred_cbv_App_1:
forall t u,
irred cbv (App t u) ->
irred cbv t.
Proof.
intros. eapply irred_irred; obvious.
Qed.
Lemma invert_irred_cbv_App_2:
forall t u,
irred cbv (App t u) ->
is_value t ->
irred cbv u.
Proof.
intros. eapply irred_irred; obvious.
Qed.
Lemma invert_irred_cbv_App_3:
forall t u,
irred cbv (App t u) ->
is_value t ->
is_value u ->
forall t', t <> Lam t'.
Proof.
intros ? ? Hirred. repeat intro. subst.
eapply Hirred. obvious.
Qed.
Lemma invert_irred_cbv_Let_1:
forall t u,
irred cbv (Let t u) ->
irred cbv t.
Proof.
intros. eapply irred_irred; obvious.
Qed.
Lemma invert_irred_cbv_Let_2:
forall t u,
irred cbv (Let t u) ->
~ is_value t.
Proof.
intros ? ? Hirred ?. eapply Hirred. obvious.
Qed.
Hint Resolve
invert_irred_cbv_App_1
invert_irred_cbv_App_2
invert_irred_cbv_Let_1
invert_irred_cbv_Let_2
: irred.
(* An analysis of irreducible terms for call-by-value reduction. A stuck
term is either an application [v1 v2] where [v1] is not a function or
a stuck term in an evaluation context. *)
Inductive stuck : term -> Prop :=
| StuckApp:
forall v1 v2,
is_value v1 ->
is_value v2 ->
(forall t, v1 <> Lam t) ->
stuck (App v1 v2)
| StuckAppL:
forall t u,
stuck t ->
stuck (App t u)
| StuckAppR:
forall v u,
is_value v ->
stuck u ->
stuck (App v u)
| StuckLetL:
forall t u,
stuck t ->
stuck (Let t u).
Hint Constructors stuck : stuck.
(* To go wrong is to reduce to a stuck term. *)
Definition goes_wrong t :=
exists t', star cbv t t' /\ stuck t'.
(* A stuck term cannot be a value. *)
Lemma stuck_nonvalue:
forall t,
stuck t ->
~ is_value t.
Proof.
induction 1; is_value.
Qed.
(* Every stuck term is irreducible. *)
Ltac prove_irred_cbv :=
do 2 intro; invert_cbv.
Lemma stuck_irred:
forall t,
stuck t ->
irred cbv t.
Proof.
induction 1; prove_irred_cbv; try solve [
eauto using irreducible_terms_do_not_reduce
| eapply stuck_nonvalue; obvious
].
(* StuckApp *)
{ congruence. }
Qed.
Hint Resolve stuck_irred : irred obvious.
(* Every irreducible term either is a value or is stuck. *)
Lemma irred_cbv_is_value_or_stuck:
forall t,
irred cbv t ->
is_value t \/ stuck t.
Proof.
induction t; intro Hirred;
try solve [ is_value ]; right.
(* App *)
{ assert (H1: irred cbv t1). { eauto with irred. }
destruct (IHt1 H1); [| eauto with stuck ].
assert (H2: irred cbv t2). { eauto with irred. }
destruct (IHt2 H2); [| eauto with stuck ].
eapply StuckApp; eauto using invert_irred_cbv_App_3. }
(* Let *)
{ assert (H: irred cbv t). { eauto with irred. }
destruct (IHt H); [| eauto with stuck ].
assert (~ is_value t). { eauto with irred. }
tauto. }
Qed.
(* The converse is true as well. *)
Lemma irred_cbv_characterization:
forall t,
irred cbv t <->
is_value t \/ stuck t.
Proof.
split.
{ eauto using irred_cbv_is_value_or_stuck. }
{ intuition eauto with irred. }
Qed.
(* A closed value must be a lambda-abstraction. *)
Lemma closed_value:
forall v,
is_value v ->
closed v ->
exists t, v = Lam t.
Proof.
intros. destruct v as [| t | | ]; try solve [ false; is_value ].
{ false. eapply closed_Var. eauto. }
{ exists t. eauto. }
Qed.
(* A stuck term cannot be closed. *)
Lemma stuck_closed:
forall t,
stuck t ->
closed t ->
False.
Proof.
induction 1; intros; eauto with closed.
(* StuckApp *)
{ assert (ht1: exists t1, v1 = Lam t1).
{ eauto using closed_value with closed. }
destruct ht1 as (?&?). subst v1. congruence. }
Qed.
(* Under call-by-value, every closed term either reduces or is a value. *)
Lemma cbv_progress:
forall t,
closed t ->
is_value t \/ exists u, cbv t u.
Local Ltac ih IH :=
destruct IH as [| [ ? ? ]]; [ eauto with closed | | obvious ].
Proof.
(* We give a direct proof, but the result also follows from
[irred_cbv_is_value_or_stuck] and [stuck_closed]. *)
induction t as [| | t1 IHt1 t2 IHt2 | t1 IHt1 t2 IHt2 ];
try solve [ left; obvious ]; right.
(* App *)
{ ih IHt1.
ih IHt2.
destruct (closed_value t1) as [ u1 ? ]; eauto with closed; subst t1.
obvious.
}
(* Let *)
{ ih IHt1. obvious. }
Qed.

679
coq/LambdaCalculusStandardization.v Normal file
View file

@ -0,0 +1,679 @@
Require Import Sequences.
Require Import Relations.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusValues.
Require Import LambdaCalculusReduction.
Require Import LambdaCalculusParallelReduction.
Require Import MyTactics.
(* This is an adaptation of the paper "A Simple Proof of Call-by-Value
Standardization", by Karl Crary (2009). We establish two main results:
First, parallel call-by-value reduction is adequate, i.e., is contained in
contextual equivalence: if [t1] parallel-reduces to [t2], then [t1] halts
if and only if [t2] halts (where halting is considered with respect to
ordinary call-by-value reduction, [cbv]).
Second, every call-by-value reduction sequence can be put in a standard
form, as defined by the predicate [stdred]. *)
(* -------------------------------------------------------------------------- *)
(* "Evaluation" in Crary's paper is [cbv] here. Parallel reduction in Crary's
paper is [pcbv] here. Internal parallel reduction, [ipcbv], is defined as
follows. It is a restricted version of parallel reduction: it is allowed to
act only under lambda, in the right-hand side of an application whose
left-hand side is not a value, and in the right-hand side of [Let]. *)
Inductive ipcbv : term -> term -> Prop :=
| IRedVar:
forall x,
ipcbv (Var x) (Var x)
| IRedLam:
forall t1 t2,
pcbv t1 t2 ->
ipcbv (Lam t1) (Lam t2)
| IRedAppLRNonValue:
forall t1 t2 u1 u2,
~ is_value t1 ->
ipcbv t1 t2 ->
pcbv u1 u2 ->
ipcbv (App t1 u1) (App t2 u2)
| IRedAppLR:
forall t1 t2 u1 u2,
is_value t1 -> (* wlog; see [ipcbv_IRedAppLR] below *)
ipcbv t1 t2 ->
ipcbv u1 u2 ->
ipcbv (App t1 u1) (App t2 u2)
| IRedLetLR:
forall t1 t2 u1 u2,
ipcbv t1 t2 ->
pcbv u1 u2 ->
ipcbv (Let t1 u1) (Let t2 u2)
.
Local Hint Constructors ipcbv : red obvious.
(* [ipcbv] is a subset of [pcbv]. *)
Lemma ipcbv_subset_pcbv:
forall t1 t2,
ipcbv t1 t2 ->
pcbv t1 t2.
Proof.
induction 1; obvious.
Qed.
Local Hint Resolve ipcbv_subset_pcbv : red obvious.
(* The side condition [is_value t1] in [IRedAppLR] does not cause any loss
of expressiveness, as the previous rule covers the case where [t1] is
not a value. *)
Lemma ipcbv_IRedAppLR:
forall t1 t2 u1 u2,
ipcbv t1 t2 ->
ipcbv u1 u2 ->
ipcbv (App t1 u1) (App t2 u2).
Proof.
intros. value_or_nonvalue t1; obvious.
Qed.
Local Hint Resolve ipcbv_IRedAppLR : red obvious.
(* [ipcbv] is reflexive. *)
Lemma ipcbv_refl:
forall t,
ipcbv t t.
Proof.
induction t; eauto using red_refl with obvious.
Qed.
Local Hint Resolve ipcbv_refl.
(* [ipcbv] preserves values, both ways. *)
Lemma ipcbv_preserves_values:
forall v1 v2, ipcbv v1 v2 -> is_value v1 -> is_value v2.
Proof.
induction 1; is_value.
Qed.
Lemma ipcbv_preserves_values_reversed:
forall v1 v2, ipcbv v1 v2 -> is_value v2 -> is_value v1.
Proof.
induction 1; is_value.
Qed.
Lemma ipcbv_preserves_values_reversed_contrapositive:
forall v1 v2, ipcbv v1 v2 -> ~ is_value v1 -> ~ is_value v2.
Proof.
induction 1; is_value.
Qed.
Local Hint Resolve ipcbv_preserves_values ipcbv_preserves_values_reversed
ipcbv_preserves_values_reversed_contrapositive.
Lemma star_ipcbv_preserves_values_reversed:
forall v1 v2, star ipcbv v1 v2 -> is_value v2 -> is_value v1.
Proof.
induction 1; eauto.
Qed.
Local Hint Resolve star_ipcbv_preserves_values_reversed.
(* Reverse internal parallel reduction preserves the property of being stuck
and (therefore) the property of being irreducible. *)
Lemma reverse_ipcbv_preserves_stuck:
forall t1 t2,
ipcbv t1 t2 ->
stuck t2 ->
stuck t1.
Proof.
induction 1; inversion 1; subst; eauto with stuck.
{ false. obvious. }
{ false. obvious. }
{ eapply StuckApp; eauto.
do 2 intro; subst. inv ipcbv. congruence. }
Qed.
Lemma reverse_star_ipcbv_preserves_stuck:
forall t1 t2,
star ipcbv t1 t2 ->
stuck t2 ->
stuck t1.
Proof.
induction 1; eauto using reverse_ipcbv_preserves_stuck.
Qed.
Lemma reverse_ipcbv_preserves_irred:
forall t1 t2,
ipcbv t1 t2 ->
irred cbv t2 ->
irred cbv t1.
Proof.
do 3 intro. rewrite !irred_cbv_characterization.
intuition eauto 2 using reverse_ipcbv_preserves_stuck.
Qed.
Local Hint Resolve
pcbv_preserves_irred
reverse_ipcbv_preserves_irred
(star_implication (irred cbv))
(star_implication_reversed (irred cbv))
: irred.
(* -------------------------------------------------------------------------- *)
(* Strong parallel reduction requires both (1) parallel reduction; and (2) a
decomposition as an ordinary call-by-value reduction sequence, followed
with an internal parallel reduction step. Our goal is to prove that strong
parallel reduction in fact coincides with parallel reduction, which means
that this decomposition always exists. *)
Inductive spcbv : term -> term -> Prop :=
| SPCbv:
forall t1 u t2,
pcbv t1 t2 ->
star cbv t1 u ->
ipcbv u t2 ->
spcbv t1 t2.
Local Hint Constructors spcbv.
(* By definition, [spcbv] is a subset of [pcbv]. *)
Lemma spcbv_subset_pcbv:
forall t1 t2,
spcbv t1 t2 ->
pcbv t1 t2.
Proof.
inversion 1; eauto.
Qed.
Local Hint Resolve spcbv_subset_pcbv.
(* [spcbv] is reflexive. *)
Lemma spcbv_refl:
forall t,
spcbv t t.
Proof.
econstructor; eauto using red_refl with sequences obvious.
Qed.
Local Hint Resolve spcbv_refl.
(* -------------------------------------------------------------------------- *)
(* The main series of technical lemmas begins here. *)
Lemma crarys_lemma2:
forall t1 t2 u1 u2,
spcbv t1 t2 ->
pcbv u1 u2 ->
~ is_value t2 ->
spcbv (App t1 u1) (App t2 u2).
Proof.
inversion 1; intros; subst. econstructor; obvious.
Qed.
Lemma crarys_lemma3_App:
forall t1 t2 u1 u2,
spcbv t1 t2 ->
spcbv u1 u2 ->
spcbv (App t1 u1) (App t2 u2).
Proof.
inversion 1; inversion 1; intros; subst.
value_or_nonvalue t2.
{ eauto 6 with obvious. }
{ eauto using crarys_lemma2. }
Qed.
Lemma crarys_lemma3_Let:
forall t1 t2 u1 u2,
spcbv t1 t2 ->
pcbv u1 u2 ->
spcbv (Let t1 u1) (Let t2 u2).
Proof.
inversion 1; intros; subst; obvious.
Qed.
Lemma crarys_lemma4:
forall {u1 u2},
spcbv u1 u2 ->
is_value u1 ->
forall {t1 t2},
ipcbv t1 t2 ->
spcbv t1.[u1/] t2.[u2/].
Proof.
induction 3; intros.
(* Var. *)
{ destruct x as [|x]; asimpl; eauto. }
(* Lam *)
{ rewrite !subst_lam. inv spcbv.
econstructor; eauto 11 with sequences obvious. (* slow *) }
(* App (nonvalue) *)
{ asimpl. eapply crarys_lemma2; obvious. eauto 9 with obvious. }
(* App *)
{ asimpl. eapply crarys_lemma3_App; obvious. }
(* Let *)
{ rewrite !subst_let.
eapply crarys_lemma3_Let; eauto 12 with obvious. }
Qed.
Lemma crarys_lemma5:
forall {t1 t2 u1 u2},
spcbv t1 t2 ->
spcbv u1 u2 ->
is_value u1 ->
spcbv t1.[u1/] t2.[u2/].
Proof.
intros _ _ u1 u2 [ t1 t t2 Hpcbvt Hstarcbv Hipcbv ] Hpcbvu Hvalue.
generalize (crarys_lemma4 Hpcbvu Hvalue Hipcbv).
inversion 1; subst.
econstructor; [| | obvious ].
{ eauto 11 with obvious. }
{ eauto using star_red_subst with sequences obvious. }
Qed.
Lemma crarys_lemma6:
forall {t1 t2},
pcbv t1 t2 ->
spcbv t1 t2.
Proof.
induction 1; try solve [ tauto ]; subst.
(* RedParBetaV *)
{ match goal with hv: is_value _ |- _ =>
generalize (crarys_lemma5 IHred1 IHred2 hv)
end.
inversion 1; subst.
econstructor; obvious.
eauto with sequences obvious. }
(* RedParLetV *)
{ match goal with hv: is_value _ |- _ =>
generalize (crarys_lemma5 IHred1 IHred2 hv)
end.
inversion 1; subst.
econstructor; obvious.
eauto with sequences obvious. }
(* RedVar *)
{ obvious. }
(* RedLam *)
{ clear IHred. eauto with sequences obvious. }
(* RedAppLR *)
{ eauto using crarys_lemma3_App. }
(* RedLetLR *)
{ eauto using crarys_lemma3_Let. }
Qed.
(* A reformulation of Lemma 6. We can now forget about [spcbv]. *)
Lemma crarys_main_lemma:
forall t1 t2,
pcbv t1 t2 ->
exists t, star cbv t1 t /\ ipcbv t t2.
Proof.
intros ? ? H.
generalize (crarys_lemma6 H); inversion 1; subst.
eauto.
Qed.
Lemma crarys_main_lemma_plus:
commutation22
cbv pcbv
(plus cbv) ipcbv.
Proof.
unfold commutation22. intros ? ? Hstarcbv ? Hpcbv.
forward1 crarys_main_lemma.
eauto with sequences.
Qed.
(* -------------------------------------------------------------------------- *)
(* Postponement. *)
Lemma crarys_lemma7:
commutation22
ipcbv cbv
cbv pcbv.
Local Ltac ih7 :=
match goal with IH: forall u, cbv _ u -> _, h: cbv _ _ |- _ =>
generalize (IH _ h)
end; intros (?&?&?).
Proof.
unfold commutation22.
induction 1; intros; subst;
try solve [ false; eauto 2 with obvious ].
(* IRedAppLRNonValue *)
{ invert_cbv. ih7. obvious. }
(* IRedAppLR *)
{ (* [t1] and [t2] are values. *)
clear IHipcbv1.
invert_cbv.
(* Case: [u1] and [u2] are values. (Case 5 in Crary's proof.) *)
{ assert (is_value u1). { obvious. }
inv ipcbv.
eexists; split.
{ eapply RedBetaV; obvious. }
{ eauto 7 with obvious. }
}
(* Case: [u1] and [u2] are nonvalues. (Case 4 in Crary's proof.) *)
{ ih7. eexists; split; obvious. }
}
(* IRedLetLR *)
{ invert_cbv.
(* Case: [t1] and [t2] are values. *)
{ eexists; split; eauto 8 with obvious. }
(* Case: [t1] and [t2] are nonvalues. *)
{ ih7. eexists; split; obvious. }
}
Qed.
(* Internal parallel reduction commutes with reduction, as follows. *)
Lemma crarys_lemma8_plus:
commutation22
ipcbv cbv
(plus cbv) ipcbv.
Proof.
eauto using crarys_lemma7, crarys_main_lemma_plus,
commutation22_transitive.
Qed.
Lemma crarys_lemma8:
commutation22
ipcbv cbv
(star cbv) ipcbv.
Proof.
eauto using crarys_lemma8_plus, commutation22_variance with sequences.
Qed.
Lemma crarys_lemma8b_plus:
commutation22
ipcbv (plus cbv)
(plus cbv) ipcbv.
Proof.
eauto using commute_R_Splus, crarys_lemma8_plus.
Qed.
Lemma crarys_lemma8b:
commutation22
ipcbv (star cbv)
(star cbv) ipcbv.
Proof.
eauto using commute_R_Sstar, crarys_lemma8.
Qed.
Lemma crarys_lemma8b_plus_star:
commutation22
(star ipcbv) (plus cbv)
(plus cbv) (star ipcbv).
Proof.
eapply commute_Rstar_Splus.
eauto using crarys_lemma8b_plus, commutation22_variance with sequences.
Qed.
(* -------------------------------------------------------------------------- *)
(* Bifurcation. *)
(* A sequence of parallel reduction steps can be reformulated as a sequence
of ordinary reduction steps, followed with a sequence of internal parallel
reduction steps. *)
Lemma crarys_lemma9:
forall t1 t2,
star pcbv t1 t2 ->
exists t,
star cbv t1 t /\ star ipcbv t t2.
Proof.
induction 1.
{ eauto with sequences. }
{ unpack.
forward1 crarys_main_lemma.
forward2 crarys_lemma8b.
eauto with sequences. }
Qed.
(* The following result does not seem to explicitly appear in Crary's paper. *)
Lemma pcbv_cbv_commutation1:
commutation22
(star pcbv) cbv
(plus cbv) (star pcbv).
Proof.
intros t1 t2 ? t3 ?.
forward1 crarys_lemma9.
assert (plus cbv t2 t3). { eauto with sequences. }
forward2 crarys_lemma8b_plus_star.
eauto 6 using ipcbv_subset_pcbv, star_covariant with sequences.
Qed.
Lemma pcbv_cbv_commutation:
commutation22
(star pcbv) (plus cbv)
(plus cbv) (star pcbv).
Proof.
eauto using pcbv_cbv_commutation1, commute_R_Splus.
Qed.
(* -------------------------------------------------------------------------- *)
(* The notion of "reducing (in zero or more steps) to a value" is the same
under [pcbv] and under [cbv]. *)
Lemma equiconvergence:
forall t v,
star pcbv t v ->
is_value v ->
exists v',
star cbv t v' /\ is_value v'.
Proof.
intros. forward1 crarys_lemma9. eauto.
Qed.
(* -------------------------------------------------------------------------- *)
(* "Adequacy of reduction". In Crary's terminology, "reduction" is the
compatible closure of "evaluation", and "evaluation" is [cbv]. A
relation is adequate iff it is contained in contextual equivalence. *)
(* The adequacy theorem. (Crary's lemma 10.) *)
Theorem pcbv_adequacy:
forall t1 t2,
star pcbv t1 t2 ->
(halts cbv t1) <-> (halts cbv t2).
Proof.
split.
(* Case: [t1] reduces to an irreducible term [u1]. *)
{ intros (u1&?&?).
(* [t1] reduces via [pcbv*] to both [u1] and [t2], so they must both
reduce via [pcbv*] to some common term [u]. *)
assert (star pcbv t1 u1). { eauto using star_covariant, cbv_subset_pcbv. }
forward2 diamond_star_pcbv.
(* The reduction of [t2] to [u] can be bifurcated. That is, [t2] first
reduces via [cbv*], then via [ipbcv], to [u]. *)
forward1 crarys_lemma9.
(* Because [pcbv] and [ipcbv] (reversed) both preserve irreducibility,
this establishes that [t2] halts. *)
eexists. split; eauto with irred.
}
(* Case: [t2] reduces to an irreducible term [u2]. *)
{ intros (u2&?&?).
(* Therefore, [t1] reduces via [pcbv*] to [u2]. *)
assert (star pcbv t1 u2).
{ eauto using cbv_subset_pcbv, star_covariant with sequences. }
(* This reduction can be bifurcated. That is, [t1] first reduces via
[cbv*], then via [ipcbv], to [u2]. *)
forward1 crarys_lemma9.
(* Because [ipcbv] (reversed) preserves irreducibility, this proves
that [t1] halts. *)
eexists. split; eauto with irred.
}
Qed.
(* The previous result implies that [pcbv] and [star pcbv] are contained in
contextual equivalence. We do not establish this result, because we do
not need it, and we have not defined contextual equivalence. *)
(* -------------------------------------------------------------------------- *)
(* Preservation of divergence. *)
(* If we have an infinite [cbv] reduction sequence with [pcbv] steps in it,
then we have an infinite [cbv] reduction sequence. *)
Lemma pcbv_preserves_divergence:
forall t,
infseq (composition (plus cbv) pcbv) t ->
infseq cbv t.
Proof.
intros ? Hinfseq.
(* We generalize the statement slightly by allowing any number of initial
[pcbv] steps from [t] to [u] before finding an infinite reduction sequence
out of [u]. *)
eapply infseq_coinduction_principle with (P := fun t =>
exists u, star pcbv t u /\ infseq (composition (plus cbv) pcbv) u
); [| eauto with sequences ].
(* We have to show that, under this hypothesis, we are able to take one step
of [cbv] out of [t] and reach a term that satisfies this hypothesis again. *)
clear dependent t. intros t (u&?&hInfSeq).
pick infseq invert.
pick @composition invert. unpack.
(* Out of [t], we have [pcbv* . cbv+ . pcbv ...]. *)
(* Thus, we have [cbv+ . pcbv* . pcbv ...]. *)
forward2 pcbv_cbv_commutation.
(* Thus, we have [cbv . pcbv* ...]. *)
pick plus invert.
(* We are happy. *)
eexists. split; [ eauto |].
eexists. split; [| eauto ].
eauto 6 using cbv_subset_pcbv, star_covariant with sequences.
Qed.
(* -------------------------------------------------------------------------- *)
(* The final result in Crary's paper is a standardization theorem for
call-by-value reduction. The theorem states that any sequence of parallel
reduction steps can be put in a "standard" form, as defined by the relation
[stdred] below. *)
Inductive stdred : term -> term -> Prop :=
| StdNil:
forall t,
stdred t t
| StdCons:
forall t1 t2 t3,
cbv t1 t2 ->
stdred t2 t3 ->
stdred t1 t3
| StdLam:
forall t1 t2,
stdred t1 t2 ->
stdred (Lam t1) (Lam t2)
| StdApp:
forall t1 t2 u1 u2,
stdred t1 u1 ->
stdred t2 u2 ->
stdred (App t1 t2) (App u1 u2)
| StdLet:
forall t1 t2 u1 u2,
stdred t1 u1 ->
stdred t2 u2 ->
stdred (Let t1 t2) (Let u1 u2)
.
Hint Constructors stdred : stdred.
(* A couple of more flexible constructors for [stdred]. *)
Lemma star_cbv_subset_stdred:
forall t1 t2,
star cbv t1 t2 ->
stdred t1 t2.
Proof.
induction 1; eauto with stdred.
Qed.
Lemma StdConsStar:
forall t1 t2 t3,
star cbv t1 t2 ->
stdred t2 t3 ->
stdred t1 t3.
Proof.
induction 1; eauto with stdred.
Qed.
Hint Resolve star_cbv_subset_stdred StdConsStar : stdred.
(* The following four lemmas analyze a reduction sequence of the form [star
ipcbv t1 t2], where the head constructor of the term [t2] is known. In
every case, it can be concluded that the term [t1] exhibits the same head
constructor. *)
Lemma star_ipcbv_into_Var:
forall {t1 t2}, star ipcbv t1 t2 ->
forall {x}, t2 = Var x -> t1 = Var x.
Proof.
induction 1; intros; subst.
{ eauto. }
{ forward (IHstar _ eq_refl). inv ipcbv. eauto. }
Qed.
Lemma star_ipcbv_into_Lam:
forall {t1 t2}, star ipcbv t1 t2 ->
forall {u2}, t2 = Lam u2 ->
exists u1, t1 = Lam u1 /\ star pcbv u1 u2.
Proof.
induction 1; intros; subst.
{ eauto with sequences. }
{ forward (IHstar _ eq_refl). inv ipcbv. eauto with sequences. }
Qed.
Lemma star_ipcbv_into_App:
forall {t1 t2}, star ipcbv t1 t2 ->
forall {t21 t22}, t2 = App t21 t22 ->
exists t11 t12,
t1 = App t11 t12 /\ star pcbv t11 t21 /\ star pcbv t12 t22.
Proof.
induction 1; intros; subst.
{ eauto with sequences. }
{ forward (IHstar _ _ eq_refl). inv ipcbv;
eauto 9 using ipcbv_subset_pcbv with sequences. }
Qed.
Lemma star_ipcbv_into_Let:
forall {t1 t2}, star ipcbv t1 t2 ->
forall {t21 t22}, t2 = Let t21 t22 ->
exists t11 t12,
t1 = Let t11 t12 /\ star ipcbv t11 t21 /\ star pcbv t12 t22.
Proof.
induction 1; intros; subst.
{ eauto with sequences. }
{ forward (IHstar _ _ eq_refl). inv ipcbv. eauto 9 with sequences. }
Qed.
Ltac star_ipcbv_into :=
pick (star ipcbv) ltac:(fun h => first [
forward (star_ipcbv_into_Var h eq_refl)
| forward (star_ipcbv_into_Lam h eq_refl)
| forward (star_ipcbv_into_App h eq_refl)
| forward (star_ipcbv_into_Let h eq_refl)
]).
(* The standardization theorem. (Crary's lemma 12.) *)
Theorem cbv_standardization:
forall t2 t1,
star pcbv t1 t2 ->
stdred t1 t2.
Proof.
induction t2; intros;
forward1 crarys_lemma9;
star_ipcbv_into;
eauto 8 using ipcbv_subset_pcbv, star_covariant with stdred.
Qed.

197
coq/LambdaCalculusSyntax.v Normal file
View file

@ -0,0 +1,197 @@
Require Import Coq.Wellfounded.Inverse_Image.
Require Import MyTactics.
Require Export Autosubst.Autosubst.
Require Export AutosubstExtra.
Require Export Autosubst_IsRen.
(* Require Export Autosubst_EOS. *)
Require Export Autosubst_FreeVars.
(* The syntax of the lambda-calculus. *)
Inductive term :=
| Var (x : var)
| Lam (t : {bind term})
| App (t1 t2 : term)
| Let (t1 : term) (t2 : {bind term})
.
Instance Ids_term : Ids term. derive. Defined.
Instance Rename_term : Rename term. derive. Defined.
Instance Subst_term : Subst term. derive. Defined.
Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
Instance IdsLemmas_term : IdsLemmas term.
Proof. econstructor. intros. injections. eauto. Qed.
(* If the image of [t] through a substitution is a variable, then [t] must
itself be a variable. *)
Lemma subst_is_var:
forall t sigma x,
t.[sigma] = ids x ->
exists y,
t = ids y.
Proof.
intros ? ? ? Heq. destruct t; compute in Heq; solve [ eauto | congruence ].
Qed.
(* The identity substitution [ids] is injective. *)
Lemma inj_ids:
forall x y,
ids x = ids y ->
x = y.
Proof.
intros ? ? Heq. compute in Heq. congruence.
Qed.
(* If the composition of two substitutions [sigma1] and [sigma2] is the
identity substitution, then [sigma1] must be a renaming. *)
Lemma ids_implies_is_ren:
forall sigma1 sigma2,
sigma1 >> sigma2 = ids ->
is_ren sigma1.
Proof.
intros ? ? Hid.
eapply prove_is_ren; [ eapply inj_ids | intros x ].
eapply subst_is_var with (sigma := sigma2) (x := x).
rewrite <- Hid. reflexivity.
Qed.
Hint Resolve ids_implies_is_ren : is_ren obvious.
(* The size of a term. *)
Fixpoint size (t : term) : nat :=
match t with
| Var _ => 0
| Lam t => 1 + size t
| App t1 t2
| Let t1 t2 => 1 + size t1 + size t2
end.
(* The size of a term is preserved by renaming. *)
Lemma size_renaming:
forall t sigma,
is_ren sigma ->
size t.[sigma] = size t.
Proof.
induction t; intros sigma Hsigma; asimpl;
repeat (match goal with h: forall sigma, _ |- _ => rewrite h by obvious; clear h end);
try reflexivity.
(* [Var] *)
{ destruct Hsigma as [ xi ? ]. subst. reflexivity. }
Qed.
(* The [size] function imposes a well-founded ordering on terms. *)
Lemma smaller_wf:
well_founded (fun t1 t2 => size t1 < size t2).
Proof.
eauto using wf_inverse_image, lt_wf.
Qed.
(* The tactic [size_induction] facilitates proofs by induction on the
size of a term. The following lemmas are used in the construction
of this tactic. *)
Lemma size_induction_intro:
forall (P : term -> Prop),
(forall n t, size t < n -> P t) ->
(forall t, P t).
Proof.
eauto. (* just instantiate [n] with [size t + 1] *)
Defined.
Lemma size_induction_induction:
forall (P : term -> Prop),
(forall n, (forall t, size t < n -> P t) -> (forall t, size t < S n -> P t)) ->
(forall n t, size t < n -> P t).
Proof.
intros P IH. induction n; intros.
{ false. eapply Nat.nlt_0_r. eauto. }
{ eauto. }
Defined.
Lemma size_induction:
forall (P : term -> Prop),
(forall n, (forall t, size t < n -> P t) -> (forall t, size t < S n -> P t)) ->
(forall t, P t).
Proof.
intros P IH.
eapply size_induction_intro.
eapply size_induction_induction.
eauto.
Defined.
Ltac size_induction :=
(* We assume the goal is of the form [forall t, P t]. *)
intro t; pattern t;
match goal with |- ?P t =>
simpl; eapply (@size_induction P); clear
end;
intros n IH t Htn.
(* The goal should now be of the form [P t]
with a hypothesis [IH: (forall t, size t < n -> P t]
and a hypothesis [Htn: size t < S n]. *)
(* The tactic [size] proves goals of the form [size t < n]. The tactic
[obvious] is also extended to prove such goals. *)
Hint Extern 1 (size ?t.[?sigma] < ?n) =>
rewrite size_renaming by obvious
: size obvious.
Hint Extern 1 (size ?t < ?n) =>
simpl in *; omega
: size obvious.
Ltac size :=
eauto with size.
(* The following is a direct proof of [smaller_wf]. We do not use any
preexisting lemmas, and end the proof with [Defined] instead of [Qed],
so as to make the proof term transparent. Also, we avoid the tactic
[omega], which produces huge proof terms. This allows Coq to compute
with functions that are defined by well-founded recursion. *)
Lemma smaller_wf_transparent:
well_founded (fun t1 t2 => size t1 < size t2).
Proof.
unfold well_founded. size_induction.
constructor; intros u Hu.
eapply IH. eapply lt_S_n. eapply le_lt_trans; eauto.
Defined.
(* The following lemmas can be useful in situations where the tactic
[asimpl] performs too much simplification. *)
Lemma subst_var:
forall x sigma,
(Var x).[sigma] = sigma x.
Proof.
autosubst.
Qed.
Lemma subst_lam:
forall t sigma,
(Lam t).[sigma] = Lam (t.[up sigma]).
Proof.
autosubst.
Qed.
Lemma subst_app:
forall t1 t2 sigma,
(App t1 t2).[sigma] = App t1.[sigma] t2.[sigma].
Proof.
autosubst.
Qed.
Lemma subst_let:
forall t1 t2 sigma,
(Let t1 t2).[sigma] = Let t1.[sigma] t2.[up sigma].
Proof.
autosubst.
Qed.

179
coq/LambdaCalculusValues.v Normal file
View file

@ -0,0 +1,179 @@
Require Import MyTactics.
Require Import LambdaCalculusSyntax.
(* The syntactic subcategory of values is decidable. *)
Definition if_value {A} (t : term) (a1 a2 : A) : A :=
match t with
| Var _ | Lam _ => a1
| _ => a2
end.
Definition is_value (t : term) :=
if_value t True False.
Hint Extern 1 (is_value _) => (simpl; tauto) : is_value obvious.
(* A term either is or is not a value. *)
Lemma value_or_nonvalue:
forall t,
is_value t \/ ~ is_value t.
Proof.
destruct t; simpl; eauto.
Qed.
(* Simplification rules for [if_value]. *)
Lemma if_value_value:
forall A v (a1 a2 : A),
is_value v ->
if_value v a1 a2 = a1.
Proof.
destruct v; simpl; tauto.
Qed.
Lemma if_value_nonvalue:
forall A t (a1 a2 : A),
~ is_value t ->
if_value t a1 a2 = a2.
Proof.
destruct t; simpl; tauto.
Qed.
(* The syntactic subcategory of values is preserved by renamings. *)
Lemma is_value_renaming:
forall v xi,
is_value v ->
is_value v.[ren xi].
Proof.
destruct v; simpl; eauto.
Qed.
Lemma is_nonvalue_renaming:
forall v xi,
~ is_value v ->
~ is_value v.[ren xi].
Proof.
destruct v; simpl; eauto.
Qed.
Hint Resolve is_value_renaming is_nonvalue_renaming : is_value obvious.
Ltac is_value :=
eauto with is_value.
(* The tactic [not_a_value] can be used to prove that the current case
is impossible, because we have a hypothesis of the form [~ is_value v],
where [v] clearly is a value. *)
Ltac not_a_value :=
solve [ false; is_value ].
Ltac if_value :=
repeat first [ rewrite if_value_value by is_value |
rewrite if_value_nonvalue by is_value ].
(* The tactic [value_or_nonvalue t] creates two cases: either [t] is a value,
or it isn't. *)
Ltac value_or_nonvalue t :=
destruct (value_or_nonvalue t);
if_value.
(* The tactic [value_or_app_or_let] creates three cases: either [t] is a value,
or it is an application, or it is a [let] construct. *)
Ltac value_or_app_or_let t :=
value_or_nonvalue t; [|
destruct t as [ ? | ? | t1 t2 | t1 t2 ]; [ not_a_value | not_a_value | |]
(* In principle, we should not fix the names [t1] and [t2] here,
as it might cause name clashes. *)
].
(* The predicate [is_value_subst sigma] holds if every term in the
codomain of the substitution [sigma] is a value. *)
Definition is_value_subst (sigma : var -> term) :=
forall x, is_value (sigma x).
Lemma is_value_subst_ids:
is_value_subst ids.
Proof.
intros x. is_value.
Qed.
Lemma is_value_subst_cons:
forall v sigma,
is_value v ->
is_value_subst sigma ->
is_value_subst (v .: sigma).
Proof.
intros. intros [|x]; is_value.
Qed.
Definition is_value_subst_up:
forall sigma,
is_value_subst sigma ->
is_value_subst (up sigma).
Proof.
intros sigma h. intros [|x]; asimpl.
{ simpl. eauto. }
{ is_value. }
Qed.
Definition is_value_subst_upn:
forall sigma i,
is_value_subst sigma ->
is_value_subst (upn i sigma).
Proof.
induction i; intros; asimpl.
{ eauto. }
{ rewrite <- fold_up_upn. eauto using is_value_subst_up. }
Qed.
Lemma is_value_subst_renaming:
forall sigma i,
is_value_subst sigma ->
is_value_subst (sigma >> ren (+i)).
Proof.
intros. intro x. asimpl. is_value.
Qed.
Hint Resolve is_value_subst_up is_value_subst_upn is_value_subst_renaming
: is_value obvious.
Lemma values_are_preserved_by_value_substitutions:
forall v sigma,
is_value v ->
is_value_subst sigma ->
is_value v.[sigma].
Proof.
destruct v; simpl; intros; eauto with is_value.
Qed.
Lemma nonvalues_are_preserved_by_substitutions:
forall t sigma,
~ is_value t ->
~ is_value t.[sigma].
Proof.
destruct t; simpl; tauto.
Qed.
Hint Resolve
is_value_subst_ids
is_value_subst_cons
values_are_preserved_by_value_substitutions
nonvalues_are_preserved_by_substitutions
: is_value obvious.
Lemma is_ren_is_value_subst:
forall sigma,
is_ren sigma ->
is_value_subst sigma.
Proof.
intros ? [ xi ? ]. subst. eauto with is_value.
Qed.
Hint Resolve is_ren_is_value_subst : is_value obvious.

2
coq/Makefile Normal file
View file

@ -0,0 +1,2 @@
COQINCLUDE := -R $(shell pwd) MPRI
include Makefile.coq

188
coq/Makefile.coq Normal file
View file

@ -0,0 +1,188 @@
############################################################################
# Requirements.
# We need bash. We use the pipefail option to control the exit code of a
# pipeline.
SHELL := /usr/bin/env bash
############################################################################
# Configuration
#
#
# This Makefile relies on the following variables:
# COQBIN (default: empty)
# COQFLAGS (default: empty) (passed to coqc and coqide, not coqdep)
# COQINCLUDE (default: empty)
# V (default: *.v)
# V_AUX (default: undefined/empty)
# SERIOUS (default: 1)
# (if 0, we produce .vio files)
# (if 1, we produce .vo files in the old way)
# VERBOSE (default: undefined)
# (if defined, commands are displayed)
# We usually refer to the .v files using relative paths (such as Foo.v)
# but [coqdep -R] produces dependencies that refer to absolute paths
# (such as /bar/Foo.v). This confuses [make], which does not recognize
# that these files are the same. As a result, [make] does not respect
# the dependencies.
# We fix this by using ABSOLUTE PATHS EVERYWHERE. The paths used in targets,
# in -R options, etc., must be absolute paths.
ifndef V
PWD := $(shell pwd)
V := $(wildcard $(PWD)/*.v)
endif
# Typically, $(V) should list only the .v files that we are ultimately
# interested in checking. $(V_AUX) should list every other .v file in the
# project. $(VD) is obtained from $(V) and $(V_AUX), so [make] sees all
# dependencies and can rebuild files anywhere in the project, if needed, and
# only if needed.
ifndef VD
VD := $(patsubst %.v,%.v.d,$(V) $(V_AUX))
endif
VIO := $(patsubst %.v,%.vio,$(V))
VQ := $(patsubst %.v,%.vq,$(V))
VO := $(patsubst %.v,%.vo,$(V))
SERIOUS := 1
############################################################################
# Binaries
COQC := $(COQBIN)coqc $(COQFLAGS)
COQDEP := $(COQBIN)coqdep
COQIDE := $(COQBIN)coqide $(COQFLAGS)
############################################################################
# Targets
.PHONY: all proof depend quick proof_vo proof_vq
all: proof
ifeq ($(SERIOUS),0)
proof: proof_vq
else
proof: proof_vo
endif
proof_vq: $(VQ)
depend: $(VD)
quick: $(VIO)
proof_vo: $(VO)
############################################################################
# Verbosity control.
# Our commands are pretty long (due, among other things, to the use of
# absolute paths everywhere). So, we hide them by default, and echo a short
# message instead. However, sometimes one wants to see the command.
# By default, VERBOSE is undefined, so the .SILENT directive is read, so no
# commands are echoed. If VERBOSE is defined by the user, then the .SILENT
# directive is ignored, so commands are echoed, unless they begin with an
# explicit @.
ifndef VERBOSE
.SILENT:
endif
############################################################################
# Verbosity filter.
# Coq is way too verbose when using one of the -schedule-* commands.
# So, we grep its output and remove any line that contains 'Checking task'.
# We need a pipe that keeps the exit code of the *first* process. In
# bash, when the pipefail option is set, the exit code is the logical
# conjunction of the exit codes of the two processes. If we make sure
# that the second process always succeeds, then we get the exit code
# of the first process, as desired.
############################################################################
# Rules
# If B uses A, then the dependencies produced by coqdep are:
# B.vo: B.v A.vo
# B.vio: B.v A.vio
%.v.d: %.v
$(COQDEP) $(COQINCLUDE) $< > $@
ifeq ($(SERIOUS),0)
%.vo: %.vio
@echo "Compiling `basename $*`..."
set -o pipefail; ( \
$(COQC) $(COQINCLUDE) -schedule-vio2vo 1 $* \
2>&1 | (grep -v 'Checking task' || true))
# The recipe for producing %.vio destroys %.vo. In other words, we do not
# allow a young .vio file to co-exist with an old (possibly out-of-date) .vo
# file, because this seems to lead Coq into various kinds of problems
# ("inconsistent assumption" errors, "undefined universe" errors, warnings
# about the existence of both files, and so on). Destroying %.vo should be OK
# as long as the user does not try to build a mixture of .vo and .vio files in
# one invocation of make.
%.vio: %.v
@echo "Digesting `basename $*`..."
rm -f $*.vo
$(COQC) $(COQINCLUDE) -quick $<
%.vq: %.vio
@echo "Checking `basename $*`..."
set -o pipefail; ( \
$(COQC) $(COQINCLUDE) -schedule-vio-checking 1 $< \
2>&1 | (grep -v 'Checking task' || true))
touch $@
endif
ifeq ($(SERIOUS),1)
%.vo: %.v
@echo "Compiling `basename $*`..."
$(COQC) $(COQINCLUDE) $<
endif
_CoqProject: .FORCE
@echo $(COQINCLUDE) > $@
.FORCE:
############################################################################
# Dependencies
ifeq ($(findstring $(MAKECMDGOALS),depend clean),)
-include $(VD)
endif
############################################################################
# IDE
.PHONY: ide
.coqide:
@echo '$(COQIDE) $(COQINCLUDE) $$*' > .coqide
@chmod +x .coqide
ide: _CoqProject
$(COQIDE) $(COQINCLUDE)
############################################################################
# Clean
.PHONY: clean
clean::
rm -f *~
rm -f $(patsubst %.v,%.v.d,$(V)) # not $(VD)
rm -f $(VIO) $(VO) $(VQ)
rm -f *.aux .*.aux *.glob *.cache *.crashcoqide
rm -rf .coq-native .coqide
# TEMPORARY *~, *.aux, etc. do not make sense in a multi-directory setting

313
coq/MetalBigStep.v Normal file
View file

@ -0,0 +1,313 @@
Require Import List.
Require Import MyList.
Require Import MyTactics.
Require Import Sequences.
Require Import MetalSyntax.
Require Import Autosubst_Env.
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* A big-step call-by-value semantics with explicit environments. *)
(* Because every lambda-abstraction is closed, no closures are involved:
a lambda-abstraction evaluates to itself. Thus, an mvalue [mv] must be
either a (closed) lambda-abstraction or a pair of mvalues. *)
Inductive mvalue :=
| MVLam : {bind metal} -> mvalue
| MVPair : mvalue -> mvalue -> mvalue.
Definition dummy_mvalue : mvalue :=
MVLam (MVar 0).
(* An environment [e] is a list of mvalues. *)
Definition menv :=
list mvalue.
(* The judgement [mbigcbv e t mv] means that, under the environment [e], the
term [t] evaluates to [mv]. *)
Inductive mbigcbv : menv -> metal -> mvalue -> Prop :=
| MBigcbvVar:
forall e x mv,
(* The variable [x] must be in the domain of [e]. *)
x < length e ->
(* This allows us to safely look up [e] at [x]. *)
mv = nth x e dummy_mvalue ->
mbigcbv e (MVar x) mv
| MBigcbvLam:
forall e t,
(* The lambda-abstraction must have no free variables. *)
closed (MLam t) ->
mbigcbv e (MLam t) (MVLam t)
| MBigcbvApp:
forall e t1 t2 u1 mv2 mv,
(* Evaluate [t1] to a lambda-abstraction, *)
mbigcbv e t1 (MVLam u1) ->
(* evaluate [t2] to a value, *)
mbigcbv e t2 mv2 ->
(* and evaluate the function body in a singleton environment. *)
mbigcbv (mv2 :: nil) u1 mv ->
mbigcbv e (MApp t1 t2) mv
| MBigcbvLet:
forall e t1 t2 mv1 mv,
(* Evaluate [t1] to a value, *)
mbigcbv e t1 mv1 ->
(* and evaluate [t2] under a suitable environment. *)
mbigcbv (mv1 :: e) t2 mv ->
mbigcbv e (MLet t1 t2) mv
| MBigcbvPair:
forall e t1 t2 mv1 mv2,
(* Evaluate each component to a value, *)
mbigcbv e t1 mv1 ->
mbigcbv e t2 mv2 ->
(* and construct a pair. *)
mbigcbv e (MPair t1 t2) (MVPair mv1 mv2)
| MBigcbvPi:
forall e i t mv1 mv2 mv,
(* Evaluate [t] to a pair value, *)
mbigcbv e t (MVPair mv1 mv2) ->
(* and project out the desired component. *)
mv = match i with 0 => mv1 | _ => mv2 end ->
mbigcbv e (MPi i t) mv
.
Hint Constructors mbigcbv : mbigcbv.
(* -------------------------------------------------------------------------- *)
(* A reformulation of the evaluation rule for variables. *)
Lemma MBigcbvVarExact:
forall e1 mv e2 x,
x = length e1 ->
mbigcbv (e1 ++ mv :: e2) (MVar x) mv.
Proof.
intros. econstructor.
{ length. }
{ rewrite app_nth by eauto. reflexivity. }
Qed.
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* We now examine how the big-step semantics interacts with renamings.
We prove that if (roughly) the equation [e = xi >>> e'] holds then
evaluating [t.[xi]] under [e'] is the same as evaluating [t] under
[e]. *)
Lemma mbigcbv_ren:
forall e t mv,
mbigcbv e t mv ->
forall e' xi,
env_ren_comp e xi e' ->
mbigcbv e' t.[ren xi] mv.
Proof.
induction 1; intros;
try solve [ asimpl; eauto with env_ren_comp mbigcbv ].
(* MVar *)
{ pick @env_ren_comp invert.
econstructor; eauto. }
(* MLam *)
{ rewrite closed_unaffected by eauto.
eauto with mbigcbv. }
Qed.
(* As a special case, evaluating [eos x t] under an environment of the form
[e1 ++ mv :: e2], where length of [e1] is [x] (so [x] is mapped to [mv])
is the same as evaluating [t] under [e1 ++ e2]. The operational effect
of the end-of-scope mark [eos x _] is to delete the value stored at index
[x] in the evaluation environment. *)
Lemma mbigcbv_eos:
forall e1 e2 x t mv mw,
mbigcbv (e1 ++ e2) t mw ->
x = length e1 ->
mbigcbv (e1 ++ mv :: e2) (eos x t) mw.
Proof.
intros. eapply mbigcbv_ren; eauto with env_ren_comp.
Qed.
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* Evaluation rules for (simulated) tuples. *)
Fixpoint MVTuple mvs :=
match mvs with
| nil =>
MVLam (MVar 0)
| mv :: mvs =>
MVPair mv (MVTuple mvs)
end.
Lemma MBigcbvTuple:
forall e ts mvs,
(* Evaluate every component to a value, *)
Forall2 (mbigcbv e) ts mvs ->
(* and construct a tuple. *)
mbigcbv e (MTuple ts) (MVTuple mvs).
Proof.
induction 1; simpl; econstructor; eauto.
{ unfold closed. fv. }
Qed.
Lemma MBigcbvProj:
forall i e t mvs mv,
i < length mvs ->
(* Evaluate [t] to a tuple value, *)
mbigcbv e t (MVTuple mvs) ->
(* and project out the desired component. *)
mv = nth i mvs dummy_mvalue ->
mbigcbv e (MProj i t) mv.
Proof.
(* By induction on [i]. In either case, [mvs] cannot be an empty list. *)
induction i; intros; (destruct mvs as [| mv0 mvs ]; [ false; simpl in *; omega |]).
(* Base case. *)
{ econstructor; eauto. }
(* Step case. *)
{ assert (i < length mvs). { length. }
simpl. eauto with mbigcbv. }
Qed.
Lemma MBigcbvLetPair:
forall e t u mv mv1 mv2,
mbigcbv e t (MVPair mv1 mv2) ->
mbigcbv (mv2 :: mv1 :: e) u mv ->
mbigcbv e (MLetPair t u) mv.
Proof.
unfold MLetPair. eauto 6 using mbigcbv_ren, env_ren_comp_plus1 with mbigcbv.
Qed.
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* Evaluation rules for [MMultiLet]. *)
Local Lemma Forall2_mbigcbv_plus1:
forall ts mvs e i mv,
Forall2 (mbigcbv e) (map (fun t : metal => lift i t) ts) mvs ->
Forall2 (mbigcbv (mv :: e)) (map (fun t : metal => lift (i + 1) t) ts) mvs.
Proof.
induction ts as [| t ts]; simpl; intros;
pick Forall2 invert; econstructor; eauto.
replace (lift (i + 1) t) with (lift 1 (lift i t)) by autosubst.
eauto using mbigcbv_ren, env_ren_comp_plus1.
Qed.
Lemma MBigcbvMultiLet:
forall ts e i u mvs mv,
Forall2 (mbigcbv e) (map (fun t => lift i t) ts) mvs ->
mbigcbv (rev mvs ++ e) u mv ->
mbigcbv e (MMultiLet i ts u) mv.
Proof.
induction ts; simpl; intros; pick Forall2 invert.
{ eauto. }
{ pick mbigcbv ltac:(fun h => rewrite rev_cons_app in h).
econstructor; eauto using Forall2_mbigcbv_plus1. }
Qed.
Lemma MBigcbvMultiLet_0:
forall ts e u mvs mv,
Forall2 (mbigcbv e) ts mvs ->
mbigcbv (rev mvs ++ e) u mv ->
mbigcbv e (MMultiLet 0 ts u) mv.
Proof.
intros. eapply MBigcbvMultiLet.
{ asimpl. rewrite map_id. eauto. }
{ eauto. }
Qed.
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* An evaluation rule for [MVars]. *)
Lemma MBigcbvVars_preliminary:
forall e2 e1 e x n,
e = e1 ++ e2 ->
x = length e1 ->
n = length e2 ->
Forall2 (mbigcbv e) (map MVar (seq x n)) e2.
Proof.
induction e2 as [| mv e2 ]; intros; subst; econstructor.
{ eauto using MBigcbvVarExact. }
{ eapply IHe2 with (e1 := e1 ++ mv :: nil).
{ rewrite <- app_assoc. reflexivity. }
{ length. }
{ eauto. }
}
Qed.
Lemma MBigcbvVars:
forall e,
Forall2 (mbigcbv e) (MVars (length e)) e.
Proof.
unfold MVars, nats. intros.
eapply MBigcbvVars_preliminary with (e1 := nil); eauto.
Qed.
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* An evaluation rule for [MProjs]. If the term [t] evaluates to a tuple whose
components numbered 1, ..., n are collected in the list [mvs1], then the
family of terms [MProjs n t] evaluates to the family of values [rev mvs1]. *)
Lemma MBigcbvProjs:
forall n e t mv mvs1 mvs2,
mbigcbv e t (MVTuple (mv :: mvs1 ++ mvs2)) ->
length mvs1 = n ->
Forall2 (mbigcbv e) (MProjs n t) (rev mvs1).
Proof.
(* This result is "obvious" but requires some low-level work. *)
unfold MProjs. induction n; intros.
(* Case: [n] is zero. Then, [mvs1] must be [nil]. The result follows. *)
{ destruct mvs1; [| false; simpl in *; omega ].
econstructor. }
(* Case: [n] is nonzero. Then, the list [mvs1] must be nonempty. *)
assert (hmvs1: mvs1 <> nil).
{ intro. subst. simpl in *. omega. }
(* So, this list has one element at the end. Let us write this list in the
form [mvs1 ++ mv1]. *)
destruct (exists_last hmvs1) as (hd&mv1&?). subst mvs1. clear hmvs1.
generalize dependent hd; intro mvs1; intros.
(* Simplify. *)
rewrite rev_unit.
rewrite <- app_assoc in *.
rewrite app_length in *.
assert (length mvs1 = n). { length. }
simpl map.
econstructor.
(* The list heads. *)
{ eapply MBigcbvProj; eauto.
{ length. }
{ replace (n + 1) with (S n) by omega. simpl.
rewrite app_nth by omega.
reflexivity. }
}
(* The list tails. *)
{ eauto. }
Qed.
(* -------------------------------------------------------------------------- *)
(* An evaluation rule for the combination of [MMultiLet] and [MProjs]. If the
term [t] evaluates to a tuple whose components are [mv :: mvs], and if [n]
is the length of [mvs], then evaluating [MMultiLet 0 (MProjs n t) u] in an
environment [e] leads to evaluating [u] in environment [mvs ++ e]. *)
Lemma MBigcbvMultiLetProjs:
forall e t mvs u mv mw n,
mbigcbv e t (MVTuple (mv :: mvs)) ->
length mvs = n ->
mbigcbv (mvs ++ e) u mw ->
mbigcbv e (MMultiLet 0 (MProjs n t) u) mw.
Proof.
intros.
eapply MBigcbvMultiLet_0.
{ eapply MBigcbvProjs with (mvs2 := nil); [ rewrite app_nil_r |]; eauto. }
{ rewrite rev_involutive. eauto. }
Qed.

432
coq/MetalSyntax.v Normal file
View file

@ -0,0 +1,432 @@
Require Import List.
Require Import MyList.
Require Import MyTactics.
Require Export Autosubst.Autosubst.
Require Export AutosubstExtra.
Require Export Autosubst_EOS.
Require Export Autosubst_FreeVars.
(* -------------------------------------------------------------------------- *)
(* Metal is a lambda-calculus where every lambda-abstractions must be closed.
It is equipped with pairs and projections. It is intended to serve as the
target of closure conversion. *)
(* -------------------------------------------------------------------------- *)
(* Syntax. *)
Inductive metal :=
| MVar : var -> metal
| MLam : {bind metal} -> metal
| MApp : metal -> metal -> metal
| MLet : metal -> {bind metal} -> metal
| MPair : metal -> metal -> metal
| MPi : nat -> metal -> metal
.
Instance Ids_metal : Ids metal. derive. Defined.
Instance Rename_metal : Rename metal. derive. Defined.
Instance Subst_metal : Subst metal. derive. Defined.
Instance SubstLemmas_metal : SubstLemmas metal. derive. Qed.
Instance IdsLemmas_metal : IdsLemmas metal.
Proof. econstructor. intros. injections. eauto. Qed.
(* -------------------------------------------------------------------------- *)
(* We equip the calculus with pairs, instead of general tuples, because
this makes life in Coq simpler -- we would otherwise have an occurrence
of [list metal] in the definition of [metal], and would need to ask for
a custom induction scheme. *)
(* Instead, we simulate tuples using nested pairs. This would of course be
inefficient in real life, but fur our purposes, should be fine. *)
Fixpoint MTuple ts :=
match ts with
| nil =>
(* A dummy value serves as the tail. *)
MLam (MVar 0)
| t :: ts =>
MPair t (MTuple ts)
end.
Fixpoint MProj i t :=
match i with
| 0 =>
(* Take the left pair component. *)
MPi 0 t
| S i =>
(* Take the right pair component and continue. *)
MProj i (MPi 1 t)
end.
Definition MLetPair t u :=
MLet (* x_0 = *) (MPi 0 t) (
MLet (* x_1 = *) (MPi 1 (lift 1 t))
u
).
(* -------------------------------------------------------------------------- *)
(* [MMultiLet 0 ts u] is a sequence of [MLet] bindings. [n] variables, where
[n] is [length ts], are bound to the terms [ts] in the term [u]. The
recursive structure of the definition is such that the *last* term in the
list [ts] is bound *last*, hence is referred to as variable 0 in [u]. *)
Fixpoint MMultiLet i ts u :=
match ts with
| nil =>
u
| t :: ts =>
MLet (lift i t) (MMultiLet (i + 1) ts u)
end.
(* The auxiliary parameter [i] in [MMultiLet i ts u] is required for the
recursive definition to go through, but, as far as the end user is
concerned, is not very useful. It can be eliminated as follows. *)
Lemma MMultiLet_ij:
forall ts delta i j u,
i + delta = j ->
MMultiLet j ts u = MMultiLet i (map (fun t => lift delta t) ts) u.
Proof.
induction ts; intros; simpl; eauto.
f_equal.
{ asimpl. congruence. }
{ erewrite IHts. eauto. omega. }
Qed.
Lemma MMultiLet_i0:
forall i ts u,
MMultiLet i ts u = MMultiLet 0 (map (fun t => lift i t) ts) u.
Proof.
eauto using MMultiLet_ij with omega.
Qed.
(* -------------------------------------------------------------------------- *)
(* [MVars n] is the list [MVar 0, ..., MVar (n-1)]. *)
Definition MVars (n : nat) : list metal :=
map MVar (nats n).
(* -------------------------------------------------------------------------- *)
(* [MProjs n t] is the list [MProj n t, ..., MProj 1 t]. *)
Definition MProjs (n : nat) (t : metal) :=
map (fun i => MProj (i + 1) t) (rev_nats n).
(* This list has length [n]. *)
Lemma length_MProjs:
forall n t,
length (MProjs n t) = n.
Proof.
unfold MProjs. intros. rewrite map_length, length_rev_nats. eauto.
Qed.
Hint Rewrite length_MProjs : length.
(* -------------------------------------------------------------------------- *)
(* Substitution (boilerplate lemmas). *)
Lemma subst_MVar:
forall x sigma,
(MVar x).[sigma] = sigma x.
Proof.
intros. autosubst.
Qed.
Lemma subst_MLam:
forall t sigma,
(MLam t).[sigma] = MLam t.[up sigma].
Proof.
intros. autosubst.
Qed.
Lemma subst_MApp:
forall t1 t2 sigma,
(MApp t1 t2).[sigma] = MApp t1.[sigma] t2.[sigma].
Proof.
intros. autosubst.
Qed.
Lemma subst_MLet:
forall t1 t2 sigma,
(MLet t1 t2).[sigma] = MLet t1.[sigma] t2.[up sigma].
Proof.
intros. autosubst.
Qed.
Lemma subst_MPair:
forall t1 t2 sigma,
(MPair t1 t2).[sigma] = MPair t1.[sigma] t2.[sigma].
Proof.
intros. autosubst.
Qed.
Lemma subst_MPi:
forall i t sigma,
(MPi i t).[sigma] = MPi i t.[sigma].
Proof.
intros. autosubst.
Qed.
Lemma subst_MTuple:
forall ts sigma,
(MTuple ts).[sigma] = MTuple (map (subst sigma) ts).
Proof.
induction ts; intros; asimpl; [ | rewrite IHts ]; reflexivity.
Qed.
Lemma subst_MProj:
forall n t sigma,
(MProj n t).[sigma] = MProj n t.[sigma].
Proof.
induction n; intros; asimpl; [ | rewrite IHn ]; autosubst.
Qed.
Lemma subst_MLetPair:
forall t u sigma,
(MLetPair t u).[sigma] = MLetPair t.[sigma] u.[upn 2 sigma].
Proof.
unfold MLetPair. intros. autosubst.
Qed.
Lemma subst_MMultiLet:
forall ts i u sigma,
(MMultiLet i ts u).[upn i sigma] =
MMultiLet i (map (subst sigma) ts) u.[upn (length ts) (upn i sigma)].
Proof.
induction ts; intros; asimpl; f_equal.
{ erewrite plus_upn by tc. eauto. }
{ rewrite IHts.
repeat erewrite upn_upn by tc.
do 3 f_equal. omega. }
Qed.
Lemma subst_MMultiLet_0:
forall ts u sigma,
(MMultiLet 0 ts u).[sigma] =
MMultiLet 0 (map (subst sigma) ts) u.[upn (length ts) sigma].
Proof.
intros.
change sigma with (upn 0 sigma) at 1.
eapply subst_MMultiLet.
Qed.
Lemma subst_MVars:
forall n sigma,
map (subst sigma) (MVars n) = map sigma (nats n).
Proof.
intros. unfold MVars. rewrite map_map. reflexivity.
Qed.
Lemma subst_MProjs:
forall n t sigma,
map (subst sigma) (MProjs n t) = MProjs n t.[sigma].
Proof.
unfold MProjs. induction n; intros; simpl; eauto.
rewrite subst_MProj, IHn. eauto.
Qed.
Hint Rewrite
subst_MVar subst_MLam subst_MApp subst_MLet subst_MPair subst_MPi
subst_MTuple subst_MProj subst_MLetPair
subst_MMultiLet subst_MMultiLet_0
subst_MVars subst_MProjs
: subst.
(* -------------------------------------------------------------------------- *)
(* Free variables (boilerplate lemmas). *)
Lemma fv_MVar:
forall x k,
fv k (MVar x) <-> x < k.
Proof.
eauto using fv_ids_eq.
Qed.
Ltac prove_fv :=
unfold fv; intros; asimpl;
split; intros; unpack; [ injections | f_equal ]; eauto.
Lemma fv_MLam:
forall t k,
fv k (MLam t) <-> fv (k + 1) t.
Proof.
prove_fv.
Qed.
Lemma fv_MApp:
forall t1 t2 k,
fv k (MApp t1 t2) <-> fv k t1 /\ fv k t2.
Proof.
prove_fv.
Qed.
Lemma fv_MLet:
forall t1 t2 k,
fv k (MLet t1 t2) <-> fv k t1 /\ fv (k + 1) t2.
Proof.
prove_fv.
Qed.
Lemma fv_MPair:
forall t1 t2 k,
fv k (MPair t1 t2) <-> fv k t1 /\ fv k t2.
Proof.
prove_fv.
Qed.
Lemma fv_MPi:
forall i t k,
fv k (MPi i t) <-> fv k t.
Proof.
prove_fv.
Qed.
Hint Rewrite fv_MVar fv_MLam fv_MApp fv_MLet fv_MPair fv_MPi : fv.
Lemma fv_MTuple:
forall k ts,
fv k (MTuple ts) <-> Forall (fv k) ts.
Proof.
induction ts; simpl; intros; fv; split; intros; unpack.
{ econstructor. }
{ omega. }
{ rewrite IHts in *. econstructor; eauto. }
{ rewrite IHts in *. pick Forall invert. eauto. }
Qed.
Lemma fv_MProj:
forall k n t,
fv k (MProj n t) <-> fv k t.
Proof.
induction n; intros; simpl; [ | rewrite IHn ]; fv; tauto.
Qed.
Lemma fv_MLetPair:
forall k t u,
fv k (MLetPair t u) <-> fv k t /\ fv (k + 2) u.
Proof.
intros. unfold MLetPair. fv; tc.
replace (k + 1 + 1) with (k + 2) by omega.
tauto.
Qed.
Local Lemma MLet_inj:
forall t1 u1 t2 u2,
MLet t1 u1 = MLet t2 u2 <-> t1 = t2 /\ u1 = u2.
Proof.
split; intros; injections; unpack; subst; eauto.
Qed.
Local Lemma cons_cons_eq:
forall {A} (x1 x2 : A) xs1 xs2,
x1 :: xs1 = x2 :: xs2 <->
x1 = x2 /\ xs1 = xs2.
Proof.
split; intros; injections; unpack; subst; eauto.
Qed.
Local Lemma MMultiLet_inj:
forall ts1 u1 ts2 u2 i,
length ts1 = length ts2 ->
MMultiLet i ts1 u1 = MMultiLet i ts2 u2 <->
ts1 = ts2 /\ u1 = u2.
Proof.
induction ts1; destruct ts2; intros; simpl;
try solve [ false; simpl in *; omega ].
{ tauto. }
{ rewrite MLet_inj.
rewrite lift_injn_eq.
rewrite IHts1 by (simpl in *; omega).
rewrite cons_cons_eq.
tauto. }
Qed.
Local Lemma map_inj:
forall {A} (f : A -> A) xs,
map f xs = xs <->
Forall (fun x => f x = x) xs.
Proof.
induction xs; simpl; intros; split; intros; eauto using Forall;
injections.
{ econstructor; tauto. }
{ pick Forall invert. f_equal; tauto. }
Qed.
Lemma fv_MMultiLet_0:
forall ts u k,
fv k (MMultiLet 0 ts u) <->
Forall (fv k) ts /\ fv (k + length ts) u.
Proof.
intros. unfold fv.
autorewrite with subst.
rewrite MMultiLet_inj by eauto using map_length.
rewrite upn_upn, Nat.add_comm.
rewrite map_inj.
tauto.
Qed.
Lemma fv_MVars:
forall n,
Forall (fv n) (MVars n) <->
True.
Proof.
split; [ eauto | intros _ ].
unfold MVars, nats.
eapply Forall_map.
eapply Forall_seq; intros.
fv. omega.
Qed.
Lemma fv_MProjs:
forall k n t,
fv k t -> (* not an equivalence, as [k] could be zero *)
Forall (fv k) (MProjs n t).
Proof.
unfold MProjs. induction n; simpl; intros;
econstructor; [ rewrite fv_MProj |]; eauto.
Qed.
Hint Rewrite
fv_MTuple fv_MProj fv_MLetPair fv_MMultiLet_0
fv_MVars
(* not fv_MProjs *)
: fv.
(* -------------------------------------------------------------------------- *)
(* The following lemma is analogous to [fv_unaffected_regular], except it does
not have a regularity hypothesis, which makes it more pleasant to use. It is
proved by induction on terms, which is why we are unable to prove it in a
generic setting. *)
Lemma fv_unaffected:
forall t k sigma,
fv k t ->
t.[upn k sigma] = t.
Proof.
induction t; intros; fv; unpack; asimpl; repeat rewrite Nat.add_1_r in *;
try solve [ eauto using upn_k_sigma_x with typeclass_instances
| f_equal; eauto ].
Qed.
(* A corollary. *)
Lemma closed_unaffected:
forall t sigma,
closed t ->
t.[sigma] = t.
Proof.
unfold closed. intros.
rewrite <- (upn0 sigma).
eauto using fv_unaffected.
Qed.

125
coq/MyList.v Normal file
View file

@ -0,0 +1,125 @@
Require Import List.
Require Import MyTactics.
(* A few random additions to the [List] module, which is woefully incomplete. *)
(* -------------------------------------------------------------------------- *)
Lemma rev_cons_app:
forall {A} (x : A) xs ys,
rev (x :: xs) ++ ys = rev xs ++ x :: ys.
Proof.
intros. simpl. rewrite <- app_assoc. reflexivity.
Qed.
(* -------------------------------------------------------------------------- *)
Lemma length_nil:
forall A,
length (@nil A) = 0.
Proof.
reflexivity.
Qed.
Lemma length_cons:
forall A (x : A) xs,
length (x :: xs) = 1 + length xs.
Proof.
reflexivity.
Qed.
Hint Rewrite length_nil length_cons app_length map_length : length.
Ltac length :=
autorewrite with length in *;
try omega.
(* -------------------------------------------------------------------------- *)
(* We have [app_nth1] and [app_nth2], but the following lemma, which can be
viewed as a special case of [app_nth2], is missing. *)
Lemma app_nth:
forall {A} (xs ys : list A) x n,
n = length xs ->
nth n (xs ++ ys) x = nth 0 ys x.
Proof.
intros.
rewrite app_nth2 by omega.
replace (n - length xs) with 0 by omega.
reflexivity.
Qed.
(* -------------------------------------------------------------------------- *)
(* [rev_nats n] is the semi-open interval (n, 0], counted down. *)
(* It could also be defined as [rev (seq 0 n)], but a direct definition
is easier to work with, as it is immediately amenable to proofs by
induction. *)
Fixpoint rev_nats (n : nat) : list nat :=
match n with
| 0 =>
nil
| S n =>
n :: rev_nats n
end.
(* [nats n] is the semi-open interval [0, n), counted up. *)
Definition nats (n : nat) : list nat :=
seq 0 n.
(* These sequences have length [n]. *)
Lemma length_rev_nats:
forall n,
length (rev_nats n) = n.
Proof.
induction n; intros; simpl; [| rewrite IHn ]; eauto.
Qed.
Lemma length_nats:
forall n,
length (nats n) = n.
Proof.
unfold nats. intros. eauto using seq_length.
Qed.
(* -------------------------------------------------------------------------- *)
(* A few basic lemmas about [Forall]. *)
Lemma Forall_map:
forall A B (f : A -> B) (P : B -> Prop) xs,
Forall (fun x => P (f x)) xs ->
Forall P (map f xs).
Proof.
induction 1; intros; subst; simpl; econstructor; eauto.
Qed.
Lemma Forall_app:
forall A (P : A -> Prop) xs ys,
Forall P xs ->
Forall P ys ->
Forall P (xs ++ ys).
Proof.
induction 1; intros; subst; simpl; eauto.
Qed.
Lemma Forall_rev:
forall A (P : A -> Prop) xs,
Forall P xs ->
Forall P (rev xs).
Proof.
induction 1; intros; subst; simpl; eauto using Forall_app.
Qed.
Lemma Forall_seq:
forall (P : nat -> Prop) len start,
(forall i, start <= i < start + len -> P i) ->
Forall P (seq start len).
Proof.
induction len; intros; simpl; econstructor; eauto with omega.
Qed.

182
coq/MyTactics.v Normal file
View file

@ -0,0 +1,182 @@
Require Export Omega.
(* -------------------------------------------------------------------------- *)
(* [false] replaces the current goal with [False]. *)
Ltac false :=
elimtype False.
(* -------------------------------------------------------------------------- *)
(* [tc] is a shortcut for [eauto with typeclass_instances]. For some reason,
it is often necessary to use [rewrite ... by tc]. *)
Ltac tc :=
eauto with typeclass_instances.
(* -------------------------------------------------------------------------- *)
(* The tactic [obvious] does nothing by default, but can be extended with hints
so as to solve relatively easy goals -- e.g., proving that a term is a value,
proving a size inequality, proving that a substitution is a renaming, etc.
These predicates are sometimes interrelated (e.g., size is preserved by
renamings; the property of being a value is preserved by renamings) so it
would be counterproductive to distinguish several hint databases. *)
Create HintDb obvious.
Ltac obvious :=
eauto with obvious typeclass_instances.
(* -------------------------------------------------------------------------- *)
(* The tactic [pick R k] picks a hypothesis [h] whose statement is an
application of the inductive predicate [R], and passes [h] to the (Ltac)
continuation [k]. *)
Ltac pick R k :=
match goal with
| h: R _ |- _ => k h
| h: R _ _ |- _ => k h
| h: R _ _ _ |- _ => k h
| h: R _ _ _ _ |- _ => k h
| h: R _ _ _ _ _ |- _ => k h
end.
(* -------------------------------------------------------------------------- *)
(* The tactic [invert h] case-analyzes the hypothesis [h], whose statement
should be an application of an inductive predicate. *)
Ltac invert h :=
inversion h; clear h; try subst.
(* The tactic [inv R] looks for a hypothesis [h] whose statement is an
application of the inductive predicate [R], and case-analyzes this
hypothesis. *)
Ltac inv R :=
pick R invert.
(* -------------------------------------------------------------------------- *)
(* The tactic [unpack] decomposes conjunctions and existential quantifiers
in the hypotheses. Then, it attempts to perform substitutions, if possible. *)
Ltac unpack :=
repeat match goal with
| h: _ /\ _ |- _ =>
destruct h
| h: exists _, _ |- _ =>
destruct h
end;
try subst.
(* -------------------------------------------------------------------------- *)
(* The tactic [forward H] introduces the term [H] as a new hypothesis, and
unpacks it (if necessary). *)
Ltac forward H :=
generalize H; intro; unpack.
(* -------------------------------------------------------------------------- *)
(* [push h] moves the hypothesis [h] into the goal. *)
Ltac push h :=
generalize h; clear h.
(* [ltac_Mark] and [ltac_mark] are dummies. They are used as sentinels by
certain tactics, to mark a position in the context or in the goal. *)
Inductive ltac_Mark : Type :=
| ltac_mark : ltac_Mark.
(* [push_until_mark] moves all hypotheses from the context into the goal,
starting from the bottom and stopping as soon as a mark (that is, a
hypothesis of type [ltac_Mark]) is reached. The mark is thrown away. The
tactic fails if no mark appears in the context. *)
Ltac push_until_mark :=
match goal with h: ?T |- _ =>
match T with
| ltac_Mark => clear h
| _ => push h; push_until_mark
end end.
(** [pop_until_mark] moves all hypotheses from the goal into the context,
until a hypothesis of type [ltac_Mark] is reached. The mark is thrown
away. The tactic fails if no mark appears in the goal. *)
Ltac pop_until_mark :=
match goal with
| |- (ltac_Mark -> _) => intros _
| _ => intro; pop_until_mark
end.
Ltac injections :=
(* Place an initial mark, so as to not disturb the goal. *)
generalize ltac_mark;
(* Look at every equality hypothesis. *)
repeat match goal with
| h: _ = _ |- _ =>
(* Try to apply the primitive tactic [injection] to this hypothesis.
If this succeeds, clear [h] and replace it with the results of
[injection]. Another mark is used for this purpose. If this fails,
just push [h] into the goal, as we do not wish to see it any more. *)
first [
generalize ltac_mark; injection h; clear h; pop_until_mark
| push h ]
end;
(* Pop all of the hypotheses that have been set aside above. *)
pop_until_mark.
(* -------------------------------------------------------------------------- *)
(* The following incantation means that [eauto with omega] can solve a goal
of the form [_ < _]. The tactic [zify] is a preprocessor which increases
the number of goals that [omega] can accept; e.g., it expands away [min]
and [max]. *)
Hint Extern 1 (le _ _) => (zify; omega) : omega.
(* -------------------------------------------------------------------------- *)
(* A little extra help for [eauto with omega]. *)
Lemma arith_le_SS: forall x y, x < y -> S x < S y.
Proof. intros. omega. Qed.
Lemma arith_SS_le: forall x y, S x < S y -> x < y.
Proof. intros. omega. Qed.
Hint Resolve arith_le_SS arith_SS_le : omega.
(* -------------------------------------------------------------------------- *)
(* [dblib_by_cases] simplifies goals in which a decidable integer comparison
appears. *)
Ltac dblib_intro_case_clear :=
let h := fresh in
intro h; case h; clear h.
Ltac dblib_inspect_cases :=
match goal with
| |- context [le_gt_dec ?n ?n'] =>
case (le_gt_dec n n')
| h: context [le_gt_dec ?n ?n'] |- _ =>
revert h; case (le_gt_dec n n'); intro h
| |- context [eq_nat_dec ?n ?n'] =>
case (eq_nat_dec n n')
| h: context [eq_nat_dec ?n ?n'] |- _ =>
revert h; case (eq_nat_dec n n'); intro h
| |- context [(lt_eq_lt_dec ?n ?n')] =>
case (lt_eq_lt_dec n n'); [ dblib_intro_case_clear | idtac ]
| h: context [(lt_eq_lt_dec ?n ?n')] |- _ =>
revert h; case (lt_eq_lt_dec n n'); [ dblib_intro_case_clear | idtac ]; intro h
end.
Ltac dblib_by_cases :=
repeat dblib_inspect_cases; try solve [ intros; elimtype False; omega ]; intros.

120
coq/Option.v Normal file
View file

@ -0,0 +1,120 @@
(* -------------------------------------------------------------------------- *)
(* The [bind] combinator of the option monad. *)
Definition bind {A B} (f : option A) (k : A -> option B) : option B :=
match f with
| None =>
None
| Some a =>
k a
end.
(* The standard syntactic sugar for [bind]. [f >>= k] can be read as ``first
do [f]; then, if successful, with the result of [f], do [k]''. *)
Notation "f >>= k" := (bind f k) (at level 55).
(* -------------------------------------------------------------------------- *)
(* These lemmas help prove an equation of the form [f >>= k = b]. *)
Lemma prove_bind_None:
forall {A B} {f} {k : A -> option B},
f = None ->
f >>= k = None.
Proof.
intros. subst. eauto.
Qed.
Lemma prove_bind_Some:
forall {A B} {f} {k : A -> option B} {a b},
f = Some a ->
k a = b ->
f >>= k = b.
Proof.
intros. subst. eauto.
Qed.
(* This lemma helps exploit an equation of the form [f >>= k = Some b]. *)
Lemma invert_bind_Some:
forall {A B} {f} {k : A -> option B} {b},
f >>= k = Some b ->
exists a, f = Some a /\ k a = Some b.
Proof.
destruct f; simpl; intros.
{ eauto. }
{ congruence. }
Qed.
Ltac invert_bind_Some :=
match goal with
h: ?f >>= _ = Some _ |- _ =>
let heq := fresh in
generalize (invert_bind_Some h); clear h; intros (?&?&h)
end.
(* -------------------------------------------------------------------------- *)
(* The standard ordering on options, where [None] is less defined then
everything, and every element of the form [Some a] is less defined
than itself only. *)
Definition less_defined {A} (o1 o2 : option A) :=
forall a, o1 = Some a -> o2 = Some a.
(* -------------------------------------------------------------------------- *)
(* This lemma exploits an assertion of the form [less_defined (Some _) _]. *)
Lemma invert_less_defined_Some:
forall {A} {a : A} {o : option A},
less_defined (Some a) o ->
Some a = o.
Proof.
unfold less_defined. intros. symmetry. eauto.
Qed.
Ltac invert_less_defined :=
match goal with
| h: less_defined (Some _) _ |- _ =>
generalize (invert_less_defined_Some h); clear h; intro h
end.
(* -------------------------------------------------------------------------- *)
(* These lemmas help prove assertions of the form [less_defined _ _]. *)
Lemma prove_less_defined_None:
forall {A} {o : option A},
less_defined None o.
Proof.
unfold less_defined. intros. congruence.
Qed.
Lemma reflexive_less_defined:
forall {A} {o : option A},
less_defined o o.
Proof.
unfold less_defined. eauto.
Qed.
Local Hint Extern 1 (_ <> _) => congruence : congruence.
Lemma prove_less_defined_bind:
forall {A B} {f1 f2 : option A} {k1 k2 : A -> option B},
less_defined f1 f2 ->
(f1 <> None -> forall a, less_defined (k1 a) (k2 a)) ->
less_defined (f1 >>= k1) (f2 >>= k2).
Proof.
intros. destruct f1; simpl in *.
(* Case: [f1] is [Some _]. *)
{ invert_less_defined. subst. simpl. eauto with congruence. }
(* Case: [f1] is [None]. *)
{ eauto using prove_less_defined_None. }
Qed.
Hint Resolve
prove_less_defined_None reflexive_less_defined prove_less_defined_bind
: less_defined.

17
coq/README.md Normal file
View file

@ -0,0 +1,17 @@
This code has been tested with Coq 8.5pl3.
For now, this code requires my slightly patched version of Autosubst.
To install this library, proceed as follows:
```
git clone git@github.com:fpottier/autosubst.git
cd autosubst
make && make install
```
You can then compile the Coq code as follows:
```
make _CoqProject
make -j4
```

498
coq/Relations.v Normal file
View file

@ -0,0 +1,498 @@
Require Import Coq.Setoids.Setoid.
Require Import MyTactics.
Require Import Sequences.
(* This file offers a few definitions and tactics that help deal with
relations and commutative diagrams. *)
(* -------------------------------------------------------------------------- *)
Section Relations.
Context {A : Type}.
Implicit Types R S : A -> A -> Prop.
(* Composition of relations. *)
Definition composition R S a c :=
exists b, R a b /\ S b c.
(* Transposition of relations. *)
Definition transpose R a b :=
R b a.
(* Inclusion of relations. *)
Definition inclusion R S :=
forall a b, R a b -> S a b.
(* A typical (square) commutative diagram, where the composition [R; S] can be
replaced with the composition [S; R]. This notion can be stated in several
equivalent ways; see [commutation22_eq] and [commutation22_reverse]. *)
Definition commutation22 R S S' R' :=
forall a1 b1,
R a1 b1 ->
forall b2,
S b1 b2 ->
exists a2,
S' a1 a2 /\ R' a2 b2.
(* A typical diamond diagram, where a divergence [R | S] is resolved
via [S' | R']. *)
Definition diamond22 R S R' S' :=
forall a1 b1,
R a1 b1 ->
forall a2,
S a1 a2 ->
exists b2,
R' a2 b2 /\ S' b1 b2.
Definition diamond R :=
diamond22 R R R R.
End Relations.
(* -------------------------------------------------------------------------- *)
(* The tactic [forward1 lemma] applies [lemma], forwards, to a hypothesis
found in the context. The lemma must have one hypothesis. *)
Ltac forward1 lemma :=
match type of lemma with
| (forall _ _, ?R _ _ -> _) =>
match goal with hR: R ?a1 ?b1 |- _ =>
generalize (lemma _ _ hR); intro
end
| (forall _, ?R _ _ -> _) =>
match goal with hR: R ?a1 ?b1 |- _ =>
generalize (lemma _ hR); intro
end
end;
unpack.
(* The tactic [forward2 lemma] applies [lemma], forwards, to two hypotheses
found in the context. The lemma must be a commutation lemma or a diamond
lemma, as defined above. *)
Ltac forward2 lemma :=
match type of lemma with
| (forall a1 b1, ?R a1 b1 -> forall b2, ?S b1 b2 -> _) =>
match goal with hR: R ?a1 ?b1, hS: S ?b1 ?b2 |- _ =>
generalize (lemma _ _ hR _ hS); intro
end
| commutation22 ?R ?S _ _ =>
match goal with hR: R ?a1 ?b1, hS: S ?b1 ?b2 |- _ =>
generalize (lemma _ _ hR _ hS); intro
end
| (forall a1 b1, ?R a1 b1 -> forall a2, ?S a1 a2 -> _) =>
match goal with hR: R ?a1 ?b1, hS: S ?a1 ?a2 |- _ =>
generalize (lemma _ _ hR _ hS); intro
end
| diamond22 ?R ?S _ _ =>
match goal with hR: R ?a1 ?b1, hS: S ?a1 ?a2 |- _ =>
generalize (lemma _ _ hR _ hS); intro
end
| diamond ?R =>
match goal with hR: R ?a1 ?b1, hS: R ?a1 ?a2 |- _ =>
generalize (lemma _ _ hR _ hS); intro
end
end;
unpack.
(* -------------------------------------------------------------------------- *)
Section RelationLemmas.
Context {A : Type}.
Implicit Types R S : A -> A -> Prop.
(* Inclusion of relations is transitive. *)
Lemma inclusion_transitive:
forall R S T,
inclusion R S ->
inclusion S T ->
inclusion R T.
Proof.
unfold inclusion. eauto.
Qed.
(* [star] is covariant with respect to inclusion. *)
Lemma star_covariant_inclusion:
forall R S,
inclusion R S ->
inclusion (star R) (star S).
Proof.
unfold inclusion. eauto using star_covariant.
Qed.
(* If [R] is reflexive and transitive, then [star R] is [R]. *)
Lemma star_of_reflexive_transitive_relation:
forall {A} (R : A -> A -> Prop),
(forall a, R a a) ->
(forall a b c, R a b -> R b c -> R a c) ->
inclusion (star R) R.
Proof.
intros. induction 1; eauto.
Qed.
(* Thus, [star (star R)] is [star R]. *)
Lemma inclusion_star_star:
forall {A} (R : A -> A -> Prop),
inclusion (star (star R)) (star R).
Proof.
intros.
eapply star_of_reflexive_transitive_relation; eauto with sequences.
Qed.
(* Composition is associative. *)
Lemma composition_assoc_direct:
forall R S T,
inclusion
(composition R (composition S T))
(composition (composition R S) T).
Proof.
unfold inclusion, composition. intros. unpack. eauto.
Qed.
Lemma composition_assoc_reverse:
forall R S T,
inclusion
(composition (composition R S) T)
(composition R (composition S T)).
Proof.
unfold inclusion, composition. intros. unpack. eauto.
Qed.
(* Composition is covariant. *)
Lemma composition_covariant:
forall R1 R2 S1 S2,
inclusion R1 R2 ->
inclusion S1 S2 ->
inclusion (composition R1 S1) (composition R2 S2).
Proof.
unfold inclusion, composition. intros. unpack. eauto.
Qed.
(* A commutative diagram can be stated in terms of inclusion of relations. *)
Lemma commutation22_eq:
forall R S S' R',
commutation22 R S S' R' <->
inclusion (composition R S) (composition S' R').
Proof.
intros. unfold commutation22, inclusion, composition.
split; intros; unpack.
{ forward2 H. eauto. }
{ eauto. }
Qed.
(* Thus, two commutative diagrams can be glued. *)
Lemma commutation22_transitive:
forall R S S' R' S'' R'',
commutation22 R S S' R' ->
commutation22 S' R' S'' R'' ->
commutation22 R S S'' R''.
Proof.
intros. rewrite !commutation22_eq in *.
eauto using inclusion_transitive.
Qed.
(* A commutation diagram can also be stated with its two hypotheses in reverse
order. This can be useful, e.g. when the diagram must be established by
induction on the second hypothesis. *)
Lemma commutation22_reverse:
forall R S S' R',
commutation22 R S S' R' <->
(
forall b1 b2,
S b1 b2 ->
forall a1,
R a1 b1 ->
exists a2,
S' a1 a2 /\ R' a2 b2
).
Proof.
unfold commutation22. split; eauto.
Qed.
(* [commutation22 R S S' R'] is contravariant in [R] and [S] and
covariant in [S'] and [R']. *)
Lemma commutation22_variance:
forall R1 S1 S'1 R'1 R2 S2 S'2 R'2,
commutation22 R1 S1 S'1 R'1 ->
(forall a b, R2 a b -> R1 a b) ->
(forall a b, S2 a b -> S1 a b) ->
(forall a b, S'1 a b -> S'2 a b) ->
(forall a b, R'1 a b -> R'2 a b) ->
commutation22 R2 S2 S'2 R'2.
Proof.
do 8 intro. intros Hcomm. do 4 intro. intros a1 b1 ? b2 ?.
assert (R1 a1 b1). { eauto. }
assert (S1 b1 b2). { eauto. }
forward2 Hcomm. eauto.
Qed.
(* If [S] can move left through [R], giving rise to (zero or more) [S'],
then [star S] can move left through [R] in the same manner. Think of
many [S] sheep jumping right-to-left above one [R] barrier. *)
(* If [R S ] rewrites to [S'* R]
then [R S*] rewrites to [S'* R]. *)
(* If desired, [star S'] could be replaced in this statement with any
reflexive and transitive relation. *)
Lemma commute_R_Sstar:
forall {R S S'},
commutation22
R S
(star S') R
->
commutation22
R (star S)
(star S') R.
Proof.
intros ? ? ? Hdiagram.
rewrite commutation22_reverse.
induction 1; intros.
{ eauto with sequences. }
{ forward2 Hdiagram.
forward1 IHstar.
eauto with sequences. }
Qed.
(* An analogous result, with [plus] instead of [star]. *)
(* If [R S ] rewrites to [S'+ R]
then [R S+] rewrites to [S'+ R]. *)
(* If desired, [plus S'] could be replaced in this statement with any
transitive relation. *)
Lemma commute_R_Splus:
forall {R S S'},
commutation22
R S
(plus S') R
->
commutation22
R (plus S)
(plus S') R.
Proof.
intros ? ? ? Hcomm.
rewrite commutation22_reverse.
induction 1 using plus_ind_direct; intros.
(* Case: one step. *)
{ forward2 Hcomm. eauto. }
(* Case: more than one step. *)
{ forward2 Hcomm.
forward1 IHplus.
eauto with sequences. }
Qed.
(* If [S] can move left through [R], giving rise to (zero or more) [S],
then [S] can move left through [star R]. Think of many [S] sheep jumping
right-to-left above many [R] barriers. *)
(* If [R S ] rewrites to [S* R ]
then [R* S*] rewrites to [S* R*]. *)
Lemma commute_Rstar_Sstar:
forall {R S},
commutation22
R S
(star S) R
->
commutation22
(star R) (star S)
(star S) (star R).
Proof.
intros ? ? Hdiagram.
induction 1; intros.
{ eauto with sequences. }
{ forward1 IHstar.
forward2 (commute_R_Sstar Hdiagram).
eauto with sequences. }
Qed.
(* If [R S] rewrites to [S+ R ]
then [R* S] rewrites to [S+ R*]. *)
Lemma commute_Rstar_S:
forall {R S},
commutation22
R S
(plus S) R
->
commutation22
(star R) S
(plus S) (star R).
Proof.
intros ? ? Hdiagram.
induction 1; intros.
{ eauto with sequences. }
{ forward1 IHstar.
forward2 (commute_R_Splus Hdiagram).
eauto with sequences. }
Qed.
(* If [R S ] rewrites to [S+ R ]
then [R* S+] rewrites to [S+ R*]. *)
Lemma commute_Rstar_Splus:
forall {R S},
commutation22
R S
(plus S) R
->
commutation22
(star R) (plus S)
(plus S) (star R).
Proof.
intros ? ? Hdiagram.
assert (Hdiagram2:
commutation22
(star R) (star S)
(star S) (star R)
).
{ eapply commute_Rstar_Sstar.
eauto using commutation22_variance with sequences. }
(* We have [R* S+]. *)
induction 2; intros.
(* We have [R* S S*]. *)
forward2 (commute_Rstar_S Hdiagram).
(* We have [S+ R* S*]. *)
forward2 Hdiagram2.
(* We have [S+ S* R*]. *)
eauto with sequences.
Qed.
(* [transpose] is involutive. *)
Lemma transpose_transpose:
forall R,
transpose (transpose R) = R.
Proof.
reflexivity. (* it's just eta-expansion *)
Qed.
(* [diamond22] can be viewed as an instance of [commutation22]. *)
Lemma diamond22_as_commutation22:
forall R S R' S',
diamond22 R S R' S' <->
commutation22 (transpose R) S S' (transpose R').
Proof.
unfold diamond22, commutation22. split; intros H; intros.
{ unfold transpose in *. forward2 H. eauto. }
{ assert (transpose R b1 a1). { eauto. }
forward2 H. eauto. }
Qed.
Lemma commutation22_as_diamond22:
forall R S R' S',
commutation22 R S S' R' <->
diamond22 (transpose R) S (transpose R') S'.
Proof.
intros.
rewrite diamond22_as_commutation22.
rewrite !transpose_transpose. tauto.
Qed.
(* [diamond22 is symmetric. *)
Lemma diamond22_symmetric:
forall R S R' S',
diamond22 R S R' S' ->
diamond22 S R S' R'.
Proof.
intros ? ? ? ? Hcon.
unfold diamond22. intros.
forward2 Hcon. eauto.
Qed.
(* If [R] is diamond, then [star R] is diamond. *)
Lemma star_diamond_left:
forall R R' S,
diamond22 R S R' S ->
diamond22 (star R) S (star R') S.
Proof.
intros R R' S Hcon. induction 1; intros.
{ eauto with sequences. }
{ forward2 Hcon. forward1 IHstar. eauto with sequences. }
Qed.
Lemma star_diamond_right:
forall R S S',
diamond22 R S R S' ->
diamond22 R (star S) R (star S').
Proof.
eauto using star_diamond_left, diamond22_symmetric.
Qed.
Lemma star_diamond_both:
forall R S,
diamond22 R S R S ->
diamond22 (star R) (star S) (star R) (star S).
Proof.
eauto using star_diamond_left, star_diamond_right.
Qed.
Lemma star_diamond:
forall R,
diamond R ->
diamond (star R).
Proof.
unfold diamond. eauto using star_diamond_both.
Qed.
(* If, through a simulation diagram, a step of [R] in the source is
translated to (at least) one step of [R'] in the target, then
divergence in the source implies divergence in the target. *)
Lemma infseq_simulation:
forall R R' S,
diamond22 R S R' S ->
forall a,
infseq R a ->
forall b,
S a b ->
infseq R' b.
Proof.
intros.
eapply infseq_coinduction_principle
with (P := fun b => exists a, S a b /\ infseq R a); [| eauto ].
clear dependent a. clear b. intros b (a&?&?).
pick infseq invert.
pick @diamond22 forward2.
eauto with sequences.
Qed.
Lemma infseq_simulation_plus:
forall R R' S,
diamond22 R S (plus R') S ->
forall a,
infseq R a ->
forall b,
S a b ->
infseq R' b.
Proof.
eauto using infseq_simulation, infseq_plus.
Qed.
End RelationLemmas.

321
coq/Sequences.v Normal file
View file

@ -0,0 +1,321 @@
(** A library of relation operators defining sequences of transitions
and useful properties about them. Originally by Xavier Leroy, with
some improvements and additions by François Pottier. *)
Set Implicit Arguments.
Section SEQUENCES.
Variable A: Type.
Implicit Types R S : A -> A -> Prop.
Implicit Types P : A -> Prop.
(** Zero, one or several transitions: reflexive, transitive closure of [R]. *)
Inductive star R : A -> A -> Prop :=
| star_refl:
forall a,
star R a a
| star_step:
forall a b c,
R a b -> star R b c -> star R a c.
Hint Constructors star.
Lemma star_refl_eq:
forall R a b, a = b -> star R a b.
Proof.
intros. subst. eauto.
Qed.
Lemma star_one:
forall R a b, R a b -> star R a b.
Proof.
eauto.
Qed.
Lemma star_trans:
forall R a b, star R a b ->
forall c, star R b c -> star R a c.
Proof.
induction 1; eauto.
Qed.
Lemma star_covariant:
forall R S,
(forall a b, R a b -> S a b) ->
(forall a b, star R a b -> star S a b).
Proof.
induction 2; eauto.
Qed.
(* If [R] preserves some property [P], then [star R] preserves [P]. *)
Lemma star_implication:
forall P R,
(forall a1 a2, R a1 a2 -> P a1 -> P a2) ->
(forall a1 a2, star R a1 a2 -> P a1 -> P a2).
Proof.
induction 2; eauto.
Qed.
(* The same implication holds in the reverse direction (right to left). *)
Lemma star_implication_reversed:
forall P R,
(forall a1 a2, R a1 a2 -> P a2 -> P a1) ->
(forall a1 a2, star R a1 a2 -> P a2 -> P a1).
Proof.
induction 2; eauto.
Qed.
(** One or several transitions: transitive closure of [R]. *)
Inductive plus R: A -> A -> Prop :=
| plus_left:
forall a b c,
R a b -> star R b c -> plus R a c.
Hint Constructors plus.
Lemma plus_one:
forall R a b, R a b -> plus R a b.
Proof.
eauto.
Qed.
Lemma plus_star:
forall R a b, plus R a b -> star R a b.
Proof.
inversion 1; eauto.
Qed.
Lemma plus_covariant:
forall R S,
(forall a b, R a b -> S a b) ->
(forall a b, plus R a b -> plus S a b).
Proof.
induction 2; eauto using star_covariant.
Qed.
(* A direct induction principle for [plus]: when [plus R a b] holds,
either there is just one step, or there is one, followed with more. *)
Lemma plus_ind_direct:
forall R P : A -> A -> Prop,
(forall a b, R a b -> P a b) ->
(forall a b c, R a b -> plus R b c -> P b c -> P a c) ->
forall a b, plus R a b -> P a b.
Proof.
intros ? ? Hone Hmore a c Hplus. destruct Hplus as [ ? b ? hR hRStar ].
generalize b c hRStar a hR.
clear b c hRStar a hR.
induction 1; eauto.
Qed.
Lemma plus_star_trans:
forall R a b c, plus R a b -> star R b c -> plus R a c.
Proof.
inversion 1; eauto using star_trans.
Qed.
Lemma star_plus_trans:
forall R a b c, star R a b -> plus R b c -> plus R a c.
Proof.
inversion 1; inversion 1; eauto using star_trans.
Qed.
Lemma plus_trans:
forall R a b c, plus R a b -> plus R b c -> plus R a c.
Proof.
eauto using plus_star_trans, plus_star.
Qed.
Lemma plus_right:
forall R a b c, star R a b -> R b c -> plus R a c.
Proof.
eauto using star_plus_trans.
Qed.
(** Absence of transitions. *)
Definition irred R a :=
forall b, ~ R a b.
Definition halts R a :=
exists b, star R a b /\ irred R b.
(** Infinitely many transitions. *)
CoInductive infseq R : A -> Prop :=
| infseq_step:
forall a b,
R a b -> infseq R b -> infseq R a.
(** Properties of [irred]. *)
Lemma irred_irred:
forall R t1 u1,
irred R t1 ->
(forall u2, R u1 u2 -> exists t2, R t1 t2) ->
irred R u1.
Proof.
unfold irred. intros ? ? ? Hirred Himpl u2 Hu2.
destruct (Himpl _ Hu2) as [ t2 Ht2 ].
eapply Hirred. eauto.
Qed.
Lemma irreducible_terms_do_not_reduce:
forall R a b, irred R a -> R a b -> False.
Proof.
unfold irred, not. eauto.
Qed.
(** Coinduction principles to show the existence of infinite sequences. *)
Lemma infseq_coinduction_principle:
forall R P,
(forall a, P a -> exists b, R a b /\ P b) ->
forall a, P a -> infseq R a.
Proof.
intros ? ? Hstep. cofix COINDHYP; intros a hPa.
destruct (Hstep a hPa) as (?&?&?).
econstructor; eauto.
Qed.
Lemma infseq_coinduction_principle_2:
forall R P a,
P a ->
(forall a, P a -> exists b, plus R a b /\ P b) ->
infseq R a.
Proof.
intros ? ? ? ? Hinv.
apply infseq_coinduction_principle with
(P := fun a => exists b, star R a b /\ P b).
(* Proof that the invariant is preserved. *)
{ clear dependent a.
intros a (b&hStar&hPb).
inversion hStar; subst.
{ destruct (Hinv b hPb) as [c [hPlus ?]].
inversion hPlus; subst. eauto. }
{ eauto. }
}
(* Proof that the invariant initially holds. *)
{ eauto. }
Qed.
Lemma infseq_plus:
forall R a,
infseq (plus R) a ->
infseq R a.
Proof.
intros. eapply infseq_coinduction_principle_2
with (P := fun a => infseq (plus R) a).
{ eauto. }
clear dependent a. intros a hInfSeq.
destruct hInfSeq. eauto.
Qed.
(** An example of use of [infseq_coinduction_principle]. *)
Lemma infseq_alternate_characterization:
forall R a,
(forall b, star R a b -> exists c, R b c) ->
infseq R a.
Proof.
intros R. apply infseq_coinduction_principle.
intros a Hinv. destruct (Hinv a); eauto.
Qed.
Lemma infseq_covariant:
forall R S,
(forall a b, R a b -> S a b) ->
forall a, infseq R a -> infseq S a.
Proof.
intros. eapply infseq_coinduction_principle
with (P := fun a => infseq R a); [| eauto ].
clear dependent a. intros a hInfSeq.
destruct hInfSeq. eauto.
Qed.
(** A sequence either is infinite or stops on an irreducible term.
This property needs excluded middle from classical logic. *)
Require Import Classical.
Lemma infseq_or_finseq:
forall R a,
infseq R a \/ halts R a.
Proof.
intros.
destruct (classic (forall b, star R a b -> exists c, R b c)).
{ left. eauto using infseq_alternate_characterization. }
{ right.
destruct (not_all_ex_not _ _ H) as [b Hb].
destruct (imply_to_and _ _ Hb).
unfold halts, irred, not. eauto. }
Qed.
(** Additional properties for deterministic transition relations. *)
Section DETERMINISM.
Variable R : A -> A -> Prop.
Hypothesis R_determ: forall a b c, R a b -> R a c -> b = c.
Ltac R_determ :=
match goal with h1: R ?a ?b1, h2: R ?a ?b2 |- _ =>
assert (b1 = b2); [ eauto | subst ]
end.
(** Uniqueness of transition sequences. *)
Lemma star_star_inv:
forall a b, star R a b -> forall c, star R a c -> star R b c \/ star R c b.
Proof.
induction 1; inversion 1; intros; subst; try R_determ; eauto.
Qed.
Lemma finseq_unique:
forall a b b',
star R a b -> irred R b ->
star R a b' -> irred R b' ->
b = b'.
Proof.
unfold irred, not.
intros ? ? ? Hab Hirred Hab' Hirred'.
destruct (star_star_inv Hab Hab') as [ Hbb' | Hbb' ];
inversion Hbb'; subst;
solve [ eauto | elimtype False; eauto ].
Qed.
Lemma infseq_star_inv:
forall a b, star R a b -> infseq R a -> infseq R b.
Proof.
induction 1; inversion 1; intros; try R_determ; eauto.
Qed.
Lemma infseq_finseq_excl:
forall a b,
star R a b -> irred R b -> infseq R a -> False.
Proof.
unfold irred, not. intros.
assert (h: infseq R b). { eauto using infseq_star_inv. }
inversion h. eauto.
Qed.
Lemma infseq_halts_excl:
forall a,
halts R a -> infseq R a -> False.
Proof.
intros ? (?&?&?). eauto using infseq_finseq_excl.
Qed.
End DETERMINISM.
End SEQUENCES.
Hint Resolve star_refl star_step star_one star_trans plus_left plus_one
plus_star plus_star_trans star_plus_trans plus_right: sequences.

164
ocaml/EvalCBNCPS.ml Normal file
View file

@ -0,0 +1,164 @@
(* -------------------------------------------------------------------------- *)
(* The type of lambda-terms, in de Bruijn's representation. *)
type var = int (* a de Bruijn index *)
type term =
| Var of var
| Lam of (* bind: *) term
| App of term * term
| Let of (* bind: *) term * term
(* -------------------------------------------------------------------------- *)
(* Under a call-by-name regime, in a function call, the actual argument is not
evaluated immediately; instead, a thunk is built (a pair of the argument
and the environment in which it must be evaluated). Thus, an environment is
a list of thunks. As in call-by-value, a closure is a pair of a term and an
environment. (Closures and thunks differ in that a closure binds a
variable, the formal argument, in the term. A thunk does not.) *)
type cvalue =
| Clo of (* bind: *) term * cenv
and cenv =
thunk list
and thunk =
| Thunk of term * cenv
(* -------------------------------------------------------------------------- *)
(* Environments. *)
let empty : cenv =
[]
exception RuntimeError
let lookup (e : cenv) (x : var) : thunk =
try
List.nth e x
with Failure _ ->
raise RuntimeError
(* -------------------------------------------------------------------------- *)
(* An environment-based big-step call-by-name interpreter. *)
let rec eval (e : cenv) (t : term) : cvalue =
match t with
| Var x ->
let Thunk (t, e) = lookup e x in
eval e t
| Lam t ->
Clo (t, e)
| App (t1, t2) ->
let cv1 = eval e t1 in
let Clo (u1, e') = cv1 in
eval (Thunk(t2, e) :: e') u1
| Let (t1, t2) ->
eval (Thunk (t1, e) :: e) t2
(* -------------------------------------------------------------------------- *)
(* The CPS-transformed interpreter. *)
let rec evalk (e : cenv) (t : term) (k : cvalue -> 'a) : 'a =
match t with
| Var x ->
let Thunk (t, e) = lookup e x in
evalk e t k
| Lam t ->
k (Clo (t, e))
| App (t1, t2) ->
evalk e t1 (fun cv1 ->
let Clo (u1, e') = cv1 in
evalk (Thunk(t2, e) :: e') u1 k)
| Let (t1, t2) ->
evalk (Thunk (t1, e) :: e) t2 k
let eval (e : cenv) (t : term) : cvalue =
evalk e t (fun cv -> cv)
(* -------------------------------------------------------------------------- *)
(* The CPS-transformed, defunctionalized interpreter. *)
type kont =
| AppL of { e: cenv; t2: term; k: kont }
| Init
let rec evalkd (e : cenv) (t : term) (k : kont) : cvalue =
match t with
| Var x ->
let Thunk (t, e) = lookup e x in
evalkd e t k
| Lam t ->
apply k (Clo (t, e))
| App (t1, t2) ->
evalkd e t1 (AppL { e; t2; k })
| Let (t1, t2) ->
evalkd (Thunk (t1, e) :: e) t2 k
and apply (k : kont) (cv : cvalue) : cvalue =
match k with
| AppL { e; t2; k } ->
let cv1 = cv in
let Clo (u1, e') = cv1 in
evalkd (Thunk(t2, e) :: e') u1 k
| Init ->
cv
let eval (e : cenv) (t : term) : cvalue =
evalkd e t Init
(* -------------------------------------------------------------------------- *)
(* Because [apply] has only one call site, it can be inlined, yielding a
slightly more compact and readable definition. *)
let rec evalkd (e : cenv) (t : term) (k : kont) : cvalue =
match t, k with
| Var x, _ ->
let Thunk (t, e) = lookup e x in
evalkd e t k
| Lam t, AppL { e; t2; k } ->
let cv1 = Clo (t, e) in
let Clo (u1, e') = cv1 in
evalkd (Thunk(t2, e) :: e') u1 k
| Lam t, Init ->
Clo (t, e)
| App (t1, t2), _ ->
evalkd e t1 (AppL { e; t2; k })
| Let (t1, t2), _ ->
evalkd (Thunk (t1, e) :: e) t2 k
let eval (e : cenv) (t : term) : cvalue =
evalkd e t Init
(* -------------------------------------------------------------------------- *)
(* The type [kont] is isomorphic to [(cenv * term) list]. Using the latter
type makes the code slightly prettier, although slightly less efficient. *)
(* At this point, one recognizes Krivine's machine. *)
let rec evalkd (e : cenv) (t : term) (k : (cenv * term) list) : cvalue =
match t, k with
| Var x, _ ->
let Thunk (t, e) = lookup e x in
evalkd e t k
| Lam t, (e, t2) :: k ->
let cv1 = Clo (t, e) in
let Clo (u1, e') = cv1 in
evalkd (Thunk(t2, e) :: e') u1 k
| Lam t, [] ->
Clo (t, e)
| App (t1, t2), _ ->
evalkd e t1 ((e, t2) :: k)
| Let (t1, t2), _ ->
evalkd (Thunk (t1, e) :: e) t2 k
let eval (e : cenv) (t : term) : cvalue =
evalkd e t []

208
ocaml/EvalCBVCPS.ml Normal file
View file

@ -0,0 +1,208 @@
(* -------------------------------------------------------------------------- *)
(* The type of lambda-terms, in de Bruijn's representation. *)
type var = int (* a de Bruijn index *)
type term =
| Var of var
| Lam of (* bind: *) term
| App of term * term
| Let of (* bind: *) term * term
(* -------------------------------------------------------------------------- *)
(* An environment-based big-step interpreter. This is the same interpreter
that we programmed in Coq, except here, in OCaml, fuel is not needed. *)
type cvalue =
| Clo of (* bind: *) term * cenv
and cenv =
cvalue list
let empty : cenv =
[]
exception RuntimeError
let lookup (e : cenv) (x : var) : cvalue =
try
List.nth e x
with Failure _ ->
raise RuntimeError
let rec eval (e : cenv) (t : term) : cvalue =
match t with
| Var x ->
lookup e x
| Lam t ->
Clo (t, e)
| App (t1, t2) ->
let cv1 = eval e t1 in
let cv2 = eval e t2 in
let Clo (u1, e') = cv1 in
eval (cv2 :: e') u1
| Let (t1, t2) ->
eval (eval e t1 :: e) t2
(* -------------------------------------------------------------------------- *)
(* Term/value/environment printers. *)
open Printf
let rec print_term f = function
| Var x ->
fprintf f "(Var %d)" x
| Lam t ->
fprintf f "(Lam %a)" print_term t
| App (t1, t2) ->
fprintf f "(App %a %a)" print_term t1 print_term t2
| Let (t1, t2) ->
fprintf f "(Let %a %a)" print_term t1 print_term t2
let rec print_cvalue f = function
| Clo (t, e) ->
fprintf f "< %a | %a >" print_term t print_cenv e
and print_cenv f = function
| [] ->
fprintf f "[]"
| cv :: e ->
fprintf f "%a :: %a" print_cvalue cv print_cenv e
let print_cvalue cv =
fprintf stdout "%a\n" print_cvalue cv
(* -------------------------------------------------------------------------- *)
(* A tiny test suite. *)
let id =
Lam (Var 0)
let idid =
App (id, id)
let apply =
Lam (Lam (App (Var 1, Var 0)))
let test1 eval t =
print_cvalue (eval empty t)
let test name eval =
printf "Testing %s...\n%!" name;
test1 eval idid;
test1 eval (App (apply, id));
test1 eval (App (App (apply, id), id));
()
(* -------------------------------------------------------------------------- *)
(* Test. *)
let () =
test "the direct-style evaluator" eval
(* -------------------------------------------------------------------------- *)
(* A CPS-transformed, environment-based big-step interpreter. *)
(* In this code, every recursive call to [evalk] is a tail call. Thus,
it is compiled by the OCaml compiler to a loop, and requires only O(1)
space on the OCaml stack. *)
let rec evalk (e : cenv) (t : term) (k : cvalue -> 'a) : 'a =
match t with
| Var x ->
k (lookup e x)
| Lam t ->
k (Clo (t, e))
| App (t1, t2) ->
evalk e t1 (fun cv1 ->
evalk e t2 (fun cv2 ->
let Clo (u1, e') = cv1 in
evalk (cv2 :: e') u1 k))
| Let (t1, t2) ->
evalk e t1 (fun cv1 ->
evalk (cv1 :: e) t2 k)
(* It is possible to explicitly assert that these calls are tail calls.
The compiler would tell us if we were wrong. *)
let rec evalk (e : cenv) (t : term) (k : cvalue -> 'a) : 'a =
match t with
| Var x ->
(k[@tailcall]) (lookup e x)
| Lam t ->
(k[@tailcall]) (Clo (t, e))
| App (t1, t2) ->
(evalk[@tailcall]) e t1 (fun cv1 ->
(evalk[@tailcall]) e t2 (fun cv2 ->
let Clo (u1, e') = cv1 in
(evalk[@tailcall]) (cv2 :: e') u1 k))
| Let (t1, t2) ->
(evalk[@tailcall]) e t1 (fun cv1 ->
(evalk[@tailcall]) (cv1 :: e) t2 k)
let eval (e : cenv) (t : term) : cvalue =
evalk e t (fun cv -> cv)
(* -------------------------------------------------------------------------- *)
(* Test. *)
let () =
test "the CPS evaluator" eval
(* -------------------------------------------------------------------------- *)
(* The above code uses heap-allocated closures, which form a linked list in the
heap. In fact, the interpreter's "stack" is now heap-allocated. To see this
more clearly, let us defunctionalize the CPS-transformed interpreter. *)
(* There are four places in the above code where an anonymous continuation is
built, so defunctionalization yields a data type of four possible kinds of
continuations. This data type describes a linked list of stack frames! *)
type kont =
| AppL of { e: cenv; t2: term; k: kont }
| AppR of { cv1: cvalue; k: kont }
| LetL of { e: cenv; t2: term; k: kont }
| Init
let rec evalkd (e : cenv) (t : term) (k : kont) : cvalue =
match t with
| Var x ->
apply k (lookup e x)
| Lam t ->
apply k (Clo (t, e))
| App (t1, t2) ->
evalkd e t1 (AppL { e; t2; k })
| Let (t1, t2) ->
evalkd e t1 (LetL { e; t2; k })
and apply (k : kont) (cv : cvalue) : cvalue =
match k with
| AppL { e; t2; k } ->
let cv1 = cv in
evalkd e t2 (AppR { cv1; k })
| AppR { cv1; k } ->
let cv2 = cv in
let Clo (u1, e') = cv1 in
evalkd (cv2 :: e') u1 k
| LetL { e; t2; k } ->
let cv1 = cv in
evalkd (cv1 :: e) t2 k
| Init ->
cv
let eval e t =
evalkd e t Init
(* -------------------------------------------------------------------------- *)
(* Test. *)
let () =
test "the defunctionalized CPS evaluator" eval

71
ocaml/EvalCBVExercise.ml Normal file
View file

@ -0,0 +1,71 @@
(* -------------------------------------------------------------------------- *)
(* The type of lambda-terms, in de Bruijn's representation. *)
type var = int (* a de Bruijn index *)
type term =
| Var of var
| Lam of (* bind: *) term
| App of term * term
| Let of (* bind: *) term * term
(* -------------------------------------------------------------------------- *)
(* An environment-based big-step interpreter. This is the same interpreter
that we programmed in Coq, except here, in OCaml, fuel is not needed. *)
type cvalue =
| Clo of (* bind: *) term * cenv
and cenv =
cvalue list
let empty : cenv =
[]
exception RuntimeError
let lookup (e : cenv) (x : var) : cvalue =
try
List.nth e x
with Failure _ ->
raise RuntimeError
let rec eval (e : cenv) (t : term) : cvalue =
match t with
| Var x ->
lookup e x
| Lam t ->
Clo (t, e)
| App (t1, t2) ->
let cv1 = eval e t1 in
let cv2 = eval e t2 in
let Clo (u1, e') = cv1 in
eval (cv2 :: e') u1
| Let (t1, t2) ->
eval (eval e t1 :: e) t2
(* -------------------------------------------------------------------------- *)
(* The CPS-transformed interpreter. *)
let rec evalk (e : cenv) (t : term) (k : cvalue -> 'a) : 'a =
assert false
let eval (e : cenv) (t : term) : cvalue =
evalk e t (fun cv -> cv)
(* -------------------------------------------------------------------------- *)
(* The CPS-transformed, defunctionalized interpreter. *)
type kont
let rec evalkd (e : cenv) (t : term) (k : kont) : cvalue =
assert false
and apply (k : kont) (cv : cvalue) : cvalue =
assert false
let eval e t =
evalkd e t (assert false)

203
ocaml/Graph.ml Normal file
View file

@ -0,0 +1,203 @@
open Printf
(* -------------------------------------------------------------------------- *)
(* A simple type of binary trees. *)
type tree =
| Leaf
| Node of { data: int; left: tree; right: tree }
(* -------------------------------------------------------------------------- *)
(* Constructors. *)
let node data left right =
Node { data; left; right }
let singleton data =
node data Leaf Leaf
(* -------------------------------------------------------------------------- *)
(* A sample tree. *)
let christmas =
node 6
(node 2 (singleton 0) (singleton 1))
(node 5 (singleton 3) (singleton 4))
(* -------------------------------------------------------------------------- *)
(* A test procedure. *)
let test name walk =
printf "Testing %s...\n%!" name;
walk christmas;
walk christmas;
flush stdout
(* -------------------------------------------------------------------------- *)
(* A recursive depth-first traversal, with postfix printing. *)
let rec walk (t : tree) : unit =
match t with
| Leaf ->
()
| Node { data; left; right } ->
walk left;
walk right;
printf "%d\n" data
let () =
test "walk" walk
(* -------------------------------------------------------------------------- *)
(* A CPS traversal. *)
let rec walkk (t : tree) (k : unit -> 'a) : 'a =
match t with
| Leaf ->
k()
| Node { data; left; right } ->
walkk left (fun () ->
walkk right (fun () ->
printf "%d\n" data;
k()))
let walk t =
walkk t (fun t -> t)
let () =
test "walkk" walk
(* -------------------------------------------------------------------------- *)
(* A CPS-defunctionalized traversal. *)
type kont =
| Init
| GoneL of { data: int; tail: kont; right: tree }
| GoneR of { data: int; tail: kont }
let rec walkkd (t : tree) (k : kont) : unit =
match t with
| Leaf ->
apply k ()
| Node { data; left; right } ->
walkkd left (GoneL { data; tail = k; right })
and apply k () =
match k with
| Init ->
()
| GoneL { data; tail; right } ->
walkkd right (GoneR { data; tail })
| GoneR { data; tail } ->
printf "%d\n" data;
apply tail ()
let walk t =
walkkd t Init
let () =
test "walkkd" walk
(* CPS, defunctionalized, with in-place allocation of continuations. *)
(* [Init] is encoded by [Leaf].
[GoneL { data; tail; right }] is encoded by:
- setting [status] to [GoneL]; and
- storing [tail] in the [left] field.
- the [data] and [right] fields retain their original value.
[GoneR { data; tail }] is encoded by:
- setting [status] to [GoneR]; and
- storing [tail] in the [right] field.
- the [data] and [left] fields retain their original value.
The [status] field is meaningful only when the memory block is
being viewed as a continuation. If it is being viewed as a tree,
then (by convention) [status] must be [GoneL]. (We could also
let the type [status] have three values, but I prefer to use just
two, for the sake of economy.)
Does that sound crazy? Well, it is, in a way. *)
type status = GoneL | GoneR
type mtree = Leaf | Node of {
data: int; mutable status: status;
mutable left: mtree; mutable right: mtree
}
type mkont = mtree
(* Constructors. *)
let node data left right =
Node { data; status = GoneL; left; right }
let singleton data =
node data Leaf Leaf
(* A sample tree. *)
let christmas =
node 6
(node 2 (singleton 0) (singleton 1))
(node 5 (singleton 3) (singleton 4))
(* A test. *)
let test name walk =
printf "Testing %s...\n%!" name;
walk christmas;
walk christmas;
flush stdout
(* The code. *)
let rec walkkdi (t : mtree) (k : mkont) : unit =
match t with
| Leaf ->
(* We decide to let [apply] takes a tree as a second argument,
instead of just a unit value. Indeed, in order to restore
the [left] or [right] fields of [k], we need the address
of the child [t] out of which we are coming. *)
apply k t
| Node ({ left; _ } as n) ->
(* At this point, [t] is a tree.
[n] is a name for its root record. *)
(* Change this tree to a [GoneL] continuation. *)
assert (n.status = GoneL);
n.left (* n.tail *) <- k;
(* [t] now represents a continuation. Go down into the left
child, with this continuation. *)
walkkdi left (t : mkont)
and apply (k : mkont) (child : mtree) : unit =
match k with
| Leaf -> ()
| Node ({ status = GoneL; left = tail; right; _ } as n) ->
(* We are popping a [GoneL] frame, that is, coming out of
a left child. *)
n.status <- GoneR; (* update continuation! *)
n.left <- child; (* restore orig. left child! *)
n.right (* n.tail *) <- tail;
(* [k] now represents a [GoneR] continuation. Go down into
the right child, with [k] as a continuation. *)
walkkdi right k
| Node ({ data; status = GoneR; right = tail; _ } as n) ->
printf "%d\n" data;
n.status <- GoneL; (* change back to a tree! *)
n.right <- child; (* restore orig. right child! *)
(* [k] now represents a valid tree again. *)
apply tail (k : mtree)
let walk t =
walkkdi t Leaf
let () =
test "walkkdi" walk

175
ocaml/Lambda.ml Normal file
View file

@ -0,0 +1,175 @@
(* -------------------------------------------------------------------------- *)
(* The type of lambda-terms, in de Bruijn's representation. *)
type var = int (* a de Bruijn index *)
type term =
| Var of var
| Lam of (* bind: *) term
| App of term * term
| Let of (* bind: *) term * term
(* -------------------------------------------------------------------------- *)
(* [lift_ i k] represents the substitution [upn i (ren (+k))]. Its effect is to
add [k] to every variable that occurs free in [t] and whose index is at
least [i]. *)
let rec lift_ i k (t : term) : term =
match t with
| Var x ->
if x < i then t else Var (x + k)
| Lam t ->
Lam (lift_ (i + 1) k t)
| App (t1, t2) ->
App (lift_ i k t1, lift_ i k t2)
| Let (t1, t2) ->
Let (lift_ i k t1, lift_ (i + 1) k t2)
(* [lift k t] adds [k] to every variable that occurs free in [t]. *)
let lift k t =
lift_ 0 k t
(* [subst i sigma] represents the substitution [upn i sigma]. *)
let rec subst_ i (sigma : var -> term) (t : term) : term =
match t with
| Var x ->
if x < i then t else lift i (sigma (x - i))
| Lam t ->
Lam (subst_ (i + 1) sigma t)
| App (t1, t2) ->
App (subst_ i sigma t1, subst_ i sigma t2)
| Let (t1, t2) ->
Let (subst_ i sigma t1, subst_ (i + 1) sigma t2)
(* [subst sigma t] applies the substitution [sigma] to the term [t]. *)
let subst sigma t =
subst_ 0 sigma t
(* A singleton substitution [u .: ids]. *)
let singleton (u : term) : var -> term =
function 0 -> u | x -> Var (x - 1)
(* -------------------------------------------------------------------------- *)
(* Recognizing a value. *)
let is_value = function
| Var _
| Lam _ ->
true
| App _ ->
false
| Let _ ->
false
(* -------------------------------------------------------------------------- *)
(* An auxiliary function: the [map] function for the type [_ option]. *)
(* We name this function [in_context] because we use it below to perform
reduction under an evaluation context. *)
let in_context f ox =
match ox with
| None -> None
| Some x -> Some (f x)
(* -------------------------------------------------------------------------- *)
(* Stepping in call-by-value. *)
(* This is a naive, direct implementation of the call-by-value reduction
relation, following Plotkin's formulation. The function [step t] returns
[Some t'] if and only if the relation [cbv t t'] holds, and returns [None]
if no such term [t'] exists. *)
let rec step (t : term) : term option =
match t with
| Lam _ | Var _ -> None
(* Plotkin's BetaV *)
| App (Lam t, v) when is_value v ->
Some (subst (singleton v) t)
(* Plotkin's AppL *)
| App (t, u) when not (is_value t) ->
in_context (fun t' -> App (t', u)) (step t)
(* Plotkin's AppVR *)
| App (v, u) when is_value v ->
in_context (fun u' -> App (v, u')) (step u)
(* All cases covered already, but OCaml cannot see it. *)
| App (_, _) ->
assert false
| Let (t, u) when not (is_value t) ->
in_context (fun t' -> Let (t', u)) (step t)
| Let (v, u) when is_value v ->
Some (subst (singleton v) u)
| Let (_, _) ->
assert false
let rec eval (t : term) : term =
match step t with
| None ->
t
| Some t' ->
eval t'
(* -------------------------------------------------------------------------- *)
(* A naive, substitution-based big-step interpreter. *)
exception RuntimeError
let rec eval (t : term) : term =
match t with
| Lam _ | Var _ -> t
| Let (t1, t2) ->
let v1 = eval t1 in
eval (subst (singleton v1) t2)
| App (t1, t2) ->
let v1 = eval t1 in
let v2 = eval t2 in
match v1 with
| Lam u1 -> eval (subst (singleton v2) u1)
| _ -> raise RuntimeError
(* -------------------------------------------------------------------------- *)
(* A term printer. *)
open Printf
let rec print f = function
| Var x ->
fprintf f "(Var %d)" x
| Lam t ->
fprintf f "(Lam %a)" print t
| App (t1, t2) ->
fprintf f "(App %a %a)" print t1 print t2
| Let (t1, t2) ->
fprintf f "(Let %a %a)" print t1 print t2
let print t =
fprintf stdout "%a\n" print t
(* -------------------------------------------------------------------------- *)
(* Test. *)
let id =
Lam (Var 0)
let idid =
App (id, id)
let () =
match step idid with
| None ->
assert false
| Some reduct ->
print reduct
let () =
print (eval idid)

151
ocaml/NewtonRaphson.ml Normal file
View file

@ -0,0 +1,151 @@
(* A couple abbreviations. *)
type 'a thunk = 'a Lazy.t
let force = Lazy.force
(* The definition of (finite or infinite) lazy lists. *)
type 'a stream =
'a head thunk
and 'a head =
| Nil
| Cons of 'a * 'a stream
(* Calling [tail xs] demands the head of the stream, that is, forces
the computation of the first element of the stream (if there is one). *)
let tail xs =
match force xs with
| Nil -> assert false
| Cons (_, xs) -> xs
(* Newton-Raphson approximation, following Hughes,
"Why functional programming matters", 1990. *)
let next n x =
(x +. n /. x) /. 2.
(* An infinite stream obtained by iterating [f]. *)
(* The following definition, copied almost literally from Hughes'
paper, is correct but somewhat unsatisfactory; can you see why? Can
you fix it? Think about it before reading the solution below. *)
let rec repeat (f : 'a -> 'a) (a : 'a) : 'a stream =
lazy (Cons (a, repeat f (f a)))
(*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*)
(* In the above definition of [repeat], the function call [f a] takes
place when the *first* element of the list is demanded by the consumer.
That's too early -- ideally, this function call should take place only
when the *second* element is demanded, since the result of [f a] is the
second element in the infinite stream [a], [f a], [f (f a)], ... *)
(* This code exhibits the problem: *)
let () =
let x = ref 0 in
let f () = incr x; () in
let xs = repeat f () in
let xs = tail xs in
(* This assertion fails because [x] has been incremented once: *)
assert (!x = 0);
ignore xs
(* This can be fixed in several ways. One solution is to let [repeat] take an
argument of type ['a thunk] instead of ['a]. This approach is in fact the
standard encoding of call-by-need into call-by-value, applied to Hughes'
code. *)
let rec repeat (f : 'a -> 'a) (a : 'a thunk) : 'a stream =
lazy (
Cons (
force a,
repeat f (lazy (f (force a)))
)
)
(* It can also be written as follows. *)
let rec repeat (f : 'a -> 'a) (a : 'a thunk) : 'a stream =
lazy (
let a = force a in
Cons (
a,
repeat f (lazy (f a))
)
)
(* We define a wrapper so [repeat] has the desired type again: *)
let repeat (f : 'a -> 'a) (a : 'a) : 'a stream =
repeat f (lazy a)
(* The problematic code now behaves as desired: *)
let () =
let x = ref 0 in
let f () = incr x; () in
let xs = repeat f () in
(* These assertions succeed: *)
let xs = tail xs in
assert (!x = 0);
let xs = tail xs in
assert (!x = 1);
let xs = tail xs in
assert (!x = 2);
ignore xs
(* Back to Newton-Rapshon. *)
let rec within (eps : float) (xs : float stream) : float =
match force xs with
| Nil -> assert false
| Cons (a, xs) ->
match force xs with
| Nil -> assert false
| Cons (b, _) ->
if abs_float (a /. b -. 1.) <= eps then b
else within eps xs
let sqrt (n : float) : float =
within 0.0001 (repeat (next n) n)
let sqrt2 =
sqrt 2.

BIN
slides/fpottier-00.pdf Normal file
View file

Binary file not shown.

BIN
slides/fpottier-01a.pdf Normal file
View file

Binary file not shown.

BIN
slides/fpottier-01b.pdf Normal file
View file

Binary file not shown.

BIN
slides/fpottier-02.pdf Normal file
View file

Binary file not shown.

BIN
slides/fpottier-03.pdf Normal file
View file

Binary file not shown.

BIN
slides/fpottier-04.pdf Normal file
View file

Binary file not shown.

BIN
slides/fpottier-05.pdf Normal file
View file

Binary file not shown.