Update prelude. Reorganize list functions.

theories/base.v

@@ -266,6 +266,22 @@ Class Filter A B :=
 
 (* Arguments filter {_ _ _} _ {_} !_ / : simpl nomatch. *)
 
+(** We define variants of the relations [(≡)] and [(⊆)] that are indexed by
+an environment. *)
+Class EquivEnv A B := equiv_env : A → relation B.
+Notation "X ≡@{ E } Y" := (equiv_env E X Y)
+  (at level 70, format "X  ≡@{ E }  Y") : C_scope.
+Notation "(≡@{ E } )" := (equiv_env E)
+  (E at level 1, only parsing) : C_scope.
+Instance: Params (@equiv_env) 4.
+
+Class SubsetEqEnv A B := subseteq_env : A → relation B.
+Notation "X ⊆@{ E } Y" := (subseteq_env E X Y)
+  (at level 70, format "X  ⊆@{ E }  Y") : C_scope.
+Notation "(⊆@{ E } )" := (subseteq_env E)
+  (E at level 1, only parsing) : C_scope.
+Instance: Params (@subseteq_env) 4.
+
 (** ** Monadic operations *)
 (** We define operational type classes for the monadic operations bind, join 
 and fmap. These type classes are defined in a non-standard way by taking the
@@ -282,7 +298,7 @@ in the appropriate way, and so that it can be used for mutual recursion
 (the mapped function [f] is not part of the fixpoint) as well. This is a hack,
 and should be replaced by something more appropriate in future versions. *)
 
-(* We use these type classes merely for convenient overloading of notations and
+(** We use these type classes merely for convenient overloading of notations and
 do not formalize any theory on monads (we do not even define a class with the
 monad laws). *)
 Class MRet (M : Type → Type) := mret: ∀ {A}, A → M A.
@@ -316,11 +332,12 @@ Class MGuard (M : Type → Type) :=
   mguard: ∀ P {dec : Decision P} {A}, M A → M A.
 Notation "'guard' P ; o" := (mguard P o)
   (at level 65, only parsing, next at level 35, right associativity) : C_scope.
+Arguments mguard _ _ _ !_ _ !_ / : simpl nomatch.
 
 (** ** Operations on maps *)
 (** In this section we define operational type classes for the operations
 on maps. In the file [fin_maps] we will axiomatize finite maps.
-The function lookup [m !! k] should yield the element at key [k] in [m]. *)
+The function look up [m !! k] should yield the element at key [k] in [m]. *)
 Class Lookup (K A M : Type) :=
   lookup: K → M → option A.
 Instance: Params (@lookup) 4.

theories/mapset.v

@@ -47,9 +47,14 @@ Proof.
     apply option_eq. intros []. by apply E.
 Qed.
 
-Global Instance mapset_eq_dec `{∀ m1 m2 : M unit, Decision (m1 = m2)} :
-  ∀ X1 X2 : mapset M, Decision (X1 = X2) | 1.
-Proof. solve_decision. Defined.
+Global Instance mapset_eq_dec `{∀ m1 m2 : M unit, Decision (m1 = m2)}
+    (X1 X2 : mapset M) : Decision (X1 = X2) | 1.
+Proof.
+ refine
+  match X1, X2 with
+  | Mapset m1, Mapset m2 => cast_if (decide (m1 = m2))
+  end; abstract congruence.
+Defined.
 Global Instance mapset_elem_of_dec x (X : mapset M) :
   Decision (x ∈ X) | 1.
 Proof. solve_decision. Defined.

theories/nmap.v

@@ -12,9 +12,15 @@ Arguments Nmap_0 {_} _.
 Arguments Nmap_pos {_} _.
 Arguments NMap {_} _ _.
 
-Instance Pmap_dec `{∀ x y : A, Decision (x = y)} :
-  ∀ x y : Nmap A, Decision (x = y).
-Proof. solve_decision. Defined.
+Instance Nmap_eq_dec `{∀ x y : A, Decision (x = y)} (t1 t2 : Nmap A) :
+  Decision (t1 = t2).
+Proof.
+ refine
+  match t1, t2 with
+  | NMap x t1, NMap y t2 =>
+    cast_if_and (decide (x = y)) (decide (t1 = t2))
+  end; abstract congruence.
+Defined.
 
 Instance Nempty {A} : Empty (Nmap A) := NMap None ∅.
 Instance Nlookup {A} : Lookup N A (Nmap A) := λ i t,

theories/option.v

@@ -122,6 +122,14 @@ Instance option_fmap: FMap option := @option_map.
 Instance option_guard: MGuard option := λ P dec A x,
   if dec then x else None.
 
