Add the Coq formalization of the CPS transformation.

coq/CPSContextSubstitution.v

@@ -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.

coq/CPSCorrectness.v

@@ -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.

coq/CPSCounterExample.v

@@ -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. *)

coq/CPSDefinition.v

@@ -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.

coq/CPSIndifference.v

@@ -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. *)

coq/CPSKubstitution.v

@@ -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.

coq/CPSRenaming.v

@@ -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.

coq/CPSSimulation.v

@@ -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.

coq/CPSSimulationWithoutLet.v

@@ -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.

coq/CPSSpecialCases.v

@@ -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.

coq/CPSSubstitution.v

@@ -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.

coq/FixExtra.v

@@ -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.

coq/LambdaCalculusParallelReduction.v

@@ -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.

coq/LambdaCalculusStandardization.v

@@ -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.

coq/Relations.v

@@ -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.