CHANGELOG.md

@@ -7,8 +7,38 @@ API-breaking change is listed.
 - Add lemma `lookup_total_fmap`.
 - Add lemmas about `last` and `head`: `last_app_Some`, `last_app_None`,
   `head_app_Some`, `head_app_None` and `head_app`. (by Marijn van Wezel)
-- Add tactic `notypeclasses apply` that works like `notypeclasses refine` but
-  automatically adds `_` until the given lemma takes no more arguments.
+- Rename `map_filter_empty_iff` to `map_empty_filter` and add
+  `map_empty_filter_1` and `map_empty_filter_2`. (by Michael Sammler)
+- Add lemma about `zip_with`: `lookup_zip_with_None` and add lemmas for `zip`:
+ `length_zip`, `zip_nil_inv`, `lookup_zip_Some`,`lookup_zip_None`. (by Kimaya Bedarkar)
+- Add `elem_of_seq` and `seq_nil`. (by Kimaya Bedarkar)
+- Add lemmas `StronglySorted_app`, `StronglySorted_cons` and
+  `StronglySorted_app_2`. Rename lemmas
+  `elem_of_StronglySorted_app` → `StronglySorted_app_1_elem_of`,
+  `StronglySorted_app_inv_l` → `StronglySorted_app_1_l`
+  `StronglySorted_app_inv_r` → `StronglySorted_app_1_r`. (by Marijn van Wezel)
+- Add `SetUnfoldElemOf` instance for `dom` on `gmultiset`. (by Marijn van Wezel)
+- Split up `stdpp.list` into smaller files. Users should keep importing
+  `stdpp.list`; the organization into smaller modules is considered an
+  implementation detail. `stdpp.list_numbers` is now re-exported by `stdpp.list`
+  and also considered part of the list module, so existing imports should be
+  updated.
+- Remove `list_remove` and `list_remove_list`. There were no lemmas about these
+  functions; they existed solely to facilitate the proofs of decidability of
+  `submseteq` and `≡ₚ`, which have been refactored.
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+# length
+s/\bmap_filter_empty_iff\b/map_empty_filter/g
+# StronglySorted
+s/\belem_of_StronglySorted_app\b/StronglySorted_app_1_elem_of/g
+s/\bStronglySorted_app_inv_(l|r)\b/StronglySorted_app_1_\1/g
+EOF
+```
 
 ## std++ 1.11.0 (2024-10-30)
 

Makefile.coq.local

@@ -45,7 +45,7 @@ tests/.coqdeps.d: $(TESTFILES)
 # - Cleanup, and mark as done for make.
 $(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref) $(NORMALIZER)
 	$(HIDE)REF=$*".ref" && \
-	  echo "COQTEST$(if $(COQ_REF),$(if $(MAKE_REF), [make ref],), [ref diff ignored]) $< (ref: $$REF)" && \
+	  echo "COQTEST$(if $(COQ_REF),$(if $(MAKE_REF), [make ref],), [ref ignored]) $< (ref: $$REF)" && \
 	  TMPFILE="$$(mktemp)" && \
 	  unset OCAMLRUNPARAM && \
 	  $(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
@@ -53,7 +53,7 @@ $(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref) $(NORMALIZER)
 	  mv "$$TMPFILE".new "$$TMPFILE" && \
 	  $(if $(COQ_REF),\
 	    $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff --strip-trailing-cr -u "$$REF" "$$TMPFILE"), \
-	    (diff --strip-trailing-cr -u "$$REF" "$$TMPFILE" || true) \
+	    true \
 	  ) && \
 	  rm -f "$$TMPFILE" && \
 	  touch $@

_CoqProject

@@ -52,6 +52,11 @@ stdpp/lexico.v
 stdpp/propset.v
 stdpp/decidable.v
 stdpp/list.v
+stdpp/list_basics.v
+stdpp/list_relations.v
+stdpp/list_monad.v
+stdpp/list_misc.v
+stdpp/list_tactics.v
 stdpp/list_numbers.v
 stdpp/functions.v
 stdpp/hlist.v

coq-lint.sh

-#!/bin/bash
+#!/bin/sh
 set -e
 ## A simple shell script checking for some common Coq issues.
 

stdpp/countable.v

@@ -313,6 +313,18 @@ Qed.
 (** ** Generic trees *)
 Local Close Scope positive.
 
+(** This type can help you construct a [Countable] instance for an arbitrary
+(even recursive) inductive datatype. The idea is tht you make [T] something like
+[T1 + T2 + ...], covering all the data types that can be contained inside your
+type.
+- Each non-recursive constructor to a [GenLeaf]. Different constructors must use
+  different variants of [T] to ensure they remain distinguishable!
+- Each recursive constructor to a [GenNode] where the [nat] is a (typically
+  small) constant representing the constructor itself, and then all the data in
+  the constructor (recursive or otherwise) is put into child nodes.
+
+This data type is the same as [GenTree.tree] in mathcomp, see
+https://github.com/math-comp/math-comp/blob/master/ssreflect/choice.v *)
 Inductive gen_tree (T : Type) : Type :=
   | GenLeaf : T → gen_tree T
   | GenNode : nat → list (gen_tree T) → gen_tree T.

stdpp/fin_maps.v

@@ -1858,7 +1858,7 @@ Section map_filter.
 
   Lemma map_filter_empty : filter P ∅ =@{M A} ∅.
   Proof. apply map_fold_empty. Qed.
-  Lemma map_filter_empty_iff m :
+  Lemma map_empty_filter m :
     filter P m = ∅ ↔ map_Forall (λ i x, ¬P (i,x)) m.
   Proof.
     rewrite map_empty. setoid_rewrite map_lookup_filter_None. split.
@@ -1866,6 +1866,14 @@ Section map_filter.
     - intros Hm i. destruct (m !! i) as [x|] eqn:?; [|by auto].
       right; intros ? [= <-]. by apply Hm.
   Qed.
+  Lemma map_empty_filter_1 m :
+    filter P m = ∅ →
+    map_Forall (λ i x, ¬P (i,x)) m.
+  Proof. apply map_empty_filter. Qed.
+  Lemma map_empty_filter_2 m :
+    map_Forall (λ i x, ¬P (i,x)) m →
+    filter P m = ∅.
+  Proof. apply map_empty_filter. Qed.
 
   Lemma map_filter_delete m i : filter P (delete i m) = delete i (filter P m).
   Proof.

stdpp/gmultiset.v

@@ -159,6 +159,13 @@ Section basic_lemmas.
 
   Global Instance gmultiset_elem_of_dec : RelDecision (∈@{gmultiset A}).
   Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
+
+  Lemma gmultiset_elem_of_dom x X : x ∈ dom X ↔ x ∈ X.
+  Proof.
+    unfold dom, gmultiset_dom, elem_of at 2, gmultiset_elem_of, multiplicity.
+    destruct X as [X]; simpl; rewrite elem_of_dom, <-not_eq_None_Some.
+    destruct (X !! x); naive_solver lia.
+  Qed.
 End basic_lemmas.
 
 (** * A solver for multisets *)
@@ -299,6 +306,9 @@ Section multiset_unfold.
     intros ??; constructor. rewrite gmultiset_elem_of_intersection.
     by rewrite (set_unfold_elem_of x X P), (set_unfold_elem_of x Y Q).
   Qed.
+  Global Instance set_unfold_gmultiset_dom x X :
+    SetUnfoldElemOf x (dom X) (x ∈ X).
+  Proof. constructor. apply gmultiset_elem_of_dom. Qed.
 End multiset_unfold.
 
 (** Step 3: instantiate hypotheses *)
@@ -554,12 +564,6 @@ Section more_lemmas.
       exists (x,n); split; [|by apply elem_of_map_to_list].
       apply elem_of_replicate; auto with lia.
   Qed.
-  Lemma gmultiset_elem_of_dom x X : x ∈ dom X ↔ x ∈ X.
-  Proof.
-    unfold dom, gmultiset_dom, elem_of at 2, gmultiset_elem_of, multiplicity.
-    destruct X as [X]; simpl; rewrite elem_of_dom, <-not_eq_None_Some.
-    destruct (X !! x); naive_solver lia.
-  Qed.
 
   (** Properties of the set_fold operation *)
   Lemma gmultiset_set_fold_empty {B} (f : A → B → B) (b : B) :

stdpp/list_numbers.v

 (** This file collects general purpose definitions and theorems on
 lists of numbers that are not in the Coq standard library. *)
-From stdpp Require Export list.
+From stdpp Require Export list_basics list_monad list_misc list_tactics.
 From stdpp Require Import options.
 
 (** * Definitions *)
@@ -98,6 +98,12 @@ Section seq.
     k ∈ seq j n ↔ j ≤ k < j + n.
   Proof. rewrite elem_of_list_In, in_seq. done. Qed.
 
+  Lemma seq_nil n m : seq n m = [] ↔ m = 0.
+  Proof. by destruct m. Qed.
+
+  Lemma seq_subseteq_mono m n1 n2 : n1 ≤ n2 → seq m n1 ⊆ seq m n2.
+  Proof. by intros Hle i Hi%elem_of_seq; apply elem_of_seq; lia. Qed.
+
   Lemma Forall_seq (P : nat → Prop) i n :
     Forall P (seq i n) ↔ ∀ j, i ≤ j < i + n → P j.
   Proof. rewrite Forall_forall. setoid_rewrite elem_of_seq. auto with lia. Qed.
@@ -118,6 +124,7 @@ Section seq.
     - rewrite take_nil. replace (m `min` 0) with 0 by lia. done.
     - destruct m; simpl; auto with f_equal.
   Qed.
+
 End seq.
 
 (** ** Properties of the [seqZ] function *)

stdpp/list_tactics.v

+From Coq Require Export Permutation.
+From stdpp Require Export numbers base option list_basics list_relations list_monad.
+From stdpp Require Import options.
+
+(** * Reflection over lists *)
+(** We define a simple data structure [rlist] to capture a syntactic
+representation of lists consisting of constants, applications and the nil list.
+Note that we represent [(x ::.)] as [rapp (rnode [x])]. For now, we abstract
+over the type of constants, but later we use [nat]s and a list representing
+a corresponding environment. *)
+Inductive rlist (A : Type) :=
+  rnil : rlist A | rnode : A → rlist A | rapp : rlist A → rlist A → rlist A.
+Global Arguments rnil {_} : assert.
+Global Arguments rnode {_} _ : assert.
+Global Arguments rapp {_} _ _ : assert.
+
+Module rlist.
+Fixpoint to_list {A} (t : rlist A) : list A :=
+  match t with
+  | rnil => [] | rnode l => [l] | rapp t1 t2 => to_list t1 ++ to_list t2
+  end.
+Notation env A := (list (list A)) (only parsing).
+Definition eval {A} (E : env A) : rlist nat → list A :=
+  fix go t :=
+  match t with
+  | rnil => []
+  | rnode i => default [] (E !! i)
+  | rapp t1 t2 => go t1 ++ go t2
+  end.
+
+(** A simple quoting mechanism using type classes. [QuoteLookup E1 E2 x i]
+means: starting in environment [E1], look up the index [i] corresponding to the
+constant [x]. In case [x] has a corresponding index [i] in [E1], the original
+environment is given back as [E2]. Otherwise, the environment [E2] is extended
+with a binding [i] for [x]. *)
+Section quote_lookup.
+  Context {A : Type}.
+  Class QuoteLookup (E1 E2 : list A) (x : A) (i : nat) := {}.
+  Global Instance quote_lookup_here E x : QuoteLookup (x :: E) (x :: E) x 0 := {}.
+  Global Instance quote_lookup_end x : QuoteLookup [] [x] x 0 := {}.
+  Global Instance quote_lookup_further E1 E2 x i y :
+    QuoteLookup E1 E2 x i → QuoteLookup (y :: E1) (y :: E2) x (S i) | 1000 := {}.
+End quote_lookup.
+
+Section quote.
+  Context {A : Type}.
+  Class Quote (E1 E2 : env A) (l : list A) (t : rlist nat) := {}.
+  Global Instance quote_nil E1 : Quote E1 E1 [] rnil := {}.
+  Global Instance quote_node E1 E2 l i:
+    QuoteLookup E1 E2 l i → Quote E1 E2 l (rnode i) | 1000 := {}.
+  Global Instance quote_cons E1 E2 E3 x l i t :
+    QuoteLookup E1 E2 [x] i →
+    Quote E2 E3 l t → Quote E1 E3 (x :: l) (rapp (rnode i) t) := {}.
+  Global Instance quote_app E1 E2 E3 l1 l2 t1 t2 :
+    Quote E1 E2 l1 t1 → Quote E2 E3 l2 t2 → Quote E1 E3 (l1 ++ l2) (rapp t1 t2) := {}.
+End quote.
+
+Section eval.
+  Context {A} (E : env A).
+
+  Lemma eval_alt t : eval E t = to_list t ≫= default [] ∘ (E !!.).
+  Proof.
+    induction t; csimpl.
+    - done.
+    - by rewrite (right_id_L [] (++)).
+    - rewrite bind_app. by f_equal.
+  Qed.
+  Lemma eval_eq t1 t2 : to_list t1 = to_list t2 → eval E t1 = eval E t2.
+  Proof. intros Ht. by rewrite !eval_alt, Ht. Qed.
+  Lemma eval_Permutation t1 t2 :
+    to_list t1 ≡ₚ to_list t2 → eval E t1 ≡ₚ eval E t2.
+  Proof. intros Ht. by rewrite !eval_alt, Ht. Qed.
+  Lemma eval_submseteq t1 t2 :
+    to_list t1 ⊆+ to_list t2 → eval E t1 ⊆+ eval E t2.
+  Proof. intros Ht. by rewrite !eval_alt, Ht. Qed.
+End eval.
+End rlist.
+
+(** * Tactics *)
+Ltac quote_Permutation :=
+  match goal with
+  | |- ?l1 ≡ₚ ?l2 =>
+    match type of (_ : rlist.Quote [] _ l1 _) with rlist.Quote _ ?E2 _ ?t1 =>
+    match type of (_ : rlist.Quote E2 _ l2 _) with rlist.Quote _ ?E3 _ ?t2 =>
+      change (rlist.eval E3 t1 ≡ₚ rlist.eval E3 t2)
+    end end
+  end.
+Ltac solve_Permutation :=
+  quote_Permutation; apply rlist.eval_Permutation;
+  compute_done.
+
+Ltac quote_submseteq :=
+  match goal with
+  | |- ?l1 ⊆+ ?l2 =>
+    match type of (_ : rlist.Quote [] _ l1 _) with rlist.Quote _ ?E2 _ ?t1 =>
+    match type of (_ : rlist.Quote E2 _ l2 _) with rlist.Quote _ ?E3 _ ?t2 =>
+      change (rlist.eval E3 t1 ⊆+ rlist.eval E3 t2)
+    end end
+  end.
+Ltac solve_submseteq :=
+  quote_submseteq; apply rlist.eval_submseteq;
+  compute_done.
+
+Ltac decompose_elem_of_list := repeat
+  match goal with
+  | H : ?x ∈ [] |- _ => by destruct (not_elem_of_nil x)
+  | H : _ ∈ _ :: _ |- _ => apply elem_of_cons in H; destruct H
+  | H : _ ∈ _ ++ _ |- _ => apply elem_of_app in H; destruct H
+  end.
+Ltac solve_length :=
+  simplify_eq/=;
+  repeat (rewrite length_fmap || rewrite length_app);
+  repeat match goal with
+  | H : _ =@{list _} _ |- _ => apply (f_equal length) in H
+  | H : Forall2 _ _ _ |- _ => apply Forall2_length in H
+  | H : context[length (_ <$> _)] |- _ => rewrite length_fmap in H
+  end; done || congruence.
+Ltac simplify_list_eq ::= repeat
+  match goal with
+  | _ => progress simplify_eq/=
+  | H : [?x] !! ?i = Some ?y |- _ =>
+    destruct i; [change (Some x = Some y) in H | discriminate]
+  | H : _ <$> _ = [] |- _ => apply fmap_nil_inv in H
+  | H : [] = _ <$> _ |- _ => symmetry in H; apply fmap_nil_inv in H
+  | H : zip_with _ _ _ = [] |- _ => apply zip_with_nil_inv in H; destruct H
+  | H : [] = zip_with _ _ _ |- _ => symmetry in H
+  | |- context [(_ ++ _) ++ _] => rewrite <-(assoc_L (++))
+  | H : context [(_ ++ _) ++ _] |- _ => rewrite <-(assoc_L (++)) in H
+  | H : context [_ <$> (_ ++ _)] |- _ => rewrite fmap_app in H
+  | |- context [_ <$> (_ ++ _)]  => rewrite fmap_app
+  | |- context [_ ++ []] => rewrite (right_id_L [] (++))
+  | H : context [_ ++ []] |- _ => rewrite (right_id_L [] (++)) in H
+  | |- context [take _ (_ <$> _)] => rewrite <-fmap_take
+  | H : context [take _ (_ <$> _)] |- _ => rewrite <-fmap_take in H
+  | |- context [drop _ (_ <$> _)] => rewrite <-fmap_drop
+  | H : context [drop _ (_ <$> _)] |- _ => rewrite <-fmap_drop in H
+  | H : _ ++ _ = _ ++ _ |- _ =>
+    repeat (rewrite <-app_comm_cons in H || rewrite <-(assoc_L (++)) in H);
+    apply app_inj_1 in H; [destruct H|solve_length]
+  | H : _ ++ _ = _ ++ _ |- _ =>
+    repeat (rewrite app_comm_cons in H || rewrite (assoc_L (++)) in H);
+    apply app_inj_2 in H; [destruct H|solve_length]
+  | |- context [zip_with _ (_ ++ _) (_ ++ _)] =>
+    rewrite zip_with_app by solve_length
+  | |- context [take _ (_ ++ _)] => rewrite take_app_length' by solve_length
+  | |- context [drop _ (_ ++ _)] => rewrite drop_app_length' by solve_length
+  | H : context [zip_with _ (_ ++ _) (_ ++ _)] |- _ =>
+    rewrite zip_with_app in H by solve_length
+  | H : context [take _ (_ ++ _)] |- _ =>
+    rewrite take_app_length' in H by solve_length
+  | H : context [drop _ (_ ++ _)] |- _ =>
+    rewrite drop_app_length' in H by solve_length
+  | H : ?l !! ?i = _, H2 : context [(_ <$> ?l) !! ?i] |- _ =>
+     rewrite list_lookup_fmap, H in H2
+  end.
+Ltac decompose_Forall_hyps :=
+  repeat match goal with
+  | H : Forall _ [] |- _ => clear H
+  | H : Forall _ (_ :: _) |- _ => rewrite Forall_cons in H; destruct H
+  | H : Forall _ (_ ++ _) |- _ => rewrite Forall_app in H; destruct H
+  | H : Forall2 _ [] [] |- _ => clear H
+  | H : Forall2 _ (_ :: _) [] |- _ => destruct (Forall2_cons_nil_inv _ _ _ H)
+  | H : Forall2 _ [] (_ :: _) |- _ => destruct (Forall2_nil_cons_inv _ _ _ H)
+  | H : Forall2 _ [] ?k |- _ => apply Forall2_nil_inv_l in H
+  | H : Forall2 _ ?l [] |- _ => apply Forall2_nil_inv_r in H
+  | H : Forall2 _ (_ :: _) (_ :: _) |- _ =>
+    apply Forall2_cons_1 in H; destruct H
+  | H : Forall2 _ (_ :: _) ?k |- _ =>
+    let k_hd := fresh k "_hd" in let k_tl := fresh k "_tl" in
+    apply Forall2_cons_inv_l in H; destruct H as (k_hd&k_tl&?&?&->);
+    rename k_tl into k
+  | H : Forall2 _ ?l (_ :: _) |- _ =>
+    let l_hd := fresh l "_hd" in let l_tl := fresh l "_tl" in
+    apply Forall2_cons_inv_r in H; destruct H as (l_hd&l_tl&?&?&->);
+    rename l_tl into l
+  | H : Forall2 _ (_ ++ _) ?k |- _ =>
+    let k1 := fresh k "_1" in let k2 := fresh k "_2" in
+    apply Forall2_app_inv_l in H; destruct H as (k1&k2&?&?&->)
+  | H : Forall2 _ ?l (_ ++ _) |- _ =>
+    let l1 := fresh l "_1" in let l2 := fresh l "_2" in
+    apply Forall2_app_inv_r in H; destruct H as (l1&l2&?&?&->)
+  | _ => progress simplify_eq/=
+  | H : Forall3 _ _ (_ :: _) _ |- _ =>
+    apply Forall3_cons_inv_m in H; destruct H as (?&?&?&?&?&?&?&?)
+  | H : Forall2 _ (_ :: _) ?k |- _ =>
+    apply Forall2_cons_inv_l in H; destruct H as (?&?&?&?&?)
+  | H : Forall2 _ ?l (_ :: _) |- _ =>
+    apply Forall2_cons_inv_r in H; destruct H as (?&?&?&?&?)
+  | H : Forall2 _ (_ ++ _) (_ ++ _) |- _ =>
+    apply Forall2_app_inv in H; [destruct H|solve_length]
+  | H : Forall2 _ ?l (_ ++ _) |- _ =>
+    apply Forall2_app_inv_r in H; destruct H as (?&?&?&?&?)
+  | H : Forall2 _ (_ ++ _) ?k |- _ =>
+    apply Forall2_app_inv_l in H; destruct H as (?&?&?&?&?)
+  | H : Forall3 _ _ (_ ++ _) _ |- _ =>
+    apply Forall3_app_inv_m in H; destruct H as (?&?&?&?&?&?&?&?)
+  | H : Forall ?P ?l, H1 : ?l !! _ = Some ?x |- _ =>
+    (* to avoid some stupid loops, not fool proof *)
+    unless (P x) by auto using Forall_app_2, Forall_nil_2;
+    let E := fresh in
+    assert (P x) as E by (apply (Forall_lookup_1 P _ _ _ H H1)); lazy beta in E
+  | H : Forall2 ?P ?l ?k |- _ =>
+    match goal with
+    | H1 : l !! ?i = Some ?x, H2 : k !! ?i = Some ?y |- _ =>
+      unless (P x y) by done; let E := fresh in
+      assert (P x y) as E by (by apply (Forall2_lookup_lr P l k i x y));
+      lazy beta in E
+    | H1 : l !! ?i = Some ?x |- _ =>
+      try (match goal with _ : k !! i = Some _ |- _ => fail 2 end);
+      destruct (Forall2_lookup_l P _ _ _ _ H H1) as (?&?&?)
+    | H2 : k !! ?i = Some ?y |- _ =>
+      try (match goal with _ : l !! i = Some _ |- _ => fail 2 end);
+      destruct (Forall2_lookup_r P _ _ _ _ H H2) as (?&?&?)
+    end
+  | H : Forall3 ?P ?l ?l' ?k |- _ =>
+    lazymatch goal with
+    | H1:l !! ?i = Some ?x, H2:l' !! ?i = Some ?y, H3:k !! ?i = Some ?z |- _ =>
+      unless (P x y z) by done; let E := fresh in
+      assert (P x y z) as E by (by apply (Forall3_lookup_lmr P l l' k i x y z));
+      lazy beta in E
+    | H1 : l !! _ = Some ?x |- _ =>
+      destruct (Forall3_lookup_l P _ _ _ _ _ H H1) as (?&?&?&?&?)
+    | H2 : l' !! _ = Some ?y |- _ =>
+      destruct (Forall3_lookup_m P _ _ _ _ _ H H2) as (?&?&?&?&?)
+    | H3 : k !! _ = Some ?z |- _ =>
+      destruct (Forall3_lookup_r P _ _ _ _ _ H H3) as (?&?&?&?&?)
+    end
+  end.
+Ltac list_simplifier :=
+  simplify_eq/=;
+  repeat match goal with
+  | _ => progress decompose_Forall_hyps
+  | _ => progress simplify_list_eq
+  | H : _ <$> _ = _ :: _ |- _ =>
+    apply fmap_cons_inv in H; destruct H as (?&?&?&?&?)
+  | H : _ :: _ = _ <$> _ |- _ => symmetry in H
+  | H : _ <$> _ = _ ++ _ |- _ =>
+    apply fmap_app_inv in H; destruct H as (?&?&?&?&?)
+  | H : _ ++ _ = _ <$> _ |- _ => symmetry in H
+  | H : zip_with _ _ _ = _ :: _ |- _ =>
+    apply zip_with_cons_inv in H; destruct H as (?&?&?&?&?&?&?&?)
+  | H : _ :: _ = zip_with _ _ _ |- _ => symmetry in H
+  | H : zip_with _ _ _ = _ ++ _ |- _ =>
+    apply zip_with_app_inv in H; destruct H as (?&?&?&?&?&?&?&?&?)
+  | H : _ ++ _ = zip_with _ _ _ |- _ => symmetry in H
+  end.
+Ltac decompose_Forall := repeat
+  match goal with
+  | |- Forall _ _ => by apply Forall_true
+  | |- Forall _ [] => constructor
+  | |- Forall _ (_ :: _) => constructor
+  | |- Forall _ (_ ++ _) => apply Forall_app_2
+  | |- Forall _ (_ <$> _) => apply Forall_fmap
+  | |- Forall _ (_ ≫= _) => apply Forall_bind
+  | |- Forall2 _ _ _ => apply Forall_Forall2_diag
+  | |- Forall2 _ [] [] => constructor
+  | |- Forall2 _ (_ :: _) (_ :: _) => constructor
+  | |- Forall2 _ (_ ++ _) (_ ++ _) => first
+    [ apply Forall2_app; [by decompose_Forall |]
+    | apply Forall2_app; [| by decompose_Forall]]
+  | |- Forall2 _ (_ <$> _) _ => apply Forall2_fmap_l
+  | |- Forall2 _ _ (_ <$> _) => apply Forall2_fmap_r
+  | _ => progress decompose_Forall_hyps
+  | H : Forall _ (_ <$> _) |- _ => rewrite Forall_fmap in H
+  | H : Forall _ (_ ≫= _) |- _ => rewrite Forall_bind in H
+  | |- Forall _ _ =>
+    apply Forall_lookup_2; intros ???; progress decompose_Forall_hyps
+  | |- Forall2 _ _ _ =>
+    apply Forall2_same_length_lookup_2; [solve_length|];
+    intros ?????; progress decompose_Forall_hyps
+  end.
+
+(** The [simplify_suffix] tactic removes [suffix] hypotheses that are
+tautologies, and simplifies [suffix] hypotheses involving [(::)] and
+[(++)]. *)
+Ltac simplify_suffix := repeat
+  match goal with
+  | H : suffix (_ :: _) _ |- _ => destruct (suffix_cons_not _ _ H)
+  | H : suffix (_ :: _) [] |- _ => apply suffix_nil_inv in H
+  | H : suffix (_ ++ _) (_ ++ _) |- _ => apply suffix_app_inv in H
+  | H : suffix (_ :: _) (_ :: _) |- _ =>
+    destruct (suffix_cons_inv _ _ _ _ H); clear H
+  | H : suffix ?x ?x |- _ => clear H
+  | H : suffix ?x (_ :: ?x) |- _ => clear H
+  | H : suffix ?x (_ ++ ?x) |- _ => clear H
+  | _ => progress simplify_eq/=
+  end.
+
+(** The [solve_suffix] tactic tries to solve goals involving [suffix]. It
+uses [simplify_suffix] to simplify hypotheses and tries to solve [suffix]
+conclusions. This tactic either fails or proves the goal. *)
+Ltac solve_suffix := by intuition (repeat
+  match goal with
+  | _ => done
+  | _ => progress simplify_suffix
+  | |- suffix [] _ => apply suffix_nil
+  | |- suffix _ _ => reflexivity
+  | |- suffix _ (_ :: _) => apply suffix_cons_r
+  | |- suffix _ (_ ++ _) => apply suffix_app_r
+  | H : suffix _ _ → False |- _ => destruct H
+  end).

stdpp/sorting.v

@@ -2,6 +2,7 @@
 standard library, but without using the module system. *)
 From Coq Require Export Sorted.
 From stdpp Require Export orders list.
+From stdpp Require Import sets.
 From stdpp Require Import options.
 
 Section merge_sort.
@@ -48,25 +49,36 @@ Inductive TlRel {A} (R : relation A) (a : A) : list A → Prop :=
 Section sorted.
   Context {A} (R : relation A).
 
-  Lemma elem_of_StronglySorted_app l1 l2 x1 x2 :
-    StronglySorted R (l1 ++ l2) → x1 ∈ l1 → x2 ∈ l2 → R x1 x2.
+  Lemma StronglySorted_cons l x :
+    StronglySorted R (x :: l) ↔
+      Forall (R x) l ∧ StronglySorted R l.
+  Proof. split; [inv 1|constructor]; naive_solver. Qed.
+
+  Lemma StronglySorted_app l1 l2 :
+    StronglySorted R (l1 ++ l2) ↔
+      (∀ x1 x2, x1 ∈ l1 → x2 ∈ l2 → R x1 x2) ∧
+      StronglySorted R l1 ∧
+      StronglySorted R l2.
   Proof.
-    induction l1 as [|x1' l1 IH]; simpl; [by rewrite elem_of_nil|].
-    intros [? Hall]%StronglySorted_inv [->|?]%elem_of_cons ?; [|by auto].
-    rewrite Forall_app, !Forall_forall in Hall. naive_solver.
+    induction l1 as [|x1' l1 IH]; simpl.
+    - set_solver by eauto using SSorted_nil.
+    - rewrite !StronglySorted_cons, IH, !Forall_forall. set_solver.
   Qed.
-  Lemma StronglySorted_app_inv_l l1 l2 :
+  Lemma StronglySorted_app_2 l1 l2 :
+    (∀ x1 x2, x1 ∈ l1 → x2 ∈ l2 → R x1 x2) →
+    StronglySorted R l1 →
+    StronglySorted R l2 →
+    StronglySorted R (l1 ++ l2).
+  Proof. by rewrite StronglySorted_app. Qed.
+  Lemma StronglySorted_app_1_elem_of l1 l2 x1 x2 :
+    StronglySorted R (l1 ++ l2) → x1 ∈ l1 → x2 ∈ l2 → R x1 x2.
+  Proof. rewrite StronglySorted_app. naive_solver. Qed.
+  Lemma StronglySorted_app_1_l l1 l2 :
     StronglySorted R (l1 ++ l2) → StronglySorted R l1.
-  Proof.
-    induction l1 as [|x1' l1 IH]; simpl;
-      [|inv 1]; decompose_Forall; constructor; auto.
-  Qed.
-  Lemma StronglySorted_app_inv_r l1 l2 :
+  Proof. rewrite StronglySorted_app. naive_solver. Qed.
+  Lemma StronglySorted_app_1_r l1 l2 :
     StronglySorted R (l1 ++ l2) → StronglySorted R l2.
-  Proof.
-    induction l1 as [|x1' l1 IH]; simpl;
-      [|inv 1]; decompose_Forall; auto.
-  Qed.
+  Proof. rewrite StronglySorted_app. naive_solver. Qed.
 
   Lemma Sorted_StronglySorted `{!Transitive R} l :
     Sorted R l → StronglySorted R l.

