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
  
  
  
  
  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.

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`