From 555822838f0267bdf7da1a7c4650266906544e84 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Pottier?= Date: Wed, 11 Oct 2017 15:28:20 +0200 Subject: [PATCH] Add the Coq formalization of the CPS transformation. --- coq/CPSContextSubstitution.v | 77 +++ coq/CPSCorrectness.v | 138 ++++++ coq/CPSCounterExample.v | 107 ++++ coq/CPSDefinition.v | 446 +++++++++++++++++ coq/CPSIndifference.v | 262 ++++++++++ coq/CPSKubstitution.v | 120 +++++ coq/CPSRenaming.v | 92 ++++ coq/CPSSimulation.v | 177 +++++++ coq/CPSSimulationWithoutLet.v | 137 ++++++ coq/CPSSpecialCases.v | 48 ++ coq/CPSSubstitution.v | 149 ++++++ coq/FixExtra.v | 20 + coq/LambdaCalculusParallelReduction.v | 174 +++++++ coq/LambdaCalculusStandardization.v | 679 ++++++++++++++++++++++++++ coq/Relations.v | 498 +++++++++++++++++++ 15 files changed, 3124 insertions(+) create mode 100644 coq/CPSContextSubstitution.v create mode 100644 coq/CPSCorrectness.v create mode 100644 coq/CPSCounterExample.v create mode 100644 coq/CPSDefinition.v create mode 100644 coq/CPSIndifference.v create mode 100644 coq/CPSKubstitution.v create mode 100644 coq/CPSRenaming.v create mode 100644 coq/CPSSimulation.v create mode 100644 coq/CPSSimulationWithoutLet.v create mode 100644 coq/CPSSpecialCases.v create mode 100644 coq/CPSSubstitution.v create mode 100644 coq/FixExtra.v create mode 100644 coq/LambdaCalculusParallelReduction.v create mode 100644 coq/LambdaCalculusStandardization.v create mode 100644 coq/Relations.v diff --git a/coq/CPSContextSubstitution.v b/coq/CPSContextSubstitution.v new file mode 100644 index 0000000..11864a8 --- /dev/null +++ b/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. diff --git a/coq/CPSCorrectness.v b/coq/CPSCorrectness.v new file mode 100644 index 0000000..a8bedb7 --- /dev/null +++ b/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. diff --git a/coq/CPSCounterExample.v b/coq/CPSCounterExample.v new file mode 100644 index 0000000..5db8181 --- /dev/null +++ b/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. *) diff --git a/coq/CPSDefinition.v b/coq/CPSDefinition.v new file mode 100644 index 0000000..4757cd1 --- /dev/null +++ b/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. diff --git a/coq/CPSIndifference.v b/coq/CPSIndifference.v new file mode 100644 index 0000000..28d1d69 --- /dev/null +++ b/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. *) diff --git a/coq/CPSKubstitution.v b/coq/CPSKubstitution.v new file mode 100644 index 0000000..5cda6d2 --- /dev/null +++ b/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. diff --git a/coq/CPSRenaming.v b/coq/CPSRenaming.v new file mode 100644 index 0000000..9af3ae3 --- /dev/null +++ b/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. diff --git a/coq/CPSSimulation.v b/coq/CPSSimulation.v new file mode 100644 index 0000000..bb3a758 --- /dev/null +++ b/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. diff --git a/coq/CPSSimulationWithoutLet.v b/coq/CPSSimulationWithoutLet.v new file mode 100644 index 0000000..ccbe944 --- /dev/null +++ b/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. diff --git a/coq/CPSSpecialCases.v b/coq/CPSSpecialCases.v new file mode 100644 index 0000000..33fc4e3 --- /dev/null +++ b/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. diff --git a/coq/CPSSubstitution.v b/coq/CPSSubstitution.v new file mode 100644 index 0000000..a292aeb --- /dev/null +++ b/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. diff --git a/coq/FixExtra.v b/coq/FixExtra.v new file mode 100644 index 0000000..43c57a3 --- /dev/null +++ b/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. diff --git a/coq/LambdaCalculusParallelReduction.v b/coq/LambdaCalculusParallelReduction.v new file mode 100644 index 0000000..e66fd15 --- /dev/null +++ b/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. diff --git a/coq/LambdaCalculusStandardization.v b/coq/LambdaCalculusStandardization.v new file mode 100644 index 0000000..5c066dc --- /dev/null +++ b/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. diff --git a/coq/Relations.v b/coq/Relations.v new file mode 100644 index 0000000..2251b7e --- /dev/null +++ b/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.