stdpp/tactics.v

@@ -628,28 +628,30 @@ Ltac opose_core p tac :=
 (** Turn all leading ∀ and → of [p] into evars (∀-evars will be shelved), and
 call [tac] with the term applied with those evars. This fill unfold definitions
 to find leading ∀/→.
+The type of [p] will be normalized by calling the [normalizer] function.
 
 [_name_guard] is an unused argument where you can pass anything you want. If the
 argument is an intro pattern, those will be taken into account by the [fresh]
 that is inside this tactic, avoiding name collisions that can otherwise arise.
 This is a work-around for https://github.com/coq/coq/issues/18109. *)
-Ltac ospecialize_foralls p _name_guard tac :=
+Ltac evar_foralls p _name_guard normalizer tac :=
   let T := type of p in
-  lazymatch eval hnf in T with
+  lazymatch normalizer T with
   | ?T1 → ?T2 =>
     (* This is the [fresh] where the presence of [_name_guard] matters.
     Note that the "opose_internal" is nice but not sufficient because
     it gets ignored when name mangling is enabled. *)
-    let pT1 := fresh "opose_internal" in
-    assert T1 as pT1; [| ospecialize_foralls (p pT1) _name_guard tac; clear pT1]
+    let pT1 := fresh "__evar_foralls_internal" in
+    assert T1 as pT1; [| evar_foralls (p pT1) _name_guard normalizer tac; clear pT1]
   | ∀ x : ?T1, _ =>
     let e := mk_evar T1 in
-    ospecialize_foralls (p e) _name_guard tac
+    evar_foralls (p e) _name_guard normalizer tac
   | ?T1 => tac p
   end.
 
 Ltac opose_specialize_foralls_core p _name_guard tac :=
-  opose_core p ltac:(fun p => ospecialize_foralls p _name_guard tac).
+  opose_core p ltac:(fun p =>
+    evar_foralls p _name_guard ltac:(fun t => eval hnf in t) tac).
 
 Tactic Notation "opose" "proof" uconstr(p) "as" simple_intropattern(pat) :=
   opose_core p ltac:(fun p => pose proof p as pat).
@@ -736,12 +738,6 @@ Tactic Notation "ospecialize" "*" uconstr(p) :=
       pose proof p as H'; clear H; rename H' into H
   )).
 
