diff --git a/ModelChecking.v b/ModelChecking.v new file mode 100644 index 0000000..cf8251c --- /dev/null +++ b/ModelChecking.v @@ -0,0 +1,211 @@ +(** Formal Reasoning About Programs + * Chapter 5: Model Checking + * Author: Adam Chlipala + * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) + +Require Import Frap TransitionSystems. + +Set Implicit Arguments. + + +Definition oneStepClosure_current {state} (sys : trsys state) + (invariant1 invariant2 : state -> Prop) := + forall st, invariant1 st + -> invariant2 st. + +Definition oneStepClosure_new {state} (sys : trsys state) + (invariant1 invariant2 : state -> Prop) := + forall st st', invariant1 st + -> sys.(Step) st st' + -> invariant2 st'. + +Definition oneStepClosure {state} (sys : trsys state) + (invariant1 invariant2 : state -> Prop) := + oneStepClosure_current sys invariant1 invariant2 + /\ oneStepClosure_new sys invariant1 invariant2. + +Theorem prove_oneStepClosure : forall state (sys : trsys state) (inv1 inv2 : state -> Prop), + (forall st, inv1 st -> inv2 st) + -> (forall st st', inv1 st -> sys.(Step) st st' -> inv2 st') + -> oneStepClosure sys inv1 inv2. +Proof. + unfold oneStepClosure. + propositional. +Qed. + +Theorem oneStepClosure_done : forall state (sys : trsys state) (invariant : state -> Prop), + (forall st, sys.(Initial) st -> invariant st) + -> oneStepClosure sys invariant invariant + -> invariantFor sys invariant. +Proof. + unfold oneStepClosure, oneStepClosure_current, oneStepClosure_new. + propositional. + apply invariant_induction. + assumption. + simplify. + eapply H2. + eassumption. + assumption. +Qed. + +Inductive multiStepClosure {state} (sys : trsys state) + : (state -> Prop) -> (state -> Prop) -> Prop := +| MscDone : forall inv, + oneStepClosure sys inv inv + -> multiStepClosure sys inv inv +| MscStep : forall inv inv' inv'', + oneStepClosure sys inv inv' + -> multiStepClosure sys inv' inv'' + -> multiStepClosure sys inv inv''. + +Lemma multiStepClosure_ok' : forall state (sys : trsys state) (inv inv' : state -> Prop), + multiStepClosure sys inv inv' + -> (forall st, sys.(Initial) st -> inv st) + -> invariantFor sys inv'. +Proof. + induct 1; simplify. + + apply oneStepClosure_done. + assumption. + assumption. + + apply IHmultiStepClosure. + simplify. + unfold oneStepClosure, oneStepClosure_current in *. (* <-- *) + propositional. + apply H3. + apply H1. + assumption. +Qed. + +Theorem multiStepClosure_ok : forall state (sys : trsys state) (inv : state -> Prop), + multiStepClosure sys sys.(Initial) inv + -> invariantFor sys inv. +Proof. + simplify. + eapply multiStepClosure_ok'. + eassumption. + propositional. +Qed. + +Theorem oneStepClosure_empty : forall state (sys : trsys state), + oneStepClosure sys (constant nil) (constant nil). +Proof. + unfold oneStepClosure, oneStepClosure_current, oneStepClosure_new; propositional. +Qed. + +Theorem oneStepClosure_split : forall state (sys : trsys state) st sts (inv1 inv2 : state -> Prop), + (forall st', sys.(Step) st st' -> inv1 st') + -> oneStepClosure sys (constant sts) inv2 + -> oneStepClosure sys (constant (st :: sts)) ({st} \cup inv1 \cup inv2). +Proof. + unfold oneStepClosure, oneStepClosure_current, oneStepClosure_new; propositional. + + invert H0. + + left. + left. + simplify. + propositional. + + right. + apply H1. + assumption. + + simplify. + propositional. + + left. + right. + apply H. + equality. + + right. + eapply H2. + eassumption. + assumption. +Qed. + +Definition fact_correct (original_input : nat) (st : fact_state) : Prop := + match st with + | AnswerIs ans => fact original_input = ans + | WithAccumulator _ _ => True + end. + +Theorem fact_init_is : forall original_input, + fact_init original_input = {WithAccumulator original_input 1}. +Proof. + simplify. + apply sets_equal; simplify. + propositional. + + invert H. + equality. + + rewrite <- H0. + constructor. +Qed. + +Theorem singleton_in : forall {A} (x : A), + {x} x. +Proof. + simplify. + equality. +Qed. + +Theorem factorial_ok_2 : + invariantFor (factorial_sys 2) (fact_correct 2). +Proof. + simplify. + eapply invariantFor_weaken. + + apply multiStepClosure_ok. + simplify. + rewrite fact_init_is. + + eapply MscStep. + apply oneStepClosure_split; simplify. + invert H; simplify. + apply singleton_in. + apply oneStepClosure_empty. + simplify. + + eapply MscStep. + apply oneStepClosure_split; simplify. + invert H; simplify. + apply singleton_in. + apply oneStepClosure_split; simplify. + invert H; simplify. + apply singleton_in. + apply oneStepClosure_empty. + simplify. + + eapply MscStep. + apply oneStepClosure_split; simplify. + invert H; simplify. + apply singleton_in. + apply oneStepClosure_split; simplify. + invert H; simplify. + apply singleton_in. + apply oneStepClosure_split; simplify. + invert H; simplify. + apply singleton_in. + apply oneStepClosure_split; simplify. + invert H; simplify. + apply singleton_in. + apply oneStepClosure_empty. + simplify. + + apply MscDone. + apply prove_oneStepClosure; simplify. + propositional. + propositional; invert H0; try equality. + invert H; equality. + invert H1; equality. + invert H; equality. + invert H; try equality. + + simplify. + propositional; subst; simplify; propositional. + (* ^-- *) +Qed. diff --git a/Sets.v b/Sets.v index 7df06d3..2e7923b 100644 --- a/Sets.v +++ b/Sets.v @@ -112,6 +112,17 @@ Section properties. specialize (H1 x0). tauto. Qed. + + Variables ss1 ss2 : list A. + + Theorem union_constant : constant ss1 \cup constant ss2 = constant (ss1 ++ ss2). + Proof. + unfold constant, union; simpl. + + apply sets_equal; simpl; intuition. + Qed. End properties. Hint Resolve subseteq_refl subseteq_In. + +Hint Rewrite union_constant. diff --git a/TransitionSystems.v b/TransitionSystems.v index 164a2e6..ef37767 100644 --- a/TransitionSystems.v +++ b/TransitionSystems.v @@ -190,6 +190,8 @@ Lemma invariant_induction' : forall {state} (sys : trsys state) -> invariant s'. Proof. induct 2; propositional. + (* [propositional]: simplify the goal according to the rules of propositional + * logic. *) apply IHtrc. eapply H. @@ -647,13 +649,13 @@ Qed. * a more general fact, about when one invariant implies another. *) Theorem invariantFor_weaken : forall {state} (sys : trsys state) (invariant1 invariant2 : state -> Prop), - (forall s, invariant1 s -> invariant2 s) - -> invariantFor sys invariant1 + invariantFor sys invariant1 + -> (forall s, invariant1 s -> invariant2 s) -> invariantFor sys invariant2. Proof. unfold invariantFor; simplify. - apply H. - eapply H0. + apply H0. + eapply H. eassumption. assumption. Qed. @@ -676,6 +678,8 @@ Proof. (* Note the use of a [with] clause to specify a quantified variable's * value. *) + apply increment2_invariant_ok. + simplify. invert H0. unfold increment2_right_answer; simplify. @@ -685,6 +689,5 @@ Proof. simplify. equality. - apply increment2_invariant_ok. assumption. Qed.