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

From Stdlib Require Import BinInt.
From Stdlib Require Import Zorder.
From Stdlib Require Import Zmin.
From Stdlib Require Import Zabs.
From Stdlib Require Import Zcompare.
From Stdlib Require Import Znat.
From Stdlib Require Import auxiliary.
From Stdlib Require Import Zmisc.
From Stdlib Require Import Wf_Z.

Simplification lemmas

No subgoal or smaller subgoals

#[global]
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 Z.gt

  Zsucc_gt_compat
  Zgt_succ
  Zorder.Zgt_pos_0
  Zplus_gt_compat_l
  Zplus_gt_compat_r

Lemmas ending by Z.lt

  Pos2Z.is_pos
  Z.lt_succ_diag_r
  Zsucc_lt_compat
  Z.lt_pred_l
  Zplus_lt_compat_l
  Zplus_lt_compat_r

Lemmas ending by Z.le

  Nat2Z.is_nonneg
  Pos2Z.is_nonneg
  Z.le_refl
  Z.le_succ_diag_r
  Zsucc_le_compat
  Z.le_pred_l
  Z.le_min_l
  Z.le_min_r
  Zplus_le_compat_l
  Zplus_le_compat_r
  Z.abs_nonneg

Irreversible simplification lemmas

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

Lemmas ending by eq

  Z_eq_mult
  Zplus_eq_compat

Lemmas ending by Z.ge

  Zorder.Zmult_ge_compat_r
  Zorder.Zmult_ge_compat_l
  Zorder.Zmult_ge_compat

Lemmas ending by Z.lt

  Zorder.Zmult_gt_0_compat
  Z.lt_lt_succ_r

Lemmas ending by Z.le

  Z.mul_nonneg_nonneg
  Zorder.Zmult_le_compat_r
  Zorder.Zmult_le_compat_l
  Z.add_nonneg_nonneg
  Z.le_le_succ_r
  Z.add_le_mono

  : zarith.