diff --git a/Frap.v b/Frap.v index 245a755..26480e9 100644 --- a/Frap.v +++ b/Frap.v @@ -43,7 +43,8 @@ Ltac invert0 e := invert e; fail. Ltac invert1 e := invert0 e || (invert e; []). Ltac invert2 e := invert1 e || (invert e; [|]). -Ltac simplify := repeat progress (simpl in *; intros; try autorewrite with core in *); repeat removeDups. +Ltac simplify := repeat progress (simpl in *; intros; try autorewrite with core in *); + repeat (removeDups || doSubtract). Ltac propositional := intuition idtac. Ltac linear_arithmetic := intros; diff --git a/ModelChecking.v b/ModelChecking.v index 94e18ce..8e303f0 100644 --- a/ModelChecking.v +++ b/ModelChecking.v @@ -251,3 +251,169 @@ Theorem factorial_ok_4 : Proof. model_check. Qed. + + +(** * Getting smarter about not exploring from the same state twice *) + +(*Theorem oneStepClosure_new_done : forall state (sys : trsys state) (invariant : state -> Prop), + (forall st, sys.(Initial) st -> invariant st) + -> oneStepClosure_new sys invariant invariant + -> invariantFor sys invariant. +Proof. + unfold oneStepClosure_new. + propositional. + apply invariant_induction. + assumption. + simplify. + eapply H2. + eassumption. + assumption. +Qed.*) + +Inductive multiStepClosure_smarter {state} (sys : trsys state) + : (state -> Prop) -> (state -> Prop) -> (state -> Prop) -> Prop := +| MscsDone : forall inv worklist, + oneStepClosure sys inv inv + -> multiStepClosure_smarter sys inv worklist inv +| MscsStep : forall inv worklist inv' inv'', + oneStepClosure_new sys worklist inv' + -> multiStepClosure_smarter sys (inv \cup inv') (inv' \setminus inv) inv'' + -> multiStepClosure_smarter sys inv worklist inv''. + +Lemma multiStepClosure_smarter_ok' : forall state (sys : trsys state) + (inv worklist inv' : state -> Prop), + multiStepClosure_smarter sys inv worklist inv' + -> (forall st, sys.(Initial) st -> inv st) + -> invariantFor sys inv'. +Proof. + induct 1; simplify. + + apply oneStepClosure_done. + assumption. + assumption. + + apply IHmultiStepClosure_smarter. + simplify. + left. + apply H1. + assumption. +Qed. + +Theorem multiStepClosure_smarter_ok : forall state (sys : trsys state) (inv : state -> Prop), + multiStepClosure_smarter sys sys.(Initial) sys.(Initial) inv + -> invariantFor sys inv. +Proof. + simplify. + eapply multiStepClosure_smarter_ok'. + eassumption. + propositional. +Qed. + +Theorem oneStepClosure_new_empty : forall state (sys : trsys state), + oneStepClosure_new sys (constant nil) (constant nil). +Proof. + unfold oneStepClosure_new; propositional. +Qed. + +Theorem oneStepClosure_new_split : forall state (sys : trsys state) st sts (inv1 inv2 : state -> Prop), + (forall st', sys.(Step) st st' -> inv1 st') + -> oneStepClosure_new sys (constant sts) inv2 + -> oneStepClosure_new sys (constant (st :: sts)) (inv1 \cup inv2). +Proof. + unfold oneStepClosure_new; propositional. + + invert H1. + + left. + apply H. + assumption. + + right. + eapply H0. + eassumption. + assumption. +Qed. + +Theorem factorial_ok_2_smarter : + invariantFor (factorial_sys 2) (fact_correct 2). +Proof. + simplify. + eapply invariantFor_weaken. + + apply multiStepClosure_smarter_ok. + simplify. + + eapply MscsStep. + apply oneStepClosure_new_split; simplify. + invert H; simplify. + apply singleton_in. + apply oneStepClosure_new_empty. + simplify. + + eapply MscsStep. + apply oneStepClosure_new_split; simplify. + invert H; simplify. + apply singleton_in. + apply oneStepClosure_empty. + simplify. + + eapply MscsStep. + apply oneStepClosure_new_split; simplify. + invert H; simplify. + apply singleton_in. + apply oneStepClosure_empty. + simplify. + + apply MscsDone. + apply prove_oneStepClosure; simplify. + propositional. + propositional; invert H0; try equality. + invert H; equality. + invert H1; equality. + + simplify. + propositional; subst; simplify; propositional. +Qed. + +Ltac smodel_check_done := + apply MscsDone; apply prove_oneStepClosure; simplify; propositional; subst; + repeat match goal with + | [ H : _ |- _ ] => invert H + end; simplify; equality. + +Ltac smodel_check_step := + eapply MscsStep; [ + repeat ((apply oneStepClosure_new_empty; simplify) + || (apply oneStepClosure_new_split; [ simplify; + repeat match goal with + | [ H : _ |- _ ] => invert H + end; apply singleton_in | ])) + | simplify ]. + +Ltac smodel_check_steps1 := smodel_check_done || smodel_check_step. +Ltac smodel_check_steps := repeat smodel_check_steps1. + +Ltac smodel_check_find_invariant := + simplify; eapply invariantFor_weaken; [ + apply multiStepClosure_smarter_ok; simplify; smodel_check_steps + | ]. + +Ltac smodel_check := smodel_check_find_invariant; model_check_finish. + +Theorem factorial_ok_2_smarter_snazzy : + invariantFor (factorial_sys 2) (fact_correct 2). +Proof. + smodel_check. +Qed. + +Theorem factorial_ok_3_smarter_snazzy : + invariantFor (factorial_sys 3) (fact_correct 3). +Proof. + smodel_check. +Qed. + +Theorem factorial_ok_5_smarter_snazzy : + invariantFor (factorial_sys 5) (fact_correct 5). +Proof. + smodel_check. +Qed. diff --git a/Sets.v b/Sets.v index bf91761..c808620 100644 --- a/Sets.v +++ b/Sets.v @@ -18,6 +18,7 @@ Section set. Definition union (s1 s2 : set) : set := fun x => s1 x \/ s2 x. Definition intersection (s1 s2 : set) : set := fun x => s1 x /\ s2 x. + Definition minus (s1 s2 : set) : set := fun x => s1 x /\ ~s2 x. Definition complement (s : set) : set := fun x => ~s x. Definition subseteq (s1 s2 : set) := forall x, s1 x -> s2 x. @@ -39,6 +40,7 @@ Notation "{ x1 , .. , xN }" := (constant (cons x1 (.. (cons xN nil) ..))). Notation "[ P ]" := (check P). Infix "\cup" := union (at level 40). Infix "\cap" := intersection (at level 40). +Infix "\setminus" := minus (at level 70). Infix "\subseteq" := subseteq (at level 70). Infix "\subset" := subset (at level 70). Notation "[ x | P ]" := (scomp (fun x => P)). @@ -175,3 +177,64 @@ Ltac removeDups := || (apply RdNew; [ simpl; intuition congruence | ]) || (apply RdDup; [ simpl; intuition congruence | ])) end. + + +(** * Simplifying set subtraction with constant sets *) + +Inductive doSubtract A : list A -> list A -> list A -> Prop := +| DsNil : forall ls, doSubtract nil ls nil +| DsKeep : forall x ls ls0 ls', + ~List.In x ls0 + -> doSubtract ls ls0 ls' + -> doSubtract (x :: ls) ls0 (x :: ls') +| DsDrop : forall x ls ls0 ls', + List.In x ls + -> doSubtract ls ls0 ls' + -> doSubtract (x :: ls) ls0 ls'. + +Theorem doSubtract_fwd : forall A x (ls ls0 ls' : list A), + doSubtract ls ls0 ls' + -> List.In x ls + -> ~List.In x ls0 + -> List.In x ls'. +Proof. + induction 1; simpl; intuition. + subst; eauto. +Qed. + +Theorem doSubtract_bwd1 : forall A x (ls ls0 ls' : list A), + doSubtract ls ls0 ls' + -> List.In x ls' + -> List.In x ls. +Proof. + induction 1; simpl; intuition. +Qed. + +Theorem doSubtract_bwd2 : forall A x (ls ls0 ls' : list A), + doSubtract ls ls0 ls' + -> List.In x ls' + -> List.In x ls0 + -> False. +Proof. + induction 1; simpl; intuition. + subst; eauto. +Qed. + +Theorem doSubtract_ok : forall A (ls ls0 ls' : list A), + doSubtract ls ls0 ls' + -> constant ls \setminus constant ls0 = constant ls'. +Proof. + unfold minus. + intros. + apply sets_equal. + unfold constant; intuition eauto using doSubtract_fwd, doSubtract_bwd1, doSubtract_bwd2. +Qed. + +Ltac doSubtract := + match goal with + | [ |- context[constant ?ls \setminus constant ?ls0] ] => + erewrite (@doSubtract_ok _ ls ls0) + by repeat (apply DsNil + || (apply DsKeep; [ simpl; intuition congruence | ]) + || (apply DsDrop; [ simpl; intuition congruence | ])) + end.