From 8193ca191cc435c108a4842ae38a11d74c7c20a5 Mon Sep 17 00:00:00 2001
From: BESSON Frederic
Date: Wed, 31 Mar 2021 22:16:50 +0200
Subject: [zify] More aggressive application of saturation rules

The role of the `zify_saturate` tactic is to augment the goal with
positivity constraints.  The premisses were previously obtained from
the context. If they are not present, we instantiate the saturation
lemma anyway.

Also,
- Remove saturation rules for Z.mul, the reasoning is performed by lia/nia
- Run zify_saturate after zify_to_euclidean_division_equations
- Better lemma for Z.power
- Ensure that lemma are generated once

Co-authored-by:  Andrej Dudenhefner  <mrhaandi>

Closes #12184, #11656
---
 theories/Numbers/Cyclic/Int63/Cyclic63.v | 1 -
 theories/Numbers/Cyclic/Int63/Int63.v    | 3 +--
 2 files changed, 1 insertion(+), 3 deletions(-)

(limited to 'theories/Numbers')

diff --git a/theories/Numbers/Cyclic/Int63/Cyclic63.v b/theories/Numbers/Cyclic/Int63/Cyclic63.v
index 2a26b6b12a..4bf971668d 100644
--- a/theories/Numbers/Cyclic/Int63/Cyclic63.v
+++ b/theories/Numbers/Cyclic/Int63/Cyclic63.v
@@ -218,7 +218,6 @@ Lemma div_lt : forall p x y, 0 <= x < y -> x / 2^p < y.
   apply Zdiv_lt_upper_bound;auto with zarith.
   apply Z.lt_le_trans with y;auto with zarith.
   rewrite <- (Zmult_1_r y);apply Zmult_le_compat;auto with zarith.
-  assert (0 < 2^p);auto with zarith.
   replace (2^p) with 0.
   destruct x;change (0<y);auto with zarith.
   destruct p;trivial;discriminate.
diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v
index a3ebe67325..d3fac82d09 100644
--- a/theories/Numbers/Cyclic/Int63/Int63.v
+++ b/theories/Numbers/Cyclic/Int63/Int63.v
@@ -1428,7 +1428,7 @@ Proof.
  assert (Hp3: (0 < Φ (WW ih il))).
  {simpl zn2z_to_Z;apply Z.lt_le_trans with (φ ih * wB)%Z; auto with zarith.
   apply Zmult_lt_0_compat; auto with zarith.
-  refine (Z.lt_le_trans _ _ _ _ Hih); auto with zarith. }
+ }
  cbv zeta.
  case_eq (ih <? j)%int63;intros Heq.
  rewrite -> ltb_spec in Heq.
@@ -1465,7 +1465,6 @@ Proof.
  apply Hrec; rewrite H; clear u H.
  assert (Hf1: 0 <= Φ (WW ih il) / φ j) by (apply Z_div_pos; auto with zarith).
  case (Zle_lt_or_eq 1 (φ j)); auto with zarith; intros Hf2.
- 2: contradict Heq0; apply Zle_not_lt; rewrite <- Hf2, Zdiv_1_r; auto with zarith.
  split.
  replace (φ j + Φ (WW ih il) / φ j)%Z with
         (1 * 2 + ((φ j - 2) + Φ (WW ih il) / φ j)) by lia.
-- 
cgit v1.2.3