From 9dc6a84e2c5707b1edd2b302014b0e7be4c118e7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 29 Mar 2025 10:57:31 +0100
Subject: [PATCH] Move `discriminate_list` and `simplify_list_eq` to basics.

---
 stdpp/list_basics.v    | 27 +++++++++++++++++++++++++++
 stdpp/list_relations.v | 28 ----------------------------
 2 files changed, 27 insertions(+), 28 deletions(-)

diff --git a/stdpp/list_basics.v b/stdpp/list_basics.v
index 5e14f50c..90a7410a 100644
--- a/stdpp/list_basics.v
+++ b/stdpp/list_basics.v
@@ -1280,3 +1280,30 @@ Proof.
   apply list_filter_iff. naive_solver.
 Qed.
 End general_properties.
+
+(** * Basic tactics on lists *)
+(** These are used already in [list_relations] so we cannot have them in
+[list_tactics]. *)
+
+(** The tactic [discriminate_list] discharges a goal if there is a hypothesis
+[l1 = l2] where [l1] and [l2] have different lengths. The tactic is guaranteed
+to work if [l1] and [l2] contain solely [ [] ], [(::)] and [(++)]. *)
+Tactic Notation "discriminate_list" hyp(H) :=
+  apply (f_equal length) in H;
+  repeat (csimpl in H || rewrite length_app in H); exfalso; lia.
+Tactic Notation "discriminate_list" :=
+  match goal with H : _ =@{list _} _ |- _ => discriminate_list H end.
+
+(** The tactic [simplify_list_eq] simplifies hypotheses involving
+equalities on lists using injectivity of [(::)] and [(++)]. Also, it simplifies
+lookups in singleton lists. *)
+Ltac simplify_list_eq :=
+  repeat match goal with
+  | _ => progress simplify_eq/=
+  | H : _ ++ _ = _ ++ _ |- _ => first
+    [ apply app_inv_head in H | apply app_inv_tail in H
+    | apply app_inj_1 in H; [destruct H|done]
+    | apply app_inj_2 in H; [destruct H|done] ]
+  | H : [?x] !! ?i = Some ?y |- _ =>
+    destruct i; [change (Some x = Some y) in H | discriminate]
+  end.
diff --git a/stdpp/list_relations.v b/stdpp/list_relations.v
index e4dda3cb..9ad236bb 100644
--- a/stdpp/list_relations.v
+++ b/stdpp/list_relations.v
@@ -61,33 +61,6 @@ Inductive submseteq {A} : relation (list A) :=
 Infix "⊆+" := submseteq (at level 70) : stdpp_scope.
 Global Hint Extern 0 (_ ⊆+ _) => reflexivity : core.
 
-
-(** * Basic tactics on lists *)
-(** These are used already in this file so we cannot have them in [list_tactics]. *)
-
-(** The tactic [discriminate_list] discharges a goal if there is a hypothesis
-[l1 = l2] where [l1] and [l2] have different lengths. The tactic is guaranteed
-to work if [l1] and [l2] contain solely [ [] ], [(::)] and [(++)]. *)
-Tactic Notation "discriminate_list" hyp(H) :=
-  apply (f_equal length) in H;
-  repeat (csimpl in H || rewrite length_app in H); exfalso; lia.
-Tactic Notation "discriminate_list" :=
-  match goal with H : _ =@{list _} _ |- _ => discriminate_list H end.
-
-(** The tactic [simplify_list_eq] simplifies hypotheses involving
-equalities on lists using injectivity of [(::)] and [(++)]. Also, it simplifies
-lookups in singleton lists. *)
-Ltac simplify_list_eq :=
-  repeat match goal with
-  | _ => progress simplify_eq/=
-  | H : _ ++ _ = _ ++ _ |- _ => first
-    [ apply app_inv_head in H | apply app_inv_tail in H
-    | apply app_inj_1 in H; [destruct H|done]
-    | apply app_inj_2 in H; [destruct H|done] ]
-  | H : [?x] !! ?i = Some ?y |- _ =>
-    destruct i; [change (Some x = Some y) in H | discriminate]
-  end.
-
 Section prefix_suffix_ops.
   Context `{EqDecision A}.
 
@@ -114,7 +87,6 @@ Inductive Forall3 {A B C} (P : A → B → C → Prop) :
   | Forall3_cons x y z l k k' :
      P x y z → Forall3 P l k k' → Forall3 P (x :: l) (y :: k) (z :: k').
 
-
 Section general_properties.
 Context {A : Type}.
 Implicit Types x y z : A.
-- 
GitLab