+Definition mapM `{!MBind M} `{!MRet M} {A B}
+    (f : A → M B) : list A → M (list B) :=
+  fix go l :=
+  match l with
+  | [] => mret []
+  | x :: l => y ← f x; k ← go l; mret (y :: k)
+  end.
+
 Lemma fmap_is_Some {A B} (f : A → B) (x : option A) :
   is_Some (f <$> x) ↔ is_Some x.
 Proof. split; inversion 1. by destruct x. done. Qed.
@@ -138,6 +146,51 @@ Proof. by destruct x. Qed.
 Lemma option_bind_assoc {A B C} (f : A → option B)
     (g : B → option C) (x : option A) : (x ≫= f) ≫= g = x ≫= (mbind g ∘ f).
 Proof. by destruct x; simpl. Qed.
+Lemma option_bind_ext {A B} (f g : A → option B) x y :
+  (∀ a, f a = g a) →
+  x = y →
+  x ≫= f = y ≫= g.
+Proof. intros. destruct x, y; simplify_equality; simpl; auto. Qed.
+Lemma option_bind_ext_fun {A B} (f g : A → option B) x :
+  (∀ a, f a = g a) →
+  x ≫= f = x ≫= g.
+Proof. intros. by apply option_bind_ext. Qed.
+
+Section mapM.
+  Context {A B : Type} (f : A → option B).
+
+  Lemma mapM_ext (g : A → option B) l :
+    (∀ x, f x = g x) → mapM f l = mapM g l.
+  Proof. intros Hfg. by induction l; simpl; rewrite ?Hfg, ?IHl. Qed.
+  Lemma Forall2_mapM_ext (g : A → option B) l k :
+    Forall2 (λ x y, f x = g y) l k → mapM f l = mapM g k.
+  Proof.
+    induction 1 as [|???? Hfg ? IH]; simpl. done. by rewrite Hfg, IH.
+  Qed.
+  Lemma Forall_mapM_ext (g : A → option B) l :
+    Forall (λ x, f x = g x) l → mapM f l = mapM g l.
+  Proof.
+    induction 1 as [|?? Hfg ? IH]; simpl. done. by rewrite Hfg, IH.
+  Qed.
+
+  Lemma mapM_Some_1 l k :
+    mapM f l = Some k → Forall2 (λ x y, f x = Some y) l k.
+  Proof.
+    revert k. induction l as [|x l]; intros [|y k]; simpl; try done.
+    * destruct (f x); simpl; [|discriminate]. by destruct (mapM f l).
+    * destruct (f x) eqn:?; simpl; [|discriminate].
+      destruct (mapM f l); intros; simplify_equality. constructor; auto.
+  Qed.
+  Lemma mapM_Some_2 l k :
+    Forall2 (λ x y, f x = Some y) l k → mapM f l = Some k.
+  Proof.
+    induction 1 as [|???? Hf ? IH]; simpl; [done |].
+    rewrite Hf. simpl. by rewrite IH.
+  Qed.
+  Lemma mapM_Some l k :
+    mapM f l = Some k ↔ Forall2 (λ x y, f x = Some y) l k.
+  Proof. split; auto using mapM_Some_1, mapM_Some_2. Qed.
+End mapM.
 
 Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat
   match goal with
@@ -222,11 +275,13 @@ Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat
     assert (y = x) by congruence; clear H2
   | H1 : ?o = Some ?x, H2 : ?o = None |- _ =>
     congruence
+  | H : mapM _ _ = Some _ |- _ => apply mapM_Some in H
   end.
 Tactic Notation "simplify_option_equality" :=
   simplify_option_equality by eauto.
 
-Hint Extern 100 => simplify_option_equality : simplify_option_equality.
+Hint Extern 800 =>
+  progress simplify_option_equality : simplify_option_equality.
 
 (** * Union, intersection and difference *)
 Instance option_union_with {A} : UnionWith A (option A) := λ f x y,

theories/orders.v

@@ -209,7 +209,7 @@ Section bounded_join_sl.
         by transitivity (X ∪ Y); [auto | rewrite E].
     * intros [E1 E2]. by rewrite E1, E2, (left_id _ _).
   Qed.
-  Lemma empty_list_union Xs : ⋃ Xs ≡ ∅ ↔ Forall (≡ ∅) Xs.
+  Lemma empty_union_list Xs : ⋃ Xs ≡ ∅ ↔ Forall (≡ ∅) Xs.
   Proof.
     split.
     * induction Xs; simpl; rewrite ?empty_union; intuition.
