diff options
| author | Vincent Laporte | 2019-11-25 10:25:50 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2020-03-24 09:49:07 +0100 |
| commit | d48757f04b1a23e2d47448da843409a7b44bd091 (patch) | |
| tree | a7051aa33d8c9d33c91fd451ad1e58250792057d | |
| parent | 0cc90c16000ba0afbb3ae74ebb022cc04747ee3c (diff) | |
[stdlib] Do not rely on failing “auto”
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Cyclic31.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int63/Int63.v | 10 |
2 files changed, 5 insertions, 7 deletions
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index 1c790a37a0..f6b2544b6e 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -2226,7 +2226,7 @@ Section Int31_Specs. < ([|iter312_sqrt n rec ih il j|] + 1) ^ 2. Proof. revert rec ih il j; elim n; unfold iter312_sqrt; fold iter312_sqrt; clear n. - intros rec ih il j Hi Hj Hij Hrec; apply sqrt312_step_correct; auto with zarith. + intros rec ih il j Hi Hj Hij Hrec; apply sqrt312_step_correct. 1-3: lia. intros; apply Hrec. 2: rewrite Z.pow_0_r. 1-3: lia. intros n Hrec rec ih il j Hi Hj Hij HHrec. apply sqrt312_step_correct; auto. diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index a8c645deb2..c4f738ac39 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -1316,9 +1316,8 @@ Lemma iter_sqrt_correct n rec i j: 0 < φ i -> 0 < φ j -> φ (iter_sqrt n rec i j) ^ 2 <= φ i < (φ (iter_sqrt n rec i j) + 1) ^ 2. Proof. revert rec i j; elim n; unfold iter_sqrt; fold iter_sqrt; clear n. - intros rec i j Hi Hj Hij H31 Hrec; apply sqrt_step_correct; auto with zarith. - intros; apply Hrec; auto with zarith. - rewrite Zpower_0_r; auto with zarith. + intros rec i j Hi Hj Hij H31 Hrec; apply sqrt_step_correct. 1-4: lia. + intros; apply Hrec; only 2: rewrite Zpower_0_r; auto with zarith. intros n Hrec rec i j Hi Hj Hij H31 HHrec. apply sqrt_step_correct; auto. intros j1 Hj1 Hjp1; apply Hrec; auto with zarith. @@ -1516,9 +1515,8 @@ Lemma iter2_sqrt_correct n rec ih il j: < (φ (iter2_sqrt n rec ih il j) + 1) ^ 2. Proof. revert rec ih il j; elim n; unfold iter2_sqrt; fold iter2_sqrt; clear n. - intros rec ih il j Hi Hj Hij Hrec; apply sqrt2_step_correct; auto with zarith. - intros; apply Hrec; auto with zarith. - rewrite Zpower_0_r; auto with zarith. + intros rec ih il j Hi Hj Hij Hrec; apply sqrt2_step_correct. 1-3: lia. + intros; apply Hrec; only 2: rewrite Zpower_0_r; auto with zarith. intros n Hrec rec ih il j Hi Hj Hij HHrec. apply sqrt2_step_correct; auto. intros j1 Hj1 Hjp1; apply Hrec; auto with zarith. |