Optimizing tactics for faster state-space exploration

ConcurrentSeparationLogic.v

@@ -1329,7 +1329,7 @@ Lemma lockChunks_lock' : forall l I linvs (f : nat -> nat) a,
     ~f a \in l
     -> nth_error linvs a = Some I
     -> (forall x y, f x = f y -> x = y)
-    -> bigstar (fun i I => (~f i \in l) ===> I)%sep linvs ===> I * bigstar (fun i I => (~(f i \in l \cup {f a})) ===> I)%sep linvs.
+    -> bigstar (fun i I => (~f i \in l) ===> I)%sep linvs ===> I * bigstar (fun i I => (~(f i \in {f a} \cup l)) ===> I)%sep linvs.
 Proof.
   induct linvs; simplify.
 
@@ -1362,7 +1362,7 @@ Qed.
 Lemma lockChunks_lock : forall a l I linvs,
     ~a \in l
     -> nth_error linvs a = Some I
-    -> lockChunks l linvs ===> I * lockChunks (l \cup {a}) linvs.
+    -> lockChunks l linvs ===> I * lockChunks ({a} \cup l) linvs.
 Proof.
   simp.
   apply lockChunks_lock' with (f := fun n => n); auto.

ConcurrentSeparationLogic_template.v

@@ -1232,7 +1232,7 @@ Lemma lockChunks_lock' : forall l I linvs (f : nat -> nat) a,
     ~f a \in l
     -> nth_error linvs a = Some I
     -> (forall x y, f x = f y -> x = y)
-    -> bigstar (fun i I => (~f i \in l) ===> I)%sep linvs ===> I * bigstar (fun i I => (~(f i \in l \cup {f a})) ===> I)%sep linvs.
+    -> bigstar (fun i I => (~f i \in l) ===> I)%sep linvs ===> I * bigstar (fun i I => (~(f i \in {f a} \cup l)) ===> I)%sep linvs.
 Proof.
   induct linvs; simplify.
 
@@ -1265,7 +1265,7 @@ Qed.
 Lemma lockChunks_lock : forall a l I linvs,
     ~a \in l
     -> nth_error linvs a = Some I
-    -> lockChunks l linvs ===> I * lockChunks (l \cup {a}) linvs.
+    -> lockChunks l linvs ===> I * lockChunks ({a} \cup l) linvs.
 Proof.
   simp.
   apply lockChunks_lock' with (f := fun n => n); auto.

Frap.v

@@ -174,7 +174,7 @@ Ltac simplify := repeat (unifyTails; pose proof I);
                        | [ H : True |- _ ] => clear H
                        end;
                 repeat progress (simpl in *; intros; try autorewrite with core in *; simpl_maps);
-                                 repeat (removeDups || doSubtract).
+                                 repeat (normalize_set || doSubtract).
 Ltac propositional := intuition idtac.
 
 Ltac linear_arithmetic := intros;
@@ -284,10 +284,21 @@ Ltac closure :=
 Ltac model_check_done :=
   apply MscDone; eapply oneStepClosure_solve; [ closure | simplify; solve [ sets ] ].
 
-Ltac model_check_step :=
+Ltac model_check_step0 :=
   eapply MscStep; [ closure | simplify ].
 
-Ltac model_check_steps1 := model_check_done || model_check_step.
+Ltac model_check_step :=
+  match goal with
+  | [ |- multiStepClosure _ ?inv1 _ _ ] =>
+    model_check_step0;
+    match goal with
+    | [ |- multiStepClosure _ ?inv2 _ _ ] =>
+      (assert (inv1 = inv2) by compare_sets; fail 3)
+      || idtac
+    end
+  end.
+
+Ltac model_check_steps1 := model_check_step || model_check_done.
 Ltac model_check_steps := repeat model_check_steps1.
 
 Ltac model_check_finish := simplify; propositional; subst; simplify; try equality; try linear_arithmetic.

Map.v

@@ -161,8 +161,8 @@ Module Type S.
   Hint Rewrite merge_empty1 merge_empty2 using solve [ eauto 1 ].
   Hint Rewrite merge_empty1_alt merge_empty2_alt using congruence.
 
