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

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.

Simplification lemmas


No subgoal or smaller subgoals

Hint Resolve
  

Reversible simplification lemmas (no loss of information)

  
Should clearly be declared as hints

  
Lemmas ending by eq
  Zsucc_eq_compat

  
Lemmas ending by Zgt
  Zsucc_gt_compat
  Zgt_succ
  Zorder.Zgt_pos_0
  Zplus_gt_compat_l
  Zplus_gt_compat_r

  
Lemmas ending by Zlt
  Zlt_succ
  Zsucc_lt_compat
  Zlt_pred
  Zplus_lt_compat_l
  Zplus_lt_compat_r

  
Lemmas ending by Zle
  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

  

Irreversible simplification lemmas

  
Probably to be declared as hints, when no other simplification is possible

  
Lemmas ending by eq
  BinInt.Z_eq_mult
  Zplus_eq_compat

  
Lemmas ending by Zge
  Zorder.Zmult_ge_compat_r
  Zorder.Zmult_ge_compat_l
  Zorder.Zmult_ge_compat

  
Lemmas ending by Zlt
  Zorder.Zmult_gt_0_compat
  Zlt_lt_succ

  
Lemmas ending by Zle
  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.

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)`

Useful Bottom-up lemmas


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`