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

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