From c4be95afab87b5a6d12b3020854163fbf38fb1ed Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 19 Mar 2017 12:32:40 -0400 Subject: [PATCH] CompilerCorrectness: simulation_multiple --- CompilerCorrectness.v | 355 ++++++++++++++++++++++++++++++++++++++---- Frap.v | 6 +- 2 files changed, 333 insertions(+), 28 deletions(-) diff --git a/CompilerCorrectness.v b/CompilerCorrectness.v index 43ca749..d1ad1d4 100644 --- a/CompilerCorrectness.v +++ b/CompilerCorrectness.v @@ -376,6 +376,49 @@ Fixpoint cfold (c : cmd) : cmd := | Output e => Output (cfoldArith e) end. +Notation silent_cstep := (fun a b => cstep a None b). + +Lemma silent_generate_fwd : forall ns vc vc', + silent_cstep^* vc vc' + -> generate vc ns + -> generate vc' ns. +Proof. + induct 1; simplify; eauto. + invert H1; auto. + + eapply deterministic in H; eauto. + propositional; subst. + auto. + + eapply deterministic in H; eauto. + equality. +Qed. + +Lemma silent_generate_bwd : forall ns vc vc', + silent_cstep^* vc vc' + -> generate vc' ns + -> generate vc ns. +Proof. + induct 1; eauto. +Qed. + +Lemma generate_Skip : forall v a ns, + generate (v, Skip) (a :: ns) + -> False. +Proof. + induct 1; simplify. + + invert H. + invert H3. + invert H4. + + invert H. + invert H3. + invert H4. +Qed. + +Hint Resolve silent_generate_fwd silent_generate_bwd generate_Skip. + Section simulation_skipping. Variable R : nat -> valuation * cmd -> valuation * cmd -> Prop. @@ -409,23 +452,6 @@ Section simulation_skipping. unfold traceInclusion; eauto using simulation_skipping_fwd'. Qed. - Lemma generate_Skip : forall v a ns, - generate (v, Skip) (a :: ns) - -> False. - Proof. - induct 1; simplify. - - invert H. - invert H3. - invert H4. - - invert H. - invert H3. - invert H4. - Qed. - - Notation silent_cstep := (fun a b => cstep a None b). - Lemma match_step : forall n vc2 l vc2' vc1, cstep vc2 l vc2' -> R n vc1 vc2 @@ -467,16 +493,6 @@ Section simulation_skipping. eauto 6. Qed. - Lemma silent_generate : forall ns vc vc', - silent_cstep^* vc vc' - -> generate vc' ns - -> generate vc ns. - Proof. - induct 1; eauto. - Qed. - - Hint Resolve silent_generate. - Lemma simulation_skipping_bwd' : forall ns vc2, generate vc2 ns -> forall n vc1, R n vc1 vc2 -> generate vc1 ns. @@ -592,3 +608,288 @@ Proof. eauto. eauto 10. Qed. + + +(** * Simulations That Allow Taking Multiple Matching Steps *) + +Fixpoint tempVar (n : nat) : string := + match n with + | O => "_tmp" + | S n' => tempVar n' ++ "'" + end%string. + +Fixpoint noUnderscoreVar (x : var) : bool := + match x with + | String "_" _ => false + | _ => true + end. + +Lemma append_assoc : forall a b c, + (a ++ (b ++ c) = (a ++ b) ++ c)%string. +Proof. + induct a; simplify; equality. +Qed. + +Lemma append_assoc_String : forall a b, + (String a b = String a "" ++ b)%string. +Proof. + induct b; simplify; equality. +Qed. + +Lemma noUnderscoreVar_tempVar' : forall n, + exists s, tempVar n = ("_tmp" ++ s)%string. +Proof. + induct n; simplify; first_order. + + exists ""; auto. + + rewrite H. + exists (x ++ "'")%string. + repeat match goal with + | [ |- context[String ?c ?x] ] => + match x with + | "" => fail 1 + | _ => rewrite (append_assoc_String c x) + end + end. + repeat rewrite append_assoc. + reflexivity. +Qed. + +Theorem noUnderscoreVar_tempVar : forall x, + noUnderscoreVar x = true + -> forall n, x <> tempVar n. +Proof. + unfold not; simplify. + subst. + pose proof (noUnderscoreVar_tempVar' n). + first_order. + rewrite H0 in H. + simplify. + equality. +Qed. + +Lemma tempVar_inj' : forall s1 s2, + (s1 ++ "'" = s2 ++ "'")%string + -> s1 = s2. +Proof. + induct s1; simplify. + + cases s2; simplify; try equality. + invert H. + cases s2; simplify; equality. + + cases s2; simplify. + invert H. + cases s1; simplify; equality. + invert H. + f_equal; auto. +Qed. + +Theorem tempVar_inj : forall n1 n2, + tempVar n1 = tempVar n2 + -> n1 = n2. +Proof. + induct n1; simplify; cases n2; simplify; try equality. + + repeat match goal with + | [ _ : context[(?s ++ "'")%string] |- _ ] => cases s; simplify; try equality + end. + + repeat match goal with + | [ _ : context[(?s ++ "'")%string] |- _ ] => cases s; simplify; try equality + end. + + auto using tempVar_inj'. +Qed. + +Fixpoint noUnderscoreArith (e : arith) : bool := + match e with + | Const _ => true + | Var x => noUnderscoreVar x + | Plus e1 e2 => noUnderscoreArith e1 && noUnderscoreArith e2 + | Minus e1 e2 => noUnderscoreArith e1 && noUnderscoreArith e2 + | Times e1 e2 => noUnderscoreArith e1 && noUnderscoreArith e2 + end. + +Fixpoint noUnderscore (c : cmd) : bool := + match c with + | Skip => true + | Assign x e => noUnderscoreVar x && noUnderscoreArith e + | Sequence c1 c2 => noUnderscore c1 && noUnderscore c2 + | If e then_ else_ => noUnderscoreArith e && noUnderscore then_ && noUnderscore else_ + | While e body => noUnderscoreArith e && noUnderscore body + | Output e => noUnderscoreArith e + end. + +Fixpoint flattenArith (tempCount : nat) (dst : var) (e : arith) : nat * cmd := + match e with + | Const _ + | Var _ => (tempCount, Assign dst e) + | Plus e1 e2 => + let x1 := tempVar tempCount in + let (tempCount, c1) := flattenArith (S tempCount) x1 e1 in + let x2 := tempVar tempCount in + let (tempCount, c2) := flattenArith (S tempCount) x2 e2 in + (tempCount, Sequence c1 (Sequence c2 (Assign dst (Plus x1 x2)))) + | Minus e1 e2 => + let x1 := tempVar tempCount in + let (tempCount, c1) := flattenArith (S tempCount) x1 e1 in + let x2 := tempVar tempCount in + let (tempCount, c2) := flattenArith (S tempCount) x2 e2 in + (tempCount, Sequence c1 (Sequence c2 (Assign dst (Minus x1 x2)))) + | Times e1 e2 => + let x1 := tempVar tempCount in + let (tempCount, c1) := flattenArith (S tempCount) x1 e1 in + let x2 := tempVar tempCount in + let (tempCount, c2) := flattenArith (S tempCount) x2 e2 in + (tempCount, Sequence c1 (Sequence c2 (Assign dst (Times x1 x2)))) + end. + +Fixpoint flatten (c : cmd) : cmd := + match c with + | Skip => c + | Assign x e => snd (flattenArith 0 x e) + | Sequence c1 c2 => Sequence (flatten c1) (flatten c2) + | If e then_ else_ => If e (flatten then_) (flatten else_) + | While e body => While e (flatten body) + | Output _ => c + end. + +Section simulation_multiple. + Variable R : valuation * cmd -> valuation * cmd -> Prop. + + Hypothesis one_step : forall vc1 vc2, R vc1 vc2 + -> forall vc1' l, cstep vc1 l vc1' + -> exists vc2' vc2'', + silent_cstep^* vc2 vc2' + /\ cstep vc2' l vc2'' + /\ R vc1' vc2''. + + Hypothesis agree_on_termination : forall v1 v2 c2, R (v1, Skip) (v2, c2) + -> c2 = Skip. + + Lemma simulation_multiple_fwd' : forall vc1 ns, generate vc1 ns + -> forall vc2, R vc1 vc2 + -> generate vc2 ns. + Proof. + induct 1; simplify; eauto. + + eapply one_step in H; eauto. + first_order. + eauto. + + eapply one_step in H1; eauto. + first_order. + eauto. + Qed. + + Theorem simulation_multiple_fwd : forall vc1 vc2, R vc1 vc2 + -> vc1 <| vc2. + Proof. + unfold traceInclusion; eauto using simulation_multiple_fwd'. + Qed. + + (* A version of [generate] that counts how many steps run *) + Inductive generateN : nat -> valuation * cmd -> list nat -> Prop := + | GenDoneN : forall vc, + generateN 0 vc [] + | GenSilentN : forall sc vc vc' ns, + cstep vc None vc' + -> generateN sc vc' ns + -> generateN (S sc) vc ns + | GenOutputN : forall sc vc n vc' ns, + cstep vc (Some n) vc' + -> generateN sc vc' ns + -> generateN (S sc) vc (n :: ns). + + Hint Constructors generateN. + + Lemma generateN_fwd : forall sc vc ns, + generateN sc vc ns + -> generate vc ns. + Proof. + induct 1; eauto. + Qed. + + Hint Resolve generateN_fwd. + + Lemma generateN_bwd : forall vc ns, + generate vc ns + -> exists sc, generateN sc vc ns. + Proof. + induct 1; first_order; eauto. + Qed. + + Lemma generateN_silent_cstep : forall sc vc ns, + generateN sc vc ns + -> forall vc', silent_cstep^* vc vc' + -> exists sc', sc' <= sc /\ generateN sc' vc' ns. + Proof. + clear; induct 1; simplify; eauto. + + invert H1; eauto. + eapply deterministic in H; eauto. + propositional; subst. + apply IHgenerateN in H3. + first_order. + eauto. + + invert H1; eauto. + eapply deterministic in H; eauto. + equality. + Qed. + + Lemma simulation_multiple_bwd' : forall sc sc', sc' < sc + -> forall vc2 ns, generateN sc' vc2 ns + -> forall vc1, R vc1 vc2 + -> generate vc1 ns. + Proof. + induct sc; simplify. + + linear_arithmetic. + + cases sc'. + invert H0. + auto. + cases vc1; cases vc2. + assert (c = Skip \/ exists v' l c', cstep (v, c) l (v', c')) by apply skip_or_step. + first_order; subst. + apply agree_on_termination in H1; subst. + cases ns; auto. + exfalso; eauto. + eapply one_step in H1; eauto. + first_order. + eapply generateN_silent_cstep in H0; eauto. + first_order. + invert H5; auto. + eapply deterministic in H3; eauto. + propositional; subst. + econstructor. + eauto. + eapply IHsc; try eassumption. + linear_arithmetic. + + eapply deterministic in H3; eauto. + propositional; subst. + eapply GenOutput. + eauto. + eapply IHsc; try eassumption. + linear_arithmetic. + Qed. + + Theorem simulation_multiple_bwd : forall vc1 vc2, R vc1 vc2 + -> vc2 <| vc1. + Proof. + unfold traceInclusion; simplify. + apply generateN_bwd in H0. + first_order. + eauto using simulation_multiple_bwd'. + Qed. + + Theorem simulation_multiple : forall vc1 vc2, R vc1 vc2 + -> vc1 =| vc2. + Proof. + simplify; split; auto using simulation_multiple_fwd, simulation_multiple_bwd. + Qed. +End simulation_multiple. diff --git a/Frap.v b/Frap.v index a06743d..85687a2 100644 --- a/Frap.v +++ b/Frap.v @@ -87,7 +87,11 @@ Ltac instantiate_obvious1 H := end end. -Ltac instantiate_obvious H := repeat instantiate_obvious1 H. +Ltac instantiate_obvious H := + match type of H with + | context[@eq string _ _] => idtac + | _ => repeat instantiate_obvious1 H + end. Ltac instantiate_obviouses := repeat match goal with