From bc17dfef58081caf0862d292e4653d35a8646363 Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Fri, 1 Jul 2016 08:54:38 -0700
Subject: Add fraction inequality reasoning tactics to ZUtil

---
 src/Util/ZUtil.v | 120 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 120 insertions(+)

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index ebfea8ebd..6d6039a6d 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -525,3 +525,123 @@ Qed.
 
 Lemma two_times_x_minus_x x : 2 * x - x = x.
 Proof. lia. Qed.
+
+(** * [Zsimplify_fractions_le] *)
+(** The culmination of this series of tactics,
+    [Zsimplify_fractions_le], will use the fact that [a * (b / c) <=
+    (a * b) / c], and do some reasoning modulo associativity and
+    commutativity in [Z] to perform such a reduction.  It may leave
+    over goals if it cannot prove that some denominators are non-zero.
+    If the rewrite [a * (b / c)] → [(a * b) / c] is safe to do on the
+    LHS of the goal, this tactic should not turn a solvable goal into
+    an unsolvable one.
+
+    After running, the tactic does some basic rewriting to simplify
+    fractions, e.g., that [a * b / b = a]. *)
+Ltac Zsplit_sums_step :=
+  match goal with
+  | [ |- _ + _ <= _ ]
+    => etransitivity; [ eapply Z.add_le_mono | ]
+  | [ |- _ - _ <= _ ]
+    => etransitivity; [ eapply Z.sub_le_mono | ]
+  end.
+Ltac Zpre_reorder_fractions_step :=
+  match goal with
+  | [ |- context[?x / ?y * ?z] ]
+    => rewrite (Z.mul_comm (x / y) z)
+  | _ => let LHS := match goal with |- ?LHS <= ?RHS => LHS end in
+         match LHS with
+         | context G[?x * (?y / ?z)]
+           => let G' := context G[(x * y) / z] in
+              transitivity G'
+         end
+  end.
+Ltac Zpre_reorder_fractions :=
+  try first [ Zsplit_sums_step; [ Zpre_reorder_fractions.. | ]
+            | Zpre_reorder_fractions_step; [ .. | Zpre_reorder_fractions ] ].
+Ltac Zsplit_comparison :=
+  match goal with
+  | [ |- ?x <= ?x ] => reflexivity
+  | [ H : _ >= _ |- _ ]
+    => apply Z.ge_le_iff in H
+  | [ |- ?x * ?y <= ?z * ?w ]
+    => lazymatch goal with
+       | [ H : 0 <= x |- _ ] => idtac
+       | [ H : x < 0 |- _ ] => fail
+       | _ => destruct (Z_lt_le_dec x 0)
+       end;
+       [ ..
+       | lazymatch goal with
+         | [ H : 0 <= y |- _ ] => idtac
+         | [ H : y < 0 |- _ ] => fail
+         | _ => destruct (Z_lt_le_dec y 0)
+         end;
+         [ ..
+         | apply Zmult_le_compat; [ | | assumption | assumption ] ] ]
+  | [ |- ?x / ?y <= ?z / ?y ]
+    => lazymatch goal with
+       | [ H : 0 < y |- _ ] => idtac
+       | [ H : y <= 0 |- _ ] => fail
+       | _ => destruct (Z_lt_le_dec 0 y)
+       end;
+       [ apply Z_div_le; [ apply gt_lt_symmetry; assumption | ]
+       | .. ]
+  | [ |- ?x / ?y <= ?x / ?z ]
+    => lazymatch goal with
+       | [ H : 0 <= x |- _ ] => idtac
+       | [ H : x < 0 |- _ ] => fail
+       | _ => destruct (Z_lt_le_dec x 0)
+       end;
+       [ ..
+       | lazymatch goal with
+         | [ H : 0 < z |- _ ] => idtac
+         | [ H : z <= 0 |- _ ] => fail
+         | _ => destruct (Z_lt_le_dec 0 z)
+         end;
+         [ apply Z.div_le_compat_l; [ assumption | split; [ assumption | ] ]
+         | .. ] ]
+  | [ |- _ + _ <= _ + _ ]
+    => apply Z.add_le_mono
+  | [ |- _ - _ <= _ - _ ]
+    => apply Z.sub_le_mono
+  | [ |- ?x * (?y / ?z) <= (?x * ?y) / ?z ]
+    => apply Z.div_mul_le
+  end.
+Ltac Zsplit_comparison_fin_step :=
+  match goal with
+  | _ => assumption
+  | _ => lia
+  | _ => progress subst
+  | [ H : ?n * ?m < 0 |- _ ]
+    => apply (proj1 (Z.lt_mul_0 n m)) in H; destruct H as [[??]|[??]]
+  | [ H : ?n / ?m < 0 |- _ ]
+    => apply (proj1 (Zlt_div_0 n m)) in H; destruct H as [[[??]|[??]]?]
+  | [ H : (?x^?y) <= ?n < _, H' : ?n < 0 |- _ ]
+    => assert (0 <= x^y) by zero_bounds; lia
+  | [ H : (?x^?y) < 0 |- _ ]
+    => assert (0 <= x^y) by zero_bounds; lia
+  | [ H : (?x^?y) <= 0 |- _ ]
+    => let H' := fresh in
+       assert (H' : 0 <= x^y) by zero_bounds;
+       assert (x^y = 0) by lia;
+       clear H H'
+  | [ H : _^_ = 0 |- _ ]
+    => apply Z.pow_eq_0_iff in H; destruct H as [?|[??]]
+  | [ H : 0 <= ?x, H' : ?x - 1 < 0 |- _ ]
+    => assert (x = 0) by lia; clear H H'
+  | [ |- ?x <= ?y ] => is_evar x; reflexivity
+  | [ |- ?x <= ?y ] => is_evar y; reflexivity
+  end.
+Ltac Zsplit_comparison_fin := repeat Zsplit_comparison_fin_step.
+Ltac Zsimplify_fractions_step :=
+  match goal with
+  | _ => rewrite Z.div_mul by (try apply Z.pow_nonzero; zero_bounds)
+  | [ |- context[?x * ?y / ?x] ]
+    => rewrite (Z.mul_comm x y)
+  | [ |- ?x <= ?x ] => reflexivity
+  end.
+Ltac Zsimplify_fractions := repeat Zsimplify_fractions_step.
+Ltac Zsimplify_fractions_le :=
+  Zpre_reorder_fractions;
+  [ repeat Zsplit_comparison; Zsplit_comparison_fin; zero_bounds..
+  | Zsimplify_fractions ].
-- 
cgit v1.2.3