diff options
| -rw-r--r-- | dev/doc/about-hints | 454 | ||||
| -rw-r--r-- | theories/ZArith/Zhints.v | 437 |
2 files changed, 454 insertions, 437 deletions
diff --git a/dev/doc/about-hints b/dev/doc/about-hints new file mode 100644 index 000000000..95712c3cf --- /dev/null +++ b/dev/doc/about-hints @@ -0,0 +1,454 @@ +An investigation of how ZArith lemmas could be classified in different +automation classes + +- Reversible lemmas relating operators (to be declared as hints but + needing precedences) +- Equivalent notions (one has to be considered as primitive and the + other rewritten into the canonical one) +- Isomorphisms between structure (one structure has to be considered + as more primitive than the other for a give operator) +- Irreversible simplifications (to be declared with precedences) +- Reversible bottom-up simplifications (to be used in hypotheses) +- Irreversible bottom-up simplifications (to be used in hypotheses + with precedences) +- Rewriting rules (relevant for autorewrite, or for an improved auto) + +Note: this analysis, made in 2001, was previously stored in +theories/ZArith/Zhints.v. It has been moved here to avoid obfuscating +the standard library. + +(**********************************************************************) +(** * 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` +>> +*) + +(* Lemmas ending by Zgt *) +(** +<< +Zmult_gt: (x,y:Z)`x > 0`->`x*y > 0`->`y > 0` +>> +*) + +(* Lemmas ending by Zlt *) +(** +<< +pZmult_lt: (x,y:Z)`x > 0`->`0 < y*x`->`0 < y` +>> +*) + +(* Lemmas ending by Zle *) +(** +<< +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 *) + +(* Hints Immediate *) +(** 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` +>> +*) diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v index 731f0252f..6a14d6934 100644 --- a/theories/ZArith/Zhints.v +++ b/theories/ZArith/Zhints.v @@ -98,440 +98,3 @@ Hint Resolve Zplus_le_compat (* :(n,m,p,q:Z)`n <= m`->`p <= q`->`n+p <= m+q` *) : 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` ->> -*) - -(* Lemmas ending by Zgt *) -(** -<< -Zmult_gt: (x,y:Z)`x > 0`->`x*y > 0`->`y > 0` ->> -*) - -(* Lemmas ending by Zlt *) -(** -<< -pZmult_lt: (x,y:Z)`x > 0`->`0 < y*x`->`0 < y` ->> -*) - -(* Lemmas ending by Zle *) -(** -<< -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 *) - -(* Hints Immediate *) -(** 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` ->> -*) - |