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
- 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
No subgoal or smaller subgoals
Reversible lemmas relating operators
Probably to be declared as hints but need to define precedences
Conversion between comparisons/predicates and arithmetic operators
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)`
Conversion between nat comparisons and Z comparisons
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)`
Conversion between comparisons
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`
Irreversible simplification involving several comparaisons
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`
What is decreasing here ?
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)`
Bottom-up simplification: should be used
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`
Other unclearly simplifying lemmas
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`
Irreversible lemmas with meta-variables
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`
Unclear or too specific lemmas
Not to be used ?
Irreversible and too specific (not enough regular)
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`
Expansion and too specific ?
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`
Reversible but too specific ?
Lemmas ending by Zlt
Zlt_minus: (n,m:Z)`0 < m`->`n-m < n`
Lemmas to be used as rewrite rules
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`