Library Coq.ZArith.Zhints
This file centralizes the lemmas about Z, classifying them
according to the way they can be used in automatic search
Lemmas which clearly leads to simplification during proof search are
declared as Hints. A definite status (Hint or not) for the other lemmas
remains to be given
Structure of the file
- simplification lemmas (only those are declared as Hints)
- reversible lemmas relating operators
- useful Bottom-up lemmas
- irreversible lemmas with meta-variables
- unclear or too specific lemmas
- lemmas to be used as rewrite rules
Lemmas involving positive and compare are not taken into account
Require Import BinInt.
Require Import Zorder.
Require Import Zmin.
Require Import Zabs.
Require Import Zcompare.
Require Import Znat.
Require Import auxiliary.
Require Import Zmisc.
Require Import Wf_Z.
No subgoal or smaller subgoals
Hint Resolve
Zsucc_eq_compat
Zsucc_gt_compat
Zgt_succ
Zorder.Zgt_pos_0
Zplus_gt_compat_l
Zplus_gt_compat_r
Zlt_succ
Zsucc_lt_compat
Zlt_pred
Zplus_lt_compat_l
Zplus_lt_compat_r
Zle_0_nat
Zorder.Zle_0_pos
Zle_refl
Zle_succ
Zsucc_le_compat
Zle_pred
Zle_min_l
Zle_min_r
Zplus_le_compat_l
Zplus_le_compat_r
Zabs_pos
BinInt.Z_eq_mult
Zplus_eq_compat
Zorder.Zmult_ge_compat_r
Zorder.Zmult_ge_compat_l
Zorder.Zmult_ge_compat
Zorder.Zmult_gt_0_compat
Zlt_lt_succ
Zorder.Zmult_le_0_compat
Zorder.Zmult_le_compat_r
Zorder.Zmult_le_compat_l
Zplus_le_0_compat
Zle_le_succ
Zplus_le_compat
: zarith.
Probably to be declared as hints but need to define precedences
Lemmas ending by eq
Zegal_left: (x,y:Z)`x = y`->`x+(-y) = 0` Zabs_eq: (x:Z)`0 <= x`->`|x| = x` Zeven_div2: (x:Z)(Zeven x)->`x = 2*(Zdiv2 x)` Zodd_div2: (x:Z)`x >= 0`->(Zodd x)->`x = 2*(Zdiv2 x)+1`
Lemmas ending by Zgt
Zgt_left_rev: (x,y:Z)`x+(-y) > 0`->`x > y` Zgt_left_gt: (x,y:Z)`x > y`->`x+(-y) > 0`
Lemmas ending by Zlt
Zlt_left_rev: (x,y:Z)`0 < y+(-x)`->`x < y` Zlt_left_lt: (x,y:Z)`x < y`->`0 < y+(-x)` Zlt_O_minus_lt: (n,m:Z)`0 < n-m`->`m < n`
Lemmas ending by Zle
Zle_left: (x,y:Z)`x <= y`->`0 <= y+(-x)` Zle_left_rev: (x,y:Z)`0 <= y+(-x)`->`x <= y` Zlt_left: (x,y:Z)`x < y`->`0 <= y+(-1)+(-x)` Zge_left: (x,y:Z)`x >= y`->`0 <= x+(-y)` Zgt_left: (x,y:Z)`x > y`->`0 <= x+(-1)+(-y)`
Lemmas ending by eq
inj_eq: (x,y:nat)x=y->`(inject_nat x) = (inject_nat y)`
Lemmas ending by Zge
inj_ge: (x,y:nat)(ge x y)->`(inject_nat x) >= (inject_nat y)`
Lemmas ending by Zgt
inj_gt: (x,y:nat)(gt x y)->`(inject_nat x) > (inject_nat y)`
Lemmas ending by Zlt
inj_lt: (x,y:nat)(lt x y)->`(inject_nat x) < (inject_nat y)`
Lemmas ending by Zle
inj_le: (x,y:nat)(le x y)->`(inject_nat x) <= (inject_nat y)`
Lemmas ending by Zge
not_Zlt: (x,y:Z)~`x < y`->`x >= y` Zle_ge: (m,n:Z)`m <= n`->`n >= m`
Lemmas ending by Zgt
Zle_gt_S: (n,p:Z)`n <= p`->`(Zs p) > n` not_Zle: (x,y:Z)~`x <= y`->`x > y` Zlt_gt: (m,n:Z)`m < n`->`n > m` Zle_S_gt: (n,m:Z)`(Zs n) <= m`->`m > n`
Lemmas ending by Zlt
not_Zge: (x,y:Z)~`x >= y`->`x < y` Zgt_lt: (m,n:Z)`m > n`->`n < m` Zle_lt_n_Sm: (n,m:Z)`n <= m`->`n < (Zs m)`
Lemmas ending by Zle
Zlt_ZERO_pred_le_ZERO: (x:Z)`0 < x`->`0 <= (Zpred x)` not_Zgt: (x,y:Z)~`x > y`->`x <= y` Zgt_le_S: (n,p:Z)`p > n`->`(Zs n) <= p` Zgt_S_le: (n,p:Z)`(Zs p) > n`->`n <= p` Zge_le: (m,n:Z)`m >= n`->`n <= m` Zlt_le_S: (n,p:Z)`n < p`->`(Zs n) <= p` Zlt_n_Sm_le: (n,m:Z)`n < (Zs m)`->`n <= m` Zlt_le_weak: (n,m:Z)`n < m`->`n <= m` Zle_refl: (n,m:Z)`n = m`->`n <= m`
useful with clear precedences
Lemmas ending by Zlt
Zlt_le_reg :(a,b,c,d:Z)`a < b`->`c <= d`->`a+c < b+d` Zle_lt_reg : (a,b,c,d:Z)`a <= b`->`c < d`->`a+c < b+d`
Lemmas ending by eq
Zplus_minus: (n,m,p:Z)`n = m+p`->`p = n-m`
Lemmas ending by Zgt
Zgt_pred: (n,p:Z)`p > (Zs n)`->`(Zpred p) > n`
Lemmas ending by Zlt
Zlt_pred: (n,p:Z)`(Zs n) < p`->`n < (Zpred p)`
Lemmas ending by eq
Zeq_add_S: (n,m:Z)`(Zs n) = (Zs m)`->`n = m` Zsimpl_plus_l: (n,m,p:Z)`n+m = n+p`->`m = p` Zplus_unit_left: (n,m:Z)`n+0 = m`->`n = m` Zplus_unit_right: (n,m:Z)`n = m+0`->`n = m`
Lemmas ending by Zgt
Zsimpl_gt_plus_l: (n,m,p:Z)`p+n > p+m`->`n > m` Zsimpl_gt_plus_r: (n,m,p:Z)`n+p > m+p`->`n > m` Zgt_S_n: (n,p:Z)`(Zs p) > (Zs n)`->`p > n`
Lemmas ending by Zlt
Zsimpl_lt_plus_l: (n,m,p:Z)`p+n < p+m`->`n < m` Zsimpl_lt_plus_r: (n,m,p:Z)`n+p < m+p`->`n < m` Zlt_S_n: (n,m:Z)`(Zs n) < (Zs m)`->`n < m`
Lemmas ending by Zle
Zsimpl_le_plus_l: (p,n,m:Z)`p+n <= p+m`->`n <= m` Zsimpl_le_plus_r: (p,n,m:Z)`n+p <= m+p`->`n <= m` Zle_S_n: (n,m:Z)`(Zs m) <= (Zs n)`->`m <= n` >> *) (** ** Bottom-up irreversible (syntactic) simplification *) (** Lemmas ending by Zle *) (** << Zle_trans_S: (n,m:Z)`(Zs n) <= m`->`n <= m`
Lemmas ending by Zeq
Zmult_eq: (x,y:Z)`x <> 0`->`y*x = 0`->`y = 0`
Zmult_gt: (x,y:Z)`x > 0`->`x*y > 0`->`y > 0`
pZmult_lt: (x,y:Z)`x > 0`->`0 < y*x`->`0 < y`
Zmult_le: (x,y:Z)`x > 0`->`0 <= y*x`->`0 <= y` OMEGA1: (x,y:Z)`x = y`->`0 <= x`->`0 <= y`
To be used by EAuto
Lemmas ending by eq
Zle_antisym: (n,m:Z)`n <= m`->`m <= n`->`n = m`
Lemmas ending by Zge
Zge_trans: (n,m,p:Z)`n >= m`->`m >= p`->`n >= p`
Lemmas ending by Zgt
Zgt_trans: (n,m,p:Z)`n > m`->`m > p`->`n > p` Zgt_trans_S: (n,m,p:Z)`(Zs n) > m`->`m > p`->`n > p` Zle_gt_trans: (n,m,p:Z)`m <= n`->`m > p`->`n > p` Zgt_le_trans: (n,m,p:Z)`n > m`->`p <= m`->`n > p`
Lemmas ending by Zlt
Zlt_trans: (n,m,p:Z)`n < m`->`m < p`->`n < p` Zlt_le_trans: (n,m,p:Z)`n < m`->`m <= p`->`n < p` Zle_lt_trans: (n,m,p:Z)`n <= m`->`m < p`->`n < p`
Lemmas ending by Zle
Zle_trans: (n,m,p:Z)`n <= m`->`m <= p`->`n <= p`
Not to be used ?
Lemmas ending by Zle
Zle_mult: (x,y:Z)`x > 0`->`0 <= y`->`0 <= y*x` Zle_mult_approx: (x,y,z:Z)`x > 0`->`z > 0`->`0 <= y`->`0 <= y*x+z` OMEGA6: (x,y,z:Z)`0 <= x`->`y = 0`->`0 <= x+y*z` OMEGA7: (x,y,z,t:Z)`z > 0`->`t > 0`->`0 <= x`->`0 <= y`->`0 <= x*z+y*t`
Lemmas ending by Zge
Zge_mult_simpl: (a,b,c:Z)`c > 0`->`a*c >= b*c`->`a >= b`
Lemmas ending by Zgt
Zgt_mult_simpl: (a,b,c:Z)`c > 0`->`a*c > b*c`->`a > b` Zgt_square_simpl: (x,y:Z)`x >= 0`->`y >= 0`->`x*x > y*y`->`x > y`
Lemmas ending by Zle
Zle_mult_simpl: (a,b,c:Z)`c > 0`->`a*c <= b*c`->`a <= b` Zmult_le_approx: (x,y,z:Z)`x > 0`->`x > z`->`0 <= y*x+z`->`0 <= y`
Lemmas ending by Zlt
Zlt_minus: (n,m:Z)`0 < m`->`n-m < n`
but can also be used as hints
Left-to-right simplification lemmas (a symbol disappears)
Zcompare_n_S: (n,m:Z)(Zcompare (Zs n) (Zs m))=(Zcompare n m) Zmin_n_n: (n:Z)`(Zmin n n) = n` Zmult_1_n: (n:Z)`1*n = n` Zmult_n_1: (n:Z)`n*1 = n` Zminus_plus: (n,m:Z)`n+m-n = m` Zle_plus_minus: (n,m:Z)`n+(m-n) = m` Zopp_Zopp: (x:Z)`(-(-x)) = x` Zero_left: (x:Z)`0+x = x` Zero_right: (x:Z)`x+0 = x` Zplus_inverse_r: (x:Z)`x+(-x) = 0` Zplus_inverse_l: (x:Z)`(-x)+x = 0` Zopp_intro: (x,y:Z)`(-x) = (-y)`->`x = y` Zmult_one: (x:Z)`1*x = x` Zero_mult_left: (x:Z)`0*x = 0` Zero_mult_right: (x:Z)`x*0 = 0` Zmult_Zopp_Zopp: (x,y:Z)`(-x)*(-y) = x*y`
Right-to-left simplification lemmas (a symbol disappears)
Zpred_Sn: (m:Z)`m = (Zpred (Zs m))` Zs_pred: (n:Z)`n = (Zs (Zpred n))` Zplus_n_O: (n:Z)`n = n+0` Zmult_n_O: (n:Z)`0 = n*0` Zminus_n_O: (n:Z)`n = n-0` Zminus_n_n: (n:Z)`0 = n-n` Zred_factor6: (x:Z)`x = x+0` Zred_factor0: (x:Z)`x = x*1`
Unclear orientation (no symbol disappears)
Zplus_n_Sm: (n,m:Z)`(Zs (n+m)) = n+(Zs m)` Zmult_n_Sm: (n,m:Z)`n*m+n = n*(Zs m)` Zmin_SS: (n,m:Z)`(Zs (Zmin n m)) = (Zmin (Zs n) (Zs m))` Zplus_assoc_l: (n,m,p:Z)`n+(m+p) = n+m+p` Zplus_assoc_r: (n,m,p:Z)`n+m+p = n+(m+p)` Zplus_permute: (n,m,p:Z)`n+(m+p) = m+(n+p)` Zplus_Snm_nSm: (n,m:Z)`(Zs n)+m = n+(Zs m)` Zminus_plus_simpl: (n,m,p:Z)`n-m = p+n-(p+m)` Zminus_Sn_m: (n,m:Z)`(Zs (n-m)) = (Zs n)-m` Zmult_plus_distr_l: (n,m,p:Z)`(n+m)*p = n*p+m*p` Zmult_minus_distr: (n,m,p:Z)`(n-m)*p = n*p-m*p` Zmult_assoc_r: (n,m,p:Z)`n*m*p = n*(m*p)` Zmult_assoc_l: (n,m,p:Z)`n*(m*p) = n*m*p` Zmult_permute: (n,m,p:Z)`n*(m*p) = m*(n*p)` Zmult_Sm_n: (n,m:Z)`n*m+m = (Zs n)*m` Zmult_Zplus_distr: (x,y,z:Z)`x*(y+z) = x*y+x*z` Zmult_plus_distr: (n,m,p:Z)`(n+m)*p = n*p+m*p` Zopp_Zplus: (x,y:Z)`(-(x+y)) = (-x)+(-y)` Zplus_sym: (x,y:Z)`x+y = y+x` Zplus_assoc: (x,y,z:Z)`x+(y+z) = x+y+z` Zmult_sym: (x,y:Z)`x*y = y*x` Zmult_assoc: (x,y,z:Z)`x*(y*z) = x*y*z` Zopp_Zmult: (x,y:Z)`(-x)*y = (-(x*y))` Zplus_S_n: (x,y:Z)`(Zs x)+y = (Zs (x+y))` Zopp_one: (x:Z)`(-x) = x*(-1)` Zopp_Zmult_r: (x,y:Z)`(-(x*y)) = x*(-y)` Zmult_Zopp_left: (x,y:Z)`(-x)*y = x*(-y)` Zopp_Zmult_l: (x,y:Z)`(-(x*y)) = (-x)*y` Zred_factor1: (x:Z)`x+x = x*2` Zred_factor2: (x,y:Z)`x+x*y = x*(1+y)` Zred_factor3: (x,y:Z)`x*y+x = x*(1+y)` Zred_factor4: (x,y,z:Z)`x*y+x*z = x*(y+z)` Zminus_Zplus_compatible: (x,y,n:Z)`x+n-(y+n) = x-y` Zmin_plus: (x,y,n:Z)`(Zmin (x+n) (y+n)) = (Zmin x y)+n`
nat <-> Z
inj_S: (y:nat)`(inject_nat (S y)) = (Zs (inject_nat y))` inj_plus: (x,y:nat)`(inject_nat (plus x y)) = (inject_nat x)+(inject_nat y)` inj_mult: (x,y:nat)`(inject_nat (mult x y)) = (inject_nat x)*(inject_nat y)` inj_minus1: (x,y:nat)(le y x)->`(inject_nat (minus x y)) = (inject_nat x)-(inject_nat y)` inj_minus2: (x,y:nat)(gt y x)->`(inject_nat (minus x y)) = 0`
Too specific ?
Zred_factor5: (x,y:Z)`x*0+y = y`