Smarter ModelChecking with a worklist

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;

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.

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.