@@ -248,8 +248,8 @@ Section bounded_join_sl.
 
     Lemma empty_union_L X Y : X ∪ Y = ∅ ↔ X = ∅ ∧ Y = ∅.
     Proof. unfold_leibniz. apply empty_union. Qed.
-    Lemma empty_list_union_L Xs : ⋃ Xs = ∅ ↔ Forall (= ∅) Xs.
-    Proof. unfold_leibniz. apply empty_list_union. Qed.
+    Lemma empty_union_list_L Xs : ⋃ Xs = ∅ ↔ Forall (= ∅) Xs.
+    Proof. unfold_leibniz. apply empty_union_list. Qed.
   End leibniz.
 
   Section dec.
@@ -257,14 +257,14 @@ Section bounded_join_sl.
 
     Lemma non_empty_union X Y : X ∪ Y ≢ ∅ → X ≢ ∅ ∨ Y ≢ ∅.
     Proof. rewrite empty_union. destruct (decide (X ≡ ∅)); intuition. Qed.
-    Lemma non_empty_list_union Xs : ⋃ Xs ≢ ∅ → Exists (≢ ∅) Xs.
-    Proof. rewrite empty_list_union. apply (not_Forall_Exists _). Qed.
+    Lemma non_empty_union_list Xs : ⋃ Xs ≢ ∅ → Exists (≢ ∅) Xs.
+    Proof. rewrite empty_union_list. apply (not_Forall_Exists _). Qed.
 
     Context `{!LeibnizEquiv A}.
     Lemma non_empty_union_L X Y : X ∪ Y ≠ ∅ → X ≠ ∅ ∨ Y ≠ ∅.
     Proof. unfold_leibniz. apply non_empty_union. Qed.
-    Lemma non_empty_list_union_L Xs : ⋃ Xs ≠ ∅ → Exists (≠ ∅) Xs.
-    Proof. unfold_leibniz. apply non_empty_list_union. Qed.
+    Lemma non_empty_union_list_L Xs : ⋃ Xs ≠ ∅ → Exists (≠ ∅) Xs.
+    Proof. unfold_leibniz. apply non_empty_union_list. Qed.
   End dec.
 End bounded_join_sl.
 

theories/pmap.v

@@ -69,7 +69,7 @@ thereby obtain a data type that ensures canonicity. *)
 Definition Pmap A := dsig (@Pmap_wf A).
 
 (** * Operations on the data structure *)
-Global Instance Pmap_dec `{∀ x y : A, Decision (x = y)} (t1 t2 : Pmap A) :
+Global Instance Pmap_eq_dec `{∀ x y : A, Decision (x = y)} (t1 t2 : Pmap A) :
     Decision (t1 = t2) :=
   match Pmap_raw_eq_dec (`t1) (`t2) with
   | left H => left (proj2 (dsig_eq _ t1 t2) H)

theories/tactics.v

@@ -55,14 +55,10 @@ Ltac case_match :=
   | |- context [ match ?x with _ => _ end ] => destruct x eqn:?
   end.
 
-(** The tactic [assert T unless tac_fail by tac_success] is used to assert
-[T] only if it is not provable by [tac_fail]. This is useful to build other
-tactics where only propositions that are not trivially provable are being
-asserted. *)
-Tactic Notation "assert" constr(T)
-    "unless" tactic3(tac_fail) "by" tactic3(tac_success)  := first
-  [ assert T by tac_fail; fail 1
-  | assert T by tac_success ].
+(** The tactic [unless T by tac_fail] succeeds if [T] is not provable by
+the tactic [tac_fail]. *)
+Tactic Notation "unless" constr(T) "by" tactic3(tac_fail) :=
+  first [assert T by tac_fail; fail 1 | idtac].
 
 (** The tactic [repeat_on_hyps tac] repeatedly applies [tac] in unspecified
 order on all hypotheses until it cannot be applied to any hypothesis anymore. *)
@@ -255,21 +251,33 @@ Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) :=
   feed (fun p => let H':=fresh in pose proof p as H'; destruct H' as IP) H.
 
 (** Coq's [firstorder] tactic fails or loops on rather small goals already. In 
-particular, on those generated by the tactic [unfold_elem_ofs] to solve
-propositions on collections. The [naive_solver] tactic implements an ad-hoc
-and incomplete [firstorder]-like solver using Ltac's backtracking mechanism.
-The tactic suffers from the following limitations:
+particular, on those generated by the tactic [unfold_elem_ofs] which is used
+to solve propositions on collections. The [naive_solver] tactic implements an
+ad-hoc and incomplete [firstorder]-like solver using Ltac's backtracking
+mechanism. The tactic suffers from the following limitations:
 - It might leave unresolved evars as Ltac provides no way to detect that.
-- To avoid the tactic going into pointless loops, it just does not allow a
-  universally quantified hypothesis to be used more than once.
+- To avoid the tactic becoming too slow, we allow a universally quantified
+  hypothesis to be instantiated only once during each search path.
 - It does not perform backtracking on instantiation of universally quantified
   assumptions.
 
+We use a counter to make the search breath first. Breath first search ensures
+that a minimal number of hypotheses is instantiated, and thus reduced the
+posibility that an evar remains unresolved.
+
 Despite these limitations, it works much better than Coq's [firstorder] tactic
 for the purposes of this development. This tactic either fails or proves the
 goal. *)
+Lemma forall_and_distr (A : Type) (P Q : A → Prop) :
+  (∀ x, P x ∧ Q x) ↔ (∀ x, P x) ∧ (∀ x, Q x).
+Proof. firstorder. Qed.
+
 Tactic Notation "naive_solver" tactic(tac) :=
   unfold iff, not in *;
+  repeat match goal with
+  | H : context [∀ _, _ ∧ _ ] |- _ =>
+     repeat setoid_rewrite forall_and_distr in H; revert H
+  end;
   let rec go n :=
   repeat match goal with
   (**i intros *)
@@ -278,52 +286,43 @@ Tactic Notation "naive_solver" tactic(tac) :=
   | H : False |- _ => destruct H
   | H : _ ∧ _ |- _ => destruct H
   | H : ∃ _, _  |- _ => destruct H
+  | H : ?P → ?Q, H2 : ?Q |- _ => specialize (H H2)
   (**i simplify and solve equalities *)
   | |- _ => progress simpl in *
   | |- _ => progress simplify_equality
   (**i solve the goal *)
-  | |- _ => solve
-            [ eassumption
-            | symmetry; eassumption
-            | apply not_symmetry; eassumption
-            | reflexivity ]
+  | |- _ =>
+    solve
+    [ eassumption
+    | symmetry; eassumption
+    | apply not_symmetry; eassumption
+    | reflexivity ]
   (**i operations that generate more subgoals *)
   | |- _ ∧ _ => split
   | H : _ ∨ _ |- _ => destruct H
   (**i solve the goal using the user supplied tactic *)
   | |- _ => solve [tac]
   end;
-  (**i use recursion to enable backtracking on the following clauses. We use
-  a counter to minimize the number of instantiations, and thus to reduce the
-  number of potentially unresolved meta variables. *)
-  first
-  [ iter (fun n' =>
-    match goal with 
-    (**i instantiations of assumptions *)
-    | H : _ → _ |- _ =>
-      is_non_dependent H;
-      eapply H; clear H; go n'
-    | H : _ → _ |- _ =>
-      is_non_dependent H;
-      (**i create subgoals for all premises *)
-      efeed H using (fun p =>
-        match type of p with
-        | _ ∧ _ =>
-          let H' := fresh in pose proof p as H'; destruct H'
-        | ∃ _, _ =>
-          let H' := fresh in pose proof p as H'; destruct H'
-        | _ ∨ _ =>
-          let H' := fresh in pose proof p as H'; destruct H'
-        | False =>
-          let H' := fresh in pose proof p as H'; destruct H'
-        end) by (clear H; go n');
-      (**i solve these subgoals, but clear [H] to avoid loops *)
-      clear H; go n
-    end) (eval compute in (seq 0 n))
-  | match goal with
-    (**i instantiation of the conclusion *)
-    | |- ∃ x, _ => eexists; go n
-    | |- _ ∨ _ => first [left; go n | right; go n]
-    end]
-  in go 10.
+  (**i use recursion to enable backtracking on the following clauses. *)
+  match goal with
+  (**i instantiation of the conclusion *)
+  | |- ∃ x, _ => eexists; go n
+  | |- _ ∨ _ => first [left; go n | right; go n]
+  | _ =>
+    (**i instantiations of assumptions. *)
+    lazymatch n with
+    | S ?n' =>
+      (**i we give priority to assumptions that fit on the conclusion. *)
+      match goal with 
+      | H : _ → _ |- _ =>
+        is_non_dependent H;
+        eapply H; clear H; go n'
+      | H : _ → _ |- _ =>
+        is_non_dependent H;
+        try (eapply H; fail 2);
+        efeed pose proof H; clear H; go n'
+      end
+    end
+  end
+  in iter (fun n' => go n') (eval compute in (seq 0 6)).
 Tactic Notation "naive_solver" := naive_solver eauto.