From ee40e74b1f0c7dd4034847d3f93306a8f106b1d7 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sat, 14 Oct 2023 21:49:30 +0200 Subject: [PATCH] port to Coq 8.18 and later --- .github/workflows/docker-action.yml | 7 +- .github/workflows/nix-action.yml | 47 ---------- README.md | 6 +- coq-qarith-stern-brocot.opam | 4 +- dune-project | 4 +- meta.yml | 10 +-- theories/Q_to_R.v | 6 +- .../Qhomographic_Qpositive_to_Q_properties.v | 61 +++++++------ .../Qquadratic_Qpositive_to_Q_properties.v | 44 +++++----- theories/homographic_correctness.v | 88 +++++++++---------- theories/positive_fraction_encoding.v | 3 +- theories/quadratic_correctness.v | 8 +- 12 files changed, 116 insertions(+), 172 deletions(-) delete mode 100644 .github/workflows/nix-action.yml diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 62aea63..bfc7905 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -18,17 +18,16 @@ jobs: matrix: image: - 'coqorg/coq:dev' - - 'coqorg/coq:8.16' - - 'coqorg/coq:8.15' - - 'coqorg/coq:8.14' + - 'coqorg/coq:8.18' fail-fast: false steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v3 - uses: coq-community/docker-coq-action@v1 with: opam_file: 'coq-qarith-stern-brocot.opam' custom_image: ${{ matrix.image }} + # See also: # https://github.com/coq-community/docker-coq-action#readme # https://github.com/erikmd/docker-coq-github-action-demo diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml deleted file mode 100644 index 898f2bb..0000000 --- a/.github/workflows/nix-action.yml +++ /dev/null @@ -1,47 +0,0 @@ -# This file was generated from `meta.yml`, please do not edit manually. -# Follow the instructions on https://github.com/coq-community/templates to regenerate. -name: Nix CI - -on: - push: - branches: - - master - pull_request: - paths: - - .github/workflows/** - pull_request_target: - -jobs: - build: - runs-on: ubuntu-latest - strategy: - matrix: - overrides: - - 'coq = "master"' - fail-fast: false - steps: - - name: Determine which commit to test - run: | - if [[ ${{ github.event_name }} =~ "pull_request" ]]; then - merge_commit=$(git ls-remote ${{ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge | cut -f1) - if [ -z "$merge_commit" ]; then - echo "tested_commit=${{ github.event.pull_request.head.sha }}" >> $GITHUB_ENV - else - echo "tested_commit=$merge_commit" >> $GITHUB_ENV - fi - else - echo "tested_commit=${{ github.sha }}" >> $GITHUB_ENV - fi - - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - uses: cachix/cachix-action@v10 - with: - name: coq-community - authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}' - extraPullNames: coq, math-comp - - uses: actions/checkout@v2 - with: - ref: ${{ env.tested_commit }} - - run: > - nix-build https://coq.inria.fr/nix/toolbox --argstr job qarith-stern-brocot --arg override '{ ${{ matrix.overrides }}; qarith-stern-brocot = builtins.filterSource (path: _: baseNameOf path != ".git") ./.; }' diff --git a/README.md b/README.md index bfd088d..b8d2d70 100644 --- a/README.md +++ b/README.md @@ -5,7 +5,6 @@ Follow the instructions on https://github.com/coq-community/templates to regener # Binary Rational Numbers [![Docker CI][docker-action-shield]][docker-action-link] -[![Nix CI][nix-action-shield]][nix-action-link] [![Contributing][contributing-shield]][contributing-link] [![Code of Conduct][conduct-shield]][conduct-link] [![Zulip][zulip-shield]][zulip-link] @@ -14,9 +13,6 @@ Follow the instructions on https://github.com/coq-community/templates to regener [docker-action-shield]: https://github.com/coq-community/qarith-stern-brocot/workflows/Docker%20CI/badge.svg?branch=master [docker-action-link]: https://github.com/coq-community/qarith-stern-brocot/actions?query=workflow:"Docker%20CI" -[nix-action-shield]: https://github.com/coq-community/qarith-stern-brocot/workflows/Nix%20CI/badge.svg?branch=master -[nix-action-link]: https://github.com/coq-community/qarith-stern-brocot/actions?query=workflow:"Nix%20CI" - [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md @@ -42,7 +38,7 @@ field operations on them in two different ways: strict and lazy. - Coq-community maintainer(s): - Hugo Herbelin ([**@herbelin**](https://github.com/herbelin)) - License: [GNU Lesser General Public License v2.1 or later](LICENSE) -- Compatible Coq versions: 8.14 or later +- Compatible Coq versions: 8.18 or later - Additional dependencies: none - Coq namespace: `QArithSternBrocot` - Related publication(s): diff --git a/coq-qarith-stern-brocot.opam b/coq-qarith-stern-brocot.opam index ab6fbcd..c2cd905 100644 --- a/coq-qarith-stern-brocot.opam +++ b/coq-qarith-stern-brocot.opam @@ -15,8 +15,8 @@ field operations on them in two different ways: strict and lazy. build: ["dune" "build" "-p" name "-j" jobs] depends: [ - "dune" {>= "2.5"} - "coq" {(>= "8.14" & < "8.17~") | (= "dev")} + "dune" {>= "3.5"} + "coq" {>= "8.18"} ] tags: [ diff --git a/dune-project b/dune-project index 048d18c..3aebefe 100644 --- a/dune-project +++ b/dune-project @@ -1,3 +1,3 @@ -(lang dune 2.5) -(using coq 0.2) +(lang dune 3.5) +(using coq 0.6) (name qarith-stern-brocot) diff --git a/meta.yml b/meta.yml index 9b12632..b0f3fcb 100644 --- a/meta.yml +++ b/meta.yml @@ -4,7 +4,7 @@ shortname: qarith-stern-brocot organization: coq-community community: true action: true -nix: true +nix: false synopsis: Binary rational numbers in Coq @@ -34,14 +34,12 @@ license: identifier: LGPL-2.1-or-later supported_coq_versions: - text: 8.14 or later - opam: '{(>= "8.14" & < "8.17~") | (= "dev")}' + text: 8.18 or later + opam: '{>= "8.18"}' tested_coq_opam_versions: - version: dev -- version: '8.16' -- version: '8.15' -- version: '8.14' +- version: '8.18' tested_coq_nix_versions: - coq_version: 'master' diff --git a/theories/Q_to_R.v b/theories/Q_to_R.v index 168caeb..0813a63 100644 --- a/theories/Q_to_R.v +++ b/theories/Q_to_R.v @@ -436,16 +436,16 @@ Proof. destruct (interp_non_zero p) as [p0 [q0 H]]. rewrite (inv_correct p _ _ H); rewrite H. repeat rewrite <- INR_IZR_INZ. - rewrite Rpower.Rinv_Rdiv; auto. + rewrite Rinv_div; auto. (* Qneg *) unfold Q_to_R, numerator, denominator, decode_Q, Qinv, fst, snd. destruct (interp_non_zero p) as [p0 [q0 H]]. rewrite (inv_correct p _ _ H); rewrite H. repeat rewrite Ropp_Ropp_IZR; repeat rewrite <- INR_IZR_INZ. - rewrite Rpower.Rinv_Rdiv; auto. + rewrite Rinv_div; auto. unfold Rdiv; rewrite <- Rmult_opp_opp; rewrite Ropp_involutive; - rewrite Ropp_inv_permute; auto. + rewrite Rinv_opp; auto. Qed. Lemma Q_to_Rminus: forall x y, Q_to_R (Qminus x y) = (Rminus (Q_to_R x) (Q_to_R y)). diff --git a/theories/Qhomographic_Qpositive_to_Q_properties.v b/theories/Qhomographic_Qpositive_to_Q_properties.v index 52ef182..63db273 100644 --- a/theories/Qhomographic_Qpositive_to_Q_properties.v +++ b/theories/Qhomographic_Qpositive_to_Q_properties.v @@ -25,12 +25,11 @@ Lemma fraction_encoding_equal : Proof. intros m n Hn1. unfold fraction_encoding at 2; fold fraction_encoding. - functional induction (fraction_encoding m n Hn1); intros Hn2; - rewrite e; - trivial || ( - f_equal; - apply positive_fraction_encoding_equal). -Defined. + functional induction (fraction_encoding m n Hn1); intros Hn2. + - rewrite e; f_equal; apply positive_fraction_encoding_equal. + - rewrite e; f_equal; apply positive_fraction_encoding_equal. + - rewrite e0; trivial. +Defined. Ltac Rewrite_eq_ := @@ -399,7 +398,7 @@ generalize rewrite (Qhomographic_Qpositive_to_Q_0 a b c 0 p H_Qhomographic_sg_denom_nonzero2 - Hc a0 (refl_equal 0%Z)). + Hc e (refl_equal 0%Z)). apply fraction_encoding_equal. Falsum. generalize @@ -409,35 +408,35 @@ generalize rewrite (Qhomographic_Qpositive_to_Q_0 a b c 0 p H_Qhomographic_sg_denom_nonzero2 - Hc a0 (refl_equal 0%Z)). + Hc e (refl_equal 0%Z)). apply fraction_encoding_equal. Falsum. (* 2 *) rewrite (Qhomographic_Qpositive_to_Q_1 a b c d p H_Qhomographic_sg_denom_nonzero2 - b0 a0). + n e). apply fraction_encoding_equal. (* 3 *) clear e0. rewrite (h_sign_equal a b c d p H_Qhomographic_sg_denom_nonzero1 - H_Qhomographic_sg_denom_nonzero2) in a1. + H_Qhomographic_sg_denom_nonzero2) in e1. rewrite (Qhomographic_Qpositive_to_Q_2 a b c d p H_Qhomographic_sg_denom_nonzero2 - b0 a1). + n e1). reflexivity. (* 4 *) Clear_eq_. generalize (Qhomographic_Qpositive_to_Q_homographicAcc_pos_1 a b c d p - H_Qhomographic_sg_denom_nonzero1 b0 b1 a1). - assert (l1_eq_one0 := b1). + H_Qhomographic_sg_denom_nonzero1 n e1 l). + assert (l1_eq_one0 := e1). rewrite (h_sign_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) in l1_eq_one0. - assert (z0 := a1). + assert (z0 := l). rewrite (new_a_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) in z0. rewrite @@ -445,9 +444,9 @@ generalize H_Qhomographic_sg_denom_nonzero2) in z0. rewrite (Qhomographic_Qpositive_to_Q_3 a b c d p H_Qhomographic_sg_denom_nonzero2 - b0 l1_eq_one0 + n l1_eq_one0 (Qhomographic_Qpositive_to_Q_homographicAcc_pos_1 a b c d p - H_Qhomographic_sg_denom_nonzero2 b0 l1_eq_one0 z0) z0) + H_Qhomographic_sg_denom_nonzero2 n l1_eq_one0 z0) z0) . intro H_any_homographicAcc. apply f_equal with Qpositive. @@ -472,12 +471,12 @@ generalize Clear_eq_. generalize (Qhomographic_Qpositive_to_Q_homographicAcc_pos_2 a b c d p - H_Qhomographic_sg_denom_nonzero1 b0 b1 b2). - assert (l1_eq_one0 := b1). + H_Qhomographic_sg_denom_nonzero1 n e1 l). + assert (l1_eq_one0 := e1). rewrite (h_sign_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) in l1_eq_one0. - assert (z0 := b2). + assert (z0 := l). rewrite (new_a_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) in z0. @@ -486,9 +485,9 @@ generalize H_Qhomographic_sg_denom_nonzero2) in z0. rewrite (Qhomographic_Qpositive_to_Q_4 a b c d p H_Qhomographic_sg_denom_nonzero2 - b0 l1_eq_one0 + n l1_eq_one0 (Qhomographic_Qpositive_to_Q_homographicAcc_pos_2 a b c d p - H_Qhomographic_sg_denom_nonzero2 b0 l1_eq_one0 z0) z0) + H_Qhomographic_sg_denom_nonzero2 n l1_eq_one0 z0) z0) . intro H_any_homographicAcc. apply f_equal with Qpositive. @@ -512,12 +511,12 @@ generalize Clear_eq_. generalize (Qhomographic_Qpositive_to_Q_homographicAcc_neg_1 a b c d p - H_Qhomographic_sg_denom_nonzero1 b0 b1 a0). - assert (l1_eq__minus_one0 := b1). + H_Qhomographic_sg_denom_nonzero1 n e0 l). + assert (l1_eq__minus_one0 := e0). rewrite (h_sign_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) in l1_eq__minus_one0. - assert (z0 := a0). + assert (z0 := l). rewrite (new_a_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) in z0. @@ -526,9 +525,9 @@ generalize H_Qhomographic_sg_denom_nonzero2) in z0. rewrite (Qhomographic_Qpositive_to_Q_5 a b c d p H_Qhomographic_sg_denom_nonzero2 - b0 l1_eq__minus_one0 + n l1_eq__minus_one0 (Qhomographic_Qpositive_to_Q_homographicAcc_neg_1 a b c d p - H_Qhomographic_sg_denom_nonzero2 b0 l1_eq__minus_one0 z0) z0) + H_Qhomographic_sg_denom_nonzero2 n l1_eq__minus_one0 z0) z0) . intro H_any_homographicAcc. apply f_equal with Qpositive. @@ -552,12 +551,12 @@ generalize Clear_eq_. generalize (Qhomographic_Qpositive_to_Q_homographicAcc_neg_2 a b c d p - H_Qhomographic_sg_denom_nonzero1 b0 b1 b2). - assert (l1_eq__minus_one0 := b1). + H_Qhomographic_sg_denom_nonzero1 n e0 l). + assert (l1_eq__minus_one0 := e0). rewrite (h_sign_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) in l1_eq__minus_one0. - assert (z0:=b2). + assert (z0:=l). rewrite (new_a_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) in z0. @@ -566,9 +565,9 @@ generalize H_Qhomographic_sg_denom_nonzero2) in z0. rewrite (Qhomographic_Qpositive_to_Q_6 a b c d p H_Qhomographic_sg_denom_nonzero2 - b0 l1_eq__minus_one0 + n l1_eq__minus_one0 (Qhomographic_Qpositive_to_Q_homographicAcc_neg_2 a b c d p - H_Qhomographic_sg_denom_nonzero2 b0 l1_eq__minus_one0 z0) z0) + H_Qhomographic_sg_denom_nonzero2 n l1_eq__minus_one0 z0) z0) . intro H_any_homographicAcc. apply f_equal with Qpositive. diff --git a/theories/Qquadratic_Qpositive_to_Q_properties.v b/theories/Qquadratic_Qpositive_to_Q_properties.v index 50f69b1..e2705fe 100644 --- a/theories/Qquadratic_Qpositive_to_Q_properties.v +++ b/theories/Qquadratic_Qpositive_to_Q_properties.v @@ -819,26 +819,26 @@ Proof. (* 1 *) rewrite (Qquadratic_Qpositive_to_Q_3 _ _ _ _ _ _ _ _ _ _ - H_Qquadratic_sg_denom_nonzero2 a3 a0); reflexivity. + H_Qquadratic_sg_denom_nonzero2 n s); reflexivity. (* 2 *) rewrite (Qquadratic_Qpositive_to_Q_2 _ _ _ _ _ _ _ _ _ _ - H_Qquadratic_sg_denom_nonzero2 b0 a0); reflexivity. + H_Qquadratic_sg_denom_nonzero2 n s); reflexivity. (* 3 *) rewrite (Qquadratic_Qpositive_to_Q_1 _ _ _ _ _ _ _ _ _ _ - H_Qquadratic_sg_denom_nonzero2 b0 a0); reflexivity. + H_Qquadratic_sg_denom_nonzero2 n s); reflexivity. (* 4 *) rewrite (Qquadratic_Qpositive_to_Q_0 _ _ _ _ _ _ _ _ _ _ - H_Qquadratic_sg_denom_nonzero2 b0 a0); reflexivity. + H_Qquadratic_sg_denom_nonzero2 n s); reflexivity. (* 5 *) rewrite (q_sign_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero1 - H_Qquadratic_sg_denom_nonzero2) in a1; + H_Qquadratic_sg_denom_nonzero2) in e2; rewrite (Qquadratic_Qpositive_to_Q_4 _ _ _ _ _ _ _ _ _ _ - H_Qquadratic_sg_denom_nonzero2 b0 a1) + H_Qquadratic_sg_denom_nonzero2 n e2) ; reflexivity. (* 6 *) Absurd_q_sign_. @@ -864,15 +864,15 @@ Proof. H_Qquadratic_sg_denom_nonzero1); assumption. rewrite (Qquadratic_Qpositive_to_Q_5 _ _ _ _ _ _ _ _ _ _ - H_Qquadratic_sg_denom_nonzero2 b0 + H_Qquadratic_sg_denom_nonzero2 n (trans_eq (q_sign_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 - H_Qquadratic_sg_denom_nonzero1) b1) H + H_Qquadratic_sg_denom_nonzero1) e2) H (Qquadratic_Qpositive_to_Q_quadraticAcc_pos_1 _ _ _ _ _ _ _ _ _ _ - H_Qquadratic_sg_denom_nonzero2 b0 + H_Qquadratic_sg_denom_nonzero2 n (trans_eq (q_sign_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 - H_Qquadratic_sg_denom_nonzero1) b1) H)) + H_Qquadratic_sg_denom_nonzero1) e2) H)) ; apply f_equal with Qpositive; apply Qquadratic_Qpositive_to_Qpositive_equal_strong; [ apply qnew_a_equal @@ -908,15 +908,15 @@ Proof. H_Qquadratic_sg_denom_nonzero1); assumption. rewrite (Qquadratic_Qpositive_to_Q_6 _ _ _ _ _ _ _ _ _ _ - H_Qquadratic_sg_denom_nonzero2 b0 + H_Qquadratic_sg_denom_nonzero2 n (trans_eq (q_sign_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 - H_Qquadratic_sg_denom_nonzero1) b1) H + H_Qquadratic_sg_denom_nonzero1) e2) H (Qquadratic_Qpositive_to_Q_quadraticAcc_pos_2 _ _ _ _ _ _ _ _ _ _ - H_Qquadratic_sg_denom_nonzero2 b0 + H_Qquadratic_sg_denom_nonzero2 n (trans_eq (q_sign_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 - H_Qquadratic_sg_denom_nonzero1) b1) H)) + H_Qquadratic_sg_denom_nonzero1) e2) H)) . apply f_equal with Qpositive; apply Qquadratic_Qpositive_to_Qpositive_equal_strong; @@ -955,15 +955,15 @@ Proof. H_Qquadratic_sg_denom_nonzero1); assumption. rewrite (Qquadratic_Qpositive_to_Q_7 _ _ _ _ _ _ _ _ _ _ - H_Qquadratic_sg_denom_nonzero2 b0 + H_Qquadratic_sg_denom_nonzero2 n (trans_eq (q_sign_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 - H_Qquadratic_sg_denom_nonzero1) b1) H + H_Qquadratic_sg_denom_nonzero1) e1) H (Qquadratic_Qpositive_to_Q_quadraticAcc_neg_1 _ _ _ _ _ _ _ _ _ _ - H_Qquadratic_sg_denom_nonzero2 b0 + H_Qquadratic_sg_denom_nonzero2 n (trans_eq (q_sign_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 - H_Qquadratic_sg_denom_nonzero1) b1) H)) + H_Qquadratic_sg_denom_nonzero1) e1) H)) . apply f_equal with Qpositive; apply Qquadratic_Qpositive_to_Qpositive_equal_strong; @@ -1001,15 +1001,15 @@ Proof. H_Qquadratic_sg_denom_nonzero1); assumption. rewrite (Qquadratic_Qpositive_to_Q_8 _ _ _ _ _ _ _ _ _ _ - H_Qquadratic_sg_denom_nonzero2 b0 + H_Qquadratic_sg_denom_nonzero2 n (trans_eq (q_sign_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 - H_Qquadratic_sg_denom_nonzero1) b1) H + H_Qquadratic_sg_denom_nonzero1) e1) H (Qquadratic_Qpositive_to_Q_quadraticAcc_neg_2 _ _ _ _ _ _ _ _ _ _ - H_Qquadratic_sg_denom_nonzero2 b0 + H_Qquadratic_sg_denom_nonzero2 n (trans_eq (q_sign_equal a b c d _ _ _ _ _ _ H_Qquadratic_sg_denom_nonzero2 - H_Qquadratic_sg_denom_nonzero1) b1) H)) + H_Qquadratic_sg_denom_nonzero1) e1) H)) . apply f_equal with Qpositive; apply Qquadratic_Qpositive_to_Qpositive_equal_strong; diff --git a/theories/homographic_correctness.v b/theories/homographic_correctness.v index ef99dbf..49b60de 100644 --- a/theories/homographic_correctness.v +++ b/theories/homographic_correctness.v @@ -210,7 +210,7 @@ Proof. functional induction (Qmult y x); intros. (* Qneg 0: 1 *) apply False_ind. - apply (Zorder.Zlt_not_eq _ _ a0). + apply (Zorder.Zlt_not_eq _ _ l). rewrite <- Zsgn_15. apply Zsgn_6. rewrite Z_eq_mult; try reflexivity. @@ -224,7 +224,7 @@ Proof. symmetry in |- *; assumption. (* Qneg Qpos : 1 *) apply False_ind. - apply (Zlt_asym _ _ a0). + apply (Zlt_asym _ _ l). rewrite <- Zsgn_15. apply Zsgn_26. assert (Hm : (0 < m)%Z); @@ -293,7 +293,7 @@ Proof. apply Qlt_zero_pos. (* Qneg Qpos : 2 *) apply False_ind. - apply (Zlt_asym _ _ a0). + apply (Zlt_asym _ _ l). rewrite <- Zsgn_15. apply Zsgn_26. assert (Hm : (m < 0)%Z); @@ -315,7 +315,7 @@ Proof. functional induction (Qmult y x); intros. (* Qpos 0: 1 *) apply False_ind. - generalize (Z.gt_lt _ _ b); clear b; intro z. + generalize (Z.gt_lt _ _ g); clear g; intro z. apply (Zorder.Zlt_not_eq _ _ z). symmetry in |- *. rewrite <- Zsgn_15. @@ -355,7 +355,7 @@ Proof. apply Qlt_zero_pos. (* Qpos Qneg : 1 *) apply False_ind. - generalize (Z.gt_lt _ _ b); clear b; intro z. + generalize (Z.gt_lt _ _ g); clear g; intro z. apply (Zlt_asym _ _ z). rewrite <- Zsgn_15. apply Zsgn_27. @@ -376,7 +376,7 @@ Proof. symmetry in |- *; assumption. (* Qpos Qneg : 2 *) apply False_ind. - generalize (Z.gt_lt _ _ b); clear b; intro z. + generalize (Z.gt_lt _ _ g); clear g; intro z. apply (Zlt_asym _ _ z). rewrite <- Zsgn_15. apply Zsgn_27. @@ -629,14 +629,14 @@ Proof. apply H_; clear H_; [ apply eq_Z_to_Q; assumption | reflexivity]. (* (nR2) : b=0 & d<>0 & 00 & ~00 & ~00 & d=0 & 00 & d=0 & ~00 & d=0 & ~00 & d<>0 & (i1 o1 o2) *) unfold spec_Qhomographic_Qpositive_to_Q in |- *; - clear e2 e0 e1 . + clear e0 e1 e2. repeat rewrite Qsgn_15. rewrite Qsgn_28. - case (inside_interval_1_inf _ _ a0); clear a0; + case (inside_interval_1_inf _ _ i); clear i; intros (Hab, Hcd); repeat match goal with @@ -820,10 +820,10 @@ Proof. | apply Z_to_Q_neg; assumption ] ]. (* (nR9) : b<>0 & d<>0 & ~(i1 o1 o2) & (i2 o1 o2)*) unfold spec_Qhomographic_Qpositive_to_Q in |- *; - clear e3 e0 e1 e2 b2. + clear e1 e2 e3. repeat rewrite Qsgn_15. rewrite Qsgn_28. - case (inside_interval_2_inf _ _ a0); clear a0; + case (inside_interval_2_inf _ _ i); clear i; intros (Hab, Hcd); repeat match goal with @@ -889,7 +889,7 @@ Proof. (* Now we just copy-paste the above 10 cases and change nR to dL, the only different cases are recursive calls in which we use spec_Qhomographic_Qpositive_to_Q_dL instead of spec_Qhomographic_Qpositive_to_Q_nR (cases nR4,nR7,nR10 above) *) (* (dL1) : b=0 & d=0 *) - unfold spec_Qhomographic_Qpositive_to_Q in |- *; clear e1 e0. + unfold spec_Qhomographic_Qpositive_to_Q in |- *; clear e1 e3. simpl in |- *. transitivity (Qsgn (Qmult (Qmult a (Qpos (dL q))) (Qinv (Qmult c (Qpos (dL q)))))). @@ -910,14 +910,14 @@ Proof. apply H_; clear H_; [ apply eq_Z_to_Q; assumption | reflexivity]. (* (dL2) : b=0 & d<>0 & 00 & ~00 & ~00 & d=0 & 00 & d=0 & ~00 & d=0 & ~00 & d<>0 & (i1 o1 o2) *) @@ -1042,7 +1042,7 @@ Proof. clear e2 e0 e1 . repeat rewrite Qsgn_15. rewrite Qsgn_28. - case (inside_interval_1_inf _ _ a0); clear a0; + case (inside_interval_1_inf _ _ i); clear i; intros (Hab, Hcd); repeat match goal with @@ -1101,10 +1101,10 @@ Proof. | apply Z_to_Q_neg; assumption ] ]. (* (dL9) : b<>0 & d<>0 & ~(i1 o1 o2) & (i2 o1 o2)*) unfold spec_Qhomographic_Qpositive_to_Q in |- *; - clear e3 e0 e1 e2 b2. + clear e3 e0 e1 e2. repeat rewrite Qsgn_15. rewrite Qsgn_28. - case (inside_interval_2_inf _ _ a0); clear a0; + case (inside_interval_2_inf _ _ i); clear i; intros (Hab, Hcd); repeat match goal with @@ -1164,12 +1164,12 @@ Proof. [ apply Z_to_Q_nonpos; assumption | auto with * ] | apply Z_to_Q_neg; assumption ] ]. (* (dL10) : b<>0 & d<>0 & ~(i1 o1 o2) & ~(i2 o1 o2)*) - clear e3 e0 e1 e2; + clear e0 e1 e2 e3; rewrite spec_Qhomographic_Qpositive_to_Q_dL; rewrite IHp0; reflexivity. (**********************************************************) (* (One1) : (Z.sgn (a+b)) = 0 *) - unfold spec_Qhomographic_Qpositive_to_Q in |- *; clear e0. + unfold spec_Qhomographic_Qpositive_to_Q in |- *; clear e1. rewrite Qsgn_15. replace (Qsgn (Qplus (Qmult a (Qpos One)) b)) with 0%Z. abstract auto with zarith. @@ -1181,10 +1181,10 @@ Proof. assumption. (* (One2) : (Z.sgn (a+b))<>0 & (Z.sgn (a+b))=(Z.sgn (c+d)) *) Transparent Qone. - unfold spec_Qhomographic_Qpositive_to_Q in |- *; clear e1 e0 ; + unfold spec_Qhomographic_Qpositive_to_Q in |- *; clear e2 ; rewrite Qsgn_15; repeat rewrite Qmult_one_right; rewrite Qsgn_28; repeat rewrite <- Z_to_Qplus; repeat rewrite Qsgn_29; - rewrite <- a0; rewrite <- Zsgn_15; symmetry in |- *; + rewrite <- e1; rewrite <- Zsgn_15; symmetry in |- *; apply Zsgn_7'; abstract auto with zarith. (* (One2) : (Z.sgn (a+b))<>0 & (Z.sgn (a+b))<>(Z.sgn (c+d)) *) unfold spec_Qhomographic_Qpositive_to_Q in |- *; clear e1 e0; @@ -1195,8 +1195,8 @@ Proof. (Qhomographic_signok_1 _ _ _x)); intro Hcd_; generalize (Zsgn_1' (a + b)) (Zsgn_1' (c + d)); intros [[Hab| Hab]| Hab] [[Hcd| Hcd]| Hcd]; - try solve [ Falsum ]; rewrite Hab in b1; - rewrite Hcd in b1; try solve [ Falsum ]; + try solve [ Falsum ]; rewrite Hab in n0; + rewrite Hcd in n0; try solve [ Falsum ]; rewrite Hab; rewrite Hcd; constructor). Defined. @@ -1626,9 +1626,9 @@ Proof. (Qhomographic_Qpositive_to_Q a b c d p H_Qhomographic_sg_denom_nonzero). (* 1 *) - clear e e0 e1. + clear e0 e3 e2. rename x into Hc0; - rename a0 into ad_eq_bc; + rename e into ad_eq_bc; rewrite coding_Q. assert (b0_eq_zero : b = 0%Z). rewrite Zmult_0_r in ad_eq_bc. @@ -1644,9 +1644,9 @@ Proof. Anomaly: Search error. Please report. *) rewrite <- Qdiv_num_denom; [ reflexivity | discriminate ]) . - clear e e0 e1. + clear e0 e2 e3. rename x into Hc0; - rename a0 into ad_eq_bc; + rename e into ad_eq_bc; rewrite coding_Q. assert (b0_eq_zero : b = 0%Z). rewrite Zmult_0_r in ad_eq_bc. diff --git a/theories/positive_fraction_encoding.v b/theories/positive_fraction_encoding.v index a00e87b..5aedc3a 100644 --- a/theories/positive_fraction_encoding.v +++ b/theories/positive_fraction_encoding.v @@ -259,7 +259,7 @@ the term (Hyprec m n Hn) has type Ltac Irreflex := try solve - [ elimtype False; + [ exfalso; match goal with | id1:(?X1 <> ?X1) |- _ => apply id1; reflexivity | id1:(?X1 < ?X1)%Z |- _ => @@ -296,7 +296,6 @@ Proof. intros; simpl in |- *; case (Z_dec' m0 n0); [ intros [H_falsum| H_falsum]; Irreflex | trivial ]. - intros; Irreflex. diff --git a/theories/quadratic_correctness.v b/theories/quadratic_correctness.v index be7838d..f033df8 100644 --- a/theories/quadratic_correctness.v +++ b/theories/quadratic_correctness.v @@ -3228,7 +3228,7 @@ Proof. (* 1 *) rewrite coding_Q. unfold spec_fraction_encoding in |- *. - generalize a0; intros (H1, (H2, (H3, (H4, (H5, H6))))); + generalize s; intros (H1, (H2, (H3, (H4, (H5, H6))))); repeat match goal with | id1:(_ = _ :>Z) |- _ => @@ -3244,7 +3244,7 @@ Proof. (* 2 *) rewrite coding_Q. unfold spec_fraction_encoding in |- *. - generalize a0; intros (H1, (H2, (H3, (H4, (H5, H6))))); + generalize s; intros (H1, (H2, (H3, (H4, (H5, H6))))); repeat match goal with | id1:(_ = _ :>Z) |- _ => @@ -3260,7 +3260,7 @@ Proof. (* 3 *) rewrite coding_Q. unfold spec_fraction_encoding in |- *. - generalize a0; intros (H1, (H2, (H3, (H4, (H5, H6))))); + generalize s; intros (H1, (H2, (H3, (H4, (H5, H6))))); repeat match goal with | id1:(_ = _ :>Z) |- _ => @@ -3276,7 +3276,7 @@ Proof. (* 4 *) rewrite coding_Q. unfold spec_fraction_encoding in |- *. - generalize a0; intros (H1, (H2, (H3, (H4, (H5, H6))))); + generalize s; intros (H1, (H2, (H3, (H4, (H5, H6))))); repeat match goal with | id1:(_ = _ :>Z) |- _ =>