-(** Tactic that works like [notypeclasses refine] but automatically determines
-the right number of [_]. This is *not* goal-directed, it will add [_] until the
-given term no longer has a function type (determined via syntactic matching). *)
-Tactic Notation "notypeclasses" "apply" uconstr(p) :=
-  opose_specialize_foralls_core p () ltac:(fun p => notypeclasses refine p).
-
 (** The block definitions are taken from [Coq.Program.Equality] and can be used
 by tactics to separate their goal from hypotheses they generalize over. *)
 Definition block {A : Type} (a : A) := a.

stdpp_bitvector/definitions.v

@@ -755,7 +755,7 @@ Global Hint Resolve bv_wrap_simplify_mul | 10 : bv_wrap_simplify_db.
  tries to simplify them by removing any [bv_wrap] inside z1. *)
 Ltac bv_wrap_simplify_left :=
   lazymatch goal with |- bv_wrap _ _ = _ => idtac end;
-  etrans; [ notypeclasses apply bv_wrap_simplify_proof;
+  etrans; [ notypeclasses refine (bv_wrap_simplify_proof _ _ _);
             typeclasses eauto with bv_wrap_simplify_db | ]
 .
 

tests/multiset_solver.v

@@ -58,6 +58,9 @@ Section test.
   Lemma test_elem_of_6 x y X : {[+ x; y +]} ⊆ X → x ∈ X ∧ y ∈ X.
   Proof. multiset_solver. Qed.
 
+  Lemma test_elem_of_dom x X : x ∈ dom X ↔ x ∈ X.
+  Proof. multiset_solver. Qed.
+
   (** Tests where the goals do not involve the multiset connectives *)
   Lemma test_goal_1 x y X : {[+ x +]} ∪ X ⊆ {[+ y +]} → x = y.
   Proof. multiset_solver. Qed.

tests/tactics.ref

@@ -65,27 +65,9 @@ use opose proof instead.
   H' : even n
   ============================
   even n
-"notypeclasses_apply_test"
-     : string
-1 goal
-  
-  n : nat
-  ============================
-  Decision (n = 0)
-1 goal
-  
-  n : nat
-  ============================
-  Decision (n = 0)
 "notypeclasses_apply_error"
      : string
 The command has indeed failed with message:
-In environment
-P, Q : Prop
-H : P → Q
-HQ : Q
-opose_internal : P
-The term "H opose_internal" has type "Q" while it is expected to have type
- "P".
+The reference notypeclasses was not found in the current environment.
 The command has indeed failed with message:
 No such assumption.

tests/tactics.v

@@ -234,16 +234,6 @@ Proof.
   done.
 Qed.
 
-Check "notypeclasses_apply_test".
-Lemma notypeclasses_apply_test n : {n = 0} + {¬ n = 0}.
-Proof.
-  (* Partially applied lemma with typeclass in one of the trailing [_]. *)
-  notypeclasses apply (@decide (n = 0)). Show.
-Restart. Proof.
-  (* Partially applied lemma with typeclass in one of the explicit [_]. *)
-  notypeclasses apply (@decide (n = 0) _). Show.
-Abort.
-
 Check "notypeclasses_apply_error".
 Lemma notypeclasses_apply_error (P Q : Prop) : (P → Q) → Q → P.
 Proof.