Various minor improvements

examples/coq/Queens.v

@@ -68,7 +68,7 @@ Definition solveNQueens (n:nat) : Result (list (Int * Int)).
     (bind (nListSpace (range zero (natToInt n)) n)
       (fun xs:list Int => _))).
   refine (let ps := index xs in _).
-  refine (if isLegal ps then single ps else empty).
+  refine (guard isLegal ps).
 Defined.
 
 (* Proofs of completation and soundness for solution *)
@@ -674,12 +674,6 @@ Proof.
   apply indexPreservesFst'.
 Qed.
 
-Fixpoint countUp (n : nat) (start : Int) : list Int :=
-  match n with
-  | S n' => start :: countUp n' (plus one start)
-  | O => []
-  end.
-
 Lemma sndIndexCountsUp' {A} : forall (l : list A) (i : Int),
     map snd (index' i l) = countUp (length l) i.
 Proof.
@@ -762,22 +756,6 @@ Proof.
   * congruence.
 Qed.
 
-Fixpoint zCountUp (n : nat) (start : Z) : list Z :=
-  match n with
-  | S n' => start :: zCountUp n' (1 + start)
-  | O => []
-  end.
-
-Lemma countUpToZCountUp : forall (n : nat) (start : Int),
-    countUp n start = map zToInt (zCountUp n ⟦ start ⟧).
-Proof.
-  intro n. induction n; intros.
-  * reflexivity.
-  * cbn [countUp zCountUp map].
-    rewrite IHn.
-    space_crush.
-Qed.
-
 Lemma sortedBySecond : forall (l : list (Z*Z)),
     Sorted.LocallySorted (fun p1 p2 => is_true (leb (snd p1) (snd p2))) l
     -> Sorted.LocallySorted (fun z1 z2 => is_true (leb z1 z2)) (map snd l).
@@ -818,12 +796,13 @@ Proof.
       lia.
     }
     specialize (IHStronglySorted (length l) (1 + i) eq_refl ltac:(auto) Range').
+    change (zCountUp _ _) with (i :: zCountUp (length l) (1 + i)).
     rewrite <- IHStronglySorted.
 
     f_equal.
     destruct l as [|b l].
     + specialize (Range _ (or_introl eq_refl)). simpl in Range. omega.
-    + assert (b = 1 + i) by (cbn [length zCountUp] in IHStronglySorted; congruence).
+    + assert (b = 1 + i) by (cbn [length zCountUp tabulate] in IHStronglySorted; congruence).
       assert (a < b) by intuition.
       omega.
 Qed.
@@ -910,9 +889,7 @@ Lemma correctArrangementsInIndex : forall (p : list (Z*Z)) (n : nat),
     correct n p ->
     (exists p', Permutation p p'
            /\ Ensembles.In ⟦ bind (nListSpace (range zero (natToInt n)) n)
-                                 (fun xs:list Int => if isLegal (index xs)
-                                                  then single (index xs)
-                                                  else empty) ⟧
+                                 (fun xs:list Int => guard isLegal (index xs)) ⟧
                           (map zTupleToIntTuple p')).
 Proof.
   intros.
@@ -937,6 +914,7 @@ Proof.
     destruct Hin.
     assumption.
   * erewrite <- sortedIndex by eauto.
+    space_crush.
     rewrite (proj2 (isLegalIffNoCollisions _))
       by (rewrite intToZInvolutiveMap; unfold correct in *; intuition).
     space_crush.

src/coq/BasicTactics.v

@@ -23,18 +23,17 @@ Ltac break_match :=
   | [ |- context [match ?X with _ => _ end] ] => destruct X eqn:?
   end.
 
+Lemma implb_true_iff : forall b1 b2,
+      implb b1 b2 = true <->
+      (b1 = true -> b2 =true).
+Proof.
+  destruct b1, b2; simpl; intuition congruence.
+Qed.
+
+Hint Rewrite andb_true_iff orb_true_iff negb_true_iff implb_true_iff : bool.
+Hint Rewrite andb_false_iff orb_false_iff negb_false_iff : bool.
+Hint Rewrite Z.leb_le Z.ltb_lt : bool.
+
 (* Convert various boolean things to Propositional things, eg && becomes /\, etc. *)
 Ltac do_bool :=
-  repeat
-    match goal with
-    | [ H : _ && _ = true |- _ ] => apply andb_true_iff in H; destruct H
-    | [ H : _ || _ = false |- _ ] => apply orb_false_iff in H; destruct H
-    | [ H : negb _ = true |- _ ] => apply negb_true_iff in H
-    | [ H : context [(_ <=? _) = true] |- _ ] => rewrite Z.leb_le in H
-    | [ H : context [(_ <? _) = true] |- _ ] => rewrite Z.ltb_lt in H
-    | [ |- context [_ && _ = true] ] => rewrite andb_true_iff
-    | [ |- context [_ || _ = false] ] => rewrite orb_false_iff
-    | [ |- context [negb _ = true] ] => rewrite negb_true_iff
-    | [ |- context [(_ <=? _) = true] ] => rewrite Z.leb_le
-    | [ |- context [(_ <? _) = true] ] => rewrite Z.ltb_lt
-    end.
+  autorewrite with bool in *.

src/coq/EnsemblesEx.v

@@ -5,8 +5,16 @@ Arguments In {_} / _ _.
 Arguments Same_set / {_} _ _.
 Arguments Included / {_} _ _.
 
+Module EnsembleNotations.
+  Delimit Scope ensemble with ensemble.
+  Bind Scope ensemble with Ensemble.
+  Notation "x ∈ E" := (Ensembles.In E x) (at level 42) : ensemble.
+  Open Scope ensemble.
+End EnsembleNotations.
+Import EnsembleNotations.
+
 Inductive BigUnion A B (s:Ensemble A) (f:A -> Ensemble B) : Ensemble B :=
-| bigUnion a b : In s a -> In (f a) b -> In (BigUnion A B s f) b.
+| bigUnion a b : a ∈ s -> b ∈ f a -> b ∈ BigUnion A B s f.
 
 Lemma singletonIsEqual {A a} : Singleton A a = (fun a' => a = a').
   apply Extensionality_Ensembles.

src/coq/ListEx.v

@@ -53,6 +53,7 @@ Proof.
   induction l; simpl; intros.
   - constructor.
   - do_bool.
+    intuition.
     constructor; auto.
     rewrite <- elem_In with (H := H).
     congruence.
@@ -85,3 +86,19 @@ Proof.
   invc H0.
   f_equal; auto.
 Qed.
+
+Definition tabulate {A} (f : A -> A) :=
+  fix rec (n : nat) (acc : A) : list A :=
+    match n with
+    | 0 => []
+    | S n => acc :: rec n (f acc)
+    end.
+
+Lemma tabulate_map :
+  forall A B fA fB (g : A -> B),
+    (forall b, fA (g b) = g (fB b)) ->
+    forall n a b, a = g b -> tabulate fA n a = List.map g (tabulate fB n b).
+Proof.
+  induction n; simpl; intros; auto.
+  f_equal; auto. apply IHn. congruence.
+Qed.

src/coq/Space/Basic.v

@@ -1,6 +1,7 @@
 Require Import EnsemblesEx.
 Require Import Denotation.
 Require Import Basics.
+Require Import BasicTactics.
 
 Export EnsemblesEx.
 Export Denotation.
@@ -23,3 +24,15 @@ Class Basic := {
 }.
 
 Definition map `{S:Basic} {A B} (f:A->B) s := bind s (single ∘ f).
+
+Definition guard `{Basic}{A} (p : A -> bool) (a : A) : Space A :=
+  if p a then single a else empty.
+
+Lemma denoteGuardOk : forall `{Basic} A (p : A -> bool) (a : A),
+    denote (guard p a) = if p a then denote (single a) else denote empty.
+Proof.
+  unfold guard.
+  intros.
+  break_if; auto.
+Qed.
+

src/coq/Space/Integer.v

@@ -2,6 +2,7 @@ Require Import Basic.
 Require Import Full.
 Require Import ZArith.
 Require Import EqDec.
+Require ListEx.
 
 Export ZArith.
 
@@ -98,5 +99,34 @@ Section Definitions.
     refine (if (andb (le n v) (lt v m))
             then single v else empty).
   Defined.
+
+  Definition countUp (n : nat) (start : Int) : list Int :=
+    ListEx.tabulate (plus one) n start.
+
+  Definition zCountUp (n : nat) (start : Z) : list Z :=
+    ListEx.tabulate (Z.add 1) n start.
+
+  Lemma countUpToZCountUp : forall (n : nat) (start : Int),
+      countUp n start = List.map fromZ (zCountUp n ⟦ start ⟧).
+  Proof.
+    intros.
+    unfold countUp, zCountUp.
+    apply ListEx.tabulate_map.
+    intros.
+    - apply denoteInjective.
+      now rewrite denotePlusOk, denoteOneOk, !denoteFromZOk.
+    - now rewrite fromZInv.
+  Qed.
 End Definitions.
 
+Module IntegerNotations.
+  Delimit Scope int with int.
+  Bind Scope int with Int.
+
+  Infix "+"   := plus   : int.
+  Infix "-"   := minus  : int.
+  Infix "<=?" := le     : int.
+  Infix "<?"  := lt     : int.
+
+  Open Scope int.
+End IntegerNotations.

src/coq/Space/Tactics.v

@@ -8,7 +8,7 @@ Require Export BasicTactics.
 (* Add all the denotation lemmas to a rewrite database. As SpaceSearch expands,
    any new denotation lemmas should be added to the database. *)
 Hint Rewrite @denoteEmptyOk @denoteSingleOk @denoteBindOk @bigUnionIsExists : space.
-Hint Rewrite @denoteFullOk : space.
+Hint Rewrite @denoteFullOk @denoteGuardOk : space.
 Hint Rewrite @denoteZeroOk @denoteOneOk @denotePlusOk @denoteLeOk @denoteEqualOk : space.
 Hint Rewrite @denoteLtOk @denoteFromZOk @denoteMinusOk @fromZInv : space.
 
@@ -42,11 +42,17 @@ Ltac break_space :=
   repeat
     match goal with
     | [ H : Ensembles.In (fun _ => exists _, _ /\ _) _ |- _ ] => destruct H as (? & ? & ?)
-    | [ H : Ensembles.In (fun _ => Singleton _ _ _) _ |- _ ] => inversion H; clear H; subst
-    | [ H : Ensembles.In (fun _ => Empty_set _ _) _ |- _ ] => inversion H
+    | [ H : Ensembles.In (Singleton _ _) _ |- _ ] => invc H
+    | [ H : Ensembles.In (Empty_set _) _ |- _ ] => invc H
     | [ H : exists _, _ /\ _ |- _ ] => destruct H as (? & ? & ?)
-    | [ H : Singleton _ _ _ |- _ ] => inversion H; clear H; subst
-    | [ H : Empty_set _ _ |- _ ] => inversion H
+    | [ H : Singleton _ _ _ |- _ ] => invc H
+    | [ H : Empty_set _ _ |- _ ] => invc H
+    end.
+
+Ltac break_and :=
+  repeat
+    match goal with
+    | [ H : _ /\ _ |- _ ] => destruct H
     end.
 
 (* The main SpaceSearch workhorse tactic. Repeatedly rewrite by denotation
@@ -57,5 +63,5 @@ Ltac space_crush :=
   repeat
     (autorewrite with list space in *;
      break_space;
-     do_bool);
+     do_bool; break_and);
   auto with space.