From d677f255c4c377b90ee841b46cd5eaaad2294c85 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 21 Feb 2016 15:01:24 -0500 Subject: [PATCH] OperationalSemantics: manually proved invariant and determinism --- OperationalSemantics.v | 248 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 248 insertions(+) diff --git a/OperationalSemantics.v b/OperationalSemantics.v index 21ccb3e..d6a7383 100644 --- a/OperationalSemantics.v +++ b/OperationalSemantics.v @@ -513,6 +513,201 @@ Proof. model_check. Qed. +Inductive isEven : nat -> Prop := +| EvenO : isEven 0 +| EvenSS : forall n, isEven n -> isEven (S (S n)). + +Definition my_loop := + while "n" do + "a" <- "a" + "n";; + "n" <- "n" - 2 + done. + +Definition all_programs := { + (while "n" do + "a" <- "a" + "n";; + "n" <- "n" - 2 + done), + ("a" <- "a" + "n";; + "n" <- "n" - 2), + (Skip;; + "n" <- "n" - 2), + ("n" <- "n" - 2), + (("a" <- "a" + "n";; + "n" <- "n" - 2);; + while "n" do + "a" <- "a" + "n";; + "n" <- "n" - 2 + done), + ((Skip;; + "n" <- "n" - 2);; + while "n" do + "a" <- "a" + "n";; + "n" <- "n" - 2 + done), + ("n" <- "n" - 2;; + while "n" do + "a" <- "a" + "n";; + "n" <- "n" - 2 + done), + (Skip;; + while "n" do + "a" <- "a" + "n";; + "n" <- "n" - 2 + done), + Skip +}. + +Lemma isEven_minus2 : forall n, isEven n -> isEven (n - 2). +Proof. + induct 1; simplify. + + constructor. + + replace (n - 0) with n by linear_arithmetic. + assumption. +Qed. + +Lemma isEven_plus : forall n m, + isEven n + -> isEven m + -> isEven (n + m). +Proof. + induct 1; simplify. + + assumption. + + constructor. + apply IHisEven. + assumption. +Qed. + +Lemma manually_proved_invariant' : + invariantFor (trsys_of ($0 $+ ("n", 0) $+ ("a", 0)) (while "n" do "a" <- "a" + "n";; "n" <- "n" - 2 done)) + (fun s => all_programs (snd s) + /\ exists n a, fst s $? "n" = Some n + /\ fst s $? "a" = Some a + /\ isEven n + /\ isEven a). +Proof. + apply invariant_induction; simplify. + + first_order. + unfold all_programs. + subst; simplify; equality. + subst; simplify. + exists 0, 0. + propositional. + constructor. + constructor. + + invert H. + invert H2. + invert H. + invert H2. + invert H3. + invert H4. + (* Note our use here of [invert] to break down hypotheses with [exists] and + * [/\]. *) + invert H0; simplify. + + unfold all_programs in *; simplify; propositional; try equality. + invert H1; simplify. + rewrite H. + exists (x - 2), x0; propositional. + apply isEven_minus2; assumption. + + unfold all_programs in *; simplify; propositional; try equality. + invert H1. + invert H4; equality. + invert H1. + invert H4. + rewrite H, H2; simplify. + eexists; eexists. + propositional; try eassumption. + apply isEven_plus; assumption. + invert H0. + invert H4. + invert H0. + invert H4. + invert H0. + invert H4. + invert H1. + equality. + invert H0. + invert H4. + invert H1. + rewrite H, H2; simplify. + eexists; eexists; propositional; try eassumption. + apply isEven_plus; assumption. + invert H1. + invert H4. + invert H1. + equality. + invert H1. + invert H4. + invert H1. + eexists; eexists; propositional; eassumption. + invert H0. + invert H4. + equality. + invert H0. + invert H4. + rewrite H; simplify. + do 2 eexists; propositional; try eassumption. + apply isEven_minus2; assumption. + invert H1. + invert H4. + invert H1. + invert H4. + unfold all_programs in *; simplify; propositional; try equality. + invert H0. + do 2 eexists; propositional; try eassumption. + invert H1. + do 2 eexists; propositional; try eassumption. + unfold all_programs in *; simplify; propositional; equality. + unfold all_programs in *; simplify; propositional; equality. + unfold all_programs in *; simplify; propositional; try equality. + invert H0. + do 2 eexists; propositional; try eassumption. + unfold all_programs in *; simplify; propositional; try equality. + invert H0. + do 2 eexists; propositional; try eassumption. +Qed. + +(* That manual proof was quite a pain. Here's a bonus automated proof. *) +Hint Constructors isEven. +Hint Resolve isEven_minus2 isEven_plus. + +Lemma manually_proved_invariant'_snazzy : + invariantFor (trsys_of ($0 $+ ("n", 0) $+ ("a", 0)) (while "n" do "a" <- "a" + "n";; "n" <- "n" - 2 done)) + (fun s => all_programs (snd s) + /\ exists n a, fst s $? "n" = Some n + /\ fst s $? "a" = Some a + /\ isEven n + /\ isEven a). +Proof. + apply invariant_induction; simplify; unfold all_programs in *; first_order; subst; simplify; + try match goal with + | [ H : step _ _ |- _ ] => invert H; simplify + end; + repeat (match goal with + | [ H : _ = Some _ |- _ ] => rewrite H + | [ H : @eq cmd (_ _ _) _ |- _ ] => invert H + | [ H : @eq cmd (_ _ _ _) _ |- _ ] => invert H + | [ H : step _ _ |- _ ] => invert2 H + end; simplify); equality || eauto 7. +Qed. + +Theorem manually_proved_invariant : + invariantFor (trsys_of ($0 $+ ("n", 0) $+ ("a", 0)) (while "n" do "a" <- "a" + "n";; "n" <- "n" - 2 done)) + (fun s => exists a, fst s $? "a" = Some a /\ isEven a). +Proof. + eapply invariant_weaken. + apply manually_proved_invariant'. + first_order. +Qed. + (* We'll return to these systems and their abstractions in the next few * chapters. *) @@ -684,3 +879,56 @@ Theorem cstep_step_snazzy : forall v c v' c', Proof. induct 1; eauto. Qed. + + +(** * Determinism *) + +(* Each of the relations we have defined turns out to be deterministic. Let's + * prove it. *) + +Theorem eval_det : forall v c v1, + eval v c v1 + -> forall v2, eval v c v2 + -> v1 = v2. +Proof. + induct 1; invert 1; try first_order. + + apply IHeval2. + apply IHeval1 in H5. + subst. + assumption. + + apply IHeval2. + apply IHeval1 in H7. + subst. + assumption. +Qed. + +Theorem step_det : forall s out1, + step s out1 + -> forall out2, step s out2 + -> out1 = out2. +Proof. + induct 1; invert 1; try first_order. + + apply IHstep in H5. + equality. + + invert H. + + invert H4. +Qed. + +Theorem cstep_det : forall s out1, + cstep s out1 + -> forall out2, cstep s out2 + -> out1 = out2. +Proof. + simplify. + cases s; cases out1; cases out2. + eapply step_det. + apply cstep_step. + eassumption. + apply cstep_step. + eassumption. +Qed.