-  Hint Rewrite merge_add1 using solve [ eauto | unfold Sets.In; autorewrite with core in *; simpl in *; intuition congruence ].
+  Hint Rewrite merge_add1 using solve [ eauto | unfold Sets.In; autorewrite with core in *; simpl in *; try (normalize_set; simpl); intuition congruence ].
-  Hint Rewrite merge_add1_alt using solve [ congruence | unfold Sets.In; autorewrite with core in *; simpl in *; intuition congruence ].
+  Hint Rewrite merge_add1_alt using solve [ congruence | unfold Sets.In; autorewrite with core in *; simpl in *; try (normalize_set; simpl); intuition congruence ].
 
   Axiom includes_intro : forall K V (m1 m2 : fmap K V),
       (forall k v, m1 $? k = Some v -> m2 $? k = Some v)

ModelChecking.v

@@ -161,11 +161,12 @@ Proof.
   simplify.
   propositional.
   
-  left.
   right.
+  left.
   apply H.
   equality.
 
+  right.
   right.
   eapply H2.
   eassumption.
@@ -197,6 +198,8 @@ Theorem fact_init_is : forall original_input,
 Proof.
   simplify.
   apply sets_equal; simplify.
+  (* Note the use of a theorem [sets_equal], saying that sets are equal if they
+   * have the same elements. *)
   propositional.
 
   invert H.
@@ -209,7 +212,7 @@ Qed.
 (* Now we will prove that factorial is correct, for the input 2, without needing
  * to write out an inductive invariant ourselves.  Note that it's important that
  * we choose a small, constant input, so that the reachable state space is
- * finite. *)
+ * finite and tractable. *)
 Theorem factorial_ok_2 :
   invariantFor (factorial_sys 2) (fact_correct 2).
 Proof.
@@ -297,17 +300,17 @@ Theorem singleton_in_other : forall {A} (x : A) (s1 s2 : set A),
 Proof.
   simplify.
   right.
+  right.
   assumption.
 Qed.
 
 Ltac singletoner :=
   repeat match goal with
-         (* | _ => apply singleton_in *)
          | [ |- _ ?S ] => idtac S; apply singleton_in
          | [ |- (_ \cup _) _ ] => apply singleton_in_other
          end.
 
-Ltac model_check_step :=
+Ltac model_check_step0 :=
   eapply MscStep; [
     repeat ((apply oneStepClosure_empty; simplify)
             || (apply oneStepClosure_split; [ simplify;
@@ -316,7 +319,18 @@ Ltac model_check_step :=
                                                      end; solve [ singletoner ] | ]))
   | simplify ].
 
-Ltac model_check_steps1 := model_check_done || model_check_step.
+Ltac model_check_step :=
+  match goal with
+  | [ |- multiStepClosure _ ?inv1 _ ] =>
+    model_check_step0;
+    match goal with
+    | [ |- multiStepClosure _ ?inv2 _ ] =>
+      (assert (inv1 = inv2) by compare_sets; fail 3)
+      || idtac
+    end
+  end.
+
+Ltac model_check_steps1 := model_check_step || model_check_done.
 Ltac model_check_steps := repeat model_check_steps1.
 
 Ltac model_check_finish := simplify; propositional; subst; simplify; equality.
@@ -1573,4 +1587,3 @@ Theorem twoadd6_ok :
 Proof.
   twoadd.
 Qed.
-

ModelChecking_template.v

@@ -125,11 +125,12 @@ Proof.
   simplify.
   propositional.
   
-  left.
   right.
+  left.
   apply H.
   equality.
 
+  right.
   right.
   eapply H2.
   eassumption.
@@ -213,6 +214,7 @@ Theorem singleton_in_other : forall {A} (x : A) (s1 s2 : set A),
 Proof.
   simplify.
   right.
+  right.
   assumption.
 Qed.
 
@@ -222,7 +224,7 @@ Ltac singletoner :=
          | [ |- (_ \cup _) _ ] => apply singleton_in_other
          end.
 
-Ltac model_check_step :=
+Ltac model_check_step0 :=
   eapply MscStep; [
     repeat ((apply oneStepClosure_empty; simplify)
             || (apply oneStepClosure_split; [ simplify;
@@ -231,7 +233,18 @@ Ltac model_check_step :=
                                                      end; solve [ singletoner ] | ]))
   | simplify ].
 
