From 27ef3be4e85519d343a49e250269ee90af3d1deb Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Mon, 18 Nov 2019 01:22:17 +0100
Subject: [PATCH] Add tactics for inequalities

---
 util/tactics.v | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/util/tactics.v b/util/tactics.v
index 1926cd1f4..2cc3189a1 100644
--- a/util/tactics.v
+++ b/util/tactics.v
@@ -77,3 +77,35 @@ Ltac feed_n n H := match constr:(n) with
   | O => idtac
   | (S ?m) => feed H ; [| feed_n m H]
   end.
+
+(* ************************************************************************** *)
+(** * Handier movement of inequalities. *)
+(* ************************************************************************** *)
+Ltac move_neq_down H :=
+  exfalso;
+  (move: H; rewrite ltnNge; move => /negP H; apply: H; clear H)
+  || (move: H; rewrite leqNgt; move => /negP H; apply: H; clear H).
+
+Ltac move_neq_up H :=
+  (rewrite ltnNge; apply/negP; intros H)
+  || (rewrite leqNgt; apply/negP; intros H).
+
+(** The following tactic converts inequality [t1 <= t2] into a constant
+ [k] such that [t2 = t1 + k] and substitutes all the occurrences of
+ [t2]. *)
+Ltac convert_two_instants_into_instant_and_duration t1 t2 k :=
+  match goal with
+  | [ H: (t1 <= t2) = true |- _ ] =>
+    ltac:(
+      assert (EX : exists (k: nat), t2 = t1 + k);
+      [exists (t2 - t1); rewrite subnKC; auto | ];
+      destruct EX as [k EQ]; subst t2; clear H
+    )
+  | [ H: (t1 < t2) = true |- _ ] =>
+    ltac:(
+      assert (EX : exists (k: nat), t2 = t1 + k);
+      [exists (t2 - t1); rewrite subnKC; auto using ltnW | ];
+      destruct EX as [k EQ]; subst t2; clear H
+    )
+  end.
+
-- 
GitLab