ident_is_above to compare positions of two hyps in the context

src/coqutil/Ltac2Lib/Control.v

@@ -0,0 +1,9 @@
+Require Import Ltac2.Ltac2.
+Require coqutil.Ltac2Lib.List.
+
+Ltac2 hyp_index(i: ident) :=
+  List.find_index (fun p => let (h, obody, tp) := p in Ident.equal h i) (Control.hyps ()).
+
+(* Assumes i1 and i2 are idents in the context, returns true iff i1 is higher up *)
+Ltac2 ident_is_above(i1: ident)(i2: ident) :=
+  Int.lt (hyp_index i1) (hyp_index i2).

src/coqutil/Ltac2Lib/List.v

@@ -1,4 +1,5 @@
 Require Import Ltac2.Ltac2.
+Require Export coqutil.Ltac2Lib.Pervasives.
 
 Ltac2 rec last xs :=
  match xs with
@@ -16,6 +17,27 @@ Ltac2 rec iter_until (f : 'a -> bool) (ls : 'a list) :=
   | l :: ls => if f l then true else iter_until f ls
   end.
 
+(* ('a -> bool) -> 'a list -> ('a * int) option *)
+Ltac2 find_with_index_opt f :=
+  let rec loop i xs :=
+    match xs with
+    | [] => None
+    | x :: xs => match f x with
+                 | true => Some (x, i)
+                 | false => loop (Int.add i 1) xs
+                 end
+    end in
+  loop 0.
+
+(* ('a -> bool) -> 'a list -> 'a * int *)
+Ltac2 find_with_index f xs :=
+  match find_with_index_opt f xs with
+  | Some r => r
+  | None => Control.throw Not_found
+  end.
+
+Ltac2 find_index f xs := snd (find_with_index f xs).
+
 (* Same signatures as in https://ocaml.org/p/batteries/3.6.0/doc/BatList/index.html *)
 
 Ltac2 rec take_while(p: 'a -> bool)(xs: 'a list) :=

src/coqutil/Ltac2Lib/Pervasives.v

@@ -0,0 +1,4 @@
+Require Import Ltac2.Ltac2.
+
+Ltac2 fst p := let (x, _) := p in x.
+Ltac2 snd p := let (_, x) := p in x.

src/coqutil/Tactics/ident_ops.v

@@ -1,5 +1,5 @@
 Require Import Ltac2.Ltac2. Set Default Proof Mode "Classic".
-Require coqutil.Ltac2Lib.Ident.
+Require coqutil.Ltac2Lib.Ident coqutil.Ltac2Lib.Control.
 
 Ltac _ident_starts_with := ltac2:(prefix i |-
   if Ident.starts_with (Option.get (Ltac1.to_ident prefix)) (Option.get (Ltac1.to_ident i))
@@ -19,6 +19,14 @@ Ltac _exact_append_ident := ltac2:(x y |-
 Tactic Notation "exact_append_ident" ident(x) ident(y) :=
   _exact_append_ident x y.
 
+Ltac _ident_is_above := ltac2:(i1 i2 |-
+  if Control.ident_is_above
+       (Option.get (Ltac1.to_ident i1))
+       (Option.get (Ltac1.to_ident i2))
+  then () else Control.backtrack_tactic_failure "hyp not above other hyp").
+
+Tactic Notation "ident_is_above" ident(i1) ident(i2) := _ident_is_above i1 i2.
+
 Goal True.
   assert_succeeds (idtac; ident_starts_with __a __ab).
   assert_succeeds (idtac; ident_starts_with x123 x123).
@@ -32,3 +40,9 @@ Goal forall (foo baz foobar: nat), True.
   pose ltac:(exact_append_ident foo bar).
   assert_fails (idtac; pose ltac:(exact_append_ident foo baz)).
 Abort.
+
+Goal forall (a b c d: nat), True.
+  intros.
+  assert_succeeds (idtac; ident_is_above b c).
+  assert_fails (idtac; ident_is_above c b).
+Abort.