-Ltac model_check_steps1 := model_check_done || model_check_step.
+Ltac model_check_step :=
+  match goal with
+  | [ |- multiStepClosure _ ?inv1 _ ] =>
+    model_check_step0;
+    match goal with
+    | [ |- multiStepClosure _ ?inv2 _ ] =>
+      (assert (inv1 = inv2) by compare_sets; fail 3)
+      || idtac
+    end
+  end.
+
+Ltac model_check_steps1 := model_check_step || model_check_done.
 Ltac model_check_steps := repeat model_check_steps1.
 
 Ltac model_check_finish := simplify; propositional; subst; simplify; equality.

Sets.v

@@ -127,7 +127,7 @@ End properties.
 
 Hint Resolve subseteq_refl subseteq_In.
 
-Hint Rewrite union_constant.
+(*Hint Rewrite union_constant.*)
 
 
 (** * Removing duplicates from constant sets *)
@@ -269,3 +269,320 @@ Ltac unifyTails :=
     | ?A -> Prop => unify x (constant (@nil A))
     end
   end.
+
+
+(** * But wait... there's a reflective way to do some of this, too. *)
+
+Require Import Arith.
+Import List ListNotations.
+
+Section setexpr.
+  Variable A : Type.
+
+  Inductive setexpr :=
+  | Literal (vs : list nat)
+  | Constant (s : set A)
+  | Union (e1 e2 : setexpr).
+
+  Fixpoint interp_setexpr (env : list A) (e : setexpr) : set A :=
+    match e with
+    | Literal vs =>
+      match env with
+      | [] => {}
+      | x :: _ => constant (map (nth_default x env) vs)
+      end
+    | Constant s => s
+    | Union e1 e2 => interp_setexpr env e1 \cup interp_setexpr env e2
+    end.
+
+  Record normal_form := {
+    Elements : list nat;
+    Other : option (set A)
+  }.
+
+  Fixpoint member (n : nat) (ls : list nat) : bool :=
+    match ls with
+    | [] => false
+    | m :: ls' => (n =? m) || member n ls'
+    end.
+
+  Fixpoint dedup (ls : list nat) : list nat :=
+    match ls with
+    | [] => []
+    | n :: ls =>
+      let ls' := dedup ls in
+      if member n ls' then ls' else n :: ls'
+    end.
+
+  Fixpoint setmerge (ls1 ls2 : list nat) : list nat :=
+    match ls1 with
+    | [] => ls2
+    | n :: ls1' =>
+      if member n ls2 then setmerge ls1' ls2 else n :: setmerge ls1' ls2
+    end.
+
+  Fixpoint normalize_setexpr (e : setexpr) : normal_form :=
+    match e with
+    | Literal vs => {| Elements := dedup vs; Other := None |}
+    | Constant s => {| Elements := []; Other := Some s |}
+    | Union e1 e2 =>
+      let nf1 := normalize_setexpr e1 in
+      let nf2 := normalize_setexpr e2 in
+        {| Elements := setmerge nf1.(Elements) nf2.(Elements);
+           Other := match nf1.(Other), nf2.(Other) with
+                    | None, None => None
+                    | o, None => o
+                    | None, o => o
+                    | Some s1, Some s2 => Some (s1 \cup s2)
+                    end |}
+    end.
+
+  Definition interp_normal_form (env : list A) (nf : normal_form) : set A :=
+    let cs := match env with
+              | [] => {}
+              | x :: _ => constant (map (nth_default x env) nf.(Elements))
+              end in
+    match nf.(Other) with
+    | None => cs
+    | Some o => cs \cup o
+    end.
+
+  Lemma member_ok : forall n ns,
+      if member n ns then In n ns else ~In n ns.
+  Proof.
+    induction ns; simpl; intuition.
+    case_eq (n =? a); simpl; intros.
+    apply beq_nat_true in H; auto.
+    apply beq_nat_false in H.
+    destruct (member n ns); intuition.
+  Qed.
+
+  Lemma In_dedup_fwd : forall n ns,
+      In n (dedup ns)
+      -> In n ns.
+  Proof.
+    induction ns; simpl; intuition.
+    pose proof (member_ok a (dedup ns)).
+    destruct (member a (dedup ns)); simpl in *; intuition.
+  Qed.
+
+  Lemma In_dedup_bwd : forall n ns,
+      In n ns
+      -> In n (dedup ns).
+  Proof.
+    induction ns; simpl; intuition.
+    pose proof (member_ok a (dedup ns)).
+    destruct (member a (dedup ns)); simpl in *; intuition congruence.
+    pose proof (member_ok a (dedup ns)).
+    destruct (member a (dedup ns)); simpl in *; intuition congruence.
+  Qed.
+
+  Lemma constant_dedup : forall (f : _ -> A) vs,
+      constant (map f (dedup vs)) = constant (map f vs).
+  Proof.
+    induction vs; simpl; intuition.
+    pose proof (member_ok a (dedup vs)).
+    case_eq (member a (dedup vs)); intro.
+    rewrite IHvs.
+    rewrite H0 in H.
+    apply In_dedup_fwd in H.
+    apply sets_equal.
+    unfold constant.
+    simpl.
+    intuition.
+    apply in_map_iff.
+    eauto.
+    simpl.
+    apply sets_equal.
+    simpl.
+    intuition congruence.
+  Qed.
+
+  Lemma constant_map_setmerge : forall (f : _ -> A) ns2 ns1,
+      constant (map f (setmerge ns1 ns2)) = constant (map f ns1) \cup constant (map f ns2).
+  Proof.
+    induction ns1; simpl; intros.
+
+    sets ltac:(simpl in *; intuition).
+
+    pose proof (member_ok a ns2).
+    destruct (member a ns2).
+    rewrite IHns1.
+    sets ltac:(simpl in *; intuition).
+    right.
+    eapply in_map_iff; eauto.
+
+    simpl.
+    sets ltac:(simpl in *; intuition).
+    change (In x (map f (setmerge ns1 ns2))) with ((fun x => In x (map f (setmerge ns1 ns2))) x) in H1.
+    rewrite IHns1 in H1.
+    tauto.
+    change (In x (map f (setmerge ns1 ns2))) with ((fun x => In x (map f (setmerge ns1 ns2))) x).
+    rewrite IHns1.
+    tauto.
+    change (In x (map f (setmerge ns1 ns2))) with ((fun x => In x (map f (setmerge ns1 ns2))) x).
+    rewrite IHns1.
+    tauto.
+  Qed.
+
+  Theorem normalize_setexpr_ok : forall env e,
+      interp_normal_form env (normalize_setexpr e) = interp_setexpr env e.
+  Proof.
+    induction e; simpl; intros.
+
+    unfold interp_normal_form; simpl.
+    destruct env; trivial.
+    apply constant_dedup.
+
+    unfold interp_normal_form; simpl.
+    destruct env; sets ltac:(simpl in *; intuition).
+
+    unfold interp_normal_form in *; simpl in *.
+    destruct (Other (normalize_setexpr e1)), (Other (normalize_setexpr e2)).
+    destruct env.
+    rewrite <- IHe1.
+    rewrite <- IHe2.
+    sets ltac:(simpl in *; intuition).
+    rewrite <- IHe1.
+    rewrite <- IHe2.
+    rewrite constant_map_setmerge.
+    sets ltac:(simpl in *; intuition).
+    destruct env.
+    rewrite <- IHe1.
+    rewrite <- IHe2.
+    sets ltac:(simpl in *; intuition).
+    rewrite constant_map_setmerge.
+    rewrite <- IHe1.
+    rewrite <- IHe2.
+    sets ltac:(simpl in *; intuition).
+    destruct env.
+    rewrite <- IHe1.
+    rewrite <- IHe2.
+    sets ltac:(simpl in *; intuition).
+    rewrite constant_map_setmerge.
+    rewrite <- IHe1.
+    rewrite <- IHe2.
+    sets ltac:(simpl in *; intuition).
+    destruct env.
+    rewrite <- IHe1.
+    rewrite <- IHe2.
+    sets ltac:(simpl in *; intuition).
+    rewrite constant_map_setmerge.
+    rewrite <- IHe1.
+    rewrite <- IHe2.
+    sets ltac:(simpl in *; intuition).
+  Qed.
+
+  Fixpoint included (ns1 ns2 : list nat) : bool :=
+    match ns1 with
+    | [] => true
+    | n :: ns1' => member n ns2 && included ns1' ns2
+    end.
+
+  Lemma included_true : forall ns2 ns1,
+      included ns1 ns2 = true
+      -> (forall x, In x ns1 -> In x ns2).
+  Proof.
+    induction ns1; simpl; intuition subst.
+
+    pose proof (member_ok x ns2).
+    destruct (member x ns2); simpl in *; auto; congruence.
+
+    pose proof (member_ok a ns2).
+    destruct (member a ns2); simpl in *; auto; congruence.
+  Qed.
+
+  Require Import Bool.
+
+  Theorem compare_sets : forall env e1 e2,
+      let nf1 := normalize_setexpr e1 in
+      let nf2 := normalize_setexpr e2 in
+      match Other nf1, Other nf2 with
+      | None, None => included nf1.(Elements) nf2.(Elements)
+                      && included nf2.(Elements) nf1.(Elements) = true
+      | _, _ => False
+      end
+      -> interp_setexpr env e1 = interp_setexpr env e2.
+  Proof.
+    intros.
+    do 2 rewrite <- normalize_setexpr_ok.
+    subst nf1.
+    subst nf2.
+    unfold interp_normal_form.
+    destruct (Other (normalize_setexpr e1)), (Other (normalize_setexpr e2)); intuition.
+    destruct env; trivial.
+    apply andb_true_iff in H; intuition.
+    specialize (included_true _ _ H0).
+    specialize (included_true _ _ H1).
+    clear H0 H1.
+    intros.
+    apply sets_equal.
+    unfold constant; simpl; intuition.
+    apply in_map_iff.
+    apply in_map_iff in H1.
+    firstorder.
+    apply in_map_iff.
+    apply in_map_iff in H1.
+    firstorder.
+  Qed.
+End setexpr.
+
+Ltac quote E env k :=
+  let T := type of E in
+  match eval hnf in T with
+  | ?A -> Prop => 
+    let rec lookup E env k :=
+        match env with
+        | [] => k 0 [E]
+        | E :: _ => k 0 env
+        | ?E' :: ?env' =>
+          lookup E env' ltac:(fun pos env'' => k (S pos) (E' :: env''))
+        end in
+
+    let rec lookups Es env k :=
+        match Es with
+        | [] => k (@nil nat) env
+        | ?E :: ?Es' =>
+          lookup E env ltac:(fun pos env' =>
+              lookups Es' env' ltac:(fun poss env'' =>
+                                       k (pos :: poss) env''))
+        end in
+
+    let rec quote' E env k :=
+        match E with
+        | constant ?Es =>
+          lookups Es env ltac:(fun poss env' => k (Literal A poss) env')
+        | ?E1 \cup ?E2 =>
+          quote' E1 env ltac:(fun e1 env' =>
+            quote' E2 env' ltac:(fun e2 env'' =>
+              k (Union e1 e2) env''))
+        | _ =>
+          (let pf := constr:(eq_refl : E = {}) in
+           k (Literal A []) env)
+          || k (Constant E) env
+        end in
+
+    quote' E env k
+  end.
+
+Ltac normalize_set :=
+  match goal with
+  | [ |- context[@union ?A ?X ?Y] ] =>
+    quote (@union A X Y) (@nil A) ltac:(fun e env =>
+      change (@union A X Y) with (interp_setexpr env e);
+      rewrite <- normalize_setexpr_ok;
+      cbv beta iota zeta delta [interp_normal_form normalize_setexpr nth_default
+                                setmerge Elements Other nth_error map dedup member beq_nat orb])
+  end.
+
+Ltac compare_sets :=
+  match goal with
+  | [ |- @eq ?T ?X ?Y ] =>
+    match eval hnf in T with
+    | ?A -> _ =>
+      quote X (@nil A) ltac:(fun x env =>
+        quote Y env ltac:(fun y env' =>
+          change (interp_setexpr env' x = interp_setexpr env' y);
+          apply compare_sets; reflexivity))
+    end
+  end.

_CoqProject

@@ -33,7 +33,7 @@ DeepAndShallowEmbeddings.v
 SepCancel.v
 SeparationLogic_template.v
 SeparationLogic.v
-SharedMemory.v
+#SharedMemory.v
 ConcurrentSeparationLogic_template.v
 ConcurrentSeparationLogic.v
 MessagesAndRefinement.v