Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 454 insertions, 0 deletions

diff --git a/dev/doc/about-hints b/dev/doc/about-hints
new file mode 100644
index 00000000..95712c3c
--- /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`
+>>
+*)