diff options
Diffstat (limited to 'theories/ZArith/Zhints.v')
| -rw-r--r-- | theories/ZArith/Zhints.v | 95 |
1 files changed, 48 insertions, 47 deletions
diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v index 6a14d693..8b879fbe 100644 --- a/theories/ZArith/Zhints.v +++ b/theories/ZArith/Zhints.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -43,58 +43,59 @@ Hint Resolve (** Should clearly be declared as hints *) (** Lemmas ending by eq *) - Zsucc_eq_compat (* :(n,m:Z)`n = m`->`(Zs n) = (Zs m)` *) - - (** Lemmas ending by Zgt *) - Zsucc_gt_compat (* :(n,m:Z)`m > n`->`(Zs m) > (Zs n)` *) - Zgt_succ (* :(n:Z)`(Zs n) > n` *) - Zorder.Zgt_pos_0 (* :(p:positive)`(POS p) > 0` *) - Zplus_gt_compat_l (* :(n,m,p:Z)`n > m`->`p+n > p+m` *) - Zplus_gt_compat_r (* :(n,m,p:Z)`n > m`->`n+p > m+p` *) - - (** Lemmas ending by Zlt *) - Zlt_succ (* :(n:Z)`n < (Zs n)` *) - Zsucc_lt_compat (* :(n,m:Z)`n < m`->`(Zs n) < (Zs m)` *) - Zlt_pred (* :(n:Z)`(Zpred n) < n` *) - Zplus_lt_compat_l (* :(n,m,p:Z)`n < m`->`p+n < p+m` *) - Zplus_lt_compat_r (* :(n,m,p:Z)`n < m`->`n+p < m+p` *) - - (** Lemmas ending by Zle *) - Zle_0_nat (* :(n:nat)`0 <= (inject_nat n)` *) - Zorder.Zle_0_pos (* :(p:positive)`0 <= (POS p)` *) - Zle_refl (* :(n:Z)`n <= n` *) - Zle_succ (* :(n:Z)`n <= (Zs n)` *) - Zsucc_le_compat (* :(n,m:Z)`m <= n`->`(Zs m) <= (Zs n)` *) - Zle_pred (* :(n:Z)`(Zpred n) <= n` *) - Zle_min_l (* :(n,m:Z)`(Zmin n m) <= n` *) - Zle_min_r (* :(n,m:Z)`(Zmin n m) <= m` *) - Zplus_le_compat_l (* :(n,m,p:Z)`n <= m`->`p+n <= p+m` *) - Zplus_le_compat_r (* :(a,b,c:Z)`a <= b`->`a+c <= b+c` *) - Zabs_pos (* :(x:Z)`0 <= |x|` *) + Zsucc_eq_compat (* n = m -> Z.succ n = Z.succ m *) + + (** Lemmas ending by Z.gt *) + Zsucc_gt_compat (* m > n -> Z.succ m > Z.succ n *) + Zgt_succ (* Z.succ n > n *) + Zorder.Zgt_pos_0 (* Z.pos p > 0 *) + Zplus_gt_compat_l (* n > m -> p+n > p+m *) + Zplus_gt_compat_r (* n > m -> n+p > m+p *) + + (** Lemmas ending by Z.lt *) + Pos2Z.is_pos (* 0 < Z.pos p *) + Z.lt_succ_diag_r (* n < Z.succ n *) + Zsucc_lt_compat (* n < m -> Z.succ n < Z.succ m *) + Z.lt_pred_l (* Z.pred n < n *) + Zplus_lt_compat_l (* n < m -> p+n < p+m *) + Zplus_lt_compat_r (* n < m -> n+p < m+p *) + + (** Lemmas ending by Z.le *) + Nat2Z.is_nonneg (* 0 <= Z.of_nat n *) + Pos2Z.is_nonneg (* 0 <= Z.pos p *) + Z.le_refl (* n <= n *) + Z.le_succ_diag_r (* n <= Z.succ n *) + Zsucc_le_compat (* m <= n -> Z.succ m <= Z.succ n *) + Z.le_pred_l (* Z.pred n <= n *) + Z.le_min_l (* Z.min n m <= n *) + Z.le_min_r (* Z.min n m <= m *) + Zplus_le_compat_l (* n <= m -> p+n <= p+m *) + Zplus_le_compat_r (* a <= b -> a+c <= b+c *) + Z.abs_nonneg (* 0 <= |x| *) (** ** Irreversible simplification lemmas *) (** Probably to be declared as hints, when no other simplification is possible *) (** Lemmas ending by eq *) - BinInt.Z_eq_mult (* :(x,y:Z)`y = 0`->`y*x = 0` *) - Zplus_eq_compat (* :(n,m,p,q:Z)`n = m`->`p = q`->`n+p = m+q` *) + Z_eq_mult (* y = 0 -> y*x = 0 *) + Zplus_eq_compat (* n = m -> p = q -> n+p = m+q *) - (** Lemmas ending by Zge *) - Zorder.Zmult_ge_compat_r (* :(a,b,c:Z)`a >= b`->`c >= 0`->`a*c >= b*c` *) - Zorder.Zmult_ge_compat_l (* :(a,b,c:Z)`a >= b`->`c >= 0`->`c*a >= c*b` *) + (** Lemmas ending by Z.ge *) + Zorder.Zmult_ge_compat_r (* a >= b -> c >= 0 -> a*c >= b*c *) + Zorder.Zmult_ge_compat_l (* a >= b -> c >= 0 -> c*a >= c*b *) Zorder.Zmult_ge_compat (* : - (a,b,c,d:Z)`a >= c`->`b >= d`->`c >= 0`->`d >= 0`->`a*b >= c*d` *) - - (** Lemmas ending by Zlt *) - Zorder.Zmult_gt_0_compat (* :(a,b:Z)`a > 0`->`b > 0`->`a*b > 0` *) - Zlt_lt_succ (* :(n,m:Z)`n < m`->`n < (Zs m)` *) - - (** Lemmas ending by Zle *) - Zorder.Zmult_le_0_compat (* :(x,y:Z)`0 <= x`->`0 <= y`->`0 <= x*y` *) - Zorder.Zmult_le_compat_r (* :(a,b,c:Z)`a <= b`->`0 <= c`->`a*c <= b*c` *) - Zorder.Zmult_le_compat_l (* :(a,b,c:Z)`a <= b`->`0 <= c`->`c*a <= c*b` *) - Zplus_le_0_compat (* :(x,y:Z)`0 <= x`->`0 <= y`->`0 <= x+y` *) - Zle_le_succ (* :(x,y:Z)`x <= y`->`x <= (Zs y)` *) - Zplus_le_compat (* :(n,m,p,q:Z)`n <= m`->`p <= q`->`n+p <= m+q` *) + a >= c -> b >= d -> c >= 0 -> d >= 0 -> a*b >= c*d *) + + (** Lemmas ending by Z.lt *) + Zorder.Zmult_gt_0_compat (* a > 0 -> b > 0 -> a*b > 0 *) + Z.lt_lt_succ_r (* n < m -> n < Z.succ m *) + + (** Lemmas ending by Z.le *) + Z.mul_nonneg_nonneg (* 0 <= x -> 0 <= y -> 0 <= x*y *) + Zorder.Zmult_le_compat_r (* a <= b -> 0 <= c -> a*c <= b*c *) + Zorder.Zmult_le_compat_l (* a <= b -> 0 <= c -> c*a <= c*b *) + Z.add_nonneg_nonneg (* 0 <= x -> 0 <= y -> 0 <= x+y *) + Z.le_le_succ_r (* x <= y -> x <= Z.succ y *) + Z.add_le_mono (* n <= m -> p <= q -> n+p <= m+q *) : zarith. |