diff --git a/.github/workflows/generate_docs.yml b/.github/workflows/generate_docs.yml index e76a4fdf7..a14e3aedd 100644 --- a/.github/workflows/generate_docs.yml +++ b/.github/workflows/generate_docs.yml @@ -38,7 +38,7 @@ jobs: run: opam install -y --deps-only . && opam exec -- make -j 4 - name: Install Rocqnavi - run: opam install -y rocq-navi + run: opam install -y rocq-navi.0.3.1 - name: Generate Documents run: | diff --git a/.github/workflows/nix-action-8.20-2.3.0.yml b/.github/workflows/nix-action-8.20-master.yml similarity index 86% rename from .github/workflows/nix-action-8.20-2.3.0.yml rename to .github/workflows/nix-action-8.20-master.yml index b281d45cb..3bd3789a7 100644 --- a/.github/workflows/nix-action-8.20-2.3.0.yml +++ b/.github/workflows/nix-action-8.20-master.yml @@ -39,7 +39,7 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (coq) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20-2.3.0\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch + \"8.20-master\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation failed\"; exit 1; fi\n" - id: stepCheck @@ -51,7 +51,7 @@ jobs: status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "coq" mathcomp: needs: @@ -94,7 +94,7 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20-2.3.0\" --argstr job \"mathcomp\" \\\n --dry-run 2> err > out || + \"8.20-master\" --argstr job \"mathcomp\" \\\n --dry-run 2> err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation failed\"; exit 1; fi\n" - id: stepCheck @@ -106,20 +106,21 @@ jobs: status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-character" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp" mathcomp-analysis: needs: - coq - mathcomp-reals + - mathcomp-bigenough runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -158,7 +159,7 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-analysis) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20-2.3.0\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2> err + \"8.20-master\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2> err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation failed\"; exit 1; fi\n" - id: stepCheck @@ -170,27 +171,30 @@ jobs: status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-reals' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-reals" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-analysis" mathcomp-analysis-single: needs: - coq + - mathcomp-finmap + - mathcomp-bigenough + - mathcomp-bigenough runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -229,7 +233,7 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-analysis-single) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20-2.3.0\" --argstr job \"mathcomp-analysis-single\" \\\n --dry-run + \"8.20-master\" --argstr job \"mathcomp-analysis-single\" \\\n --dry-run 2> err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation failed\"; exit 1; fi\n" - id: stepCheck @@ -241,35 +245,35 @@ jobs: status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-ssreflect" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-finmap" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-analysis-single" mathcomp-analysis-stdlib: needs: @@ -314,7 +318,7 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-analysis-stdlib) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20-2.3.0\" --argstr job \"mathcomp-analysis-stdlib\" \\\n --dry-run + \"8.20-master\" --argstr job \"mathcomp-analysis-stdlib\" \\\n --dry-run 2> err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation failed\"; exit 1; fi\n" - id: stepCheck @@ -326,23 +330,87 @@ jobs: status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-analysis' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-analysis" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-reals-stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-reals-stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-analysis-stdlib" + mathcomp-bigenough: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url + }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git + merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null + 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ + \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ + \ fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (mathcomp-bigenough) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"8.20-master\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run 2> err + > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + getting derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" + --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" + --argstr job "mathcomp-boot" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" + --argstr job "mathcomp-bigenough" mathcomp-classical: needs: - coq + - mathcomp-finmap runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -381,7 +449,7 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-classical) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20-2.3.0\" --argstr job \"mathcomp-classical\" \\\n --dry-run 2> err + \"8.20-master\" --argstr job \"mathcomp-classical\" \\\n --dry-run 2> err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation failed\"; exit 1; fi\n" - id: stepCheck @@ -393,28 +461,29 @@ jobs: status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-ssreflect" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-finmap" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-classical" mathcomp-experimental-reals: needs: - coq - mathcomp-reals + - mathcomp-bigenough runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -453,7 +522,7 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-experimental-reals) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20-2.3.0\" --argstr job \"mathcomp-experimental-reals\" \\\n --dry-run + \"8.20-master\" --argstr job \"mathcomp-experimental-reals\" \\\n --dry-run 2> err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation failed\"; exit 1; fi\n" - id: stepCheck @@ -465,24 +534,23 @@ jobs: status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-reals' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-reals" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "mathcomp-experimental-reals" - mathcomp-reals: + mathcomp-finmap: needs: - coq - - mathcomp-classical runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -519,11 +587,11 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepGetDerivation - name: Getting derivation for current job (mathcomp-reals) + name: Getting derivation for current job (mathcomp-finmap) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20-2.3.0\" --argstr job \"mathcomp-reals\" \\\n --dry-run 2> err > out - || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting - derivation failed\"; exit 1; fi\n" + \"8.20-master\" --argstr job \"mathcomp-finmap\" \\\n --dry-run 2> err > + out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + getting derivation failed\"; exit 1; fi\n" - id: stepCheck name: Checking presence of CI target for current job run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs @@ -533,20 +601,20 @@ jobs: status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-classical' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" - --argstr job "mathcomp-classical" + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" + --argstr job "mathcomp-boot" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" - --argstr job "mathcomp-reals" - mathcomp-reals-stdlib: + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" + --argstr job "mathcomp-finmap" + mathcomp-reals: needs: - coq - - mathcomp-reals + - mathcomp-classical runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -583,11 +651,11 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepGetDerivation - name: Getting derivation for current job (mathcomp-reals-stdlib) + name: Getting derivation for current job (mathcomp-reals) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20-2.3.0\" --argstr job \"mathcomp-reals-stdlib\" \\\n --dry-run 2> - err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"\ - Error: getting derivation failed\"; exit 1; fi\n" + \"8.20-master\" --argstr job \"mathcomp-reals\" \\\n --dry-run 2> err > + out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + getting derivation failed\"; exit 1; fi\n" - id: stepCheck name: Checking presence of CI target for current job run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs @@ -597,21 +665,20 @@ jobs: status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-reals' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" - --argstr job "mathcomp-reals" + name: 'Building/fetching previous CI target: mathcomp-classical' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" + --argstr job "mathcomp-classical" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" - --argstr job "mathcomp-reals-stdlib" - ssprove: + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" + --argstr job "mathcomp-reals" + mathcomp-reals-stdlib: needs: - coq - - mathcomp-analysis - - mathcomp-experimental-reals + - mathcomp-reals runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -648,11 +715,11 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepGetDerivation - name: Getting derivation for current job (ssprove) + name: Getting derivation for current job (mathcomp-reals-stdlib) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20-2.3.0\" --argstr job \"ssprove\" \\\n --dry-run 2> err > out || (touch - fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation - failed\"; exit 1; fi\n" + \"8.20-master\" --argstr job \"mathcomp-reals-stdlib\" \\\n --dry-run 2> + err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"\ + Error: getting derivation failed\"; exit 1; fi\n" - id: stepCheck name: Checking presence of CI target for current job run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs @@ -662,48 +729,24 @@ jobs: status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: equations' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" - --argstr job "equations" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-boot' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" - --argstr job "mathcomp-boot" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-analysis' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" - --argstr job "mathcomp-analysis" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-experimental-reals' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" - --argstr job "mathcomp-experimental-reals" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: extructures' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" - --argstr job "extructures" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: deriving' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" - --argstr job "deriving" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-word' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" - --argstr job "mathcomp-word" + name: 'Building/fetching previous CI target: mathcomp-reals' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" + --argstr job "mathcomp-reals" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.3.0" - --argstr job "ssprove" -name: Nix CI for bundle 8.20-2.3.0 + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-master" + --argstr job "mathcomp-reals-stdlib" +name: Nix CI for bundle 8.20-master on: pull_request: paths: - - .github/workflows/nix-action-8.20-2.3.0.yml + - .github/workflows/nix-action-8.20-master.yml pull_request_target: paths-ignore: - - .github/workflows/nix-action-8.20-2.3.0.yml + - .github/workflows/nix-action-8.20-master.yml types: - opened - synchronize diff --git a/.nix/config.nix b/.nix/config.nix index d569074e1..2b6bf88ff 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -45,21 +45,24 @@ in { ## select an entry to build in the following `bundles` set ## defaults to "default" - default-bundle = "8.20-2.4.0"; + default-bundle = "9.0"; ## write one `bundles.name` attribute set per ## alternative configuration ## When generating GitHub Action CI, one workflow file ## will be created per bundle - bundles."8.20-2.3.0".coqPackages = common-bundle // { + bundles."8.20-2.4.0".coqPackages = common-bundle // { coq.override.version = "8.20"; - mathcomp.override.version = "2.3.0"; + mathcomp.override.version = "2.4.0"; }; - bundles."8.20-2.4.0".coqPackages = common-bundle // { + bundles."8.20-master".coqPackages = common-bundle // { coq.override.version = "8.20"; - mathcomp.override.version = "2.4.0"; + mathcomp.override.version = "master"; + mathcomp-bigenough.override.version = "master"; + mathcomp-finmap.override.version = "master"; + ssprove.job = false; }; bundles."9.0" = { diff --git a/CHANGELOG.md b/CHANGELOG.md index 60e5a6de0..92964dc9a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,130 @@ # Changelog -Latest releases: [[1.12.0] - 2025-07-03](#1120---2025-07-03), [[1.11.0] - 2025-05-02](#1110---2025-05-02), and [[1.10.0] - 2025-04-21](#1100---2025-04-21) +Latest releases: [[1.13.0] - 2025-08-16](#1130---2025-08-16), [[1.12.0] - 2025-07-03](#1120---2025-07-03), and [[1.11.0] - 2025-05-02](#1110---2025-05-02) + +## [1.13.0] - 2025-08-16 + +### Added + +- in `unstable.v`: + + lemma `sqrtK` + +- in `mathcomp_extra.v`: + + lemmas `subrKC`, `sumr_le0`, `card_fset_sum1` + +- in `functions.v`: + + lemmas `fct_prodE`, `prodrfctE` + +- in `classical_orders.v`: + + lemma `big_lexi_order_prefix_closed_itv` + +- in `topology_structure.v`: + + lemmas `denseI`, `dense0` + +- in `pseudometric_normed_Zmodule.v`: + + lemma `dense_set1C` + +- in `constructive_ereal.v`: + + lemma `expe0`, `mule0n`, `muleS` + +- in `reals.v`: + + definition `irrational` + + lemmas `irrationalE`, `rationalP` + +- new file `borel_hierarchy.v`: + + definitions `Gdelta`, `Fsigma` + + lemmas `closed_Fsigma`, `Gdelta_measurable`, `Gdelta_subspace_open`, + `irrational_Gdelta`, `not_rational_Gdelta` + +- in `realfun.v`: + + instance `is_derive1_sqrt` + +- in `exp.v`: + + lemma `norm_expR` + + lemmas `expeR_eqy` + + lemmas `lt0_powR1`, `powR_eq1` + + definition `lne` + + lemmas `le0_lneNy`, `lne_EFin`, `expeRK`, `lneK`, `lneK_eq`, `lne1`, `lneM`, + `lne_inj`, `lneV`, `lne_div`, `lte_lne`, `lee_lne`, `lneXn`, `le_lne1Dx`, + `lne_sublinear`, `lne_ge0`, `lne_lt0`, `lne_gt0`, `lne_le0` + + lemma `lne_eq0` + +- in `lebesgue_measure.v`: + + lemma `countable_lebesgue_measure0` + +- in `charge.v`: + + definition `copp`, lemma `cscaleN1` + +- in `hoelder.v` + + lemma `hoelder_conj_ge1` + +### Changed + +- in `constructive_ereal.v`: + + lemma `mulN1e` + +- moved from `pi_irrational.v` to `reals.v` and changed + + definition `rational` + +- in `measurable_realfun.v`: + + generalized and renamed: + * `measurable_fun_itv_bndo_bndc` -> `measurable_fun_itv_bndo_bndcP` + * `measurable_fun_itv_obnd_cbnd` -> `measurable_fun_itv_obnd_cbndP` + +- moved from `simple_functions.v` to `measure.v` + + notations `{mfun _ >-> _}`, `[mfun of _]` + + mixin `isMeasurableFun`, structure `MesurableFun`, lemmas `measurable_funP` + + definitions `mfun`, `mfun_key`, canonical `mfun_keyed` + + definitions `mfun_Sub_subproof`, `mfun_Sub` + + lemmas `mfun_rect`, `mfun_valP`, `mfuneqP` + + lemma `measurableT_comp_subproof` + +- moved from `simple_functions.v` to `measure.v` and renamed: + + lemma `measurable_sfunP` -> `measurable_funPTI` + +- moved from `simple_functions.v` to `measurable_realfun.v` + + lemmas `mfun_subring_closed`, `mfun0`, `mfun1`, `mfunN`, + `mfunD`, `mfunB`, `mfunM`, `mfunMn`, `mfun_sum`, `mfun_prod`, `mfunX` + + definitions `mindic`, `indic_mfun`, `scale_mfun`, `max_mfun` + + lemmas `mindicE`, `max_mfun_subproof` + +- moved from `simple_functions.v` to `lebesgue_stieltjes_measure.v` and renamed: + + lemma `measurable_sfun_inP` -> `measurable_funP1` + +### Renamed + +- in `derive.v`: + + `derivemxE` -> `deriveEjacobian` + +- in `exp.v`: + + `ltr_expeR` -> `lte_expeR` + + `ler_expeR` -> `lee_expeR` + +- in `lebesgue_stieltjes_measure.v`: + + `cumulativeNy0` -> `cumulativeNy` + + `cumulativey1` -> `cumulativey` + +- `measurable_sfunP` -> `measurable_funPTI` + (and moved from from `simple_functions.v` to `measure.v`) + +- `measurable_sfun_inP` -> `measurable_funP1` + (and moved from `simple_functions.v` to `lebesgue_stieltjes_measure.v`) + +### Generalized + +- in `functions.v` + + lemma `fct_sumE` (from a pointwise equality to a functional one) + +### Removed + +- file `forms.v` (superseded by MathComp's `sesquilinear.v`) + +- in `unstable.v`: + + `dependent_choice_Type` (use Rocq's `dependent_choice` instead) + +- in `simple_functions.v`: + + duplicated hints about `measurable_set1` + + lemma `measurableT_comp_subproof` turned into a `Let` (now in `measure.v`) ## [1.12.0] - 2025-07-03 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 78d0bf711..d2d0ed195 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,92 +4,86 @@ ### Added -- in `unstable.v`: - + lemma `sqrtK` - -- in `realfun.v`: - + instance `is_derive1_sqrt` - -- in `mathcomp_extra.v`: - + lemmas `subrKC`, `sumr_le0`, `card_fset_sum1` +- in `constructive_ereal.v`: + + lemma `ltgte_fin_num` -- in `functions.v`: - + lemmas `fct_prodE`, `prodrfctE` +- in `probability.v`: + + lemmas `cdf_fin_num`, `lebesgue_stieltjes_cdf_id` -- in `exp.v`: - + lemma `norm_expR` +- in `num_normedtype.v`: + + lemma `nbhs_infty_gtr` +- in `function_spaces.v`: + + lemmas `cvg_big`, `continuous_big` -- in `hoelder.v` - + lemma `hoelder_conj_ge1` +- in `realfun.v`: + + lemma `cvg_addrl_Ny` -- in `reals.v`: - + definition `irrational` - + lemmas `irrationalE`, `rationalP` +- in `constructive_ereal.v`: + + lemmas `mule_natr`, `dmule_natr` + + lemmas `inve_eqy`, `inve_eqNy` -- in `topology_structure.v`: - + lemmas `denseI`, `dense0` +- in `uniform_structure.v`: + + lemma `continuous_injective_withinNx` +- in `constructive_ereal.v`: + + variants `Ione`, `Idummy_placeholder` + + inductives `Inatmul`, `IEFin` + + definition `parse`, `print` + + number notations in scopes `ereal_dual_scope` and `ereal_scope` + + notation `- 1` in scopes `ereal_dual_scope` and `ereal_scope` - in `pseudometric_normed_Zmodule.v`: - + lemma `dense_set1C` - -- new file `borel_hierarchy.v`: - + definitions `Gdelta`, `Fsigma` - + lemmas `closed_Fsigma`, `Gdelta_measurable`, `Gdelta_subspace_open`, - `irrational_Gdelta`, `not_rational_Gdelta` + + lemma `le0_ball0` +- in `theories/landau.v`: + + lemma `littleoE0` - in `constructive_ereal.v`: - + lemma `expe0`, `mule0n`, `muleS` - -- in `exp.v`: - + lemmas `expeR_eqy` - + lemmas `lt0_powR1`, `powR_eq1` - + definition `lne` - + lemmas `le0_lneNy`, `lne_EFin`, `expeRK`, `lneK`, `lneK_eq`, `lne1`, `lneM`, - `lne_inj`, `lneV`, `lne_div`, `lte_lne`, `lee_lne`, `lneXn`, `le_lne1Dx`, - `lne_sublinear`, `lne_ge0`, `lne_lt0`, `lne_gt0`, `lne_le0` - + lemma `lne_eq0` - -- in `charge.v`: - + definition `copp`, lemma `cscaleN1` -- in `classical_orders.v`: - + lemma `big_lexi_order_prefix_closed_itv` + + lemma `lt0_adde` -### Changed +- in `unstable.v` + + lemmas `coprime_prodr`, `Gauss_dvd_prod`, `expn_prod`, `mono_leq_infl`, + `card_big_setU` -- moved from `pi_irrational.v` to `reals.v` and changed - + definition `rational` +- file `pnt.v` + + definitions `next_prime`, `prime_seq` + + lemmas `leq_prime_seq`, `mem_prime_seq` + + theorem `dvg_sum_inv_prime_seq` -- in `constructive_ereal.v`: - + lemma `mulN1e` - -- in `measurable_realfun.v`: - + generalized and renamed: - * `measurable_fun_itv_bndo_bndc` -> `measurable_fun_itv_bndo_bndcP` - * `measurable_fun_itv_obnd_cbnd` -> `measurable_fun_itv_obnd_cbndP` +### Changed -### Renamed +- in `lebesgue_stieltjes_measure.v` specialized from `numFieldType` to `realFieldType`: + + lemma `nondecreasing_right_continuousP` + + definition `CumulativeBounded` -- in `lebesgue_stieltjes_measure.v`: - + `cumulativeNy0` -> `cumulativeNy` - + `cumulativey1` -> `cumulativey` +- in `lebesgue_stieltjes_measure.v`, according to generalization of `Cumulative`, modified: + + lemmas `wlength_ge0`, `cumulative_content_sub_fsum`, `wlength_sigma_subadditive`, `lebesgue_stieltjes_measure_unique` + + definitions `lebesgue_stieltjes_measure`, `completed_lebesgue_stieltjes_measure` -- in `exp.v`: - + `ltr_expeR` -> `lte_expeR` - + `ler_expeR` -> `lee_expeR` +- moved from `vitali_lemma.v` to `pseudometric_normed_Zmodule.v` and renamed: + + `closure_ball` -> `closure_ballE` -- in `derive.v`: - + `derivemxE` -> `deriveEjacobian` +### Renamed ### Generalized -- in `functions.v` - + lemma `fct_sumE` (from a pointwise equality to a functional one) +- in `pseudometric_normed_Zmodule.v`: + + lemma `closed_ball0` (`realFieldType` -> `pseudoMetricNormedZmodType`) + + lemmas `closed_ball_closed`, `subset_closed_ball` (`realFieldType` -> `numDomainType`) + + lemma `subset_closure_half` (`realFieldType` -> `numFieldType`) + + lemma `le_closed_ball` (`pseudoMetricNormedZmodType` -> `pseudoMetricType`) + +- in `lebesgue_stieltjes_measure.v` generalized (codomain is now an `orderNbhsType`): + + lemma `right_continuousW` + + record `isCumulative` + + definition `Cumulative` ### Deprecated ### Removed -- file `forms.v` (superseded by MathComp's `sesquilinear.v`) +- file `interval_inference.v` (now in MathComp) + +- in file `all_reals.v` + + export of `interval_inference` (now in mathcomp-algebra, but not automatically exported) ### Infrastructure diff --git a/INSTALL.md b/INSTALL.md index 9b3639952..951c73123 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -3,7 +3,7 @@ ## Requirements - [The Coq Proof Assistant version ≥ 8.20 / Rocq Prover version ≥ 9.0](https://rocq-prover.org) -- [Mathematical Components version ≥ 2.2.0](https://github.com/math-comp/math-comp) +- [Mathematical Components version ≥ 2.4.0](https://github.com/math-comp/math-comp) - [Finmap library version ≥ 2.1.0](https://github.com/math-comp/finmap) - [Hierarchy builder version ≥ 1.8.0](https://github.com/math-comp/hierarchy-builder) - [bigenough ≥ 1.0.0](https://github.com/math-comp/bigenough) @@ -50,7 +50,7 @@ $ opam install coq-mathcomp-analysis ``` To install a precise version, type, say ``` -$ opam install coq-mathcomp-analysis.1.12.0 +$ opam install coq-mathcomp-analysis.1.13.0 ``` 4. Everytime you want to work in this same context, you need to type ``` @@ -73,7 +73,7 @@ using [proof general for emacs](https://github.com/ProofGeneral/PG) ## Break-down of phase 3 of the installation procedure step by step -With the example of Coq 8.20.1 and MathComp 2.3.0. For other versions, update the +With the example of Coq 8.20.1 and MathComp 2.4.0. For other versions, update the version numbers accordingly. 1. Install Coq 8.20.1 @@ -82,11 +82,11 @@ $ opam install coq.8.20.1 ``` 2. Install the Mathematical Components ``` -$ opam install coq-mathcomp-ssreflect.2.3.0 -$ opam install coq-mathcomp-fingroup.2.3.0 -$ opam install coq-mathcomp-algebra.2.3.0 -$ opam install coq-mathcomp-solvable.2.3.0 -$ opam install coq-mathcomp-field.2.3.0 +$ opam install coq-mathcomp-ssreflect.2.4.0 +$ opam install coq-mathcomp-fingroup.2.4.0 +$ opam install coq-mathcomp-algebra.2.4.0 +$ opam install coq-mathcomp-solvable.2.4.0 +$ opam install coq-mathcomp-field.2.4.0 ``` 3. Install the Finite maps library ``` diff --git a/Makefile.common b/Makefile.common index 6422f2d73..827fb5940 100644 --- a/Makefile.common +++ b/Makefile.common @@ -45,25 +45,6 @@ all: config build .PHONY: pre-makefile Makefile.coq: pre-makefile $(COQPROJECT) Makefile - (echo "From mathcomp.algebra Require Import interval_inference." > test_interval_inference.v \ - && ($(COQC) test_interval_inference.v > /dev/null 2>&1) \ - && test -f interval_inference.v -o -f reals/interval_inference.v \ - && touch rm_interval_inference) || true - $(RM) test_interval_inference.v - test -f rm_interval_inference \ - && sed -i.bak '/interval_inference/ d' $(COQPROJECT) \ - && $(RM) $(COQPROJECT).bak || true - test -f rm_interval_inference \ - && sed -i.bak '/interval_inference/ d' all_reals.v \ - && $(RM) all_reals.v.bak || true - test -f rm_interval_inference \ - && sed -i.bak '/interval_inference/ d' reals/all_reals.v \ - && $(RM) reals/all_reals.v.bak || true - test -f rm_interval_inference && $(RM) interval_inference.v || true - test -f rm_interval_inference && $(RM) reals/interval_inference.v || true - $(RM) rm_interval_inference - # Remove everything above when requiring mathcomp >= 2.4.0 - # (also remove file reals/interval_inference.v and references to it) $(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT) -o Makefile.coq # Global config, build, clean and distclean -------------------------- @@ -132,33 +113,15 @@ $(DOCDIR)/dependency_graph.dot: $(DOCDIR)/dependency_graph.pre tred $(DOCDIR)/dependency_graph.pre > $(DOCDIR)/dependency_graph.dot html: build $(DOCDIR)/dependency_graph.dot + etc/rocqnavi_generate-hierarchy-graph.sh $(DOCDIR)/hierarchy_graph.dot mkdir -p $(DOCDIR) find . -not -path '*/.*' -name "*.v" -or -name "*.glob" | xargs rocqnavi \ -title "Mathcomp Analysis" \ -d $(DOCDIR) -base mathcomp -Q theories analysis \ -coqlib https://rocq-prover.org/doc/V8.20.1/stdlib/ \ -dependency-graph $(DOCDIR)/dependency_graph.dot \ - -external https://math-comp.github.io/htmldoc_2_3_0/ mathcomp.ssreflect \ - -external https://math-comp.github.io/htmldoc_2_3_0/ mathcomp.algebra - -machtml: build $(DOCDIR)/dependency_graph.dot - coqdep -f _CoqProject > depend.d - cat -n depend.d >&2 - gsed -i 's/Classical/mathcomp\.classical/' depend.dot - gsed -i 's/Theories/mathcomp\.analysis/' depend.dot - gsed -i 's/Reals_stdlib/mathcomp\.reals_stdlib/' depend.dot - gsed -i 's/Experimental_reals/mathcomp\.experimental_reals/' depend.dot - gsed -i 's/Reals/mathcomp\.reals/' depend.dot - gsed -i 's/Analysis_stdlib/mathcomp\.analysis_stdlib/' depend.dot - gsed -i 's/\//\./g' depend.dot - ../coq2html/tools/generate-hierarchy-graph.sh - rm test_interval_inference.glob - find . -not -path '*/.*' -name "*.v" -or -name "*.glob" | xargs ../coq2html/rocqnavi \ - -title "Mathcomp Analysis" \ - -d $(DOCDIR) -base mathcomp -Q theories analysis \ - -coqlib https://rocq-prover.org/doc/V8.20.1/stdlib/ \ - -hierarchy-graph "hierarchy-graph.dot" \ - -dependency-graph $(DOCDIR)/dependency_graph.dot \ - -external https://math-comp.github.io/htmldoc_2_3_0/ mathcomp.ssreflect \ - -external https://math-comp.github.io/htmldoc_2_3_0/ mathcomp.algebra \ - -index-blacklist ../coq2html/tools/index-blacklist + -hierarchy-graph $(DOCDIR)/hierarchy_graph.dot \ + -index-blacklist etc/rocqnavi_index-blacklist \ + -show-type-information-using-coqtop-process \ + -external https://math-comp.github.io/htmldoc_2_4_0/ mathcomp.ssreflect \ + -external https://math-comp.github.io/htmldoc_2_4_0/ mathcomp.algebra diff --git a/README.md b/README.md index 442313974..5762203c4 100644 --- a/README.md +++ b/README.md @@ -26,12 +26,12 @@ In terms of [opam](https://opam.ocaml.org/doc/Install.html), it comes as the fol - License: [CeCILL-C](LICENSE) - Compatible Rocq versions: Coq 8.20, Rocq 9.0 (or dev) - Additional dependencies: - - [MathComp ssreflect 2.1.0 or later](https://math-comp.github.io) - - [MathComp fingroup 2.1.0 or later](https://math-comp.github.io) - - [MathComp algebra 2.1.0 or later](https://math-comp.github.io) - - [MathComp solvable 2.1.0 or later](https://math-comp.github.io) - - [MathComp field 2.1.0 or later](https://math-comp.github.io) - - [MathComp finmap 2.0.0](https://github.com/math-comp/finmap) + - [MathComp ssreflect 2.4.0 or later](https://math-comp.github.io) + - [MathComp fingroup 2.4.0 or later](https://math-comp.github.io) + - [MathComp algebra 2.4.0 or later](https://math-comp.github.io) + - [MathComp solvable 2.4.0 or later](https://math-comp.github.io) + - [MathComp field 2.4.0 or later](https://math-comp.github.io) + - [MathComp finmap 2.1.0](https://github.com/math-comp/finmap) - [MathComp bigenough 1.0.0](https://github.com/math-comp/bigenough) - [Hierarchy Builder 1.8.0 or later](https://github.com/math-comp/hierarchy-builder) - Coq/Rocq namespace: `mathcomp.analysis` @@ -73,7 +73,7 @@ We try to preserve backward compatibility as best as we can. Each file is documented in its header in ASCII. -[HTML rendering of the source code](https://math-comp.github.io/analysis/htmldoc_1_12_0/index.html) (using [`rocqnavi`](https://github.com/affeldt-aist/rocqnavi)). +[HTML rendering of the source code](https://math-comp.github.io/analysis/htmldoc_1_13_0/index.html) (using [`rocqnavi`](https://github.com/affeldt-aist/rocqnavi)). It includes inheritance diagrams for the mathematical structures that MathComp-Analysis adds on top of MathComp's ones. Overview presentations: diff --git a/_CoqProject b/_CoqProject index 47e426cfc..afa7fd3af 100644 --- a/_CoqProject +++ b/_CoqProject @@ -30,7 +30,6 @@ reals/constructive_ereal.v reals/reals.v reals/real_interval.v reals/signed.v -reals/interval_inference.v reals/prodnormedzmodule.v reals/all_reals.v experimental_reals/xfinmap.v @@ -120,5 +119,6 @@ theories/kernel.v theories/pi_irrational.v theories/gauss_integral.v theories/showcase/summability.v +theories/showcase/pnt.v analysis_stdlib/Rstruct_topology.v analysis_stdlib/showcase/uniform_bigO.v diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 2e7d9f38e..0038fbcd6 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -147,22 +147,22 @@ Context {R : archiDomainType}. Implicit Type x : R. Lemma ge_floor x : (Num.floor x)%:~R <= x. -Proof. exact: Num.Theory.ge_floor. Qed. +Proof. exact: Num.Theory.floor_le_tmp. Qed. #[deprecated(since="mathcomp 2.4.0", note="Use floor_ge_int_tmp instead.")] Lemma floor_ge_int x (z : int) : (z%:~R <= x) = (z <= Num.floor x). -Proof. exact: Num.Theory.floor_ge_int. Qed. +Proof. by rewrite floor_ge_int_tmp. Qed. Lemma lt_succ_floor x : x < (Num.floor x + 1)%:~R. Proof. exact: Num.Theory.lt_succ_floor. Qed. #[deprecated(since="mathcomp-analysis 1.3.0", note="use `Num.Theory.le_ceil` instead")] Lemma ceil_ge x : x <= (Num.ceil x)%:~R. -Proof. exact: Num.Theory.le_ceil. Qed. +Proof. exact: Num.Theory.ceil_ge. Qed. #[deprecated(since="mathcomp-analysis 1.3.0", note="use `Num.Theory.ceil_le_int`")] Lemma ceil_ge_int x (z : int) : (x <= z%:~R) = (Num.ceil x <= z). -Proof. exact: Num.Theory.ceil_le_int. Qed. +Proof. by rewrite Num.Theory.ceil_le_int_tmp. Qed. Lemma ceilN x : Num.ceil (- x) = - Num.floor x. Proof. by rewrite ?ceilNfloor /Num.ceil opprK. Qed. @@ -331,7 +331,7 @@ by move=> ?; rewrite [RHS]real_ltNge ?realz -?real_floor_ge_int_tmp -?ltNge. Qed. Lemma le_floor : {homo (@Num.floor R) : x y / x <= y}. -Proof. exact: floor_le. Qed. +Proof. exact: le_floor. Qed. Lemma real_floor_eq x n : x \is Num.real -> (Num.floor x == n) = (n%:~R <= x < (n + 1)%:~R). @@ -392,7 +392,7 @@ by move=> xr; apply/eqP/idP => [<-|]; [exact: real_ceil_itv|exact: ceil_def]. Qed. Lemma le_ceil_tmp : {homo (@Num.ceil R) : x y / x <= y}. -Proof. exact: ceil_le. Qed. +Proof. exact: le_ceil_tmp. Qed. Lemma real_ceil_ge0 x : x \is Num.real -> (0 <= Num.ceil x) = (-1 < x). Proof. diff --git a/classical/set_interval.v b/classical/set_interval.v index 5cda86b55..2b9fce511 100644 --- a/classical/set_interval.v +++ b/classical/set_interval.v @@ -20,9 +20,10 @@ From mathcomp Require Import functions. (* factor a b x := (x - a) / (b - a) *) (* set_itvE == multirule to turn intervals into inequalities *) (* disjoint_itv i j == intervals i and j are disjoint *) -(* itv_is_ray i == i is either `]x,+oo[ or `]-oo,x[ *) -(* itv_is_bd_open i == i is `]x,y[ *) -(* itv_open_ends i == i has open endpoints, E.G. is one of the two above *) +(* itv_is_ray i == i is either `]x, +oo[ or `]-oo, x[ *) +(* itv_is_bd_open i == i is `]x, y[ *) +(* itv_open_ends i == i has open endpoints, i.e., it is one of the two *) +(* above *) (* is_open_itv A == the set A can be written as an open interval *) (* open_itv_cover A == the set A can be covered by open intervals *) (* ``` *) diff --git a/classical/unstable.v b/classical/unstable.v index 2b6b090b7..9b57974e4 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -35,26 +35,53 @@ Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Theory. Local Open Scope ring_scope. -(* NB: Coq 8.17.0 generalizes dependent_choice from Set to Type - making the following lemma redundant *) -Section dependent_choice_Type. -Context X (R : X -> X -> Prop). +Lemma coprime_prodr (I : Type) (r : seq I) (P : {pred I}) (F : I -> nat) (a : I) + (l : seq I) : + all (coprime (F a)) [seq F i | i <- [seq i <- l | P i]] -> + coprime (F a) (\prod_(j <- l | P j) F j). +Proof. +elim: l => /= [_|h t ih]; first by rewrite big_nil coprimen1. +rewrite big_cons; case: ifPn => // Ph. +rewrite map_cons => /= /andP[FaFh FatP]. +by rewrite coprimeMr FaFh/= ih. +Qed. + +Lemma Gauss_dvd_prod (I : eqType) (r : seq I) (P : {pred I}) (F : I -> nat) + (n : nat) : + pairwise coprime [seq F i | i <- [seq i <- r | P i]] -> + reflect (forall i, i \in r -> P i -> F i %| n) + (\prod_(i <- r | P i) F i %| n). +Proof. +elim: r => /= [_|a l HI]. + by rewrite big_nil dvd1n; apply: ReflectT => i; rewrite in_nil. +rewrite big_cons; case: ifP => [Pa|nPa]; last first. + move/HI/equivP; apply; split=> [Fidvdn i|Fidvdn i il]. + by rewrite in_cons => /predU1P[->|]; [rewrite nPa|exact: Fidvdn]. + by apply: Fidvdn; rewrite in_cons il orbT. +rewrite map_cons pairwise_cons => /andP[allcoprimea pairwisecoprime]. +rewrite Gauss_dvd; last exact: coprime_prodr. +apply: (equivP (andPP idP (HI pairwisecoprime))). +split=> [[Fadvdn Fidvdn] i|Fidvdn]. + by rewrite in_cons => /predU1P[->//|]; exact: Fidvdn. +split=> [|i il]. + by apply: Fidvdn => //; exact: mem_head. +by apply: Fidvdn; rewrite in_cons il orbT. +Qed. -Lemma dependent_choice_Type : (forall x, {y | R x y}) -> - forall x0, {f | f 0%N = x0 /\ forall n, R (f n) (f n.+1)}. +Lemma expn_prod (I : eqType) (r : seq I) (P : {pred I}) (F : I -> nat) + (n : nat) : + ((\prod_(i <- r | P i) F i) ^ n = \prod_(i <- r | P i) (F i) ^ n)%N. Proof. -move=> h x0. -set (f := fix f n := if n is n'.+1 then proj1_sig (h (f n')) else x0). -exists f; split => //. -intro n; induction n; simpl; apply: proj2_sig. +elim: r => [|a l]; first by rewrite !big_nil exp1n. +by rewrite !big_cons; case: ifPn => // Pa <-; rewrite expnMn. Qed. -End dependent_choice_Type. Section max_min. Variable R : realFieldType. Let nz2 : 2%:R != 0 :> R. Proof. by rewrite pnatr_eq0. Qed. +(* NB: to appear in MathComp 2.5.0 (PR #1416) *) Lemma maxr_absE (x y : R) : Num.max x y = (x + y + `|x - y|) / 2%:R. Proof. apply: canRL (mulfK _) _ => //; rewrite ?pnatr_eq0//. @@ -63,6 +90,7 @@ case: lerP => _; (* TODO: ring *) rewrite [2%:R]mulr2n mulrDr mulr1. by rewrite (addrC (x + y)) subrKA. Qed. +(* NB: to appear in MathComp 2.5.0 (PR #1416) *) Lemma minr_absE (x y : R) : Num.min x y = (x + y - `|x - y|) / 2%:R. Proof. apply: (addrI (Num.max x y)); rewrite addr_max_min maxr_absE. (* TODO: ring *) @@ -77,7 +105,8 @@ Section bigmax_seq. Context d {T : orderType d} {x : T} {I : eqType}. Variables (r : seq I) (i0 : I) (P : pred I). -(* NB: as of [2023-08-28], bigop.leq_bigmax_seq already exists for nat *) +(* NB: as of [2023-08-28], bigop.leq_bigmax_seq already exists for nat, + PRed to MathComp (PR #1449) *) Lemma le_bigmax_seq F : i0 \in r -> P i0 -> (F i0 <= \big[Order.max/x]_(i <- r | P i) F i)%O. Proof. @@ -86,7 +115,8 @@ move=> /predU1P[<-|i0t]; first by rewrite Pi0 le_max// lexx. by case: ifPn => Ph; [rewrite le_max ih// orbT|rewrite ih]. Qed. -(* NB: as of [2023-08-28], bigop.bigmax_sup_seq already exists for nat *) +(* NB: as of [2023-08-28], bigop.bigmax_sup_seq already exists for nat, + PRed to MathComp (PR #1449) *) Lemma bigmax_sup_seq (m : T) (F : I -> T) : i0 \in r -> P i0 -> (m <= F i0)%O -> (m <= \big[Order.max/x]_(i <- r | P i) F i)%O. @@ -108,6 +138,12 @@ Qed. Definition monotonous d (T : porderType d) (pT : predType T) (A : pT) (f : T -> T) := {in A &, {mono f : x y / (x <= y)%O}} \/ {in A &, {mono f : x y /~ (x <= y)%O}}. +Lemma mono_leq_infl f : {mono f : m n / (m <= n)%N} -> forall n, (n <= f n)%N. +Proof. +move=> fincr; elim=> [//| n HR]; rewrite (leq_ltn_trans HR)//. +by rewrite ltn_neqAle fincr (inj_eq (incn_inj fincr)) -ltn_neqAle. +Qed. + (* NB: these lemmas have been introduced to develop the theory of bounded variation *) Section path_lt. Context d {T : orderType d}. @@ -188,6 +224,14 @@ Arguments big_rmcond_in {R idx op I r} P. Reserved Notation "`1- x" (format "`1- x", at level 2). +Lemma card_big_setU (I : Type) (T : finType) (r : seq I) (P : {pred I}) + (F : I -> {set T}) : + (#|\bigcup_(i <- r | P i) F i| <= \sum_(i <- r | P i) #|F i|)%N. +Proof. +elim/big_ind2 : _ => // [|m A n B Am Bn]; first by rewrite cards0. +by rewrite (leq_trans (leq_card_setU _ _))// leq_add. +Qed. + Section onem. Variable R : numDomainType. Implicit Types r : R. @@ -319,7 +363,7 @@ Implicit Type x : R. Lemma abs_ceil_ge x : `|x| <= `|Num.ceil x|.+1%:R. Proof. rewrite -natr1 natr_absz; have [x0|x0] := ltP 0 x. - by rewrite !gtr0_norm ?ceil_gt0// (le_trans (Num.Theory.le_ceil _))// lerDl. + by rewrite !gtr0_norm ?ceil_gt0// (le_trans (Num.Theory.ceil_ge _))// lerDl. by rewrite !ler0_norm ?ceil_le0// ?ceilNfloor opprK intrD1 ltW// floorD1_gt. Qed. diff --git a/coq-mathcomp-classical.opam b/coq-mathcomp-classical.opam index 14509ef40..423b07edc 100644 --- a/coq-mathcomp-classical.opam +++ b/coq-mathcomp-classical.opam @@ -17,7 +17,7 @@ install: [make "-C" "classical" "install"] depends: [ ("coq" {>= "8.20" & < "8.21~"} | "coq-core" { (>= "9.0" & < "9.1~") | (= "dev") }) - "coq-mathcomp-ssreflect" { (>= "2.3.0" & < "2.5~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.5~") | (= "dev") } "coq-mathcomp-fingroup" "coq-mathcomp-algebra" "coq-mathcomp-finmap" { (>= "2.1.0") } diff --git a/etc/rocqnavi_generate-hierarchy-graph.sh b/etc/rocqnavi_generate-hierarchy-graph.sh new file mode 100755 index 000000000..aeaa8e98d --- /dev/null +++ b/etc/rocqnavi_generate-hierarchy-graph.sh @@ -0,0 +1,12 @@ +DST=$1 +coqtop -Q classical mathcomp.classical -Q reals mathcomp.reals -Q reals_stdlib mathcomp.reals_stdlib -Q experimental_reals mathcomp.experimental_reals -Q theories mathcomp.analysis -Q analysis_stdlib mathcomp.analysis_stdlib < |==| %:R%:E with a sequence | *) +(* | | | of digits | *) +(* | - |==| - %:R%:E with a sequence | *) +(* | | | of digits | *) (* | `+%E, -%E, *%E` |==| addition/opposite/multiplication for | *) (* | | | extended reals | *) (* | `x^-1`, `x / y` |==| inverse and division for extended reals | *) @@ -59,6 +65,12 @@ From mathcomp Require Import mathcomp_extra interval_inference. (* \bar R == coproduct of R and {+oo, -oo}; *) (* notation for extended (R:Type) *) (* r%:E == injects real numbers into \bar R *) +(* - x == opposite of x : \bar R *) +(* 0, 1, -1 == 0%R, 1%R%:E, - 1%R%:E *) +(* == %:R%:E with a sequence *) +(* of digits *) +(* - == - %:R%:E with a sequence *) +(* of digits *) (* +%E, -%E, *%E == addition/opposite/multiplication for extended *) (* reals *) (* x^-1, x / y == inverse and division for extended reals *) @@ -582,6 +594,53 @@ Notation "x ^+ n" := (expe x%E n) : ereal_scope. Notation "x *+ n" := (ednatmul x%dE n) : ereal_dual_scope. Notation "x *+ n" := (enatmul x%E n) : ereal_scope. +(**md Notation for constant numerals. This has been introduced so +that, e.g., in the scope `ereal_scope`, `-` is correctly parsed +without requiring one writes `- %:E`. See the Rocq reference manual +for the `Number Notation` command +and [PR #1704](https://github.com/math-comp/analysis/pull/1704) +for more explanations. *) +Variant Ione := IOne : Ione. +Inductive Inatmul := INatmul : Ione -> nat -> Inatmul. +Inductive IEFin := IEFinP : Inatmul -> IEFin | IEFinN : IEFin -> IEFin. +Variant Idummy_placeholder :=. + +Definition parse (x : Number.int) : IEFin := + match x with + | Number.IntDecimal (Decimal.Pos u) => IEFinP (INatmul IOne (Nat.of_uint u)) + | Number.IntDecimal (Decimal.Neg u) => + IEFinN (IEFinP (INatmul IOne (Nat.of_uint u))) + | Number.IntHexadecimal (Hexadecimal.Pos u) => + IEFinP (INatmul IOne (Nat.of_hex_uint u)) + | Number.IntHexadecimal (Hexadecimal.Neg u) => + IEFinN (IEFinP (INatmul IOne (Nat.of_hex_uint u))) + end. + +Definition print (x : IEFin) : option Number.int := + match x with + | IEFinP (INatmul IOne n) => + Some (Number.IntDecimal (Decimal.Pos (Nat.to_uint n))) + | IEFinN (IEFinP (INatmul IOne n)) => + Some (Number.IntDecimal (Decimal.Neg (Nat.to_uint n))) + | _ => None + end. + +Arguments GRing.one {_}. +#[warnings="-via-type-remapping,-via-type-mismatch"] +Number Notation Idummy_placeholder parse print (via IEFin + mapping [[EFin] => IEFinP, [oppe] => IEFinN, + [GRing.natmul] => INatmul, [GRing.one] => IOne]) + : ereal_scope. +#[warnings="-via-type-remapping,-via-type-mismatch"] +Number Notation Idummy_placeholder parse print (via IEFin + mapping [[EFin] => IEFinP, [oppe] => IEFinN, + [GRing.natmul] => INatmul, [GRing.one] => IOne]) + : ereal_dual_scope. +Arguments GRing.one : clear implicits. + +Notation "- 1" := (oppe 1 : dual_extended _) : ereal_dual_scope. +Notation "- 1" := (oppe 1) : ereal_scope. + Notation "\- f" := (fun x => - f x)%dE : ereal_dual_scope. Notation "\- f" := (fun x => - f x)%E : ereal_scope. Notation "f \+ g" := (fun x => f x + g x)%dE : ereal_dual_scope. @@ -684,10 +743,10 @@ Proof. by rewrite lee_fin ler0N1. Qed. Lemma lte0N1 : 0 < (-1)%:E :> \bar R = false. Proof. by rewrite lte_fin ltr0N1. Qed. -Lemma lteN10 : - 1%E < 0 :> \bar R. +Lemma lteN10 : -1 < 0 :> \bar R. Proof. by rewrite lte_fin ltrN10. Qed. -Lemma leeN10 : - 1%E <= 0 :> \bar R. +Lemma leeN10 : -1 <= 0 :> \bar R. Proof. by rewrite lee_fin lerN10. Qed. Lemma lte0n n : (0 < n%:R%:E :> \bar R) = (0 < n)%N. @@ -1273,13 +1332,13 @@ Proof. by move=> rreal; rewrite muleC real_mulrNy. Qed. Definition real_mulr_infty := (real_mulry, real_mulyr, real_mulrNy, real_mulNyr). -Lemma mulN1e x : (- 1%E) * x = - x. +Lemma mulN1e x : -1 * x = - x. Proof. by case: x => [r| |]/=; rewrite /mule ?mulN1r// eqe oppr_eq0 oner_eq0/= lte_fin oppr_gt0 ltr10. Qed. -Lemma muleN1 x : x * (- 1%E) = - x. Proof. by rewrite muleC mulN1e. Qed. +Lemma muleN1 x : x * -1 = - x. Proof. by rewrite muleC mulN1e. Qed. Lemma mule_neq0 x y : x != 0 -> y != 0 -> x * y != 0. Proof. @@ -1695,6 +1754,12 @@ Proof. by move: x => [x| |]//=; rewrite lee_fin => x0; rewrite ltNyr. Qed. Lemma lt0_fin_numE x : x < 0 -> (x \is a fin_num) = (-oo < x). Proof. by move/ltW; exact: le0_fin_numE. Qed. +Lemma ltgte_fin_num x a b : a < x < b -> x \is a fin_num. +Proof. +rewrite fin_numE -ltey -ltNye. +by move=> /andP[/(le_lt_trans (leNye _))->/=] /lt_le_trans -> //; exact: leey. +Qed. + Lemma eqyP x : x = +oo <-> (forall A, (0 < A)%R -> A%:E <= x). Proof. split=> [-> // A A0|Ax]; first by rewrite leey. @@ -1737,6 +1802,17 @@ Qed. Lemma lte_add_pinfty x y : x < +oo -> y < +oo -> x + y < +oo. Proof. by move: x y => -[r [r'| |]| |] // ? ?; rewrite -EFinD ltry. Qed. +Lemma lt0_adde x y : x + y < 0 -> (x < 0) || (y < 0). +Proof. +move: x y => [x| |] [y| |]//; rewrite ?lee_fin ?lte_fin. +- rewrite !ltNge -negb_and; apply: contra. + by move=> /andP[? ?]; rewrite addr_ge0. +- by move=> _; rewrite ltNyr orbT. +- by move=> _; rewrite ltNyr. +- by move=> _; rewrite ltNy0. +- by rewrite ltNy0. +Qed. + Lemma lte_sum_pinfty I (s : seq I) (P : pred I) (f : I -> \bar R) : (forall i, P i -> f i < +oo) -> \sum_(i <- s | P i) f i < +oo. Proof. @@ -2305,7 +2381,7 @@ Qed. Lemma iter_mule n x y : iter n ( *%E x) y = x ^+ n * y. Proof. by elim: n => [|n ih]; rewrite ?mul1e// [LHS]/= ih expeS muleA. Qed. -HB.instance Definition _ := Monoid.isComLaw.Build (\bar R) 1%E mule +HB.instance Definition _ := Monoid.isComLaw.Build (\bar R) 1 mule muleA muleC mul1e. Lemma muleCA : left_commutative ( *%E : \bar R -> \bar R -> \bar R ). @@ -2434,6 +2510,15 @@ move: x => [x| |]/=. - by rewrite inveNy. Qed. +Lemma inve_eqy x : (x^-1 == +oo) = (x == 0). +Proof. +case: x => [r| |] //=; apply/idP/idP => [|]; first by rewrite inver; case: ifPn. +by rewrite eqe => /eqP ->; rewrite inver// eqxx. +Qed. + +Lemma inve_eqNy x : (x^-1 == -oo) = (x == -oo). +Proof. by case: x => [r| |] //=; rewrite inver; case: ifPn. Qed. + Lemma inve_ge0 x : (0 <= x^-1) = (0 <= x). Proof. by case: inveP; rewrite ?le0y ?lexx //= => r; rewrite lee_fin invr_ge0. @@ -2744,6 +2829,9 @@ move: x => [x| |] ih. - by rewrite mulrNy gtr0_sg// mul1e enatmul_ninfty. Qed. +Lemma mule_natr x n : x * n%:R%:E = x *+ n. +Proof. by rewrite muleC mule_natl. Qed. + Lemma lte_pmul x1 y1 x2 y2 : 0 <= x1 -> 0 <= x2 -> x1 < y1 -> x2 < y2 -> x1 * x2 < y1 * y2. Proof. @@ -3280,6 +3368,9 @@ Proof. by move=> x y z; rewrite !dual_addeE oppe_min adde_maxr oppe_max. Qed. Lemma dmule_natl x n : n%:R%:E * x = x *+ n. Proof. by rewrite mule_natl ednatmulE. Qed. +Lemma dmule_natr x n : x * n%:R%:E = x *+ n. +Proof. by rewrite mule_natr ednatmulE. Qed. + Lemma lee_pdaddl y x z : 0 <= x -> y <= z -> y <= x + z. Proof. by move=> *; rewrite -[y]dadd0e lee_dD. Qed. diff --git a/reals/interval_inference.v b/reals/interval_inference.v deleted file mode 100644 index d3be1c30e..000000000 --- a/reals/interval_inference.v +++ /dev/null @@ -1,1642 +0,0 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) -From HB Require Import structures. -From mathcomp Require Import ssreflect ssrfun ssrbool. -From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint. -From mathcomp Require Import interval. -From mathcomp Require Import mathcomp_extra. - -(* N.B.: This file has been backported in mathcomp-algebra 2.4.0, when -performing changes here, be careful to keep both files reasonnably in -sync during the transition period before we can remove the current -file (i.e. the day we'll require mathcomp >= 2.4.0). *) - -(**md**************************************************************************) -(* # Numbers within an interval *) -(* *) -(* This file develops tools to make the manipulation of numbers within *) -(* a known interval easier, thanks to canonical structures. This adds types *) -(* like {itv R & `[a, b]}, a notation e%:itv that infers an enclosing *) -(* interval for expression e according to existing canonical instances and *) -(* %:num to cast back from type {itv R & i} to R. *) -(* For instance, for x : {i01 R}, we have (1 - x%:num)%:itv : {i01 R} *) -(* automatically inferred. *) -(* *) -(* ## types for values within known interval *) -(* *) -(* ``` *) -(* {itv R & i} == generic type of values in interval i : interval int *) -(* See interval.v for notations that can be used for i. *) -(* R must have a numDomainType structure. This type is shown *) -(* to be a porderType. *) -(* {i01 R} := {itv R & `[0, 1]} *) -(* Allows to solve automatically goals of the form x >= 0 *) -(* and x <= 1 when x is canonically a {i01 R}. *) -(* {i01 R} is canonically stable by common operations. *) -(* {posnum R} := {itv R & `]0, +oo[) *) -(* {nonneg R} := {itv R & `[0, +oo[) *) -(* ``` *) -(* *) -(* ## casts from/to values within known interval *) -(* *) -(* Explicit casts of x to some {itv R & i} according to existing canonical *) -(* instances: *) -(* ``` *) -(* x%:itv == cast to the most precisely known {itv R & i} *) -(* x%:i01 == cast to {i01 R}, or fail *) -(* x%:pos == cast to {posnum R}, or fail *) -(* x%:nng == cast to {nonneg R}, or fail *) -(* ``` *) -(* *) -(* Explicit casts of x from some {itv R & i} to R: *) -(* ``` *) -(* x%:num == cast from {itv R & i} *) -(* x%:posnum == cast from {posnum R} *) -(* x%:nngnum == cast from {nonneg R} *) -(* ``` *) -(* *) -(* ## sign proofs *) -(* *) -(* ``` *) -(* [itv of x] == proof that x is in the interval inferred by x%:itv *) -(* [gt0 of x] == proof that x > 0 *) -(* [lt0 of x] == proof that x < 0 *) -(* [ge0 of x] == proof that x >= 0 *) -(* [le0 of x] == proof that x <= 0 *) -(* [cmp0 of x] == proof that 0 >=< x *) -(* [neq0 of x] == proof that x != 0 *) -(* ``` *) -(* *) -(* ## constructors *) -(* *) -(* ``` *) -(* ItvNum xr lx xu == builds a {itv R & i} from proofs xr : x \in Num.real, *) -(* lx : map_itv_bound (Itv.num_sem R) l <= BLeft x *) -(* xu : BRight x <= map_itv_bound (Itv.num_sem R) u *) -(* where x : R with R : numDomainType *) -(* and l u : itv_bound int *) -(* ItvReal lx xu == builds a {itv R & i} from proofs *) -(* lx : map_itv_bound (Itv.num_sem R) l <= BLeft x *) -(* xu : BRight x <= map_itv_bound (Itv.num_sem R) u *) -(* where x : R with R : realDomainType *) -(* and l u : itv_bound int *) -(* Itv01 x0 x1 == builds a {i01 R} from proofs x0 : 0 <= x and x1 : x <= 1*) -(* where x : R with R : numDomainType *) -(* PosNum x0 == builds a {posnum R} from a proof x0 : x > 0 where x : R *) -(* NngNum x0 == builds a {posnum R} from a proof x0 : x >= 0 where x : R*) -(* ``` *) -(* *) -(* A number of canonical instances are provided for common operations, if *) -(* your favorite operator is missing, look below for examples on how to add *) -(* the appropriate Canonical. *) -(* Also note that all provided instances aren't necessarily optimal, *) -(* improvements welcome! *) -(* Canonical instances are also provided according to types, as a *) -(* fallback when no known operator appears in the expression. Look to top_typ *) -(* below for an example on how to add your favorite type. *) -(* *) -(******************************************************************************) - -Reserved Notation "{ 'itv' R & i }" - (at level 0, R at level 200, i at level 200, format "{ 'itv' R & i }"). -Reserved Notation "{ 'i01' R }" - (at level 0, R at level 200, format "{ 'i01' R }"). -Reserved Notation "{ 'posnum' R }" (at level 0, format "{ 'posnum' R }"). -Reserved Notation "{ 'nonneg' R }" (at level 0, format "{ 'nonneg' R }"). - -Reserved Notation "x %:itv" (at level 2, format "x %:itv"). -Reserved Notation "x %:i01" (at level 2, format "x %:i01"). -Reserved Notation "x %:pos" (at level 2, format "x %:pos"). -Reserved Notation "x %:nng" (at level 2, format "x %:nng"). -Reserved Notation "x %:inum" (at level 2, format "x %:inum"). -Reserved Notation "x %:num" (at level 2, format "x %:num"). -Reserved Notation "x %:posnum" (at level 2, format "x %:posnum"). -Reserved Notation "x %:nngnum" (at level 2, format "x %:nngnum"). - -Reserved Notation "[ 'itv' 'of' x ]" (format "[ 'itv' 'of' x ]"). -Reserved Notation "[ 'gt0' 'of' x ]" (format "[ 'gt0' 'of' x ]"). -Reserved Notation "[ 'lt0' 'of' x ]" (format "[ 'lt0' 'of' x ]"). -Reserved Notation "[ 'ge0' 'of' x ]" (format "[ 'ge0' 'of' x ]"). -Reserved Notation "[ 'le0' 'of' x ]" (format "[ 'le0' 'of' x ]"). -Reserved Notation "[ 'cmp0' 'of' x ]" (format "[ 'cmp0' 'of' x ]"). -Reserved Notation "[ 'neq0' 'of' x ]" (format "[ 'neq0' 'of' x ]"). - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. -Import Order.TTheory Order.Syntax. -Import GRing.Theory Num.Theory. - -Local Open Scope ring_scope. -Local Open Scope order_scope. - -Definition map_itv_bound S T (f : S -> T) (b : itv_bound S) : itv_bound T := - match b with - | BSide b x => BSide b (f x) - | BInfty b => BInfty _ b - end. - -Lemma map_itv_bound_comp S T U (f : T -> S) (g : U -> T) (b : itv_bound U) : - map_itv_bound (f \o g) b = map_itv_bound f (map_itv_bound g b). -Proof. by case: b. Qed. - -Definition map_itv S T (f : S -> T) (i : interval S) : interval T := - let 'Interval l u := i in Interval (map_itv_bound f l) (map_itv_bound f u). - -Lemma map_itv_comp S T U (f : T -> S) (g : U -> T) (i : interval U) : - map_itv (f \o g) i = map_itv f (map_itv g i). -Proof. by case: i => l u /=; rewrite -!map_itv_bound_comp. Qed. - -(* First, the interval arithmetic operations we will later use *) -Module IntItv. -Implicit Types (b : itv_bound int) (i j : interval int). - -Definition opp_bound b := - match b with - | BSide b x => BSide (~~ b) (intZmod.oppz x) - | BInfty b => BInfty _ (~~ b) - end. - -Lemma opp_bound_ge0 b : (BLeft 0%R <= opp_bound b)%O = (b <= BRight 0%R)%O. -Proof. by case: b => [[] b | []//]; rewrite /= !bnd_simp oppr_ge0. Qed. - -Lemma opp_bound_gt0 b : (BRight 0%R <= opp_bound b)%O = (b <= BLeft 0%R)%O. -Proof. -by case: b => [[] b | []//]; rewrite /= !bnd_simp ?oppr_ge0 ?oppr_gt0. -Qed. - -Definition opp i := - let: Interval l u := i in Interval (opp_bound u) (opp_bound l). -Arguments opp /. - -Definition add_boundl b1 b2 := - match b1, b2 with - | BSide b1 x1, BSide b2 x2 => BSide (b1 && b2) (intZmod.addz x1 x2) - | _, _ => BInfty _ true - end. - -Definition add_boundr b1 b2 := - match b1, b2 with - | BSide b1 x1, BSide b2 x2 => BSide (b1 || b2) (intZmod.addz x1 x2) - | _, _ => BInfty _ false - end. - -Definition add i1 i2 := - let: Interval l1 u1 := i1 in let: Interval l2 u2 := i2 in - Interval (add_boundl l1 l2) (add_boundr u1 u2). -Arguments add /. - -Variant signb := EqZero | NonNeg | NonPos. - -Definition sign_boundl b := - let: b0 := BLeft 0%Z in - if b == b0 then EqZero else if (b <= b0)%O then NonPos else NonNeg. - -Definition sign_boundr b := - let: b0 := BRight 0%Z in - if b == b0 then EqZero else if (b <= b0)%O then NonPos else NonNeg. - -Variant signi := Known of signb | Unknown | Empty. - -Definition sign i : signi := - let: Interval l u := i in - match sign_boundl l, sign_boundr u with - | EqZero, NonPos - | NonNeg, EqZero - | NonNeg, NonPos => Empty - | EqZero, EqZero => Known EqZero - | NonPos, EqZero - | NonPos, NonPos => Known NonPos - | EqZero, NonNeg - | NonNeg, NonNeg => Known NonNeg - | NonPos, NonNeg => Unknown - end. - -Definition mul_boundl b1 b2 := - match b1, b2 with - | BInfty _, _ - | _, BInfty _ - | BLeft 0%Z, _ - | _, BLeft 0%Z => BLeft 0%Z - | BSide b1 x1, BSide b2 x2 => BSide (b1 && b2) (intRing.mulz x1 x2) - end. - -Definition mul_boundr b1 b2 := - match b1, b2 with - | BLeft 0%Z, _ - | _, BLeft 0%Z => BLeft 0%Z - | BRight 0%Z, _ - | _, BRight 0%Z => BRight 0%Z - | BSide b1 x1, BSide b2 x2 => BSide (b1 || b2) (intRing.mulz x1 x2) - | _, BInfty _ - | BInfty _, _ => +oo%O - end. - -Lemma mul_boundrC b1 b2 : mul_boundr b1 b2 = mul_boundr b2 b1. -Proof. -by move: b1 b2 => [[] [[|?]|?] | []] [[] [[|?]|?] | []] //=; rewrite mulnC. -Qed. - -Lemma mul_boundr_gt0 b1 b2 : - (BRight 0%Z <= b1 -> BRight 0%Z <= b2 -> BRight 0%Z <= mul_boundr b1 b2)%O. -Proof. -case: b1 b2 => [b1b b1 | []] [b2b b2 | []]//=. -- by case: b1b b2b => -[]; case: b1 b2 => [[|b1] | b1] [[|b2] | b2]. -- by case: b1b b1 => -[[] |]. -- by case: b2b b2 => -[[] |]. -Qed. - -Definition mul i1 i2 := - let: Interval l1 u1 := i1 in let: Interval l2 u2 := i2 in - let: opp := opp_bound in - let: mull := mul_boundl in let: mulr := mul_boundr in - match sign i1, sign i2 with - | Empty, _ | _, Empty => `[1, 0] - | Known EqZero, _ | _, Known EqZero => `[0, 0] - | Known NonNeg, Known NonNeg => - Interval (mull l1 l2) (mulr u1 u2) - | Known NonPos, Known NonPos => - Interval (mull (opp u1) (opp u2)) (mulr (opp l1) (opp l2)) - | Known NonNeg, Known NonPos => - Interval (opp (mulr u1 (opp l2))) (opp (mull l1 (opp u2))) - | Known NonPos, Known NonNeg => - Interval (opp (mulr (opp l1) u2)) (opp (mull (opp u1) l2)) - | Known NonNeg, Unknown => - Interval (opp (mulr u1 (opp l2))) (mulr u1 u2) - | Known NonPos, Unknown => - Interval (opp (mulr (opp l1) u2)) (mulr (opp l1) (opp l2)) - | Unknown, Known NonNeg => - Interval (opp (mulr (opp l1) u2)) (mulr u1 u2) - | Unknown, Known NonPos => - Interval (opp (mulr u1 (opp l2))) (mulr (opp l1) (opp l2)) - | Unknown, Unknown => - Interval - (Order.min (opp (mulr (opp l1) u2)) (opp (mulr u1 (opp l2)))) - (Order.max (mulr (opp l1) (opp l2)) (mulr u1 u2)) - end. -Arguments mul /. - -Definition min i j := - let: Interval li ui := i in let: Interval lj uj := j in - Interval (Order.min li lj) (Order.min ui uj). -Arguments min /. - -Definition max i j := - let: Interval li ui := i in let: Interval lj uj := j in - Interval (Order.max li lj) (Order.max ui uj). -Arguments max /. - -Definition keep_nonneg_bound b := - match b with - | BSide _ (Posz _) => BLeft 0%Z - | BSide _ (Negz _) => -oo%O - | BInfty _ => -oo%O - end. -Arguments keep_nonneg_bound /. - -Definition keep_pos_bound b := - match b with - | BSide b 0%Z => BSide b 0%Z - | BSide _ (Posz (S _)) => BRight 0%Z - | BSide _ (Negz _) => -oo - | BInfty _ => -oo - end. -Arguments keep_pos_bound /. - -Definition keep_nonpos_bound b := - match b with - | BSide _ (Negz _) | BSide _ (Posz 0) => BRight 0%Z - | BSide _ (Posz (S _)) => +oo%O - | BInfty _ => +oo%O - end. -Arguments keep_nonpos_bound /. - -Definition keep_neg_bound b := - match b with - | BSide b 0%Z => BSide b 0%Z - | BSide _ (Negz _) => BLeft 0%Z - | BSide _ (Posz _) => +oo - | BInfty _ => +oo - end. -Arguments keep_neg_bound /. - -Definition inv i := - let: Interval l u := i in - Interval (keep_pos_bound l) (keep_neg_bound u). -Arguments inv /. - -Definition exprn_le1_bound b1 b2 := - if b2 isn't BSide _ 1%Z then +oo - else if (BLeft (-1)%Z <= b1)%O then BRight 1%Z else +oo. -Arguments exprn_le1_bound /. - -Definition exprn i := - let: Interval l u := i in - Interval (keep_pos_bound l) (exprn_le1_bound l u). -Arguments exprn /. - -Definition exprz i1 i2 := - let: Interval l2 _ := i2 in - if l2 is BSide _ (Posz _) then exprn i1 else - let: Interval l u := i1 in - Interval (keep_pos_bound l) +oo. -Arguments exprz /. - -Definition keep_sign i := - let: Interval l u := i in - Interval (keep_nonneg_bound l) (keep_nonpos_bound u). - -(* used in ereal.v *) -Definition keep_nonpos i := - let 'Interval l u := i in - Interval -oo%O (keep_nonpos_bound u). -Arguments keep_nonpos /. - -(* used in ereal.v *) -Definition keep_nonneg i := - let 'Interval l u := i in - Interval (keep_nonneg_bound l) +oo%O. -Arguments keep_nonneg /. - -End IntItv. - -Module Itv. - -Variant t := Top | Real of interval int. - -Definition sub (x y : t) := - match x, y with - | _, Top => true - | Top, Real _ => false - | Real xi, Real yi => subitv xi yi - end. - -Section Itv. -Context T (sem : interval int -> T -> bool). - -Definition spec (i : t) (x : T) := if i is Real i then sem i x else true. - -Record def (i : t) := Def { - r : T; - #[canonical=no] - P : spec i r -}. - -End Itv. - -Record typ i := Typ { - sort : Type; - #[canonical=no] - sort_sem : interval int -> sort -> bool; - #[canonical=no] - allP : forall x : sort, spec sort_sem i x -}. - -Definition mk {T f} i x P : @def T f i := @Def T f i x P. - -Definition from {T f i} {x : @def T f i} (phx : phantom T (r x)) := x. - -Definition fromP {T f i} {x : @def T f i} (phx : phantom T (r x)) := P x. - -Definition num_sem (R : numDomainType) (i : interval int) (x : R) : bool := - (x \in Num.real) && (x \in map_itv intr i). - -Definition nat_sem (i : interval int) (x : nat) : bool := Posz x \in i. - -Definition posnum (R : numDomainType) of phant R := - def (@num_sem R) (Real `]0, +oo[). - -Definition nonneg (R : numDomainType) of phant R := - def (@num_sem R) (Real `[0, +oo[). - -(* a few lifting helper functions *) -Definition real1 (op1 : interval int -> interval int) (x : Itv.t) : Itv.t := - match x with Itv.Top => Itv.Top | Itv.Real x => Itv.Real (op1 x) end. - -Definition real2 (op2 : interval int -> interval int -> interval int) - (x y : Itv.t) : Itv.t := - match x, y with - | Itv.Top, _ | _, Itv.Top => Itv.Top - | Itv.Real x, Itv.Real y => Itv.Real (op2 x y) - end. - -Lemma spec_real1 T f (op1 : T -> T) (op1i : interval int -> interval int) : - forall (x : T), (forall xi, f xi x = true -> f (op1i xi) (op1 x) = true) -> - forall xi, spec f xi x -> spec f (real1 op1i xi) (op1 x). -Proof. by move=> x + [//| xi]; apply. Qed. - -Lemma spec_real2 T f (op2 : T -> T -> T) - (op2i : interval int -> interval int -> interval int) (x y : T) : - (forall xi yi, f xi x = true -> f yi y = true -> - f (op2i xi yi) (op2 x y) = true) -> - forall xi yi, spec f xi x -> spec f yi y -> - spec f (real2 op2i xi yi) (op2 x y). -Proof. by move=> + [//| xi] [//| yi]; apply. Qed. - -Module Exports. -Arguments r {T sem i}. -Notation "{ 'itv' R & i }" := (def (@num_sem R) (Itv.Real i%Z)) : type_scope. -Notation "{ 'i01' R }" := {itv R & `[0, 1]} : type_scope. -Notation "{ 'posnum' R }" := (@posnum _ (Phant R)) : ring_scope. -Notation "{ 'nonneg' R }" := (@nonneg _ (Phant R)) : ring_scope. -Notation "x %:itv" := (from (Phantom _ x)) : ring_scope. -Notation "[ 'itv' 'of' x ]" := (fromP (Phantom _ x)) : ring_scope. -Notation num := r. -Notation "x %:inum" := (r x) (only parsing) : ring_scope. -Notation "x %:num" := (r x) : ring_scope. -Notation "x %:posnum" := (@r _ _ (Real `]0%Z, +oo[) x) : ring_scope. -Notation "x %:nngnum" := (@r _ _ (Real `[0%Z, +oo[) x) : ring_scope. -End Exports. -End Itv. -Export Itv.Exports. - -Local Notation num_spec := (Itv.spec (@Itv.num_sem _)). -Local Notation num_def R := (Itv.def (@Itv.num_sem R)). -Local Notation num_itv_bound R := (@map_itv_bound _ R intr). - -Local Notation nat_spec := (Itv.spec Itv.nat_sem). -Local Notation nat_def := (Itv.def Itv.nat_sem). - -Section POrder. -Context d (T : porderType d) (f : interval int -> T -> bool) (i : Itv.t). -Local Notation itv := (Itv.def f i). -HB.instance Definition _ := [isSub for @Itv.r T f i]. -HB.instance Definition _ : Order.POrder d itv := [POrder of itv by <:]. -End POrder. - -Section Order. -Variables (R : numDomainType) (i : interval int). -Local Notation nR := (num_def R (Itv.Real i)). - -Lemma itv_le_total_subproof : total (<=%O : rel nR). -Proof. -move=> x y; apply: real_comparable. -- by case: x => [x /=/andP[]]. -- by case: y => [y /=/andP[]]. -Qed. - -HB.instance Definition _ := Order.POrder_isTotal.Build ring_display nR - itv_le_total_subproof. - -End Order. - -Module TypInstances. - -Lemma top_typ_spec T f (x : T) : Itv.spec f Itv.Top x. -Proof. by []. Qed. - -Canonical top_typ T f := Itv.Typ (@top_typ_spec T f). - -Lemma real_domain_typ_spec (R : realDomainType) (x : R) : - num_spec (Itv.Real `]-oo, +oo[) x. -Proof. by rewrite /Itv.num_sem/= num_real. Qed. - -Canonical real_domain_typ (R : realDomainType) := - Itv.Typ (@real_domain_typ_spec R). - -Lemma real_field_typ_spec (R : realFieldType) (x : R) : - num_spec (Itv.Real `]-oo, +oo[) x. -Proof. exact: real_domain_typ_spec. Qed. - -Canonical real_field_typ (R : realFieldType) := - Itv.Typ (@real_field_typ_spec R). - -Lemma nat_typ_spec (x : nat) : nat_spec (Itv.Real `[0, +oo[) x. -Proof. by []. Qed. - -Canonical nat_typ := Itv.Typ nat_typ_spec. - -Lemma typ_inum_spec (i : Itv.t) (xt : Itv.typ i) (x : Itv.sort xt) : - Itv.spec (@Itv.sort_sem _ xt) i x. -Proof. by move: xt x => []. Qed. - -(* This adds _ <- Itv.r ( typ_inum ) - to canonical projections (c.f., Print Canonical Projections - Itv.r) meaning that if no other canonical instance (with a - registered head symbol) is found, a canonical instance of - Itv.typ, like the ones above, will be looked for. *) -Canonical typ_inum (i : Itv.t) (xt : Itv.typ i) (x : Itv.sort xt) := - Itv.mk (typ_inum_spec x). - -End TypInstances. -Export (canonicals) TypInstances. - -Class unify {T} f (x y : T) := Unify : f x y = true. -#[export] Hint Mode unify + + + + : typeclass_instances. -Class unify' {T} f (x y : T) := Unify' : f x y = true. -#[export] Instance unify'P {T} f (x y : T) : unify' f x y -> unify f x y := id. -#[export] -Hint Extern 0 (unify' _ _ _) => vm_compute; reflexivity : typeclass_instances. - -Notation unify_itv ix iy := (unify Itv.sub ix iy). - -#[export] Instance top_wider_anything i : unify_itv i Itv.Top. -Proof. by case: i. Qed. - -#[export] Instance real_wider_anyreal i : - unify_itv (Itv.Real i) (Itv.Real `]-oo, +oo[). -Proof. by case: i => [l u]; apply/andP; rewrite !bnd_simp. Qed. - -Section NumDomainTheory. -Context {R : numDomainType} {i : Itv.t}. -Implicit Type x : num_def R i. - -Lemma le_num_itv_bound (x y : itv_bound int) : - (num_itv_bound R x <= num_itv_bound R y)%O = (x <= y)%O. -Proof. -by case: x y => [[] x | x] [[] y | y]//=; rewrite !bnd_simp ?ler_int ?ltr_int. -Qed. - -Lemma num_itv_bound_le_BLeft (x : itv_bound int) (y : int) : - (num_itv_bound R x <= BLeft (y%:~R : R))%O = (x <= BLeft y)%O. -Proof. -rewrite -[BLeft y%:~R]/(map_itv_bound intr (BLeft y)). -by rewrite le_num_itv_bound. -Qed. - -Lemma BRight_le_num_itv_bound (x : int) (y : itv_bound int) : - (BRight (x%:~R : R) <= num_itv_bound R y)%O = (BRight x <= y)%O. -Proof. -rewrite -[BRight x%:~R]/(map_itv_bound intr (BRight x)). -by rewrite le_num_itv_bound. -Qed. - -Lemma num_spec_sub (x y : Itv.t) : Itv.sub x y -> - forall z : R, num_spec x z -> num_spec y z. -Proof. -case: x y => [| x] [| y] //= x_sub_y z /andP[rz]; rewrite /Itv.num_sem rz/=. -move: x y x_sub_y => [lx ux] [ly uy] /andP[lel leu] /=. -move=> /andP[lxz zux]; apply/andP; split. -- by apply: le_trans lxz; rewrite le_num_itv_bound. -- by apply: le_trans zux _; rewrite le_num_itv_bound. -Qed. - -Definition empty_itv := Itv.Real `[1, 0]%Z. - -Lemma bottom x : ~ unify_itv i empty_itv. -Proof. -case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=. -by rewrite in_itv/= => /andP[] /le_trans /[apply]; rewrite ler10. -Qed. - -Lemma gt0 x : unify_itv i (Itv.Real `]0%Z, +oo[) -> 0 < x%:num :> R. -Proof. -case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_]. -by rewrite /= in_itv/= andbT. -Qed. - -Lemma le0F x : unify_itv i (Itv.Real `]0%Z, +oo[) -> x%:num <= 0 :> R = false. -Proof. -case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=. -by rewrite in_itv/= andbT => /lt_geF. -Qed. - -Lemma lt0 x : unify_itv i (Itv.Real `]-oo, 0%Z[) -> x%:num < 0 :> R. -Proof. -by case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=; rewrite in_itv. -Qed. - -Lemma ge0F x : unify_itv i (Itv.Real `]-oo, 0%Z[) -> 0 <= x%:num :> R = false. -Proof. -case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=. -by rewrite in_itv/= => /lt_geF. -Qed. - -Lemma ge0 x : unify_itv i (Itv.Real `[0%Z, +oo[) -> 0 <= x%:num :> R. -Proof. -case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=. -by rewrite in_itv/= andbT. -Qed. - -Lemma lt0F x : unify_itv i (Itv.Real `[0%Z, +oo[) -> x%:num < 0 :> R = false. -Proof. -case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=. -by rewrite in_itv/= andbT => /le_gtF. -Qed. - -Lemma le0 x : unify_itv i (Itv.Real `]-oo, 0%Z]) -> x%:num <= 0 :> R. -Proof. -by case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=; rewrite in_itv. -Qed. - -Lemma gt0F x : unify_itv i (Itv.Real `]-oo, 0%Z]) -> 0 < x%:num :> R = false. -Proof. -case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=. -by rewrite in_itv/= => /le_gtF. -Qed. - -Lemma cmp0 x : unify_itv i (Itv.Real `]-oo, +oo[) -> 0 >=< x%:num. -Proof. by case: i x => [//| i' [x /=/andP[]]]. Qed. - -Lemma neq0 x : - unify (fun ix iy => ~~ Itv.sub ix iy) (Itv.Real `[0%Z, 0%Z]) i -> - x%:num != 0 :> R. -Proof. -case: i x => [//| [l u] [x /= Px]]; apply: contra => /eqP x0 /=. -move: Px; rewrite x0 => /and3P[_ /= l0 u0]; apply/andP; split. -- by case: l l0 => [[] l /= |//]; rewrite !bnd_simp ?lerz0 ?ltrz0. -- by case: u u0 => [[] u /= |//]; rewrite !bnd_simp ?ler0z ?ltr0z. -Qed. - -Lemma eq0F x : - unify (fun ix iy => ~~ Itv.sub ix iy) (Itv.Real `[0%Z, 0%Z]) i -> - x%:num == 0 :> R = false. -Proof. by move=> u; apply/negbTE/neq0. Qed. - -Lemma lt1 x : unify_itv i (Itv.Real `]-oo, 1%Z[) -> x%:num < 1 :> R. -Proof. -by case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=; rewrite in_itv. -Qed. - -Lemma ge1F x : unify_itv i (Itv.Real `]-oo, 1%Z[) -> 1 <= x%:num :> R = false. -Proof. -case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=. -by rewrite in_itv/= => /lt_geF. -Qed. - -Lemma le1 x : unify_itv i (Itv.Real `]-oo, 1%Z]) -> x%:num <= 1 :> R. -Proof. -by case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=; rewrite in_itv. -Qed. - -Lemma gt1F x : unify_itv i (Itv.Real `]-oo, 1%Z]) -> 1 < x%:num :> R = false. -Proof. -case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=. -by rewrite in_itv/= => /le_gtF. -Qed. - -Lemma widen_itv_subproof x i' : Itv.sub i i' -> num_spec i' x%:num. -Proof. by case: x => x /= /[swap] /num_spec_sub; apply. Qed. - -Definition widen_itv x i' (uni : unify_itv i i') := - Itv.mk (widen_itv_subproof x uni). - -Lemma widen_itvE x (uni : unify_itv i i) : @widen_itv x i uni = x. -Proof. exact/val_inj. Qed. - -Lemma posE x (uni : unify_itv i (Itv.Real `]0%Z, +oo[)) : - (widen_itv x%:num%:itv uni)%:num = x%:num. -Proof. by []. Qed. - -Lemma nngE x (uni : unify_itv i (Itv.Real `[0%Z, +oo[)) : - (widen_itv x%:num%:itv uni)%:num = x%:num. -Proof. by []. Qed. - -End NumDomainTheory. - -Arguments bottom {R i} _ {_}. -Arguments gt0 {R i} _ {_}. -Arguments le0F {R i} _ {_}. -Arguments lt0 {R i} _ {_}. -Arguments ge0F {R i} _ {_}. -Arguments ge0 {R i} _ {_}. -Arguments lt0F {R i} _ {_}. -Arguments le0 {R i} _ {_}. -Arguments gt0F {R i} _ {_}. -Arguments cmp0 {R i} _ {_}. -Arguments neq0 {R i} _ {_}. -Arguments eq0F {R i} _ {_}. -Arguments lt1 {R i} _ {_}. -Arguments ge1F {R i} _ {_}. -Arguments le1 {R i} _ {_}. -Arguments gt1F {R i} _ {_}. -Arguments widen_itv {R i} _ {_ _}. -Arguments widen_itvE {R i} _ {_}. -Arguments posE {R i} _ {_}. -Arguments nngE {R i} _ {_}. - -Notation "[ 'gt0' 'of' x ]" := (ltac:(refine (gt0 x%:itv))). -Notation "[ 'lt0' 'of' x ]" := (ltac:(refine (lt0 x%:itv))). -Notation "[ 'ge0' 'of' x ]" := (ltac:(refine (ge0 x%:itv))). -Notation "[ 'le0' 'of' x ]" := (ltac:(refine (le0 x%:itv))). -Notation "[ 'cmp0' 'of' x ]" := (ltac:(refine (cmp0 x%:itv))). -Notation "[ 'neq0' 'of' x ]" := (ltac:(refine (neq0 x%:itv))). - -#[export] Hint Extern 0 (is_true (0%R < _)%R) => solve [apply: gt0] : core. -#[export] Hint Extern 0 (is_true (_ < 0%R)%R) => solve [apply: lt0] : core. -#[export] Hint Extern 0 (is_true (0%R <= _)%R) => solve [apply: ge0] : core. -#[export] Hint Extern 0 (is_true (_ <= 0%R)%R) => solve [apply: le0] : core. -#[export] Hint Extern 0 (is_true (_ \is Num.real)) => solve [apply: cmp0] - : core. -#[export] Hint Extern 0 (is_true (0%R >=< _)%R) => solve [apply: cmp0] : core. -#[export] Hint Extern 0 (is_true (_ != 0%R)) => solve [apply: neq0] : core. -#[export] Hint Extern 0 (is_true (_ < 1%R)%R) => solve [apply: lt1] : core. -#[export] Hint Extern 0 (is_true (_ <= 1%R)%R) => solve [apply: le1] : core. - -Notation "x %:i01" := (widen_itv x%:itv : {i01 _}) (only parsing) : ring_scope. -Notation "x %:i01" := (@widen_itv _ _ - (@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `[0, 1]%Z) _) - (only printing) : ring_scope. -Notation "x %:pos" := (widen_itv x%:itv : {posnum _}) (only parsing) - : ring_scope. -Notation "x %:pos" := (@widen_itv _ _ - (@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `]0%Z, +oo[) _) - (only printing) : ring_scope. -Notation "x %:nng" := (widen_itv x%:itv : {nonneg _}) (only parsing) - : ring_scope. -Notation "x %:nng" := (@widen_itv _ _ - (@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `[0%Z, +oo[) _) - (only printing) : ring_scope. - -Local Open Scope ring_scope. - -Module Instances. - -Import IntItv. - -Section NumDomainInstances. -Context {R : numDomainType}. - -Lemma num_spec_zero : num_spec (Itv.Real `[0, 0]) (0 : R). -Proof. by apply/andP; split; [exact: real0 | rewrite /= in_itv/= lexx]. Qed. - -Canonical zero_inum := Itv.mk num_spec_zero. - -Lemma num_spec_one : num_spec (Itv.Real `[1, 1]) (1 : R). -Proof. by apply/andP; split; [exact: real1 | rewrite /= in_itv/= lexx]. Qed. - -Canonical one_inum := Itv.mk num_spec_one. - -Lemma opp_boundr (x : R) b : - (BRight (- x)%R <= num_itv_bound R (opp_bound b))%O - = (num_itv_bound R b <= BLeft x)%O. -Proof. -by case: b => [[] b | []//]; rewrite /= !bnd_simp mulrNz ?lerN2 // ltrN2. -Qed. - -Lemma opp_boundl (x : R) b : - (num_itv_bound R (opp_bound b) <= BLeft (- x)%R)%O - = (BRight x <= num_itv_bound R b)%O. -Proof. -by case: b => [[] b | []//]; rewrite /= !bnd_simp mulrNz ?lerN2 // ltrN2. -Qed. - -Lemma num_spec_opp (i : Itv.t) (x : num_def R i) (r := Itv.real1 opp i) : - num_spec r (- x%:num). -Proof. -apply: Itv.spec_real1 (Itv.P x). -case: x => x /= _ [l u] /and3P[xr lx xu]. -rewrite /Itv.num_sem/= realN xr/=; apply/andP. -by rewrite opp_boundl opp_boundr. -Qed. - -Canonical opp_inum (i : Itv.t) (x : num_def R i) := Itv.mk (num_spec_opp x). - -Lemma num_itv_add_boundl (x1 x2 : R) b1 b2 : - (num_itv_bound R b1 <= BLeft x1)%O -> (num_itv_bound R b2 <= BLeft x2)%O -> - (num_itv_bound R (add_boundl b1 b2) <= BLeft (x1 + x2)%R)%O. -Proof. -case: b1 b2 => [bb1 b1 |//] [bb2 b2 |//]. -case: bb1; case: bb2; rewrite /= !bnd_simp mulrzDr_tmp. -- exact: lerD. -- exact: ler_ltD. -- exact: ltr_leD. -- exact: ltrD. -Qed. - -Lemma num_itv_add_boundr (x1 x2 : R) b1 b2 : - (BRight x1 <= num_itv_bound R b1)%O -> (BRight x2 <= num_itv_bound R b2)%O -> - (BRight (x1 + x2)%R <= num_itv_bound R (add_boundr b1 b2))%O. -Proof. -case: b1 b2 => [bb1 b1 |//] [bb2 b2 |//]. -case: bb1; case: bb2; rewrite /= !bnd_simp mulrzDr_tmp. -- exact: ltrD. -- exact: ltr_leD. -- exact: ler_ltD. -- exact: lerD. -Qed. - -Lemma num_spec_add (xi yi : Itv.t) (x : num_def R xi) (y : num_def R yi) - (r := Itv.real2 add xi yi) : - num_spec r (x%:num + y%:num). -Proof. -apply: Itv.spec_real2 (Itv.P x) (Itv.P y). -case: x y => [x /= _] [y /= _] => {xi yi r} -[lx ux] [ly uy]/=. -move=> /andP[xr /=/andP[lxx xux]] /andP[yr /=/andP[lyy yuy]]. -rewrite /Itv.num_sem realD//=; apply/andP. -by rewrite num_itv_add_boundl ?num_itv_add_boundr. -Qed. - -Canonical add_inum (xi yi : Itv.t) (x : num_def R xi) (y : num_def R yi) := - Itv.mk (num_spec_add x y). - -Variant sign_spec (l u : itv_bound int) (x : R) : signi -> Set := - | ISignEqZero : l = BLeft 0 -> u = BRight 0 -> x = 0 -> - sign_spec l u x (Known EqZero) - | ISignNonNeg : (BLeft 0%:Z <= l)%O -> (BRight 0%:Z < u)%O -> 0 <= x -> - sign_spec l u x (Known NonNeg) - | ISignNonPos : (l < BLeft 0%:Z)%O -> (u <= BRight 0%:Z)%O -> x <= 0 -> - sign_spec l u x (Known NonPos) - | ISignBoth : (l < BLeft 0%:Z)%O -> (BRight 0%:Z < u)%O -> x \in Num.real -> - sign_spec l u x Unknown. - -Lemma signP (l u : itv_bound int) (x : R) : - (num_itv_bound R l <= BLeft x)%O -> (BRight x <= num_itv_bound R u)%O -> - x \in Num.real -> - sign_spec l u x (sign (Interval l u)). -Proof. -move=> + + xr; rewrite /sign/sign_boundl/sign_boundr. -have [lneg|lpos|->] := ltgtP l; have [uneg|upos|->] := ltgtP u => lx xu. -- apply: ISignNonPos => //; first exact: ltW. - have:= le_trans xu (eqbRL (le_num_itv_bound _ _) (ltW uneg)). - by rewrite bnd_simp. -- exact: ISignBoth. -- exact: ISignNonPos. -- have:= @ltxx _ _ (num_itv_bound R l). - rewrite (le_lt_trans lx) -?leBRight_ltBLeft ?(le_trans xu)//. - by rewrite le_num_itv_bound (le_trans (ltW uneg)). -- apply: ISignNonNeg => //; first exact: ltW. - have:= le_trans (eqbRL (le_num_itv_bound _ _) (ltW lpos)) lx. - by rewrite bnd_simp. -- have:= @ltxx _ _ (num_itv_bound R l). - rewrite (le_lt_trans lx) -?leBRight_ltBLeft ?(le_trans xu)//. - by rewrite le_num_itv_bound ?leBRight_ltBLeft. -- have:= @ltxx _ _ (num_itv_bound R (BLeft 0%Z)). - rewrite (le_lt_trans lx) -?leBRight_ltBLeft ?(le_trans xu)//. - by rewrite le_num_itv_bound -?ltBRight_leBLeft. -- exact: ISignNonNeg. -- apply: ISignEqZero => //. - by apply/le_anti/andP; move: lx xu; rewrite !bnd_simp. -Qed. - -Lemma num_itv_mul_boundl b1 b2 (x1 x2 : R) : - (BLeft 0%:Z <= b1 -> BLeft 0%:Z <= b2 -> - num_itv_bound R b1 <= BLeft x1 -> - num_itv_bound R b2 <= BLeft x2 -> - num_itv_bound R (mul_boundl b1 b2) <= BLeft (x1 * x2))%O. -Proof. -move: b1 b2 => [[] b1 | []//] [[] b2 | []//] /=; rewrite 4!bnd_simp. -- set bl := match b1 with 0%Z => _ | _ => _ end. - have -> : bl = BLeft (b1 * b2). - rewrite {}/bl; move: b1 b2 => [[|p1]|p1] [[|p2]|p2]; congr BLeft. - by rewrite mulr0. - by rewrite bnd_simp intrM -2!(ler0z R); apply: ler_pM. -- case: b1 => [[|b1] | b1]; rewrite !bnd_simp// => b1p b2p sx1 sx2. - + by rewrite mulr_ge0 ?(le_trans _ (ltW sx2)) ?ler0z. - + rewrite intrM (@lt_le_trans _ _ (b1.+1%:~R * x2)) ?ltr_pM2l//. - by rewrite ler_pM2r// (le_lt_trans _ sx2) ?ler0z. -- case: b2 => [[|b2] | b2]; rewrite !bnd_simp// => b1p b2p sx1 sx2. - + by rewrite mulr_ge0 ?(le_trans _ (ltW sx1)) ?ler0z. - + rewrite intrM (@le_lt_trans _ _ (b1%:~R * x2)) ?ler_wpM2l ?ler0z//. - by rewrite ltr_pM2r ?(lt_le_trans _ sx2). -- by rewrite -2!(ler0z R) bnd_simp intrM; apply: ltr_pM. -Qed. - -Lemma num_itv_mul_boundr b1 b2 (x1 x2 : R) : - (0 <= x1 -> 0 <= x2 -> - BRight x1 <= num_itv_bound R b1 -> - BRight x2 <= num_itv_bound R b2 -> - BRight (x1 * x2) <= num_itv_bound R (mul_boundr b1 b2))%O. -Proof. -case: b1 b2 => [b1b b1 | []] [b2b b2 | []] //= x1p x2p; last first. -- case: b2b b2 => -[[|//] | //] _ x20. - + have:= @ltxx _ (itv_bound R) (BLeft 0%:~R). - by rewrite (lt_le_trans _ x20). - + have -> : x2 = 0 by apply/le_anti/andP. - by rewrite mulr0. -- case: b1b b1 => -[[|//] |//] x10 _. - + have:= @ltxx _ (itv_bound R) (BLeft 0%Z%:~R). - by rewrite (lt_le_trans _ x10). - + by have -> : x1 = 0; [apply/le_anti/andP | rewrite mul0r]. -case: b1b b2b => -[]; rewrite -[intRing.mulz]/GRing.mul. -- case: b1 => [[|b1] | b1]; rewrite !bnd_simp => x1b x2b. - + by have:= @ltxx _ R 0; rewrite (le_lt_trans x1p x1b). - + case: b2 x2b => [[| b2] | b2] => x2b; rewrite bnd_simp. - * by have:= @ltxx _ R 0; rewrite (le_lt_trans x2p x2b). - * by rewrite intrM ltr_pM. - * have:= @ltxx _ R 0; rewrite (le_lt_trans x2p)//. - by rewrite (lt_le_trans x2b) ?lerz0. - + have:= @ltxx _ R 0; rewrite (le_lt_trans x1p)//. - by rewrite (lt_le_trans x1b) ?lerz0. -- case: b1 => [[|b1] | b1]; rewrite !bnd_simp => x1b x2b. - + by have:= @ltxx _ R 0; rewrite (le_lt_trans x1p x1b). - + case: b2 x2b => [[| b2] | b2] x2b; rewrite bnd_simp. - * exact: mulr_ge0_le0. - * by rewrite intrM (le_lt_trans (ler_wpM2l x1p x2b)) ?ltr_pM2r. - * have:= @ltxx _ _ x2. - by rewrite (le_lt_trans x2b) ?(lt_le_trans _ x2p) ?ltrz0. - + have:= @ltxx _ _ x1. - by rewrite (lt_le_trans x1b) ?(le_trans _ x1p) ?lerz0. -- case: b1 => [[|b1] | b1]; rewrite !bnd_simp => x1b x2b. - + case: b2 x2b => [[|b2] | b2] x2b; rewrite bnd_simp. - * by have:= @ltxx _ _ x2; rewrite (lt_le_trans x2b). - * by have -> : x1 = 0; [apply/le_anti/andP | rewrite mul0r]. - * have:= @ltxx _ _ x2. - by rewrite (lt_le_trans x2b) ?(le_trans _ x2p) ?lerz0. - + case: b2 x2b => [[|b2] | b2] x2b; rewrite bnd_simp. - * by have:= @ltxx _ _ x2; rewrite (lt_le_trans x2b). - * by rewrite intrM (le_lt_trans (ler_wpM2r x2p x1b)) ?ltr_pM2l. - * have:= @ltxx _ _ x2. - by rewrite (lt_le_trans x2b) ?(le_trans _ x2p) ?lerz0. - + have:= @ltxx _ _ x1. - by rewrite (le_lt_trans x1b) ?(lt_le_trans _ x1p) ?ltrz0. -- case: b1 => [[|b1] | b1]; rewrite !bnd_simp => x1b x2b. - + by have -> : x1 = 0; [apply/le_anti/andP | rewrite mul0r]. - + case: b2 x2b => [[| b2] | b2] x2b; rewrite bnd_simp. - * by have -> : x2 = 0; [apply/le_anti/andP | rewrite mulr0]. - * by rewrite intrM ler_pM. - * have:= @ltxx _ _ x2. - by rewrite (le_lt_trans x2b) ?(lt_le_trans _ x2p) ?ltrz0. - + have:= @ltxx _ _ x1. - by rewrite (le_lt_trans x1b) ?(lt_le_trans _ x1p) ?ltrz0. -Qed. - -Lemma BRight_le_mul_boundr b1 b2 (x1 x2 : R) : - (0 <= x1 -> x2 \in Num.real -> BRight 0%Z <= b2 -> - BRight x1 <= num_itv_bound R b1 -> - BRight x2 <= num_itv_bound R b2 -> - BRight (x1 * x2) <= num_itv_bound R (mul_boundr b1 b2))%O. -Proof. -move=> x1ge0 x2r b2ge0 lex1b1 lex2b2. -have /orP[x2ge0 | x2le0] := x2r; first exact: num_itv_mul_boundr. -have lem0 : (BRight (x1 * x2) <= BRight 0%R)%O. - by rewrite bnd_simp mulr_ge0_le0 // ltW. -apply: le_trans lem0 _. -rewrite -(mulr0z 1) BRight_le_num_itv_bound. -apply: mul_boundr_gt0 => //. -by rewrite -(@BRight_le_num_itv_bound R) (le_trans _ lex1b1). -Qed. - -Lemma comparable_num_itv_bound (x y : itv_bound int) : - (num_itv_bound R x >=< num_itv_bound R y)%O. -Proof. -by case: x y => [[] x | []] [[] y | []]//; apply/orP; - rewrite !bnd_simp ?ler_int ?ltr_int; - case: leP => xy; apply/orP => //; rewrite ltW ?orbT. -Qed. - -Lemma num_itv_bound_min (x y : itv_bound int) : - num_itv_bound R (Order.min x y) - = Order.min (num_itv_bound R x) (num_itv_bound R y). -Proof. -have [lexy | ltyx] := leP x y; [by rewrite !minEle le_num_itv_bound lexy|]. -rewrite minElt -if_neg -comparable_leNgt ?le_num_itv_bound ?ltW//. -exact: comparable_num_itv_bound. -Qed. - -Lemma num_itv_bound_max (x y : itv_bound int) : - num_itv_bound R (Order.max x y) - = Order.max (num_itv_bound R x) (num_itv_bound R y). -Proof. -have [lexy | ltyx] := leP x y; [by rewrite !maxEle le_num_itv_bound lexy|]. -rewrite maxElt -if_neg -comparable_leNgt ?le_num_itv_bound ?ltW//. -exact: comparable_num_itv_bound. -Qed. - -Lemma num_spec_mul (xi yi : Itv.t) (x : num_def R xi) (y : num_def R yi) - (r := Itv.real2 mul xi yi) : - num_spec r (x%:num * y%:num). -Proof. -rewrite {}/r; case: xi yi x y => [//| [xl xu]] [//| [yl yu]]. -case=> [x /=/and3P[xr /= xlx xxu]] [y /=/and3P[yr /= yly yyu]]. -rewrite -/(sign (Interval xl xu)) -/(sign (Interval yl yu)). -have ns000 : @Itv.num_sem R `[0, 0] 0 by apply/and3P. -have xyr : x * y \in Num.real by exact: realM. -case: (signP xlx xxu xr) => xlb xub xs. -- by rewrite xs mul0r; case: (signP yly yyu yr). -- case: (signP yly yyu yr) => ylb yub ys. - + by rewrite ys mulr0. - + apply/and3P; split=> //=. - * exact: num_itv_mul_boundl xlx yly. - * exact: num_itv_mul_boundr xxu yyu. - + apply/and3P; split=> //=; rewrite -[x * y]opprK -mulrN. - * by rewrite opp_boundl num_itv_mul_boundr ?oppr_ge0// opp_boundr. - * by rewrite opp_boundr num_itv_mul_boundl ?opp_boundl// opp_bound_ge0. - + apply/and3P; split=> //=. - * rewrite -[x * y]opprK -mulrN opp_boundl. - by rewrite BRight_le_mul_boundr ?realN ?opp_boundr// opp_bound_gt0 ltW. - * by rewrite BRight_le_mul_boundr// ltW. -- case: (signP yly yyu yr) => ylb yub ys. - + by rewrite ys mulr0. - + apply/and3P; split=> //=; rewrite -[x * y]opprK -mulNr. - * rewrite opp_boundl. - by rewrite num_itv_mul_boundr ?oppr_ge0 ?opp_boundr. - * by rewrite opp_boundr num_itv_mul_boundl ?opp_boundl// opp_bound_ge0. - + apply/and3P; split=> //=; rewrite -mulrNN. - * by rewrite num_itv_mul_boundl ?opp_bound_ge0 ?opp_boundl. - * by rewrite num_itv_mul_boundr ?oppr_ge0 ?opp_boundr. - + apply/and3P; split=> //=; rewrite -[x * y]opprK. - * rewrite -mulNr opp_boundl BRight_le_mul_boundr ?oppr_ge0 ?opp_boundr//. - exact: ltW. - * rewrite opprK -mulrNN. - by rewrite BRight_le_mul_boundr ?opp_boundr - ?oppr_ge0 ?realN ?opp_bound_gt0// ltW. -- case: (signP yly yyu yr) => ylb yub ys. - + by rewrite ys mulr0. - + apply/and3P; split=> //=; rewrite mulrC mul_boundrC. - * rewrite -[y * x]opprK -mulrN opp_boundl. - rewrite BRight_le_mul_boundr ?oppr_ge0 ?realN ?opp_boundr//. - by rewrite opp_bound_gt0 ltW. - * by rewrite BRight_le_mul_boundr// ltW. - + apply/and3P; split=> //=; rewrite mulrC mul_boundrC. - * rewrite -[y * x]opprK -mulNr opp_boundl. - by rewrite BRight_le_mul_boundr ?oppr_ge0 ?opp_boundr// ltW. - * rewrite -mulrNN BRight_le_mul_boundr ?oppr_ge0 ?realN ?opp_boundr//. - by rewrite opp_bound_gt0 ltW. -apply/and3P; rewrite xyr/= num_itv_bound_min num_itv_bound_max. -rewrite (comparable_ge_min _ (comparable_num_itv_bound _ _)). -rewrite (comparable_le_max _ (comparable_num_itv_bound _ _)). -case: (comparable_leP xr) => [x0 | /ltW x0]; split=> //. -- apply/orP; right; rewrite -[x * y]opprK -mulrN opp_boundl. - by rewrite BRight_le_mul_boundr ?realN ?opp_boundr// opp_bound_gt0 ltW. -- by apply/orP; right; rewrite BRight_le_mul_boundr// ltW. -- apply/orP; left; rewrite -[x * y]opprK -mulNr opp_boundl. - by rewrite BRight_le_mul_boundr ?oppr_ge0 ?opp_boundr// ltW. -- apply/orP; left; rewrite -mulrNN. - rewrite BRight_le_mul_boundr ?oppr_ge0 ?realN ?opp_boundr//. - by rewrite opp_bound_gt0 ltW. -Qed. - -Canonical mul_inum (xi yi : Itv.t) (x : num_def R xi) (y : num_def R yi) := - Itv.mk (num_spec_mul x y). - -Lemma num_spec_min (xi yi : Itv.t) (x : num_def R xi) (y : num_def R yi) - (r := Itv.real2 min xi yi) : - num_spec r (Order.min x%:num y%:num). -Proof. -apply: Itv.spec_real2 (Itv.P x) (Itv.P y). -case: x y => [x /= _] [y /= _] => {xi yi r} -[lx ux] [ly uy]/=. -move=> /andP[xr /=/andP[lxx xux]] /andP[yr /=/andP[lyy yuy]]. -apply/and3P; split; rewrite ?min_real//= num_itv_bound_min real_BSide_min//. -- apply: (comparable_le_min2 (comparable_num_itv_bound _ _)) => //. - exact: real_comparable. -- apply: (comparable_le_min2 _ (comparable_num_itv_bound _ _)) => //. - exact: real_comparable. -Qed. - -Lemma num_spec_max (xi yi : Itv.t) (x : num_def R xi) (y : num_def R yi) - (r := Itv.real2 max xi yi) : - num_spec r (Order.max x%:num y%:num). -Proof. -apply: Itv.spec_real2 (Itv.P x) (Itv.P y). -case: x y => [x /= _] [y /= _] => {xi yi r} -[lx ux] [ly uy]/=. -move=> /andP[xr /=/andP[lxx xux]] /andP[yr /=/andP[lyy yuy]]. -apply/and3P; split; rewrite ?max_real//= num_itv_bound_max real_BSide_max//. -- apply: (comparable_le_max2 (comparable_num_itv_bound _ _)) => //. - exact: real_comparable. -- apply: (comparable_le_max2 _ (comparable_num_itv_bound _ _)) => //. - exact: real_comparable. -Qed. - -(* We can't directly put an instance on Order.min for R : numDomainType - since we may want instances for other porderType - (typically \bar R or even nat). So we resort on this additional - canonical structure. *) -Record min_max_typ d := MinMaxTyp { - min_max_sort : porderType d; - #[canonical=no] - min_max_sem : interval int -> min_max_sort -> bool; - #[canonical=no] - min_max_minP : forall (xi yi : Itv.t) (x : Itv.def min_max_sem xi) - (y : Itv.def min_max_sem yi), - let: r := Itv.real2 min xi yi in - Itv.spec min_max_sem r (Order.min x%:num y%:num); - #[canonical=no] - min_max_maxP : forall (xi yi : Itv.t) (x : Itv.def min_max_sem xi) - (y : Itv.def min_max_sem yi), - let: r := Itv.real2 max xi yi in - Itv.spec min_max_sem r (Order.max x%:num y%:num); -}. - -(* The default instances on porderType, for min... *) -Canonical min_typ_inum d (t : min_max_typ d) (xi yi : Itv.t) - (x : Itv.def (@min_max_sem d t) xi) (y : Itv.def (@min_max_sem d t) yi) - (r := Itv.real2 min xi yi) := - Itv.mk (min_max_minP x y). - -(* ...and for max *) -Canonical max_typ_inum d (t : min_max_typ d) (xi yi : Itv.t) - (x : Itv.def (@min_max_sem d t) xi) (y : Itv.def (@min_max_sem d t) yi) - (r := Itv.real2 min xi yi) := - Itv.mk (min_max_maxP x y). - -(* Instance of the above structure for numDomainType *) -Canonical num_min_max_typ := MinMaxTyp num_spec_min num_spec_max. - -Lemma nat_num_spec (i : Itv.t) (n : nat) : nat_spec i n = num_spec i (n%:R : R). -Proof. -case: i => [//| [l u]]; rewrite /= /Itv.num_sem realn/=; congr (_ && _). -- by case: l => [[] l |//]; rewrite !bnd_simp ?pmulrn ?ler_int ?ltr_int. -- by case: u => [[] u |//]; rewrite !bnd_simp ?pmulrn ?ler_int ?ltr_int. -Qed. - -Definition natmul_itv (i1 i2 : Itv.t) : Itv.t := - match i1, i2 with - | Itv.Top, _ => Itv.Top - | _, Itv.Top => Itv.Real `]-oo, +oo[ - | Itv.Real i1, Itv.Real i2 => Itv.Real (mul i1 i2) - end. -Arguments natmul_itv /. - -Lemma num_spec_natmul (xi ni : Itv.t) (x : num_def R xi) (n : nat_def ni) - (r := natmul_itv xi ni) : - num_spec r (x%:num *+ n%:num). -Proof. -rewrite {}/r; case: xi x ni n => [//| xi] x [| ni] n. - by apply/and3P; case: n%:num => [|?]; rewrite ?mulr0n ?realrMn. -have Pn : num_spec (Itv.Real ni) (n%:num%:R : R). - by case: n => /= n; rewrite [Itv.nat_sem ni n](nat_num_spec (Itv.Real ni)). -rewrite -mulr_natr -[n%:num%:R]/((Itv.Def Pn)%:num). -by rewrite (@num_spec_mul (Itv.Real xi) (Itv.Real ni)). -Qed. - -Canonical natmul_inum (xi ni : Itv.t) (x : num_def R xi) (n : nat_def ni) := - Itv.mk (num_spec_natmul x n). - -Lemma num_spec_int (i : Itv.t) (n : int) : - num_spec i n = num_spec i (n%:~R : R). -Proof. -case: i => [//| [l u]]; rewrite /= /Itv.num_sem num_real realz/=. -congr (andb _ _). -- by case: l => [[] l |//]; rewrite !bnd_simp intz ?ler_int ?ltr_int. -- by case: u => [[] u |//]; rewrite !bnd_simp intz ?ler_int ?ltr_int. -Qed. - -Lemma num_spec_intmul (xi ii : Itv.t) (x : num_def R xi) (i : num_def int ii) - (r := natmul_itv xi ii) : - num_spec r (x%:num *~ i%:num). -Proof. -rewrite {}/r; case: xi x ii i => [//| xi] x [| ii] i. - by apply/and3P; case: i%:inum => [[|n] | n]; rewrite ?mulr0z ?realN ?realrMn. -have Pi : num_spec (Itv.Real ii) (i%:num%:~R : R). - by case: i => /= i; rewrite [Itv.num_sem ii i](num_spec_int (Itv.Real ii)). -rewrite -mulrzr -[i%:num%:~R]/((Itv.Def Pi)%:num). -by rewrite (@num_spec_mul (Itv.Real xi) (Itv.Real ii)). -Qed. - -Canonical intmul_inum (xi ni : Itv.t) (x : num_def R xi) (n : num_def int ni) := - Itv.mk (num_spec_intmul x n). - -Lemma num_itv_bound_keep_pos (op : R -> R) (x : R) b : - {homo op : x / 0 <= x} -> {homo op : x / 0 < x} -> - (num_itv_bound R b <= BLeft x)%O -> - (num_itv_bound R (keep_pos_bound b) <= BLeft (op x))%O. -Proof. -case: b => [[] [] [| b] // | []//] hle hlt; rewrite !bnd_simp. -- exact: hle. -- by move=> blex; apply: le_lt_trans (hlt _ _) => //; apply: lt_le_trans blex. -- exact: hlt. -- by move=> bltx; apply: le_lt_trans (hlt _ _) => //; apply: le_lt_trans bltx. -Qed. - -Lemma num_itv_bound_keep_neg (op : R -> R) (x : R) b : - {homo op : x / x <= 0} -> {homo op : x / x < 0} -> - (BRight x <= num_itv_bound R b)%O -> - (BRight (op x) <= num_itv_bound R (keep_neg_bound b))%O. -Proof. -case: b => [[] [[|//] | b] | []//] hge hgt; rewrite !bnd_simp. -- exact: hgt. -- by move=> xltb; apply: hgt; apply: lt_le_trans xltb _; rewrite lerz0. -- exact: hge. -- by move=> xleb; apply: hgt; apply: le_lt_trans xleb _; rewrite ltrz0. -Qed. - -Lemma num_spec_inv (i : Itv.t) (x : num_def R i) (r := Itv.real1 inv i) : - num_spec r (x%:num^-1). -Proof. -apply: Itv.spec_real1 (Itv.P x). -case: x => x /= _ [l u] /and3P[xr /= lx xu]. -rewrite /Itv.num_sem/= realV xr/=; apply/andP; split. -- apply: num_itv_bound_keep_pos lx. - + by move=> ?; rewrite invr_ge0. - + by move=> ?; rewrite invr_gt0. -- apply: num_itv_bound_keep_neg xu. - + by move=> ?; rewrite invr_le0. - + by move=> ?; rewrite invr_lt0. -Qed. - -Canonical inv_inum (i : Itv.t) (x : num_def R i) := Itv.mk (num_spec_inv x). - -Lemma num_itv_bound_exprn_le1 (x : R) n l u : - (num_itv_bound R l <= BLeft x)%O -> - (BRight x <= num_itv_bound R u)%O -> - (BRight (x ^+ n) <= num_itv_bound R (exprn_le1_bound l u))%O. -Proof. -case: u => [bu [[//|[|//]] |//] | []//]. -rewrite /exprn_le1_bound; case: (leP _ l) => [lge1 /= |//] lx xu. -rewrite bnd_simp; case: n => [| n]; rewrite ?expr0//. -have xN1 : -1 <= x. - case: l lge1 lx => [[] l | []//]; rewrite !bnd_simp -(@ler_int R). - - exact: le_trans. - - by move=> + /ltW; apply: le_trans. -have x1 : x <= 1 by case: bu xu; rewrite bnd_simp// => /ltW. -have xr : x \is Num.real by exact: ler1_real. -case: (real_ge0P xr) => x0; first by rewrite expr_le1. -rewrite -[x]opprK exprNn; apply: le_trans (ler_piMl _ _) _. -- by rewrite exprn_ge0 ?oppr_ge0 1?ltW. -- suff: -1 <= (-1) ^+ n.+1 :> R /\ (-1) ^+ n.+1 <= 1 :> R => [[]//|]. - elim: n => [|n [IHn1 IHn2]]; rewrite ?expr1// ![_ ^+ n.+2]exprS !mulN1r. - by rewrite lerNl opprK lerNl. -- by rewrite expr_le1 ?oppr_ge0 1?lerNl// ltW. -Qed. - -Lemma num_spec_exprn (i : Itv.t) (x : num_def R i) n (r := Itv.real1 exprn i) : - num_spec r (x%:num ^+ n). -Proof. -apply: (@Itv.spec_real1 _ _ (fun x => x^+n) _ _ _ _ (Itv.P x)). -case: x => x /= _ [l u] /and3P[xr /= lx xu]. -rewrite /Itv.num_sem realX//=; apply/andP; split. -- apply: (@num_itv_bound_keep_pos (fun x => x^+n)) lx. - + exact: exprn_ge0. - + exact: exprn_gt0. -- exact: num_itv_bound_exprn_le1 lx xu. -Qed. - -Canonical exprn_inum (i : Itv.t) (x : num_def R i) n := - Itv.mk (num_spec_exprn x n). - -Lemma num_spec_exprz (xi ki : Itv.t) (x : num_def R xi) (k : num_def int ki) - (r := Itv.real2 exprz xi ki) : - num_spec r (x%:num ^ k%:num). -Proof. -rewrite {}/r; case: ki k => [|[lk uk]] k; first by case: xi x. -case: xi x => [//|xi x]; rewrite /Itv.real2. -have P : Itv.num_sem - (let 'Interval l _ := xi in Interval (keep_pos_bound l) +oo) - (x%:num ^ k%:num). - case: xi x => lx ux x; apply/and3P; split=> [||//]. - have xr : x%:num \is Num.real by case: x => x /=/andP[]. - by case: k%:num => n; rewrite ?realV realX. - apply: (@num_itv_bound_keep_pos (fun x => x ^ k%:num)); - [exact: exprz_ge0 | exact: exprz_gt0 |]. - by case: x => x /=/and3P[]. -case: lk k P => [slk [lk | lk] | slk] k P; [|exact: P..]. -case: k P => -[k | k] /= => [_ _|]; rewrite -/(exprn xi); last first. - by move=> /and3P[_ /=]; case: slk; rewrite bnd_simp -pmulrn natz. -exact: (@num_spec_exprn (Itv.Real xi)). -Qed. - -Canonical exprz_inum (xi ki : Itv.t) (x : num_def R xi) (k : num_def int ki) := - Itv.mk (num_spec_exprz x k). - -Lemma num_spec_norm {V : normedZmodType R} (x : V) : - num_spec (Itv.Real `[0, +oo[) `|x|. -Proof. by apply/and3P; split; rewrite //= ?normr_real ?bnd_simp ?normr_ge0. Qed. - -Canonical norm_inum {V : normedZmodType R} (x : V) := Itv.mk (num_spec_norm x). - -End NumDomainInstances. - -Section RcfInstances. -Context {R : rcfType}. - -Definition sqrt_itv (i : Itv.t) : Itv.t := - match i with - | Itv.Top => Itv.Real `[0%Z, +oo[ - | Itv.Real (Interval l u) => - match l with - | BSide b 0%Z => Itv.Real (Interval (BSide b 0%Z) +oo) - | BSide b (Posz (S _)) => Itv.Real `]0%Z, +oo[ - | _ => Itv.Real `[0, +oo[ - end - end. -Arguments sqrt_itv /. - -Lemma num_spec_sqrt (i : Itv.t) (x : num_def R i) (r := sqrt_itv i) : - num_spec r (Num.sqrt x%:num). -Proof. -have: Itv.num_sem `[0%Z, +oo[ (Num.sqrt x%:num). - by apply/and3P; rewrite /= num_real !bnd_simp sqrtr_ge0. -rewrite {}/r; case: i x => [//| [[bl [l |//] |//] u]] [x /= +] _. -case: bl l => -[| l] /and3P[xr /= bx _]; apply/and3P; split=> //=; - move: bx; rewrite !bnd_simp ?sqrtr_ge0// sqrtr_gt0; - [exact: lt_le_trans | exact: le_lt_trans..]. -Qed. - -Canonical sqrt_inum (i : Itv.t) (x : num_def R i) := Itv.mk (num_spec_sqrt x). - -End RcfInstances. - -Section NumClosedFieldInstances. -Context {R : numClosedFieldType}. - -Definition sqrtC_itv (i : Itv.t) : Itv.t := - match i with - | Itv.Top => Itv.Top - | Itv.Real (Interval l u) => - match l with - | BSide b (Posz _) => Itv.Real (Interval (BSide b 0%Z) +oo) - | _ => Itv.Top - end - end. -Arguments sqrtC_itv /. - -Lemma num_spec_sqrtC (i : Itv.t) (x : num_def R i) (r := sqrtC_itv i) : - num_spec r (sqrtC x%:num). -Proof. -rewrite {}/r; case: i x => [//| [l u] [x /=/and3P[xr /= lx xu]]]. -case: l lx => [bl [l |//] |[]//] lx; apply/and3P; split=> //=. - by apply: sqrtC_real; case: bl lx => /[!bnd_simp] [|/ltW]; apply: le_trans. -case: bl lx => /[!bnd_simp] lx. -- by rewrite sqrtC_ge0; apply: le_trans lx. -- by rewrite sqrtC_gt0; apply: le_lt_trans lx. -Qed. - -Canonical sqrtC_inum (i : Itv.t) (x : num_def R i) := Itv.mk (num_spec_sqrtC x). - -End NumClosedFieldInstances. - -Section NatInstances. -Local Open Scope nat_scope. -Implicit Type (n : nat). - -Lemma nat_spec_zero : nat_spec (Itv.Real `[0, 0]%Z) 0. Proof. by []. Qed. - -Canonical zeron_inum := Itv.mk nat_spec_zero. - -Lemma nat_spec_add (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) - (r := Itv.real2 add xi yi) : - nat_spec r (x%:num + y%:num). -Proof. -have Px : num_spec xi (x%:num%:R : int). - by case: x => /= x; rewrite (@nat_num_spec int). -have Py : num_spec yi (y%:num%:R : int). - by case: y => /= y; rewrite (@nat_num_spec int). -rewrite (@nat_num_spec int) natrD. -rewrite -[x%:num%:R]/((Itv.Def Px)%:num) -[y%:num%:R]/((Itv.Def Py)%:num). -exact: num_spec_add. -Qed. - -Canonical addn_inum (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) := - Itv.mk (nat_spec_add x y). - -Lemma nat_spec_succ (i : Itv.t) (n : nat_def i) - (r := Itv.real2 add i (Itv.Real `[1, 1]%Z)) : - nat_spec r (S n%:num). -Proof. -pose i1 := Itv.Real `[1, 1]%Z; have P1 : nat_spec i1 1 by []. -by rewrite -addn1 -[1%N]/((Itv.Def P1)%:num); apply: nat_spec_add. -Qed. - -Canonical succn_inum (i : Itv.t) (n : nat_def i) := Itv.mk (nat_spec_succ n). - -Lemma nat_spec_double (i : Itv.t) (n : nat_def i) (r := Itv.real2 add i i) : - nat_spec r (n%:num.*2). -Proof. by rewrite -addnn nat_spec_add. Qed. - -Canonical double_inum (i : Itv.t) (x : nat_def i) := Itv.mk (nat_spec_double x). - -Lemma nat_spec_mul (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) - (r := Itv.real2 mul xi yi) : - nat_spec r (x%:num * y%:num). -Proof. -have Px : num_spec xi (x%:num%:R : int). - by case: x => /= x; rewrite (@nat_num_spec int). -have Py : num_spec yi (y%:num%:R : int). - by case: y => /= y; rewrite (@nat_num_spec int). -rewrite (@nat_num_spec int) natrM. -rewrite -[x%:num%:R]/((Itv.Def Px)%:num) -[y%:num%:R]/((Itv.Def Py)%:num). -exact: num_spec_mul. -Qed. - -Canonical muln_inum (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) := - Itv.mk (nat_spec_mul x y). - -Lemma nat_spec_exp (i : Itv.t) (x : nat_def i) n (r := Itv.real1 exprn i) : - nat_spec r (x%:num ^ n). -Proof. -have Px : num_spec i (x%:num%:R : int). - by case: x => /= x; rewrite (@nat_num_spec int). -rewrite (@nat_num_spec int) natrX -[x%:num%:R]/((Itv.Def Px)%:num). -exact: num_spec_exprn. -Qed. - -Canonical expn_inum (i : Itv.t) (x : nat_def i) n := Itv.mk (nat_spec_exp x n). - -Lemma nat_spec_min (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) - (r := Itv.real2 min xi yi) : - nat_spec r (minn x%:num y%:num). -Proof. -have Px : num_spec xi (x%:num%:R : int). - by case: x => /= x; rewrite (@nat_num_spec int). -have Py : num_spec yi (y%:num%:R : int). - by case: y => /= y; rewrite (@nat_num_spec int). -rewrite (@nat_num_spec int) -minEnat natr_min. -rewrite -[x%:num%:R]/((Itv.Def Px)%:num) -[y%:num%:R]/((Itv.Def Py)%:num). -exact: num_spec_min. -Qed. - -Canonical minn_inum (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) := - Itv.mk (nat_spec_min x y). - -Lemma nat_spec_max (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) - (r := Itv.real2 max xi yi) : - nat_spec r (maxn x%:num y%:num). -Proof. -have Px : num_spec xi (x%:num%:R : int). - by case: x => /= x; rewrite (@nat_num_spec int). -have Py : num_spec yi (y%:num%:R : int). - by case: y => /= y; rewrite (@nat_num_spec int). -rewrite (@nat_num_spec int) -maxEnat natr_max. -rewrite -[x%:num%:R]/((Itv.Def Px)%:num) -[y%:num%:R]/((Itv.Def Py)%:num). -exact: num_spec_max. -Qed. - -Canonical maxn_inum (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) := - Itv.mk (nat_spec_max x y). - -Canonical nat_min_max_typ := MinMaxTyp nat_spec_min nat_spec_max. - -Lemma nat_spec_factorial (n : nat) : nat_spec (Itv.Real `[1%Z, +oo[) n`!. -Proof. by apply/andP; rewrite bnd_simp lez_nat fact_gt0. Qed. - -Canonical factorial_inum n := Itv.mk (nat_spec_factorial n). - -End NatInstances. - -Section IntInstances. - -Lemma num_spec_Posz n : num_spec (Itv.Real `[0, +oo[) (Posz n). -Proof. by apply/and3P; rewrite /= num_real !bnd_simp. Qed. - -Canonical Posz_inum n := Itv.mk (num_spec_Posz n). - -Lemma num_spec_Negz n : num_spec (Itv.Real `]-oo, -1]) (Negz n). -Proof. by apply/and3P; rewrite /= num_real !bnd_simp. Qed. - -Canonical Negz_inum n := Itv.mk (num_spec_Negz n). - -End IntInstances. - -End Instances. -Export (canonicals) Instances. - -Section Morph. -Context {R : numDomainType} {i : Itv.t}. -Local Notation nR := (num_def R i). -Implicit Types x y : nR. -Local Notation num := (@num R (@Itv.num_sem R) i). - -Lemma num_eq : {mono num : x y / x == y}. Proof. by []. Qed. -Lemma num_le : {mono num : x y / (x <= y)%O}. Proof. by []. Qed. -Lemma num_lt : {mono num : x y / (x < y)%O}. Proof. by []. Qed. -Lemma num_min : {morph num : x y / Order.min x y}. -Proof. by move=> x y; rewrite !minEle num_le -fun_if. Qed. -Lemma num_max : {morph num : x y / Order.max x y}. -Proof. by move=> x y; rewrite !maxEle num_le -fun_if. Qed. - -End Morph. - -Section MorphNum. -Context {R : numDomainType}. - -Lemma num_abs_eq0 (a : R) : (`|a|%:nng == 0%:nng) = (a == 0). -Proof. by rewrite -normr_eq0. Qed. - -End MorphNum. - -Section MorphReal. -Context {R : numDomainType} {i : interval int}. -Local Notation nR := (num_def R (Itv.Real i)). -Implicit Type x y : nR. -Local Notation num := (@num R (@Itv.num_sem R) i). - -Lemma num_le_max a x y : - a <= Num.max x%:num y%:num = (a <= x%:num) || (a <= y%:num). -Proof. by rewrite -comparable_le_max// real_comparable. Qed. - -Lemma num_ge_max a x y : - Num.max x%:num y%:num <= a = (x%:num <= a) && (y%:num <= a). -Proof. by rewrite -comparable_ge_max// real_comparable. Qed. - -Lemma num_le_min a x y : - a <= Num.min x%:num y%:num = (a <= x%:num) && (a <= y%:num). -Proof. by rewrite -comparable_le_min// real_comparable. Qed. - -Lemma num_ge_min a x y : - Num.min x%:num y%:num <= a = (x%:num <= a) || (y%:num <= a). -Proof. by rewrite -comparable_ge_min// real_comparable. Qed. - -Lemma num_lt_max a x y : - a < Num.max x%:num y%:num = (a < x%:num) || (a < y%:num). -Proof. by rewrite -comparable_lt_max// real_comparable. Qed. - -Lemma num_gt_max a x y : - Num.max x%:num y%:num < a = (x%:num < a) && (y%:num < a). -Proof. by rewrite -comparable_gt_max// real_comparable. Qed. - -Lemma num_lt_min a x y : - a < Num.min x%:num y%:num = (a < x%:num) && (a < y%:num). -Proof. by rewrite -comparable_lt_min// real_comparable. Qed. - -Lemma num_gt_min a x y : - Num.min x%:num y%:num < a = (x%:num < a) || (y%:num < a). -Proof. by rewrite -comparable_gt_min// real_comparable. Qed. - -End MorphReal. - -Section MorphGe0. -Context {R : numDomainType}. -Local Notation nR := (num_def R (Itv.Real `[0%Z, +oo[)). -Implicit Type x y : nR. -Local Notation num := (@num R (@Itv.num_sem R) (Itv.Real `[0%Z, +oo[)). - -Lemma num_abs_le a x : 0 <= a -> (`|a|%:nng <= x) = (a <= x%:num). -Proof. by move=> a0; rewrite -num_le//= ger0_norm. Qed. - -Lemma num_abs_lt a x : 0 <= a -> (`|a|%:nng < x) = (a < x%:num). -Proof. by move=> a0; rewrite -num_lt/= ger0_norm. Qed. -End MorphGe0. - -Section ItvNum. -Context (R : numDomainType). -Context (x : R) (l u : itv_bound int). -Context (x_real : x \in Num.real). -Context (l_le_x : (num_itv_bound R l <= BLeft x)%O). -Context (x_le_u : (BRight x <= num_itv_bound R u)%O). -Lemma itvnum_subdef : num_spec (Itv.Real (Interval l u)) x. -Proof. by apply/and3P. Qed. -Definition ItvNum : num_def R (Itv.Real (Interval l u)) := Itv.mk itvnum_subdef. -End ItvNum. - -Section ItvReal. -Context (R : realDomainType). -Context (x : R) (l u : itv_bound int). -Context (l_le_x : (num_itv_bound R l <= BLeft x)%O). -Context (x_le_u : (BRight x <= num_itv_bound R u)%O). -Lemma itvreal_subdef : num_spec (Itv.Real (Interval l u)) x. -Proof. by apply/and3P; split; first exact: num_real. Qed. -Definition ItvReal : num_def R (Itv.Real (Interval l u)) := - Itv.mk itvreal_subdef. -End ItvReal. - -Section Itv01. -Context (R : numDomainType). -Context (x : R) (x_ge0 : 0 <= x) (x_le1 : x <= 1). -Lemma itv01_subdef : num_spec (Itv.Real `[0%Z, 1%Z]) x. -Proof. by apply/and3P; split; rewrite ?bnd_simp// ger0_real. Qed. -Definition Itv01 : num_def R (Itv.Real `[0%Z, 1%Z]) := Itv.mk itv01_subdef. -End Itv01. - -Section Posnum. -Context (R : numDomainType) (x : R) (x_gt0 : 0 < x). -Lemma posnum_subdef : num_spec (Itv.Real `]0, +oo[) x. -Proof. by apply/and3P; rewrite /= gtr0_real. Qed. -Definition PosNum : {posnum R} := Itv.mk posnum_subdef. -End Posnum. - -Section Nngnum. -Context (R : numDomainType) (x : R) (x_ge0 : 0 <= x). -Lemma nngnum_subdef : num_spec (Itv.Real `[0, +oo[) x. -Proof. by apply/and3P; rewrite /= ger0_real. Qed. -Definition NngNum : {nonneg R} := Itv.mk nngnum_subdef. -End Nngnum. - -Variant posnum_spec (R : numDomainType) (x : R) : - R -> bool -> bool -> bool -> Type := -| IsPosnum (p : {posnum R}) : posnum_spec x (p%:num) false true true. - -Lemma posnumP (R : numDomainType) (x : R) : 0 < x -> - posnum_spec x x (x == 0) (0 <= x) (0 < x). -Proof. -move=> x_gt0; case: real_ltgt0P (x_gt0) => []; rewrite ?gtr0_real // => _ _. -by rewrite -[x]/(PosNum x_gt0)%:num; constructor. -Qed. - -Variant nonneg_spec (R : numDomainType) (x : R) : R -> bool -> Type := -| IsNonneg (p : {nonneg R}) : nonneg_spec x (p%:num) true. - -Lemma nonnegP (R : numDomainType) (x : R) : 0 <= x -> nonneg_spec x x (0 <= x). -Proof. by move=> xge0; rewrite xge0 -[x]/(NngNum xge0)%:num; constructor. Qed. - -Section Test1. - -Variable R : numDomainType. -Variable x : {i01 R}. - -Goal 0%:i01 = 1%:i01 :> {i01 R}. -Proof. -Abort. - -Goal (- x%:num)%:itv = (- x%:num)%:itv :> {itv R & `[-1, 0]}. -Proof. -Abort. - -Goal (1 - x%:num)%:i01 = x. -Proof. -Abort. - -End Test1. - -Section Test2. - -Variable R : realDomainType. -Variable x y : {i01 R}. - -Goal (x%:num * y%:num)%:i01 = x%:num%:i01. -Proof. -Abort. - -End Test2. - -Module Test3. -Section Test3. -Variable R : realDomainType. - -Definition s_of_pq (p q : {i01 R}) : {i01 R} := - (1 - ((1 - p%:num)%:i01%:num * (1 - q%:num)%:i01%:num))%:i01. - -Lemma s_of_p0 (p : {i01 R}) : s_of_pq p 0%:i01 = p. -Proof. by apply/val_inj; rewrite /= subr0 mulr1 subKr. Qed. - -End Test3. -End Test3. diff --git a/reals/reals.v b/reals/reals.v index a400ee645..87f3f09b8 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -507,7 +507,7 @@ Lemma Rfloor0 : Rfloor 0 = 0 :> R. Proof. by rewrite /Rfloor floor0. Qed. Lemma Rfloor1 : Rfloor 1 = 1 :> R. Proof. by rewrite /Rfloor floor1. Qed. Lemma le_Rfloor : {homo (@Rfloor R) : x y / x <= y}. -Proof. by move=> x y /Num.Theory.floor_le; rewrite ler_int. Qed. +Proof. by move=> x y /Num.Theory.le_floor; rewrite ler_int. Qed. Lemma Rfloor_ge_int x (n : int) : (n%:~R <= x)= (n%:~R <= Rfloor x). Proof. by rewrite ler_int floor_ge_int. Qed. @@ -541,20 +541,20 @@ Lemma Rceil0 : Rceil 0 = 0 :> R. Proof. by rewrite /Rceil ceil0. Qed. Lemma Rceil_ge x : x <= Rceil x. -Proof. by rewrite Num.Theory.le_ceil ?num_real. Qed. +Proof. by rewrite Num.Theory.ceil_ge ?num_real. Qed. Lemma le_Rceil : {homo (@Rceil R) : x y / x <= y}. -Proof. by move=> x y ?; rewrite /Rceil ler_int ceil_le. Qed. +Proof. by move=> x y ?; rewrite /Rceil ler_int le_ceil_tmp. Qed. Lemma Rceil_ge0 x : 0 <= x -> 0 <= Rceil x. -Proof. by move=> x0; rewrite /Rceil ler0z -(ceil0 R) ceil_le. Qed. +Proof. by move=> x0; rewrite /Rceil ler0z -(ceil0 R) le_ceil_tmp. Qed. Lemma RceilE x : Rceil x = (ceil x)%:~R. Proof. by []. Qed. #[deprecated(since="mathcomp-analysis 1.3.0", note="use `Num.Theory.ceil_le` instead")] Lemma le_ceil : {homo @Num.ceil R : x y / x <= y}. -Proof. exact: ceil_le. Qed. +Proof. exact: le_ceil_tmp. Qed. End CeilTheory. diff --git a/theories/charge.v b/theories/charge.v index 32fd4a16b..5ba168c01 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. From mathcomp Require Import finmap fingroup perm rat. @@ -711,7 +711,7 @@ rewrite setD0 => A0D. have [v [v0 Pv]] : {v : nat -> elt_type | v 0%N = exist _ (A0, d_ set0, A0) (And4 mA0 A0D (d_ge0 set0) A0d0) /\ forall n, elt_rel (v n) (v n.+1)}. - apply: dependent_choice_Type => -[[[A' ?] U] [/= mA' A'D]]. + apply: dependent_choice => -[[[A' ?] U] [/= mA' A'D]]. have [A1 [mA1 A1DU A1t1]] := next_elt U. have A1D : A1 `<=` D by apply: (subset_trans A1DU); apply: subDsetl. by exists (exist _ (A1, d_ U, U `|` A1) (And4 mA1 A1D (d_ge0 U) A1t1)). @@ -836,7 +836,7 @@ have [A0 [_ negA0 A0s0]] := next_elt set0. have [v [v0 Pv]] : {v | v 0%N = exist _ (A0, s_ set0, A0) (And3 (s_le0 set0) negA0 A0s0) /\ forall n, elt_rel (v n) (v n.+1)}. - apply: dependent_choice_Type => -[[[A s] U] [/= s_le0' nsA]]. + apply: dependent_choice => -[[[A s] U] [/= s_le0' nsA]]. have [A' [? nsA' A's'] ] := next_elt U. by exists (exist _ (A', s_ U, U `|` A') (And3 (s_le0 U) nsA' A's')). have Ubig n : U_ (v n) = \big[setU/set0]_(i < n.+1) A_ (v i). diff --git a/theories/exp.v b/theories/exp.v index e8b017da2..9deebb3f5 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -1170,8 +1170,8 @@ Proof. by case=> //=[x|]; rewrite ?lexx// leNgt expR_gt0/= expRK. Qed. Lemma lneK : {in `[0, +oo], cancel lne (@expeR R)}. Proof. -move=> [r|//|//]; rewrite in_itv => //= /andP[]; rewrite lee_fin. -by rewrite le_eqVlt => /predU1P[<- _|r0 _]; rewrite ?lexx// leNgt r0/= lnK. +case=> [r|//|//] /[!in_itv]/=/andP[]; rewrite le_eqVlt eqe lte_fin. +by move=> /predU1P[<- _|r0 _]; rewrite ?lexx// leNgt r0/= lnK. Qed. Lemma lneK_eq x : (expeR (lne x) == x) = (0 <= x). diff --git a/theories/ftc.v b/theories/ftc.v index 4abdd3a67..980be4bbc 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -99,7 +99,7 @@ apply: cvg_at_right_left_dnbhs. by rewrite -EFinD addrAC subrr add0r. have nice_E y : nicely_shrinking y (E y). split=> [n|]; first exact: measurable_itv. - exists (2, fun n => PosNum (d_gt0 n)); split => //= [n z|n]. + exists (2%R, fun n => PosNum (d_gt0 n)); split => //= [n z|n]. rewrite /E/= in_itv/= /ball/= ltr_distlC => /andP[yz ->]. by rewrite (lt_le_trans _ yz)// ltrBlDr ltrDl. rewrite (lebesgue_measure_ball _ (ltW _))// -/mu muE -EFinM lee_fin. @@ -153,7 +153,7 @@ apply: cvg_at_right_left_dnbhs. by rewrite ltrDl Nd_gt0 -EFinD opprD addrA subrr add0r. have nice_E y : nicely_shrinking y (E y). split=> [n|]; first exact: measurable_itv. - exists (2, (fun n => PosNum (Nd_gt0 n))); split => //=. + exists (2%R, (fun n => PosNum (Nd_gt0 n))); split => //=. by rewrite -oppr0; exact: cvgN. move=> n z. rewrite /E/= in_itv/= /ball/= => /andP[yz zy]. @@ -348,7 +348,7 @@ Proof. by move=> xu locf F ax fx; exact: (@continuous_FTC1 _ _ _ u). Qed. End FTC. Definition parameterized_integral {R : realType} - (mu : {measure set (g_sigma_algebraType (R.-ocitv.-measurable)) -> \bar R}) + (mu : {measure set (measurableTypeR R) -> \bar R}) a x (f : R -> R) : R := (\int[mu]_(t in `[a, x]) f t)%R. diff --git a/theories/function_spaces.v b/theories/function_spaces.v index 8be463b53..de70ede40 100644 --- a/theories/function_spaces.v +++ b/theories/function_spaces.v @@ -1557,6 +1557,43 @@ End cartesian_closed. End currying. +Section big_continuous. +Context {U : topologicalType} {I : Type}. +Variables (op : U -> U -> U) (x0 : U) (P : pred I). +Hypothesis cont_op : continuous (fun x : U * U => op x.1 x.2). + +Lemma cvg_big {T : Type} (F : set_system T) (r : seq I) + (Ff : I -> T -> U) (Fa : I -> U) : + Filter F -> + (forall i, P i -> Ff i x @[x --> F] --> Fa i) -> + \big[op/x0]_(i <- r | P i) (Ff i x) @[x --> F] --> + \big[op/x0]_(i <- r | P i) Fa i. +Proof. +move=> FF cvg_f. +elim: r => [|i r IHr]. + rewrite big_nil. + under eq_cvg do rewrite big_nil. + exact: cvg_cst. +rewrite big_cons. +under eq_cvg do rewrite big_cons. +case: ifPn => // Pi. +apply: (@cvg_comp _ _ _ + (fun x1 => (Ff i x1, \big[op/x0]_(j <- r | P j) Ff j x1)) _ _ + (nbhs (Fa i, \big[op/x0]_(j <- r | P j) Fa j)) _ _ + (continuous_curry_cvg cont_op)). +by apply: cvg_pair => //; exact: cvg_f. +Qed. + +Lemma continuous_big {T : topologicalType} (r : seq I) + (F : I -> T -> U) : + (forall i, P i -> continuous (F i)) -> + continuous (fun x => \big[op/x0]_(i <- r | P i) F i x). +Proof. +by move=> F_cont x; apply: cvg_big => // i /F_cont; exact. +Qed. + +End big_continuous. + Definition eval {X Y : topologicalType} : continuousType X Y * X -> Y := uncurry (id : continuousType X Y -> (X -> Y)). diff --git a/theories/kernel.v b/theories/kernel.v index 4d16d61f4..1be2e0d1e 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -1189,18 +1189,14 @@ Let integral_kcomp_nnsfun x (f : {nnsfun Z >-> R}) : Proof. under [in LHS]eq_integral do rewrite fimfunE -fsumEFin//. rewrite ge0_integral_fsum//; last 2 first. - - move=> r; apply/measurable_EFinP/measurableT_comp => [//|]. - have fr : measurable (f @^-1` [set r]) by exact/measurable_sfunP. - by rewrite (_ : \1__ = mindic R fr). + - by move=> r; exact/measurable_EFinP/measurableT_comp. - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0. under [in RHS]eq_integral. move=> y _. under eq_integral. by move=> z _; rewrite fimfunE -fsumEFin//; over. rewrite /= ge0_integral_fsum//; last 2 first. - - move=> r; apply/measurable_EFinP/measurableT_comp => [//|]. - have fr : measurable (f @^-1` [set r]) by exact/measurable_sfunP. - by rewrite (_ : \1__ = mindic R fr). + - by move=> r; exact/measurable_EFinP/measurableT_comp. - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0. under eq_fsbigr. move=> r _. @@ -1218,15 +1214,14 @@ rewrite /= ge0_integral_fsum//; last 2 first. apply: eq_fsbigr => r _. rewrite (integralZl_indic _ (fun r => f @^-1` [set r]))//; last first. exact: preimage_nnfun0. -rewrite /= integral_kcomp_indic; last exact/measurable_sfunP. +rewrite /= integral_kcomp_indic//. have [r0|r0] := leP 0%R r. - rewrite ge0_integralZl//; last first. - exact: measurableT_comp (measurable_kernel k (f @^-1` [set r]) _) _. - by under eq_integral do rewrite integral_indic// setIT. -rewrite integral0_eq ?mule0; last first. - move=> y _; rewrite integral0_eq// => z _. - by rewrite preimage_nnfun0// indic0. -by rewrite integral0_eq// => y _; rewrite preimage_nnfun0// measure0 mule0. + rewrite ge0_integralZl//. + by under eq_integral do rewrite integral_indic// setIT. + exact: measurableT_comp (measurable_kernel k (f @^-1` [set r]) _) _. +rewrite integral0_eq ?mule0. + by rewrite integral0_eq// => y _; rewrite preimage_nnfun0// measure0 mule0. +by move=> y _; rewrite integral0_eq// => z _; rewrite preimage_nnfun0// indic0. Qed. (* [Lemma 3, Staton 2017 ESOP] (4/4) *) @@ -1671,7 +1666,7 @@ HB.instance Definition _ := Let measure_uub : measure_fam_uub kernel_snd. Proof. -exists 2 => /= -[x y]. +exists 2%R => /= -[x y]. rewrite /kernel_snd/= (@le_lt_trans _ _ 1%:E) ?lte1n//. exact: sprob_kernel_le1. Qed. diff --git a/theories/landau.v b/theories/landau.v index 4e0ad17b9..1be397623 100644 --- a/theories/landau.v +++ b/theories/landau.v @@ -390,6 +390,11 @@ Lemma littleoE (tag : unit) (F : filter_on T) littleo_def F f h -> the_littleo tag F phF f h = f. Proof. by move=> /asboolP?; rewrite /the_littleo /insubd insubT. Qed. +Lemma littleoE0 (tag : unit) (F : filter_on T) + (phF : phantom (set (set T)) F) f h : + ~ littleo_def F f h -> the_littleo tag F phF f h = 0. +Proof. by move=> ?; rewrite /the_littleo /insubd insubN//; apply/asboolP. Qed. + Canonical the_littleo_littleo (tag : unit) (F : filter_on T) (phF : phantom (set_system T) F) f h := [littleo of the_littleo tag F phF f h]. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v index ce39a6310..b773c0c99 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v @@ -248,7 +248,7 @@ rewrite /fleg [X in _ X](_ : _ = \big[setU/set0]_(y <- fset_set (range f)) \big[setU/set0]_(x <- fset_set (range (g n)) | c * y <= x) (f @^-1` [set y] `&` (g n @^-1` [set x]))). apply: bigsetU_measurable => r _; apply: bigsetU_measurable => r' crr'. - exact/measurableI/measurable_sfunP. + exact/measurableI. rewrite predeqE => t; split => [/= cfgn|]. - rewrite -bigcup_seq; exists (f t); first by rewrite /= in_fset_set//= mem_set. rewrite -bigcup_seq_cond; exists (g n t) => //=. diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index 08d726dba..4aaae4456 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/theories/lebesgue_integral_theory/simple_functions.v @@ -29,15 +29,8 @@ From mathcomp Require Import function_spaces. (* *) (* Detailed contents: *) (* ```` *) -(* {mfun aT >-> rT} == type of measurable functions *) -(* aT and rT are sigmaRingType's. *) (* {sfun T >-> R} == type of simple functions *) -(* f \in mfun == holds for f : {mfun _ >-> _} *) (* {nnsfun T >-> R} == type of non-negative simple functions *) -(* mindic mD := \1_D where mD is a proof that D is measurable *) -(* indic_mfun mD := mindic mD *) -(* scale_mfun k f := k \o* f *) -(* max_mfun f g := f \max g *) (* indic_sfun mD := mindic _ mD *) (* cst_sfun r == constant simple function *) (* max_sfun f g := f \max f *) @@ -55,10 +48,6 @@ From mathcomp Require Import function_spaces. (* *) (******************************************************************************) -Reserved Notation "{ 'mfun' aT >-> T }" - (at level 0, format "{ 'mfun' aT >-> T }"). -Reserved Notation "[ 'mfun' 'of' f ]" - (at level 0, format "[ 'mfun' 'of' f ]"). Reserved Notation "{ 'nnfun' aT >-> T }" (at level 0, format "{ 'nnfun' aT >-> T }"). Reserved Notation "[ 'nnfun' 'of' f ]" @@ -81,31 +70,6 @@ Import numFieldNormedType.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -#[global] -Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core. - -HB.mixin Record isMeasurableFun d d' (aT : sigmaRingType d) (rT : sigmaRingType d') - (f : aT -> rT) := { - measurable_funPT : measurable_fun [set: aT] f -}. -HB.structure Definition MeasurableFun d d' aT rT := - {f of @isMeasurableFun d d' aT rT f}. -Arguments measurable_funPT {d d' aT rT} s. - -Notation "{ 'mfun' aT >-> T }" := (@MeasurableFun.type _ _ aT T) : form_scope. -Notation "[ 'mfun' 'of' f ]" := [the {mfun _ >-> _} of f] : form_scope. -#[global] Hint Extern 0 (measurable_fun [set: _] _) => - solve [apply: measurable_funPT] : core. - -Lemma measurable_funP {d d' : measure_display} - {aT : measurableType d} {rT : sigmaRingType d'} - (D : set aT) (s : {mfun aT >-> rT}) : measurable_fun D s. -Proof. -move=> mD Y mY; apply: measurableI => //. -by rewrite -(setTI (_ @^-1` _)); exact: measurable_funPT. -Qed. -Arguments measurable_funP {d d' aT rT D} s. - Module HBSimple. HB.structure Definition SimpleFun d (aT : sigmaRingType d) (rT : realType) := @@ -116,10 +80,6 @@ End HBSimple. Notation "{ 'sfun' aT >-> T }" := (@HBSimple.SimpleFun.type _ aT T) : form_scope. Notation "[ 'sfun' 'of' f ]" := [the {sfun _ >-> _} of f] : form_scope. -Lemma measurable_sfunP {d d'} {aT : measurableType d} {rT : measurableType d'} - (f : {mfun aT >-> rT}) (Y : set rT) : measurable Y -> measurable (f @^-1` Y). -Proof. by move=> mY; rewrite -[f @^-1` _]setTI; exact: measurable_funP. Qed. - Module HBNNSimple. Import HBSimple. @@ -132,137 +92,6 @@ End HBNNSimple. Notation "{ 'nnsfun' aT >-> T }" := (@HBNNSimple.NonNegSimpleFun.type _ aT%type T) : form_scope. Notation "[ 'nnsfun' 'of' f ]" := [the {nnsfun _ >-> _} of f] : form_scope. -Section mfun_pred. -Context {d d'} {aT : sigmaRingType d} {rT : sigmaRingType d'}. -Definition mfun : {pred aT -> rT} := mem [set f | measurable_fun setT f]. -Definition mfun_key : pred_key mfun. Proof. exact. Qed. -Canonical mfun_keyed := KeyedPred mfun_key. -End mfun_pred. - -Section mfun. -Context {d d'} {aT : sigmaRingType d} {rT : sigmaRingType d'}. -Notation T := {mfun aT >-> rT}. -Notation mfun := (@mfun _ _ aT rT). - -Section Sub. -Context (f : aT -> rT) (fP : f \in mfun). -Definition mfun_Sub_subproof := @isMeasurableFun.Build d _ aT rT f (set_mem fP). -#[local] HB.instance Definition _ := mfun_Sub_subproof. -Definition mfun_Sub := [mfun of f]. -End Sub. - -Lemma mfun_rect (K : T -> Type) : - (forall f (Pf : f \in mfun), K (mfun_Sub Pf)) -> forall u : T, K u. -Proof. -move=> Ksub [f [[Pf]]]/=. -by suff -> : Pf = (set_mem (@mem_set _ [set f | _] f Pf)) by apply: Ksub. -Qed. - -Lemma mfun_valP f (Pf : f \in mfun) : mfun_Sub Pf = f :> (_ -> _). -Proof. by []. Qed. - -HB.instance Definition _ := isSub.Build _ _ T mfun_rect mfun_valP. - -Lemma mfuneqP (f g : {mfun aT >-> rT}) : f = g <-> f =1 g. -Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed. - -HB.instance Definition _ := [Choice of {mfun aT >-> rT} by <:]. - -HB.instance Definition _ x := isMeasurableFun.Build d _ aT rT (cst x) - (@measurable_cst _ _ aT rT setT x). - -End mfun. - -Section mfun_realType. -Context {rT : realType}. - -HB.instance Definition _ := @isMeasurableFun.Build _ _ _ rT - (@normr rT rT) (@normr_measurable rT setT). - -HB.instance Definition _ := - isMeasurableFun.Build _ _ _ _ (@expR rT) (@measurable_expR rT). - -End mfun_realType. - -Section mfun_measurableType. -Context {d1} {T1 : measurableType d1} {d2} {T2 : measurableType d2} - {d3} {T3 : measurableType d3}. -Variables (f : {mfun T2 >-> T3}) (g : {mfun T1 >-> T2}). - -Lemma measurableT_comp_subproof : measurable_fun setT (f \o g). -Proof. exact: measurableT_comp. Qed. - -HB.instance Definition _ := isMeasurableFun.Build _ _ _ _ (f \o g) - measurableT_comp_subproof. - -End mfun_measurableType. - -Section ring. -Context d (aT : measurableType d) (rT : realType). - -Lemma mfun_subring_closed : subring_closed (@mfun _ _ aT rT). -Proof. -split=> [|f g|f g]; rewrite !inE/=. -- exact: measurable_cst. -- exact: measurable_funB. -- exact: measurable_funM. -Qed. -HB.instance Definition _ := GRing.isSubringClosed.Build _ - (@mfun d default_measure_display aT rT) mfun_subring_closed. -HB.instance Definition _ := [SubChoice_isSubComRing of {mfun aT >-> rT} by <:]. - -Implicit Types (f g : {mfun aT >-> rT}). - -Lemma mfun0 : (0 : {mfun aT >-> rT}) =1 cst 0 :> (_ -> _). Proof. by []. Qed. -Lemma mfun1 : (1 : {mfun aT >-> rT}) =1 cst 1 :> (_ -> _). Proof. by []. Qed. -Lemma mfunN f : - f = \- f :> (_ -> _). Proof. by []. Qed. -Lemma mfunD f g : f + g = f \+ g :> (_ -> _). Proof. by []. Qed. -Lemma mfunB f g : f - g = f \- g :> (_ -> _). Proof. by []. Qed. -Lemma mfunM f g : f * g = f \* g :> (_ -> _). Proof. by []. Qed. -Lemma mfunMn f n : (f *+ n) = (fun x => f x *+ n) :> (_ -> _). -Proof. by apply/funext=> x; elim: n => //= n; rewrite !mulrS !mfunD /= => ->. Qed. -Lemma mfun_sum I r (P : {pred I}) (f : I -> {mfun aT >-> rT}) (x : aT) : - (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. -Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. -Lemma mfun_prod I r (P : {pred I}) (f : I -> {mfun aT >-> rT}) (x : aT) : - (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. -Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. -Lemma mfunX f n : f ^+ n = (fun x => f x ^+ n) :> (_ -> _). -Proof. by apply/funext=> x; elim: n => [|n IHn]//; rewrite !exprS mfunM/= IHn. Qed. - -HB.instance Definition _ f g := MeasurableFun.copy (f \+ g) (f + g). -HB.instance Definition _ f g := MeasurableFun.copy (\- f) (- f). -HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g). -HB.instance Definition _ f g := MeasurableFun.copy (f \* g) (f * g). - -Definition mindic (D : set aT) of measurable D : aT -> rT := \1_D. - -Lemma mindicE (D : set aT) (mD : measurable D) : - mindic mD = (fun x => (x \in D)%:R). -Proof. by rewrite /mindic funeqE => t; rewrite indicE. Qed. - -HB.instance Definition _ D mD := @isMeasurableFun.Build _ _ aT rT (mindic mD) - (@measurable_indic _ aT rT setT D mD). - -Definition indic_mfun (D : set aT) (mD : measurable D) : {mfun aT >-> rT} := - mindic mD. - -HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst k). -Definition scale_mfun k f : {mfun aT >-> rT} := k \o* f. - -Lemma max_mfun_subproof f g : @isMeasurableFun d _ aT rT (f \max g). -Proof. by split; apply: measurable_maxr. Qed. - -HB.instance Definition _ f g := max_mfun_subproof f g. - -Definition max_mfun f g : {mfun aT >-> _} := f \max g. - -End ring. -Arguments indic_mfun {d aT rT} _. -(* TODO: move earlier?*) -#[global] Hint Extern 0 (measurable_fun _ (\1__ : _ -> _)) => - (exact: measurable_indic ) : core. - Section sfun_pred. Context {d} {aT : sigmaRingType d} {rT : realType}. Definition sfun : {pred _ -> _} := [predI @mfun _ _ aT rT & fimfun]. @@ -311,7 +140,7 @@ Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed. HB.instance Definition _ := [Choice of {sfun aT >-> rT} by <:]. -(* NB: already instantiated in cardinality.v *) +(* NB: already in cardinality.v *) HB.instance Definition _ x : @FImFun aT rT (cst x) := FImFun.on (cst x). Definition cst_sfun x : {sfun aT >-> rT} := cst x. @@ -371,16 +200,17 @@ HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g). HB.instance Definition _ f g := MeasurableFun.copy (f \* g) (f * g). Import HBSimple. -(* NB: already instantiated in lebesgue_integral.v *) + +(* TODO: mv to `measurable_realfun.v`? *) HB.instance Definition _ (D : set aT) (mD : measurable D) : @FImFun aT rT (mindic _ mD) := FImFun.on (mindic _ mD). - Definition indic_sfun (D : set aT) (mD : measurable D) : {sfun aT >-> rT} := mindic rT mD. HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst_sfun k). Definition scale_sfun k f : {sfun aT >-> rT} := k \o* f. +(* NB: already in `measurable_realfun.v` *) HB.instance Definition _ f g := max_mfun_subproof f g. Definition max_sfun f g : {sfun aT >-> _} := f \max g. @@ -441,9 +271,6 @@ Proof. by move=> /=. Qed. HB.instance Definition _ x := @isNonNegFun.Build T R (cst x%:num) (cst_nnfun_subproof x). -(* NB: already instantiated in cardinality.v *) -HB.instance Definition _ x : @FImFun T R (cst x) := FImFun.on (cst x). - Definition cst_nnsfun (r : {nonneg R}) : {nnsfun T >-> R} := cst r%:num. Definition nnsfun0 : {nnsfun T >-> R} := cst_nnsfun 0%:nng. @@ -554,18 +381,6 @@ Qed. End nnsfun_cover. -(* FIXME: shouldn't we avoid calling [done] in a hint? *) -#[global] Hint Extern 0 (measurable (_ @^-1` [set _])) => - solve [apply: measurable_sfunP; exact: measurable_set1] : core. - -Lemma measurable_sfun_inP {d} {aT : measurableType d} {rT : realType} - (f : {mfun aT >-> rT}) D (y : rT) : - measurable D -> measurable (D `&` f @^-1` [set y]). -Proof. by move=> Dm; exact: measurableI. Qed. - -#[global] Hint Extern 0 (measurable (_ `&` _ @^-1` [set _])) => - solve [apply: measurable_sfun_inP; assumption] : core. - Section measure_fsbig. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType). diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index e40e9fdfb..00719b349 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -335,7 +335,7 @@ End hlength_extension. End LebesgueMeasure. Definition lebesgue_measure {R : realType} : - set (g_sigma_algebraType R.-ocitv.-measurable) -> \bar R := + set (measurableTypeR R) -> \bar R := lebesgue_stieltjes_measure idfun. HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R). HB.instance Definition _ (R : realType) := @@ -399,7 +399,7 @@ have mF_ m : mu (F_ m) < completed_mu E + m.+1%:R^-1%:E. apply: lee_nneseries => // n _. by rewrite -((measurable_mu_extE hlength) (A m n))//; have [/(_ n)] := mA m. pose F := \bigcap_n (F_ n). -have FM : @measurable _ (g_sigma_algebraType R.-ocitv.-measurable) F. +have FM : @measurable _ (measurableTypeR R) F. apply: bigcapT_measurable => k; apply: bigcupT_measurable => i. by apply: sub_sigma_algebra; have [/(_ i)] := mA k. have EF : E `<=` F by exact: sub_bigcap. @@ -434,7 +434,7 @@ have mG_ m : mu (G_ m) < completed_mu (F `\` E) + m.+1%:R^-1%:E. apply: lee_nneseries => // n _. by rewrite -((measurable_mu_extE hlength) (B m n))//; have [/(_ n)] := mB m. pose G := \bigcap_n (G_ n). -have GM : @measurable _ (g_sigma_algebraType R.-ocitv.-measurable) G. +have GM : @measurable _ (measurableTypeR R) G. apply: bigcapT_measurable => k; apply: bigcupT_measurable => i. by apply: sub_sigma_algebra; have [/(_ i)] := mB k. have FEG : F `\` E `<=` G by exact: sub_bigcap. @@ -654,6 +654,26 @@ rewrite measureU //; apply/seteqP; split => // x []/=. by rewrite in_itv/= => + xa; rewrite xa ltxx andbF. Qed. +Lemma countable_lebesgue_measure0 (A : set R) : + countable A -> lebesgue_measure A = 0. +Proof. +move/countable_injP => [f injf]. +rewrite -(injpinv_image (fun=> 0) injf). +rewrite [X in lebesgue_measure X](_ : _ = \bigcup_(x in f @` A) + [set 'pinv_(fun=> 0) A f x]); last first. + rewrite eqEsubset; split => [r [n]|r [n]]. + by move=> [t At ftn] Afnr; exists n => //=; exists t. + by move=> [t At ftn] /= rAfn; exists n => //=; exists t. +rewrite measure_bigcup/=; last 2 first. + by move=> ? _; exact: measurable_set1. + move=> i j [r Ar <-] [s As <-]. + by rewrite !pinvKV ?inE// => -[x [/= <- <-]]. +apply: lim_near_cst => //. +apply/nearW => n. +under eq_bigr do rewrite lebesgue_measure_set1. +by rewrite big_const_idem//= addr0. +Qed. + Let lebesgue_measure_itvoo (a b : R) : (lebesgue_measure (`]a, b[ : set R) = wlength idfun `]a, b[)%classic. Proof. @@ -801,12 +821,8 @@ rewrite (_ : range _ = \bigcup_n [set ratr (f1 n)]); last first. apply/seteqP; split => [_ [q _ <-]|_ [n _ /= ->]]; last by exists (f1 n). exists (f q) => //=; rewrite /f1 pinvKV// ?in_setE// => x y _ _. by apply: bij_inj; rewrite -setTT_bijective. -rewrite measure_bigcup//; last first. - apply/trivIsetP => i j _ _ ij; apply/seteqP; split => //= _ [/= ->]. - move=> /fmorph_inj. - have /set_bij_inj /[apply] := bijpinv_bij (fun=> 0) bijf. - by rewrite in_setE => /(_ Logic.I Logic.I); exact/eqP. -by rewrite eseries0// => n _ _; exact: lebesgue_measure_set1. +apply/countable_lebesgue_measure0/bigcup_countable => //. +exact: card_lexx. Qed. Section negligible_outer_measure. @@ -1334,8 +1350,8 @@ apply: le_trans; apply: lee_nneseries => //; first by move=> *; exact: esum_ge0. move=> n _. rewrite -(set_mem_set (F n)) -nneseries_esum// -nneseries_esum// -nneseriesZl//. apply: lee_nneseries => // m mFn. -rewrite (ballE (is_ballB m))// closure_ball lebesgue_measure_closed_ball//. -rewrite scale_ballE// closure_ball lebesgue_measure_closed_ball//. +rewrite (ballE (is_ballB m))// closure_ballE lebesgue_measure_closed_ball//. +rewrite scale_ballE// closure_ballE lebesgue_measure_closed_ball//. by rewrite -EFinM mulrnAr. Qed. @@ -1374,7 +1390,7 @@ Let vitali_cover_mclosure (F : set nat) k : vitali_cover A B F -> (R.-ocitv.-measurable).-sigma.-measurable (closure (B k)). Proof. case => + _ => /(_ k)/ballE ->. -by rewrite closure_ball; exact: measurable_closed_ball. +by rewrite closure_ballE; exact: measurable_closed_ball. Qed. Let vitali_cover_measurable (F : set nat) k : @@ -1436,7 +1452,7 @@ have muGSfin C : C `<=` G -> mu (\bigcup_(k in C) closure (B k)) \is a fin_num. apply: lee_nneseries => // n _. case: ifPn => [/set_mem nC|]; last by rewrite measure0. rewrite (vitali_cover_ballE _ ABF) ifT; last exact/mem_set/CG. - by rewrite closure_ball lebesgue_measure_closed_ball// lebesgue_measure_ball. + by rewrite closure_ballE lebesgue_measure_closed_ball// lebesgue_measure_ball. have muGfin : mu (\bigcup_(k in G) closure (B k)) \is a fin_num. by rewrite -(bigB0 G) muGSfin. have [c Hc] : exists c : {posnum R}, @@ -1524,8 +1540,8 @@ have bigBG_fin (r : {posnum R}) : finite_set (bigB G r%:num). apply: lee_sum => //= i /G0G'r [iG rBi]. rewrite -[leRHS]fineK//; last first. rewrite (vitali_cover_ballE _ ABF). - by rewrite closure_ball lebesgue_measure_closed_ball. - rewrite (vitali_cover_ballE _ ABF) closure_ball. + by rewrite closure_ballE lebesgue_measure_closed_ball. + rewrite (vitali_cover_ballE _ ABF) closure_ballE. by rewrite lebesgue_measure_closed_ball// fineK// lee_fin mulr2n ler_wpDl. rewrite le_measure? inE//; last exact: bigcup_subset. - by apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF. @@ -1541,7 +1557,7 @@ have bigBG_fin (r : {posnum R}) : finite_set (bigB G r%:num). move/trivIsetP : tB => /(_ _ _ Gi Gj ij). by apply: subsetI_eq0 => //=; exact: subset_closure. rewrite /= lee_nneseries// => n _. - rewrite (vitali_cover_ballE _ ABF)// closure_ball. + rewrite (vitali_cover_ballE _ ABF)// closure_ballE. by rewrite lebesgue_measure_closed_ball// lebesgue_measure_ball. rewrite le_measure? inE//. + by apply: bigcup_measurable => k _; exact: vitali_cover_measurable ABF. diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index 9c927b202..c6eb7627d 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -60,23 +60,24 @@ Reserved Notation "R .-ocitv.-measurable" Notation right_continuous f := (forall x, f%function @ at_right x --> f%function x). -Lemma right_continuousW (R : numFieldType) (f : R -> R) : - continuous f -> right_continuous f. +Lemma right_continuousW (R : numFieldType) {d} (U : orderNbhsType d) + (f : R -> U) : continuous f -> right_continuous f. Proof. by move=> cf x; apply: cvg_within_filter; exact/cf. Qed. -HB.mixin Record isCumulative (R : numFieldType) (f : R -> R) := { - cumulative_is_nondecreasing : {homo f : x y / x <= y} ; +HB.mixin Record isCumulative (R : numFieldType) {d} (U : orderNbhsType d) + (f : R -> U) := { + cumulative_is_nondecreasing : nondecreasing f ; cumulative_is_right_continuous : right_continuous f }. #[short(type=cumulative)] -HB.structure Definition Cumulative (R : numFieldType) := - { f of isCumulative R f }. +HB.structure Definition Cumulative + (R : numFieldType) {d} (U : orderNbhsType d) := { f of isCumulative R d U f }. -Arguments cumulative_is_nondecreasing {R} _. -Arguments cumulative_is_right_continuous {R} _. +Arguments cumulative_is_nondecreasing {R d U} _. +Arguments cumulative_is_right_continuous {R d U} _. -Lemma nondecreasing_right_continuousP (R : numFieldType) (a : R) (e : R) - (f : cumulative R) : +Lemma nondecreasing_right_continuousP (R : realFieldType) (a : R) (e : R) + (f : cumulative R R) : e > 0 -> exists d : {posnum R}, f (a + d%:num) <= f a + e. Proof. move=> e0; move: (cumulative_is_right_continuous f). @@ -92,7 +93,7 @@ by rewrite opprB ltrBlDl => fa; exact: ltW. Qed. Section id_is_cumulative. -Variable R : realType. +Variable R : realFieldType. Let id_nd : {homo @idfun R : x y / x <= y}. Proof. by []. Qed. @@ -100,7 +101,7 @@ Proof. by []. Qed. Let id_rc : right_continuous (@idfun R). Proof. by apply/right_continuousW => x; exact: cvg_id. Qed. -HB.instance Definition _ := isCumulative.Build R idfun id_nd id_rc. +HB.instance Definition _ := isCumulative.Build R _ R idfun id_nd id_rc. End id_is_cumulative. (* /TODO: move? *) @@ -373,7 +374,7 @@ apply/andP; split=> //; apply: contraTneq xbj => ->. by rewrite in_itv/= le_gtF// (itvP xabi). Qed. -Lemma wlength_ge0 (f : cumulative R) (I : set (ocitv_type R)) : +Lemma wlength_ge0 (f : cumulative R R) (I : set (ocitv_type R)) : (0 <= wlength f I)%E. Proof. by rewrite -(wlength0 f) le_wlength//; exact: cumulative_is_nondecreasing. @@ -381,14 +382,14 @@ Qed. #[local] Hint Extern 0 (0%:E <= wlength _ _) => solve[apply: wlength_ge0] : core. -HB.instance Definition _ (f : cumulative R) := +HB.instance Definition _ (f : cumulative R R) := isContent.Build _ _ R (wlength f) (wlength_ge0 f) (wlength_semi_additive f). Hint Extern 0 (measurable _) => solve [apply: is_ocitv] : core. -Lemma cumulative_content_sub_fsum (f : cumulative R) (D : {fset nat}) a0 b0 +Lemma cumulative_content_sub_fsum (f : cumulative R R) (D : {fset nat}) a0 b0 (a b : nat -> R) : (forall i, i \in D -> a i <= b i) -> `]a0, b0] `<=` \big[setU/set0]_(i <- D) `]a i, b i]%classic -> f b0 - f a0 <= \sum_(i <- D) (f (b i) - f (a i)). @@ -406,7 +407,7 @@ rewrite -sumEFin fsbig_finite//= set_fsetK// big_seq [in leRHS]big_seq. by apply: lee_sum => i iD; rewrite wlength_itv_bnd// Dab. Qed. -Lemma wlength_sigma_subadditive (f : cumulative R) : +Lemma wlength_sigma_subadditive (f : cumulative R R) : measurable_subset_sigma_subadditive (wlength f). Proof. move=> I A /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym AE => -[a _ <-]. @@ -475,7 +476,7 @@ rewrite big_seq [in X in (_ <= X)%E]big_seq; apply: lee_sum => k kX. by rewrite AE leeD2l// lee_fin lerBlDl natrX De. Qed. -HB.instance Definition _ (f : cumulative R) := +HB.instance Definition _ (f : cumulative R R) := Content_SigmaSubAdditive_isMeasure.Build _ _ _ (wlength f) (wlength_sigma_subadditive f). @@ -490,17 +491,18 @@ move=> k; split => //; rewrite wlength_itv /= -EFinB. by case: ifP; rewrite ltey. Qed. -Definition lebesgue_stieltjes_measure (f : cumulative R) := +Definition lebesgue_stieltjes_measure (f : cumulative R R) := measure_extension (wlength f). -HB.instance Definition _ (f : cumulative R) := +HB.instance Definition _ (f : cumulative R R) := Measure.on (lebesgue_stieltjes_measure f). -Let sigmaT_finite_lebesgue_stieltjes_measure (f : cumulative R) : +Let sigmaT_finite_lebesgue_stieltjes_measure (f : cumulative R R) : sigma_finite setT (lebesgue_stieltjes_measure f). Proof. exact/measure_extension_sigma_finite/wlength_sigma_finite. Qed. -HB.instance Definition _ (f : cumulative R) := @Measure_isSigmaFinite.Build _ _ _ - (lebesgue_stieltjes_measure f) (sigmaT_finite_lebesgue_stieltjes_measure f). +HB.instance Definition _ (f : cumulative R R) := + @Measure_isSigmaFinite.Build _ _ _ (lebesgue_stieltjes_measure f) + (sigmaT_finite_lebesgue_stieltjes_measure f). End wlength_extension. Arguments lebesgue_stieltjes_measure {R}. @@ -508,12 +510,14 @@ Arguments lebesgue_stieltjes_measure {R}. #[deprecated(since="mathcomp-analysis 1.1.0", note="renamed `wlength_sigma_subadditive`")] Notation wlength_sigma_sub_additive := wlength_sigma_subadditive (only parsing). +Definition measurableTypeR (R : realType) := + g_sigma_algebraType R.-ocitv.-measurable. + Section lebesgue_stieltjes_measure. Variable R : realType. -Let gitvs : measurableType _ := g_sigma_algebraType (@ocitv R). -Lemma lebesgue_stieltjes_measure_unique (f : cumulative R) - (mu : {measure set gitvs -> \bar R}) : +Lemma lebesgue_stieltjes_measure_unique (f : cumulative R R) + (mu : {measure set (measurableTypeR R) -> \bar R}) : (forall X, ocitv X -> lebesgue_stieltjes_measure f X = mu X) -> forall X, measurable X -> lebesgue_stieltjes_measure f X = mu X. Proof. @@ -527,17 +531,17 @@ End lebesgue_stieltjes_measure. Section completed_lebesgue_stieltjes_measure. Context {R : realType}. -Definition completed_lebesgue_stieltjes_measure (f : cumulative R) := +Definition completed_lebesgue_stieltjes_measure (f : cumulative R R) := @completed_measure_extension _ _ _ (wlength f). -HB.instance Definition _ (f : cumulative R) := +HB.instance Definition _ (f : cumulative R R) := Measure.on (@completed_lebesgue_stieltjes_measure f). -Let sigmaT_finite_completed_lebesgue_stieltjes_measure (f : cumulative R) : +Let sigmaT_finite_completed_lebesgue_stieltjes_measure (f : cumulative R R) : sigma_finite setT (@completed_lebesgue_stieltjes_measure f). Proof. exact/completed_measure_extension_sigma_finite/wlength_sigma_finite. Qed. -HB.instance Definition _ (f : cumulative R) := +HB.instance Definition _ (f : cumulative R R) := @Measure_isSigmaFinite.Build _ _ _ (@completed_lebesgue_stieltjes_measure f) (sigmaT_finite_completed_lebesgue_stieltjes_measure f). @@ -548,14 +552,13 @@ Arguments completed_lebesgue_stieltjes_measure {R}. Section salgebra_R_ssets. Variable R : realType. -Definition measurableTypeR := g_sigma_algebraType (R.-ocitv.-measurable). Definition measurableR : set (set R) := (R.-ocitv.-measurable).-sigma.-measurable. HB.instance Definition _ := Pointed.on R. HB.instance Definition R_isMeasurable : isMeasurable default_measure_display R := - @isMeasurable.Build _ measurableTypeR measurableR + @isMeasurable.Build _ (measurableTypeR R) measurableR measurable0 (@measurableC _ _) (@bigcupT_measurable _ _). (*HB.instance (Real.sort R) R_isMeasurable.*) @@ -600,12 +603,26 @@ Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core. #[global] Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core. +#[global] Hint Extern 0 (measurable (_ @^-1` [set _])) => + solve [apply: measurable_funPTI; exact: measurable_set1] : core. + +Lemma measurable_funP1 {d} {aT : measurableType d} {rT : realType} + (f : {mfun aT >-> rT}) D (y : rT) : + measurable D -> measurable (D `&` f @^-1` [set y]). +Proof. move=> mD; exact: measurable_funP. Qed. + +#[deprecated(since="mathcomp-analysis 1.13.0", note="renamed to `measurable_funP1`")] +Notation measurable_sfun_inP := measurable_funP1 (only parsing). + +#[global] Hint Extern 0 (measurable (_ `&` _ @^-1` [set _])) => + solve [apply: measurable_funP1; assumption] : core. + HB.mixin Record isCumulativeBounded (R : numFieldType) (l r : R) (f : R -> R) := { cumulativeNy : f @ -oo --> l ; cumulativey : f @ +oo --> r }. #[short(type=cumulativeBounded)] -HB.structure Definition CumulativeBounded (R : numFieldType) (l r : R) := +HB.structure Definition CumulativeBounded (R : realFieldType) (l r : R) := { f of isCumulativeBounded R l r f & Cumulative R f}. Arguments cumulativeNy {R l r} s. @@ -615,7 +632,6 @@ Section probability_measure_of_lebesgue_stieltjes_mesure. Context {R : realType} (f : cumulativeBounded (0:R) (1:R)). Local Open Scope measure_display_scope. -Let T := g_sigma_algebraType R.-ocitv.-measurable. Let lsf := lebesgue_stieltjes_measure f. Let lebesgue_stieltjes_setT : lsf setT = 1%E. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 6f454af1f..e33e42b32 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -41,6 +41,12 @@ From mathcomp Require Export lebesgue_stieltjes_measure. (* of equivalence between emeasurable and the sigma-algebras generated by *) (* open rays and closed rays. *) (* *) +(* ``` *) +(* mindic mD := \1_D where mD is a proof that D is measurable *) +(* indic_mfun mD := mindic mD *) +(* scale_mfun k f := k \o* f *) +(* max_mfun f g := f \max g *) +(* ``` *) (******************************************************************************) Set Implicit Arguments. @@ -328,8 +334,7 @@ Proof. by rewrite ball_itv; exact: measurable_itv. Qed. Lemma measurable_closed_ball (x : R) r : measurable (closed_ball x r). Proof. -have [r0|r0] := leP r 0; first by rewrite closed_ball0. -rewrite closed_ball_itv//. +by have [r0|r0] := leP r 0; [rewrite closed_ball0|rewrite closed_ball_itv]. Qed. End salgebra_R_ssets. @@ -641,7 +646,7 @@ rewrite eqEsubset; split=> [_ -> i _/=|]; first by rewrite in_itv /= ltry. move=> [r| |/(_ O Logic.I)] // /(_ `|ceil r|%N Logic.I); rewrite /= in_itv /=. rewrite andbT lte_fin ltNge. have [r0|r0] := ltP 0%R r; last by rewrite (le_trans r0). -by rewrite natr_absz gtr0_norm// ?le_ceil// ceil_gt0. +by rewrite natr_absz gtr0_norm// ?ceil_ge// ceil_gt0. Qed. End erealwithrays. @@ -1087,6 +1092,83 @@ Proof. by apply: continuous_measurable_fun; exact: continuous_expR. Qed. #[global] Hint Extern 0 (measurable_fun _ expR) => solve [apply: measurable_expR] : core. +Section mfun_realType. +Context {rT : realType}. + +HB.instance Definition _ := @isMeasurableFun.Build _ _ _ rT + (@normr rT rT) (@normr_measurable rT setT). + +HB.instance Definition _ := + isMeasurableFun.Build _ _ _ _ (@expR rT) (@measurable_expR rT). + +End mfun_realType. + +Section ring. +Context d (aT : measurableType d) (rT : realType). + +Lemma mfun_subring_closed : subring_closed (@mfun _ _ aT rT). +Proof. +split=> [|f g|f g]; rewrite !inE/=. +- exact: measurable_cst. +- exact: measurable_funB. +- exact: measurable_funM. +Qed. +HB.instance Definition _ := GRing.isSubringClosed.Build _ + (@mfun d default_measure_display aT rT) mfun_subring_closed. +HB.instance Definition _ := [SubChoice_isSubComRing of {mfun aT >-> rT} by <:]. + +Implicit Types (f g : {mfun aT >-> rT}). + +Lemma mfun0 : (0 : {mfun aT >-> rT}) =1 cst 0 :> (_ -> _). Proof. by []. Qed. +Lemma mfun1 : (1 : {mfun aT >-> rT}) =1 cst 1 :> (_ -> _). Proof. by []. Qed. +Lemma mfunN f : - f = \- f :> (_ -> _). Proof. by []. Qed. +Lemma mfunD f g : f + g = f \+ g :> (_ -> _). Proof. by []. Qed. +Lemma mfunB f g : f - g = f \- g :> (_ -> _). Proof. by []. Qed. +Lemma mfunM f g : f * g = f \* g :> (_ -> _). Proof. by []. Qed. +Lemma mfunMn f n : (f *+ n) = (fun x => f x *+ n) :> (_ -> _). +Proof. by apply/funext=> x; elim: n => //= n; rewrite !mulrS !mfunD /= => ->. Qed. +Lemma mfun_sum I r (P : {pred I}) (f : I -> {mfun aT >-> rT}) (x : aT) : + (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. +Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. +Lemma mfun_prod I r (P : {pred I}) (f : I -> {mfun aT >-> rT}) (x : aT) : + (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. +Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. +Lemma mfunX f n : f ^+ n = (fun x => f x ^+ n) :> (_ -> _). +Proof. by apply/funext=> x; elim: n => [|n IHn]//; rewrite !exprS mfunM/= IHn. Qed. + +HB.instance Definition _ f g := MeasurableFun.copy (f \+ g) (f + g). +HB.instance Definition _ f g := MeasurableFun.copy (\- f) (- f). +HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g). +HB.instance Definition _ f g := MeasurableFun.copy (f \* g) (f * g). + +Definition mindic (D : set aT) of measurable D : aT -> rT := \1_D. + +Lemma mindicE (D : set aT) (mD : measurable D) : + mindic mD = (fun x => (x \in D)%:R). +Proof. by rewrite /mindic funeqE => t; rewrite indicE. Qed. + +HB.instance Definition _ D mD := @isMeasurableFun.Build _ _ aT rT (mindic mD) + (@measurable_indic _ aT rT setT D mD). + +Definition indic_mfun (D : set aT) (mD : measurable D) : {mfun aT >-> rT} := + mindic mD. + +HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst k). +Definition scale_mfun k f : {mfun aT >-> rT} := k \o* f. + +Lemma max_mfun_subproof f g : @isMeasurableFun d _ aT rT (f \max g). +Proof. by split; apply: measurable_maxr. Qed. + +HB.instance Definition _ f g := max_mfun_subproof f g. + +Definition max_mfun f g : {mfun aT >-> _} := f \max g. + +End ring. +Arguments indic_mfun {d aT rT} _. +(* TODO: move earlier?*) +#[global] Hint Extern 0 (measurable_fun _ (\1__ : _ -> _)) => + (exact: measurable_indic ) : core. + Lemma natmul_measurable {R : realType} D n : measurable_fun D (fun x : R => x *+ n). Proof. diff --git a/theories/measure.v b/theories/measure.v index 2536331e4..4fc78ffcc 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -211,6 +211,9 @@ From mathcomp Require Import sequences esum numfun. (* *) (* ``` *) (* measurable_fun D f == the function f with domain D is measurable *) +(* {mfun aT >-> rT} == type of measurable functions *) +(* aT and rT are sigmaRingType's. *) +(* f \in mfun == holds for f : {mfun _ >-> _} *) (* preimage_set_system D f G == set system of the preimages by f of sets in G *) (* image_set_system D f G == set system of the sets with a preimage by f *) (* in G *) @@ -359,6 +362,10 @@ Reserved Notation "f = g %[ae mu ]" (at level 70, g at next level, format "f = g '%[ae' mu ]"). Reserved Notation "{ 'outer_measure' 'set' T '->' '\bar' R }" (T at level 37, format "{ 'outer_measure' 'set' T '->' '\bar' R }"). +Reserved Notation "{ 'mfun' aT >-> T }" + (at level 0, format "{ 'mfun' aT >-> T }"). +Reserved Notation "[ 'mfun' 'of' f ]" + (at level 0, format "[ 'mfun' 'of' f ]"). Inductive measure_display := default_measure_display. Declare Scope measure_display_scope. @@ -1513,6 +1520,42 @@ Definition measurable_fun d d' (T : sigmaRingType d) (U : sigmaRingType d') (D : set T) (f : T -> U) := measurable D -> forall Y, measurable Y -> measurable (D `&` f @^-1` Y). +HB.mixin Record isMeasurableFun d d' (aT : sigmaRingType d) (rT : sigmaRingType d') + (f : aT -> rT) := { + measurable_funPT : measurable_fun [set: aT] f +}. +HB.structure Definition MeasurableFun d d' aT rT := + {f of @isMeasurableFun d d' aT rT f}. +Arguments measurable_funPT {d d' aT rT} s. + +Notation "{ 'mfun' aT >-> T }" := (@MeasurableFun.type _ _ aT T) : form_scope. +Notation "[ 'mfun' 'of' f ]" := [the {mfun _ >-> _} of f] : form_scope. +#[global] Hint Extern 0 (measurable_fun [set: _] _) => + solve [apply: measurable_funPT] : core. + +Lemma measurable_funP {d d' : measure_display} + {aT : measurableType d} {rT : sigmaRingType d'} + (D : set aT) (s : {mfun aT >-> rT}) : measurable_fun D s. +Proof. +move=> mD Y mY; apply: measurableI => //. +by rewrite -(setTI (_ @^-1` _)); exact: measurable_funPT. +Qed. +Arguments measurable_funP {d d' aT rT D} s. + +Lemma measurable_funPTI {d d'} {aT : measurableType d} {rT : measurableType d'} + (f : {mfun aT >-> rT}) (Y : set rT) : measurable Y -> measurable (f @^-1` Y). +Proof. by move=> mY; rewrite -[f @^-1` _]setTI; exact: measurable_funP. Qed. + +#[deprecated(since="mathcomp-analysis 1.13.0", note="renamed to `measurable_funPTI`")] +Notation measurable_sfunP := measurable_funPTI (only parsing). + +Section mfun_pred. +Context {d d'} {aT : sigmaRingType d} {rT : sigmaRingType d'}. +Definition mfun : {pred aT -> rT} := mem [set f | measurable_fun setT f]. +Definition mfun_key : pred_key mfun. Proof. exact. Qed. +Canonical mfun_keyed := KeyedPred mfun_key. +End mfun_pred. + Section measurable_fun. Context d1 d2 d3 (T1 : sigmaRingType d1) (T2 : sigmaRingType d2) (T3 : sigmaRingType d3). @@ -1614,6 +1657,41 @@ End measurable_fun. Arguments eq_measurable_fun {d1 d2 T1 T2 D} f {g}. Arguments measurable_fun_eqP {d1 d2 T1 T2 D} f {g}. + +Section mfun. +Context {d d'} {aT : sigmaRingType d} {rT : sigmaRingType d'}. +Notation T := {mfun aT >-> rT}. +Notation mfun := (@mfun _ _ aT rT). + +Section Sub. +Context (f : aT -> rT) (fP : f \in mfun). +Definition mfun_Sub_subproof := @isMeasurableFun.Build d _ aT rT f (set_mem fP). +#[local] HB.instance Definition _ := mfun_Sub_subproof. +Definition mfun_Sub := [mfun of f]. +End Sub. + +Lemma mfun_rect (K : T -> Type) : + (forall f (Pf : f \in mfun), K (mfun_Sub Pf)) -> forall u : T, K u. +Proof. +move=> Ksub [f [[Pf]]]/=. +by suff -> : Pf = (set_mem (@mem_set _ [set f | _] f Pf)) by apply: Ksub. +Qed. + +Lemma mfun_valP f (Pf : f \in mfun) : mfun_Sub Pf = f :> (_ -> _). +Proof. by []. Qed. + +HB.instance Definition _ := isSub.Build _ _ T mfun_rect mfun_valP. + +Lemma mfuneqP (f g : {mfun aT >-> rT}) : f = g <-> f =1 g. +Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed. + +HB.instance Definition _ := [Choice of {mfun aT >-> rT} by <:]. + +HB.instance Definition _ x := isMeasurableFun.Build d _ aT rT (cst x) + (@measurable_cst _ _ aT rT setT x). + +End mfun. + Section measurable_fun_measurableType. Context d1 d2 d3 (T1 : measurableType d1) (T2 : measurableType d2) (T3 : measurableType d3). @@ -1725,6 +1803,19 @@ End measurable_fun_measurableType. Arguments eq_measurable_fun {d1 d2 T1 T2 D} f {g}. Arguments measurable_fun_bool {d1 T1 D f} b. +Section mfun_measurableType. +Context {d1} {T1 : measurableType d1} {d2} {T2 : measurableType d2} + {d3} {T3 : measurableType d3}. +Variables (f : {mfun T2 >-> T3}) (g : {mfun T1 >-> T2}). + +Let measurableT_comp_subproof : measurable_fun setT (f \o g). +Proof. exact: measurableT_comp. Qed. + +HB.instance Definition _ := isMeasurableFun.Build _ _ _ _ (f \o g) + measurableT_comp_subproof. + +End mfun_measurableType. + Section measurability. Definition preimage_set_system {aT rT : Type} (D : set aT) (f : aT -> rT) diff --git a/theories/normedtype_theory/ereal_normedtype.v b/theories/normedtype_theory/ereal_normedtype.v index 016d59aad..2225c83b0 100644 --- a/theories/normedtype_theory/ereal_normedtype.v +++ b/theories/normedtype_theory/ereal_normedtype.v @@ -482,3 +482,36 @@ split=> [|[Py]] [x [xr Px]]; last by exists x; split=> // -[y||]//; apply: Px. by split; [|exists x; split=> // y xy]; apply: Px. Qed. End nbhs_ereal. + +Section ereal_OrderNbhs. +Variable R : realFieldType. + +Let ereal_order_nbhsE (x : \bar R) : + nbhs x = filter_from (fun i => itv_open_ends i /\ x \in i) + (fun i => [set` i]). +Proof. +apply/seteqP; split=> A. +- rewrite /nbhs/= /ereal_nbhs/=; move: x => [r [e/= e0 reA]||]. + + exists `](r - e)%:E, (r + e)%:E[ => [|[y|/andP[]//|//]]; rewrite ?in_itv/=. + * by rewrite !lte_fin ltrBlDr andbb ltrDl; split => //; right. + * by move/subset_ball_prop_in_itv : reA => /(_ y); rewrite /= !in_itv. + + case=> M [Mreal MA]. + exists `]M%:E, +oo[ => [|y/=]; rewrite in_itv/= andbT ?ltry; last exact: MA. + by split => //; left. + + case=> M [Mreal MA]. + exists `]-oo, M%:E[ => [|y/=]; rewrite in_itv/= ?ltNyr; last exact: MA. + by split => //; left. +- move=> [[ [[]/= r|[]] [[]/= s|[]] ]] [] []// _. + + move=> /[dup]/ltgte_fin_num/fineK <-; rewrite in_itv/=. + move=> /andP[rx sx] rsA; apply: (nbhs_interval rx sx) => z rz zs. + by apply: rsA =>/=; rewrite in_itv/= rz. + + rewrite nbhsE/= => rx rA; exists `]r, +oo[%classic => //. + by split => //; rewrite set_itvE; exact: open_ereal_gt_ereal. + + rewrite nbhsE/= => xs ?; exists `]-oo, s[%classic => //. + by split => //; rewrite set_itvE; exact: open_ereal_lt_ereal. + + by rewrite set_itvE/= subTset => _ ->; exact: filter_nbhsT. +Qed. + +HB.instance Definition _ := Order_isNbhs.Build _ (\bar R) ereal_order_nbhsE. + +End ereal_OrderNbhs. diff --git a/theories/normedtype_theory/num_normedtype.v b/theories/normedtype_theory/num_normedtype.v index 09773081e..8534097e9 100644 --- a/theories/normedtype_theory/num_normedtype.v +++ b/theories/normedtype_theory/num_normedtype.v @@ -499,7 +499,7 @@ Proof. split=> [/cvgryPge|/cvgnyPge] Foo. by apply/cvgnyPge => A; near do rewrite -(@ler_nat R); apply: Foo. apply/cvgryPgey; near=> A; near=> n. -rewrite pmulrn ceil_le_int// [ceil _]intEsign. +rewrite pmulrn -ceil_le_int_tmp [ceil _]intEsign. by rewrite le_gtF ?expr0 ?mul1r ?lez_nat ?ceil_ge0//; near: n; apply: Foo. Unshelve. all: by end_near. Qed. @@ -591,7 +591,7 @@ move=> dF nyF; rewrite itvNy_bnd_bigcup_BLeft eqEsubset; split. move/cvgrNy_lt : nyF => /(_ (F a - n%:R))[z [zreal zFan]]. exists `|ceil (a - z)|%N. rewrite zFan// ltrBlDr -ltrBlDl. - rewrite (le_lt_trans (Num.Theory.le_ceil _)) ?num_real//. + rewrite (le_lt_trans (Num.Theory.ceil_ge _)) ?num_real//. by rewrite (le_lt_trans (ler_norm _))// -natr1 -intr_norm ltrDl. by exists i => //=; rewrite in_itv/= yFa andbT (lt_le_trans _ Fany). - move=> z/= [n _ /=]; rewrite in_itv/= => /andP[Fanz zFa]. @@ -716,6 +716,14 @@ End near_in_itv. note="use `near_in_itvoo` instead")] Notation near_in_itv := near_in_itvoo (only parsing). +Lemma nbhs_infty_gtr {R : archiFieldType} (r : R) : + \forall n \near \oo, r < n%:R. +Proof. +exists `|ceil r|.+1 => // n/=; rewrite -(ler_nat R); apply: lt_le_trans. +rewrite -natr1 -[ltLHS]addr0 ler_ltD//. +by rewrite (le_trans (ceil_ge _))// natr_absz ler_int ler_norm. +Qed. + Lemma near_infty_natSinv_lt (R : archiFieldType) (e : {posnum R}) : \forall n \near \oo, n.+1%:R^-1 < e%:num. Proof. diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 30e6d7511..07329928f 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -400,6 +400,18 @@ Arguments cvgr0_norm_le {_ _ _ F FF}. #[global] Hint Extern 0 (is_true (`|?x| <= _)) => match goal with H : x \is_near _ |- _ => solve[near: x; now apply: cvgr0_norm_le] end : core. +Section pseudoMetricNormedZmod_realDomainType. + +Lemma le0_ball0 (R : realDomainType) (V : pseudoMetricNormedZmodType R) (a : V) (r : R) : + r <= 0 -> ball a r = set0. +Proof. +move=> r0; rewrite -subset0 => y. +rewrite -ball_normE /ball_/= ltNge => /negP; apply. +by rewrite (le_trans r0). +Qed. + +End pseudoMetricNormedZmod_realDomainType. + Section pseudoMetricNormedZmod_numFieldType. Variables (R : numFieldType) (V : pseudoMetricNormedZmodType R). @@ -420,10 +432,11 @@ Local Hint Extern 0 (hausdorff_space _) => solve[apply: norm_hausdorff] : core. (* i.e. where the generic lemma is applied, *) (* check that norm_hausdorff is not used in a hard way *) -Lemma norm_closeE (x y : V): close x y = (x = y). Proof. exact: closeE. Qed. +Lemma norm_closeE (x y : V) : close x y = (x = y). Proof. exact: closeE. Qed. Lemma norm_close_eq (x y : V) : close x y -> x = y. Proof. exact: close_eq. Qed. -Lemma norm_cvg_unique {F} {FF : ProperFilter F} : is_subset1 [set x : V | F --> x]. +Lemma norm_cvg_unique {F} {FF : ProperFilter F} : + is_subset1 [set x : V | F --> x]. Proof. exact: cvg_unique. Qed. Lemma norm_cvg_eq (x y : V) : x --> y -> x = y. Proof. exact: (@cvg_eq V). Qed. @@ -1210,26 +1223,29 @@ Definition closed_ball_ (R : numDomainType) (V : zmodType) (norm : V -> R) Definition closed_ball (R : numDomainType) (V : pseudoMetricType R) (x : V) (e : R) := closure (ball x e). -Lemma closed_ball0 (R : realFieldType) (a r : R) : - r <= 0 -> closed_ball a r = set0. +Lemma closure_ballE (R : numDomainType) (V : pseudoMetricType R) + (c : V) (r : R) : closure (ball c r) = closed_ball c r. +Proof. by []. Qed. + +Lemma closed_ball0 (R : realDomainType) (V : pseudoMetricNormedZmodType R) + (v : V) (r : R) : r <= 0 -> closed_ball v r = set0. Proof. -move=> /ball0 r0; apply/seteqP; split => // y. -by rewrite /closed_ball r0 closure0. +by move=> r0; rewrite -subset0 => w; rewrite /closed_ball le0_ball0// closure0. Qed. Lemma closed_ballxx (R : numDomainType) (V : pseudoMetricType R) (x : V) (e : R) : 0 < e -> closed_ball x e x. Proof. by move=> ?; exact/subset_closure/ballxx. Qed. -Lemma closed_ball_closed (R : realFieldType) (V : pseudoMetricType R) (x : V) +Lemma closed_ball_closed (R : numDomainType) (V : pseudoMetricType R) (x : V) (r : R) : closed (closed_ball x r). Proof. exact: closed_closure. Qed. -Lemma subset_closed_ball (R : realFieldType) (V : pseudoMetricType R) (x : V) +Lemma subset_closed_ball (R : numDomainType) (V : pseudoMetricType R) (x : V) (r : R) : ball x r `<=` closed_ball x r. Proof. exact: subset_closure. Qed. -Lemma subset_closure_half (R : realFieldType) (V : pseudoMetricType R) (x : V) +Lemma subset_closure_half (R : numFieldType) (V : pseudoMetricType R) (x : V) (r : R) : 0 < r -> closed_ball x (r / 2) `<=` ball x r. Proof. move:r => _/posnumP[r] z /(_ (ball z ((r%:num/2)%:pos)%:num)) []. @@ -1237,11 +1253,13 @@ move:r => _/posnumP[r] z /(_ (ball z ((r%:num/2)%:pos)%:num)) []. by move=> y [+/ball_sym]; rewrite [t in ball x t z]splitr; apply: ball_triangle. Qed. -Lemma le_closed_ball (R : numFieldType) (M : pseudoMetricNormedZmodType R) +Lemma le_closed_ball (R : numFieldType) (M : pseudoMetricType R) (x : M) (e1 e2 : R) : (e1 <= e2)%O -> closed_ball x e1 `<=` closed_ball x e2. Proof. by rewrite /closed_ball => le; apply/closure_subset/le_ball. Qed. End Closed_Ball. +#[deprecated(since="mathcomp-analysis 1.14.0", note="renamed to `closure_ballE`")] +Notation closure_ball := closure_ballE (only parsing). Section limit_composition_pseudometric. Context {K : numFieldType} {V : pseudoMetricNormedZmodType K} {T : Type}. diff --git a/theories/normedtype_theory/vitali_lemma.v b/theories/normedtype_theory/vitali_lemma.v index 448833277..714e1f652 100644 --- a/theories/normedtype_theory/vitali_lemma.v +++ b/theories/normedtype_theory/vitali_lemma.v @@ -202,13 +202,6 @@ Lemma is_ball_closure (A : set R) : is_ball A -> closure A = closed_ball (cpoint A) (radius A)%:num. Proof. by move=> ballA; rewrite /closed_ball -ballE. Qed. -Lemma closure_ball (c r : R) : closure (ball c r) = closed_ball c r. -Proof. -have [r0|r0] := leP r 0. - by rewrite closed_ball0// ((ball0 _ _).2 r0) closure0. -by rewrite (is_ball_closure (is_ball_ball _ _)) cpoint_ball// radius_ball ?ltW. -Qed. - Lemma scale_ballE k x r : 0 <= k -> k *` ball x r = ball x (k * r). Proof. move=> k0; have [r0|r0] := ltP 0 r. @@ -443,7 +436,7 @@ have H0 : elt_prop (D0, 0%N, set0). - by move=> F D0F FH0; apply: maxD0 => // i Fi; exact: (FH0 _ Fi).1. have [v [Hv0 HvRel]] : {v : nat -> elt_type | v 0%N = exist _ _ H0 /\ forall n, Rel (v n) (v n.+1)}. - apply: dependent_choice_Type => -[[[Dn n] Un] Hn]. + apply: dependent_choice => -[[[Dn n] Un] Hn]. pose Hn1 := H_ n.+1 (Un `|` Dn). have [Dn1 maxDn1] := ex_maximal_disjoint_subcollection (closure\o B) Hn1. diff --git a/theories/probability.v b/theories/probability.v index 5d49431e3..e150847fb 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -66,14 +66,16 @@ From mathcomp Require Import ftc gauss_integral hoelder. (* normal_prob m s == normal probability measure *) (* exponential_pdf r == pdf of the exponential distribution with rate r *) (* exponential_prob r == exponential probability measure *) +(* poisson_pmf r k == pmf of the Poisson distribution with parameter r *) +(* poisson_prob r == Poisson probability measure *) (* ``` *) (* *) (******************************************************************************) Reserved Notation "'{' 'RV' P >-> R '}'" (at level 0, format "'{' 'RV' P '>->' R '}'"). -Reserved Notation "''E_' P [ X ]" (format "''E_' P [ X ]"). -Reserved Notation "''V_' P [ X ]" (format "''V_' P [ X ]"). +Reserved Notation "''E_' P [ X ]" (at level 5, P, X at level 4, format "''E_' P [ X ]"). +Reserved Notation "''V_' P [ X ]" (at level 5, P, X at level 4, format "''V_' P [ X ]"). Reserved Notation "'M_ P X" (at level 5, P, X at level 4, format "''M_' P X"). Reserved Notation "{ 'dmfun' aT >-> T }" (format "{ 'dmfun' aT >-> T }"). Reserved Notation "'{' 'dRV' P >-> R '}'" (format "'{' 'dRV' P '>->' R '}'"). @@ -167,6 +169,11 @@ Lemma cdf_ge0 r : 0 <= cdf X r. Proof. by []. Qed. Lemma cdf_le1 r : cdf X r <= 1. Proof. exact: probability_le1. Qed. +Lemma cdf_fin_num r : cdf X r \is a fin_num. +Proof. +by rewrite ge0_fin_numE ?cdf_ge0//; exact/(le_lt_trans (cdf_le1 r))/ltry. +Qed. + Lemma cdf_nondecreasing : nondecreasing_fun (cdf X). Proof. by move=> r s rs; rewrite le_measure ?inE//; exact: subitvPr. Qed. @@ -237,27 +244,29 @@ have cdf_na : cdf X (a + n.+1%:R^-1) @[n --> \oo] --> cdf X a. suff : P (F n) @[n --> \oo] --> P (\bigcap_n F n). by rewrite [in X in _ --> X -> _]/F -preimage_bigcap -itvNycEbigcap. apply: nonincreasing_cvg_mu => [| | |m n mn]. - - by rewrite -ge0_fin_numE// fin_num_measure//; exact: measurable_sfunP. - - by move=> ?; exact: measurable_sfunP. - - by apply: bigcap_measurable => // ? _; exact: measurable_sfunP. + - by rewrite -ge0_fin_numE// fin_num_measure//; exact: measurable_funPTI. + - by move=> ?; exact: measurable_funPTI. + - by apply: bigcap_measurable => // ? _; exact: measurable_funPTI. - apply/subsetPset; apply: preimage_subset; apply: subset_itvl. by rewrite bnd_simp lerD2l lef_pV2 ?posrE// ler_nat. by rewrite -(cvg_unique _ cdf_ns cdf_na). Unshelve. all: by end_near. Qed. +HB.instance Definition _ := isCumulative.Build R _ (\bar R) (cdf X) + cdf_nondecreasing cdf_right_continuous. + End cumulative_distribution_function. -Section cdf_of_lebesgue_stieltjes_mesure. +Section cdf_of_lebesgue_stieltjes_measure. Context {R : realType} (f : cumulativeBounded (0:R) (1:R)). Local Open Scope measure_display_scope. -Let T := g_sigma_algebraType R.-ocitv.-measurable. -Let lsf := lebesgue_stieltjes_measure f. - -Let idTR : T -> R := idfun. +Let idTR : measurableTypeR R -> R := idfun. #[local] HB.instance Definition _ := - @isMeasurableFun.Build _ _ T R idTR (@measurable_id _ _ setT). + @isMeasurableFun.Build _ _ _ _ idTR (@measurable_id _ _ setT). + +Let lsf := lebesgue_stieltjes_measure f. Lemma cdf_lebesgue_stieltjes_id r : cdf (idTR : {RV lsf >-> R}) r = (f r)%:E. Proof. @@ -272,12 +281,65 @@ have : lsf `]-n%:R, r] @[n --> \oo] --> (f r)%:E. apply: (cvg_comp _ _ (cvg_comp _ _ _ (cumulativeNy f))) => //. by apply: (cvg_comp _ _ cvgr_idn); rewrite ninfty. have : lsf `]- n%:R, r] @[n --> \oo] --> lsf (\bigcup_n `]-n%:R, r]%classic). - apply: nondecreasing_cvg_mu; rewrite /I//; first exact: bigcup_measurable. + apply: nondecreasing_cvg_mu => //; first exact: bigcup_measurable. by move=> *; apply/subsetPset/subset_itv; rewrite leBSide//= lerN2 ler_nat. exact: cvg_unique. Unshelve. all: by end_near. Qed. -End cdf_of_lebesgue_stieltjes_mesure. +End cdf_of_lebesgue_stieltjes_measure. + +Section lebesgue_stieltjes_measure_of_cdf. +Context {R : realType} (P : probability (measurableTypeR R) R). +Local Open Scope measure_display_scope. + +Let idTR : measurableTypeR R -> R := idfun. + +#[local] HB.instance Definition _ := + @isMeasurableFun.Build _ _ _ _ idTR (@measurable_id _ _ setT). + +Let fcdf r := fine (cdf (idTR : {RV P >-> R}) r). + +Let fcdf_nd : nondecreasing fcdf. +Proof. +by move=> *; apply: fine_le; [exact: cdf_fin_num.. | exact: cdf_nondecreasing]. +Qed. + +Let fcdf_rc : right_continuous fcdf. +Proof. +move=> a; apply: fine_cvg. +by rewrite fineK; [exact: cdf_right_continuous | exact: cdf_fin_num]. +Qed. + +#[local] HB.instance Definition _ := + isCumulative.Build R _ R fcdf fcdf_nd fcdf_rc. + +Let fcdf_Ny0 : fcdf @ -oo --> (0:R). +Proof. exact/fine_cvg/cvg_cdfNy0. Qed. + +Let fcdf_y1 : fcdf @ +oo --> (1:R). +Proof. exact/fine_cvg/cvg_cdfy1. Qed. + +#[local] HB.instance Definition _ := + isCumulativeBounded.Build R 0 1 fcdf fcdf_Ny0 fcdf_y1. + +Let lscdf := lebesgue_stieltjes_measure fcdf. + +Lemma lebesgue_stieltjes_cdf_id (A : set _) (mA : measurable A) : lscdf A = P A. +Proof. +apply: lebesgue_stieltjes_measure_unique => [I [[a b]]/= _ <- | //]. +rewrite /lebesgue_stieltjes_measure /measure_extension/=. +rewrite measurable_mu_extE/=; last exact: is_ocitv. +have [ab | ba] := leP a b; last first. + by rewrite set_itv_ge ?wlength0 ?measure0// bnd_simp -leNgt ltW. +rewrite wlength_itv_bnd// EFinB !fineK ?cdf_fin_num//. +rewrite /cdf /distribution /pushforward !preimage_id. +have : `]a, b]%classic = `]-oo, b] `\` `]-oo, a] => [|->]. + by rewrite -[RHS]setCK setCD setCitvl setUC -[LHS]setCK setCitv. +rewrite measureD ?setIidr//; first exact: subset_itvl. +by rewrite -ge0_fin_numE// fin_num_measure. +Qed. + +End lebesgue_stieltjes_measure_of_cdf. HB.lock Definition expectation {d} {T : measurableType d} {R : realType} (P : probability T R) (X : T -> R) := (\int[P]_w (X w)%:E)%E. @@ -783,6 +845,40 @@ Qed. End markov_chebyshev_cantelli. +Section hoeffding. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType) (P : probability T R). + +Print Grammar constr. + +Lemma hoeffding (X : {RV P >-> R}) (a b s : R) : + (s > 0)%R -> + {ae P, forall i, a <= X i <= b}%R -> + 'E_P[fun i => expR (s * (X i - fine 'E_P[X]))]%R <= (expR (s ^+ 2 * (b - a) ^+ 2 * 8^-1))%:E. +Proof. +Admitted. + +(* note: requires independence, it might be that we need the product sample space *) +Lemma hoeffding_ineq n (X : n.-tuple {RV P >-> R}) (a b : n.-tuple R) (t : R) : + (forall i, {ae P, forall t, tnth a i <= tnth X i t <= tnth b i}%R) -> + let S : {RV P >-> R} := (\sum_(i < n) tnth X i)%R in + (0 < t)%R -> + P [set x | (S x)%:E - 'E_P[S] >= t%:E] <= (expR (- 2 * t^+2 / (\sum_(i < n) (tnth b i - tnth a i)^+2)))%:E. +Proof. +move=> hXab S t0. +pose s := (4 * t / (\sum_i (tnth b i - tnth a i) ^+ 2))%R. +have -> : [set x | t%:E <= (S x)%:E - 'E_P[S]] = [set x | expeR (s * t)%:E <= expeR (s%:E * (S x)%:E - 'E_P[S])]. + admit. +apply: (@le_trans _ _ (expeR (- s * t)%:E * 'E_P[fun x => expR(s * (S x - fine 'E_P[S]))])). + admit. (* Markov's inequality *) +rewrite [leLHS](_ : _ = expeR (- s * t)%:E * \prod_i 'E_P[fun x => expR (s * (tnth X i x - fine 'E_P[tnth X i]))]); last first. + admit. +rewrite [leRHS](_ : _ = expeR (- s * t)%:E * (\prod_i (expR (s ^+ 2 * (tnth b i - tnth a i) ^+ 2 * 8^-1))%:E)). + admit. +Admitted. + +End hoeffding. + HB.mixin Record MeasurableFun_isDiscrete d d' (T : measurableType d) (T' : measurableType d') (X : T -> T') of @MeasurableFun d d' T T' X := { countable_range : countable (range X) diff --git a/theories/realfun.v b/theories/realfun.v index 0b6f218a1..68502a78d 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -113,6 +113,9 @@ move=> P [r [rreal rP]]; exists (r - M); split. by move=> m/=; rewrite ltrBrDr => /rP. Qed. +Lemma cvg_addrl_Ny (M : R) : M + r @[r --> -oo] --> -oo. +Proof. by under eq_fun do rewrite addrC; exact: cvg_addrr_Ny. Qed. + (* NB: see cvg_centern in sequences.v *) Lemma cvg_centerr (M : R) (T : topologicalType) (f : R -> T) (l : T) : (f (n - M) @[n --> +oo] --> l) = (f r @[r --> +oo] --> l). @@ -164,6 +167,7 @@ rewrite neq_lt => /orP[tp|pt]. move=> z/= + _ => /lt_le_trans; apply. by rewrite ler_pdivrMr// ler_pMr// ler1n. Unshelve. all: by end_near. Qed. + End fun_cvg_realFieldType. Section cvgr_fun_cvg_seq. diff --git a/theories/showcase/pnt.v b/theories/showcase/pnt.v new file mode 100644 index 000000000..890123961 --- /dev/null +++ b/theories/showcase/pnt.v @@ -0,0 +1,455 @@ +From mathcomp Require Import all_ssreflect classical_sets boolp topology ssralg. +From mathcomp Require Import ereal ssrnum sequences reals interval rat. +From mathcomp Require Import all_analysis archimedean ssrint. +Import Order.OrdinalOrder Num.Theory Order.POrderTheory finset GRing.Theory. +Import Num.Def. + +(**md**************************************************************************) +(* # The Prime Number Theorem *) +(* *) +(* This file aims at formalizing Daboussi's proof of the prime number theorem.*) +(* The main theorem proved so far is the divergence of the sum of the *) +(* reciprocals of the prime numbers. *) +(* *) +(* ``` *) +(* prime_seq == the sequence of prime numbers *) +(* ``` *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope ring_scope. +Local Open Scope ereal_scope. +Local Open Scope order_scope. +Local Open Scope classical_set_scope. +Local Open Scope set_scope. +Local Open Scope nat_scope. + +Section prime_seq. + +Let next_prime_subproof n : {i : 'I_(n`! - n).+1 | prime (n.+1 + i)}. +Proof. +suff: [exists i : 'I_(n`! - n).+1, prime (n.+1 + (tnth (ord_tuple _) i))]. + rewrite (existsb_tnth (fun x : 'I_(n`! - n).+1 => prime (n.+1 + x))). + move=> /(nth_find ord0) ni. + by eexists; apply: ni. +apply/existsP/not_existsP => noprime. +set q := pdiv n`!.+1. +have qprime : prime q by apply/pdiv_prime/fact_gt0. +have [qlei|iltq] := leqP q n. + have /dvdn_fact : 0 < q <= n by rewrite pdiv_gt0. + by rewrite (@dvdn_add_eq _ _ 1) ?Euclid_dvd1// addn1 pdiv_dvd. +have qlt : q - n.+1 < (n`! - n).+1. + by rewrite -subSn// subSS -subSn ?fact_geq//; exact/leq_sub2r/pdiv_leq. +apply: (noprime (Ordinal qlt)). +by rewrite tnth_ord_tuple subnKC// ltnW. +Qed. + +Definition next_prime n : nat := + n.+1 + [arg min_(i < val (next_prime_subproof n) | prime (n.+1 + i)) val i]. + +Lemma prime_next_prime n : prime (next_prime n). +Proof. +by rewrite /next_prime; case: arg_minnP => //; case: next_prime_subproof. +Qed. + +Lemma next_prime_min (i j : nat) : i < j < next_prime i -> ~~ prime j. +Proof. +rewrite /next_prime. +case: arg_minnP => [|k kP kmin]; first by case: next_prime_subproof. +move=> /andP[ij]. +rewrite -(ltn_subLR _ ij) => jk. +have jlt := ltn_trans jk (ltn_ord k). +rewrite -[j](subnKC ij); apply/negP => jP. +move: (kmin (Ordinal jlt) jP) => /= /(leq_trans jk). +by rewrite ltnn. +Qed. + +Lemma next_prime_lt n : n < next_prime n. +Proof. +rewrite /next_prime. +case: arg_minnP => [|i _ _]; first by case: next_prime_subproof. +exact: leq_addr. +Qed. + +Definition prime_seq n : nat := iter n next_prime 2. + +Lemma leq_prime_seq : {mono prime_seq : m n / m <= n}. +Proof. +move=> m n. +apply: (@Order.NatMonotonyTheory.incn_inP _ nat predT) => // {m n} [n /= _ _]. +exact: next_prime_lt. +Qed. + +Lemma mem_prime_seq (p : nat) : p \in range prime_seq = prime p. +Proof. +apply/idP/idP => [|primep]. + by rewrite inE => -[] [|n] _ <- //=; apply: prime_next_prime. +case: (@Order.TotalTheory.arg_maxP _ _ 'I_p.+1 ord0 + (fun m => prime_seq m <= p) prime_seq) => /= [|n pgepsi pptargmax]. + exact: prime_gt1. +have pltpsni1: p < prime_seq n.+1. + move: (valP n). rewrite leq_eqVlt => /orP [|nltp]. + rewrite eqSS => /eqP ->. + exact/mono_leq_infl/leq_prime_seq. + have := contra (pptargmax (Ordinal nltp)). + rewrite [(_ <= _)%O](leq_prime_seq (Ordinal nltp) n) ltnn => /(_ erefl). + by rewrite ltnNge. +move: pgepsi. +rewrite leq_eqVlt => /predU1P[<-|psnltp]; first by rewrite inE. +have := @next_prime_min (prime_seq n) p; rewrite psnltp pltpsni1 => /(_ erefl). +by rewrite primep. +Qed. + +End prime_seq. + +Section dvg_sum_inv_prime_seq. + +Let P (k N : nat) := + [set n : 'I_N.+1 |all (fun p => p < prime_seq k) (primes n)]%SET. +Let G (k N : nat) := ~: P k N. + +Let cardPcardG k N : #|G k N| + #|P k N| = N.+1. +Proof. +rewrite addnC. +have : (P k N) :|: (G k N) = [set : 'I_N.+1]%SET by rewrite finset.setUCr. +rewrite -cardsUI finset.setICr cards0. +by rewrite -[X in _ + _ = X]card_ord addn0 -cardsT => ->. +Qed. + +Let cardG (R : realType) (k N : nat) : + (\sum_(k <= k0 k <= N.+1 -> ~~ odd N -> N > 0 -> (#|G k N| < (N./2)). +Proof. +set E := fun i => [set n : 'I_N.+1 | (prime_seq i) \in (primes n)]. +set Parts := fun i => [set ([set x in [seq (insubd ord0 x : 'I_N.+1) | + x <- iota ((val y).+1 - (prime_seq i)) (prime_seq i)]] + : {set 'I_N.+1}) | y in (E i)]%SET. +move=> Rklthalf kleqN1 evenN Nneq0. +suff cardEi : forall i, k <= i -> + (#|E i|%:R <= N%:R / (prime_seq i)%:R :>R)%R => [|i klti]. + have -> : G k N = \bigcup_(k <= i < N.+1) E i. + apply/eqP; rewrite finset.eqEsubset; apply/andP; split; last first. + apply/fintype.subsetP => x. + rewrite big_geq_mkord => /bigcupP[i /= klei]. + rewrite inE => pidvdx. + rewrite !inE -has_predC; apply/hasP; exists (prime_seq i) => //=. + by rewrite -leqNgt leq_prime_seq. + apply/fintype.subsetP => /= x. + rewrite !inE -has_predC => /hasP[p/=]. + rewrite mem_primes => /andP[+ /andP[xneq0 pdvdx]]. + rewrite -mem_prime_seq inE => /= -[i _ peqpi]. + move: peqpi pdvdx => <- {p} pidvdx. + rewrite -leqNgt => pklepi. + rewrite big_geq_mkord; apply/bigcupP. + have ileqN : i < N.+1. + apply: (leq_ltn_trans _ (ltn_ord x)). + apply: (leq_trans _ (dvdn_leq xneq0 pidvdx)). + exact/mono_leq_infl/leq_prime_seq. + exists (Ordinal ileqN) => /=; first by rewrite -leq_prime_seq. + by rewrite inE mem_primes xneq0 pidvdx/= andbT -mem_prime_seq inE. + apply: (leq_ltn_trans (card_big_setU _ _ E)). + rewrite -(ltr_nat R). + apply: (@le_lt_trans _ _ (N%:R * \sum_(k <= i < N.+1) (prime_seq i)%:R^-1)%R). + rewrite mulr_sumr raddf_sum /= ler_sum_nat// => i /andP[+ _]. + exact: cardEi. + have SnleqlimSn: ((\sum_(k <= i < N.+1) (prime_seq i)%:R^-1)%:E <= + \sum_(k <= i [|i leqi]; last first. + by rewrite lee_fin invr_ge0. + rewrite subnKC // raddf_sum leeDl//; apply/nneseries_ge0 => n _ _. + by rewrite lee_fin invr_ge0. + rewrite -lte_fin. + apply: (@le_lt_trans _ _ (N%:R%:E * \sum_(k <= i //. + by apply: sumr_ge0 => i _; rewrite invr_ge0. + rewrite -divn2 natf_div ?dvdn2// EFinM -lte_pdivrMl ?ltr0n//. + by rewrite muleA -EFinM mulVf ?mul1e// pnatr_eq0 -lt0n. +rewrite ler_pdivlMr; last first. + rewrite ltr0n. + have : prime_seq i \in range prime_seq by rewrite inE. + by rewrite mem_prime_seq; apply: prime_gt0. +have Eigtpi x3 : x3 \in E i -> prime_seq i - x3.+1 = 0. + have OnotinE : ord0 \notin E i => [|x3inEi]; first by rewrite /E inE. + apply/eqP; rewrite subn_eq0; apply/leqW/dvdn_leq. + case: x3 x3inEi => /= x3; have [-> N1lt0|//] := posnP x3. + by rewrite /E inE. + move: x3inEi; rewrite /E inE mem_primes -mem_prime_seq mem_range. + by case: (x3 > 0). +have: finset.trivIset (Parts i). + apply/finset.trivIsetP => A B /imsetP [] x xinEi + /imsetP [] y yinEi. + wlog xley: x y xinEi yinEi A B / x <= y. + move: (leq_total x y) => /orP [xley Hw| ylex Hw Adef Bdef]. + exact: (Hw x y). + by rewrite eq_sym disjoint_sym; apply: (Hw y x). + have [-> <- ->| xneqy] := eqVneq x y; first by rewrite eqxx. + rewrite -setI_eq0 => -> -> AneqB /=; rewrite -finset.subset0. + apply/fintype.subsetP; rewrite /sub_mem => x0. + rewrite finset.in_setI => /andP. rewrite finset.inE => -[]. + rewrite finset.inE => /mapP -[] x1 x1iniota -> /mapP -[] x2 x2iniota + /(congr1 val). + rewrite !val_insubd. move: x1iniota x2iniota. + rewrite !mem_iota !addnCB (Eigtpi x) // (Eigtpi y) // !addn0 !ltnS. + move=> /andP [] x1ge x1lt /andP [] x2ge x2lt. + rewrite (leq_trans x1lt (ltn_ord x)) (leq_trans x2lt (ltn_ord y)) => x12. + have: y.+1 - (prime_seq i) >= x.+1. + rewrite -(leq_add2r (prime_seq i)) -(@leq_sub2rE x.+1); last first. + by rewrite addnCB (Eigtpi y) // addn0. + rewrite addnCB (Eigtpi y) // addn0 -addnBAC // subnn add0n subSS. + apply: dvdn_leq; first by rewrite subn_gt0 ltn_neqAle; apply/andP. + suff pidvdEi x3 : x3 \in E i -> prime_seq i %| x3. + by apply: dvdn_sub; apply: (pidvdEi _). + by rewrite /E inE mem_primes -mem_prime_seq mem_range; case: (x3 > 0). + move=> /(fun H => leq_trans H x2ge) /(leq_ltn_trans x1lt). + by rewrite x12 ltnn. +set i1toN := [set : 'I_N.+1] :\ ord0. +have cardNeqN: #|i1toN| = N. + rewrite /i1toN. apply/eqP. + rewrite -(eqn_add2r (ord0 \in [set :'I_N.+1]%SET)). apply/eqP. + have ord0inI: ord0 \in [set: 'I_N.+1]%SET by rewrite inE. + rewrite [in RHS]ord0inI [N + 1]addn1 addnC. + by rewrite -(cardsD1 ord0 [set: 'I_N.+1]) cardsT card_ord. +rewrite -[X in (_ <= X%:R)%R]cardNeqN /finset.trivIset => /eqP. +have cardeltPi: forall X, X \in Parts i -> #|X| = (prime_seq i) => [X|]. + rewrite /(Parts i) => /finset.imsetP [] x xinEi -> {X}. + rewrite cardsE. + suff /card_uniqP -> : uniq ([seq insubd ord0 x0 | + x0 <- iota ((\val x).+1 - prime_seq i) (prime_seq i)] : seq 'I_N.+1). + by rewrite size_map size_iota. + apply/(uniqP ord0) => x1 y1 /=. + rewrite !inE size_map size_iota => x1lt y1lt. + rewrite !(nth_map 0) ?size_iota //. + rewrite !nth_iota => // /(congr1 val). rewrite !val_insubd /=. + rewrite [X in X < _]addBnA; last first. + - exact: ltnW. + - by rewrite -subn_eq0; apply/eqP/Eigtpi. + rewrite -(@prednK (prime_seq i - x1)) ?subn_gt0// !subSS. + rewrite (leq_ltn_trans _ (ltn_ord x)); last exact: sub_ord_proof. + rewrite [X in X < _]addBnA; last first. + - exact: ltnW. + - by rewrite -subn_eq0; apply/eqP/Eigtpi. + rewrite -(@prednK (prime_seq i - y1)) ?subn_gt0 // !subSS. + suff -> : x - (prime_seq i - y1).-1 < N.+1 by apply: addnI. + exact/(leq_ltn_trans _ (ltn_ord x))/sub_ord_proof. +under eq_bigr do rewrite cardeltPi//. +rewrite sum_nat_const. +suff -> : #|Parts i| = #|E i|. + suff Pisubi1toN : finset.cover (Parts i) \subset i1toN => [eqcard|]. + suff: #|E i| * prime_seq i <= #|i1toN| by rewrite -natrM ler_nat. + exact: (leq_trans (eq_leq eqcard) (subset_leq_card Pisubi1toN)). + rewrite /(Parts i) cover_imset. apply/bigcupsP => i0 i0inEi. + apply/fintype.subsetP => x. + case: (boolP (x == ord0)) => [/eqP ->|xneq0 _]; last first. + by rewrite /i1toN inE !inE xneq0. + rewrite inE /in_mem /= => /mapP /= [] x0. + rewrite mem_iota subnK => [/andP [] x0b1 x0b2|]; last first. + by rewrite -subn_eq0; apply/eqP /Eigtpi. + have x0b3: x0 < N.+1 => [|/(congr1 val)]. + exact: (leq_ltn_trans _ (ltn_ord i0)). + rewrite val_insubd x0b3 => /= /eqP. + suff xpos: x0 > 0 by rewrite ltn_eqF. + apply: (leq_ltn_trans (leq0n (i0.+1 - prime_seq i).-1)). + rewrite -(ltn_add2r 1) !addn1 prednK // subn_gt0 ltnS. + rewrite dvdn_leq //; last first. + move: i0inEi. + by rewrite /E inE mem_primes -mem_prime_seq mem_range; case: (i0 > 0). + case: i0 i0inEi x0b1 x0b2 => /= i0. + case: (posnP i0) => // -> N1lt0. + by rewrite /E inE. +rewrite /(Parts i) card_in_imset // /injective => x1 x2. +wlog: x1 x2 / x1 <= x2 => [Hw|x1lex2 x1inEi x2inEi enseq]. + move: (leq_total x1 x2) => /orP [] => // [|x2lex1 x1inEi x2inEi /eqP]. + exact: (Hw x1 x2). + rewrite eq_sym => /eqP enseq. + apply/eqP. rewrite eq_sym. apply/eqP. + exact: (Hw x2 x1). +apply: le_anti. apply/andP. split; first exact: x1lex2. +have: x2 \in [set x in [seq insubd ord0 x0 + | x0 <- iota ((\val x1).+1 - prime_seq i) (prime_seq i)]]. + rewrite enseq inE /in_mem /=. apply/mapP => /=. + exists x2; last by apply: val_inj; rewrite !val_insubd ltn_ord. + rewrite mem_iota subnK; last by rewrite -subn_eq0; apply/eqP /Eigtpi. + by rewrite ltnSn -ltnS ltn_subrL prime_gt0 // -mem_prime_seq mem_range. +rewrite inE /in_mem /= => /mapP /= [] x3. +rewrite mem_iota subnK => [/andP [] x3b1 x3b2 /(congr1 val)|]; last first. + by rewrite -subn_eq0; apply/eqP /Eigtpi. +have x3b3: x3 < N.+1 by apply: (leq_ltn_trans _ (ltn_ord x1)). +rewrite val_insubd x3b3 /= => x2eqx3. move: x3b2. +by rewrite ltnS -x2eqx3. +Qed. + +Let cardP (k : nat) : #|P k (2 ^ (k.*2 + 2))| <= (2 ^ (k.*2 + 1)).+1. +Proof. +set N := 2 ^ (k.*2 + 2). +set P' := fun k N => P k N :\ ord0. +set A := k.-tuple bool. +set B := 'I_(2 ^ (k + 1)).+1. +set a := fun n i => odd (logn (prime_seq i) n). +have eqseq : forall n k, n < k -> + [seq i <- [seq prime_seq i | i <- index_iota 0 k] | i \in primes n] + = primes n. + move=> + k0; case=> [|n nlek]; first by rewrite filter_pred0. + apply: lt_sorted_eq => [||elt]. + - apply: lt_sorted_filter. + rewrite sorted_map. + apply: (@sub_sorted _ ltn); last exact: iota_ltn_sorted. + rewrite ltEnat => i j /=. + by rewrite (leqW_mono leq_prime_seq). + - exact: sorted_primes. + rewrite mem_filter andb_idr// => eltinprimesn. + suff: prime elt /\ elt < prime_seq k0. + rewrite -mem_prime_seq inE => /= -[[i _ <-]] pilepk. + rewrite map_comp; apply: map_f. + by rewrite map_id_in // mem_iota /= add0n subn0 -(leqW_mono leq_prime_seq). + split. + by apply/(@allP _ _ (primes n.+1)); first exact: all_prime_primes. + apply: (@leq_ltn_trans n.+1). + rewrite dvdn_leq//. + move: eltinprimesn. + by rewrite mem_primes => /andP[_ /andP[]]. + apply: (@leq_ltn_trans k0.-1); first by rewrite ltn_predRL. + rewrite prednK ?(ltn_trans _ nlek)//. + exact/mono_leq_infl/leq_prime_seq. +have binB (n : 'I_N.+1) : + (\prod_(i < k) (prime_seq i) ^ (logn (prime_seq i) n)./2) < + (2 ^ (k + 1)).+1. + have [->/=|nneq0] := eqVneq n ord0. + under eq_bigr do rewrite logn0 -divn2 div0n expn0. + by rewrite big1_eq -[X in _ < X]addn1 -[X in X < _]add0n ltn_add2r expn_gt0. + rewrite -ltn_sqr expn_prod. + under eq_bigr do rewrite -expnM muln2 halfK. + apply: (@leq_ltn_trans + (\prod_(i < k) prime_seq i ^ (logn (prime_seq i) n))). + apply: leq_prod => i _. rewrite leq_exp2l; first exact: leq_subr. + by apply: prime_gt1; rewrite -mem_prime_seq inE. + apply: (@leq_ltn_trans n); last first. + apply: (ltn_trans (ltn_ord n)); rewrite /N. + rewrite -[X in X ^ 2]addn1 sqrnD exp1n addn1 -expnM mulnDl. + rewrite muln1 -expnS addn1 mul1n [in X in _ < X]mulnC. + by rewrite mul2n -addn1 leq_add2l// expn_gt0. + rewrite [X in _ <= X]prod_prime_decomp ?lt0n// prime_decompE big_map /=. + rewrite -(big_mkord predT (fun i => + (prime_seq i) ^ logn (prime_seq i) n)) -(big_map prime_seq predT + (fun i => i ^ logn i n)) /=. + rewrite (bigID (mem (primes n))) /=. + rewrite [X in _ * X]big1 => [|i inotinprimesn]; last first. + have [/predU1P[->|/eqP->]//|] := boolP ((i == 0) || (i == 1)). + move=> /norP[ineq0 ineq1]. + rewrite -(expn0 i); apply/eqP; rewrite eqn_exp2l. + apply/eqP; move: inotinprimesn. + by rewrite -logn_gt0 lt0n negbK => /eqP. + by rewrite ltn_neqAle lt0n ineq0 eq_sym ineq1. + rewrite muln1 -big_filter. + have [nltk|klen] := ltnP n k; first by rewrite (eqseq n). + rewrite -[in X in _ <= X](eqseq n n.+1); last exact: ltnSn. + rewrite -[X in index_iota _ X.+1](subnKC (leq_trans klen (ltnSn n))). + rewrite -addnS -subSn//. + rewrite !big_filter /index_iota !subn0 iotaD map_cat big_cat add0n /=. + by apply/leq_pmulr/prodn_gt0 => i; exact: pfactor_gt0. +set f : 'I_N.+1 -> A * B := fun n => ([tuple a n i | i < k], Ordinal (binB n)). +set g : A * B -> nat := fun c => let (a, b) := c in + b ^ 2 * \prod_(i < k) (prime_seq i) ^ (tnth a i). +have finj x y : x \in P' k N -> y \in P' k N -> f x = f y -> x = y. + move=> xinPkN yinPkN /(congr1 g). + suff: forall x, x \in P' k N -> g (f x) = x. + by move=> /[dup] /(_ _ xinPkN) -> /(_ _ yinPkN) ->; apply: val_inj. + move=> {yinPkN y} {}x {}xinPkN /=. + rewrite expn_prod. + under eq_bigr do rewrite -expnM muln2 halfK. + rewrite -big_split /=. + under eq_bigr => i _. + rewrite -expnD tnth_mktuple /a subnK. + over. + by case: (boolP (odd (logn (prime_seq i) x))); first exact: odd_gt0. + have [xeq0|xneq0] := eqVneq x ord0. + by move: xeq0 xinPkN => ->; rewrite /P' !inE. + rewrite [RHS]prod_prime_decomp ?lt0n// prime_decompE big_map /=. + rewrite [in LHS](bigID (fun i : 'I_k => prime_seq i \in primes x)) /=. + under [X in _ * X = _]eq_bigr => i. + rewrite mem_primes lognE => /negbTE ->. + rewrite expn0; over. + rewrite big1_eq muln1 -(big_map _ (fun i => prime_seq i \in primes x) + (fun i => prime_seq i ^ logn (prime_seq i) x)) + -(big_map _ _ (fun j => j ^ logn j x)) -big_filter. + apply: congr_big => //. + rewrite -map_comp functions.compE. + apply: lt_sorted_eq => [||elt]. + - apply: lt_sorted_filter. + rewrite map_comp sorted_map -[X in map _ X]filter_predT val_enum_ord. + apply: (@sub_sorted _ ltn); last exact: iota_ltn_sorted. + rewrite ltEnat => i j /=. + by rewrite (leqW_mono leq_prime_seq). + - exact: sorted_primes. + rewrite mem_filter; apply: andb_idr. + move: xinPkN; rewrite /P' /P inE => /andP[_]. + rewrite inE => /allP primesxlepk eltinprimesx. + have [] : prime elt /\ elt < prime_seq k. + split; last exact: primesxlepk. + by apply/(@allP _ _ (primes x)) => //; exact: all_prime_primes. + rewrite -mem_prime_seq inE => /= -[i _ <-] pilepk. + rewrite map_comp; apply: map_f. + rewrite -[X in map _ X]filter_predT val_enum_ord mem_iota /= add0n. + by rewrite -(leqW_mono leq_prime_seq). +have -> : P k N = P' k N :|: [set ord0]. + by rewrite /P' finset.setUC finset.setD1K // inE. +rewrite finset.setUC cardsU1 [in X in X + _]/P' !inE /= add1n ltnS. +rewrite -(card_in_imset finj). +have imfleqAB : + #|[set f x | x in P' k N]| <= #|finset.setX [set: A] (~: [set ord0 : B])|. + apply/subset_leq_card/fintype.subsetP => y. + rewrite !inE => /imsetP [] x xinPkN -> /=. + apply: (contra_not_neq (@congr1 _ _ val _ _)) => /=. + apply/eqP; rewrite -lt0n; apply: prodn_gt0 => i. + by rewrite expn_gt0 prime_gt0//= -mem_prime_seq inE. +apply: (leq_trans imfleqAB). +rewrite cardsX cardsE card_tuple card_bool cardsC1 card_ord. +by rewrite -expnD addnA addnn. +Qed. + +Theorem dvg_sum_inv_prime_seq (R : realType) : + (\sum_(0 <= i < n) (((prime_seq i)%:R : R)^-1)%:E)%R @[n --> \oo] --> +oo%E. +Proof. +set un := fun i => (((prime_seq i)%:R : R)^-1)%:E. +set Sn := fun n => (\sum_(0 <= i < n) (un i))%R. +have unpos n : 0 <= n -> true -> (0 <= un n)%E => [_ _|]. + by rewrite /un lee_fin invr_ge0 ler0n. +have := is_cvg_nneseries unpos. +have := leey (limn Sn). +rewrite le_eqVlt => /predU1P[-> //|]. +have := nneseries_ge0 unpos. +move leqlimnSn : (limn Sn) => l. +case: l leqlimnSn => // l leqlimnSn _ _ /subsetP llimnSn. +have /llimnSn : `](l - (1/2))%:E, (l + (1/2))%:E[ \in nbhs (l%:E). + rewrite inE; exists (1/2)%R => /=; first exact: divr_gt0. + exact/subset_ball_prop_in_itv. +rewrite inE => -[] k /= _ /subsetP/(_ k). +set N := 2 ^ (k.*2 + 2). +set PN := P k N. +set GN := G k N. +rewrite inE /= leqnn set_interval.set_itvoo inE /= EFinB EFinD -leqlimnSn. +move=> /(_ erefl) /andP[+ _]. +rewrite lte_subel_addl; last by rewrite leqlimnSn. +rewrite -lteBlDr; last exact/sum_fin_numP. +rewrite (nneseries_split _ k); last by move=> k0 _; exact: unpos. +rewrite /Sn add0n addrAC subee; last exact/sum_fin_numP. +rewrite add0e => Rklthalf. +suff: N.+1 < N.+1 by rewrite ltnn. +rewrite -[X in X < _](cardPcardG k N). +have Neq : N./2 + (2 ^ (k.*2 + 1)).+1 = N.+1. + rewrite addnC addSn /N -divn2. + rewrite -[X in _ %/ X]expn1 -expnB //; last by rewrite addn2. + rewrite -addnBA /subn //= addnn. + by rewrite -mul2n -expnS -[X in 2 ^ X]addn1 -addnA. +rewrite -[X in _ < X]Neq -addSn. +apply: leq_add; last exact: cardP. +apply: (@cardG R); first by move: Rklthalf; rewrite /un div1r. +- rewrite /N; apply/leqW/(leq_trans (ltnW (ltn_expl k (ltnSn 1)))). + by rewrite leq_exp2l// -addnn -addnA leq_addr. +- by rewrite /N addn2 expnS mul2n odd_double. +- by rewrite /N expn_gt0. +Qed. + +End dvg_sum_inv_prime_seq. diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index 28d54db18..e265bb2ea 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -33,8 +33,7 @@ Variable (R : numDomainType). Lemma nbhs_filter (p : R^o) : ProperFilter (nbhs p). Proof. split. - move=> [] e e0 /subsetP/(_ p). - by rewrite !in_setE/= subrr normr0. + by move=> [] e e0 /subsetP/(_ p); rewrite !in_setE/= subrr normr0. split=> [|P Q|P Q]. - by exists 1; [exact: ltr01|exact: subsetT]. - move=> [] /= e e0 /subsetP eP [] /= f f0 /subsetP fQ. @@ -89,9 +88,9 @@ Proof. rewrite eqEsubset; split => U. case => _ /posnumP[e] xeU. exists (`]x - e%:num, x + e%:num[); first split; first by right. - by rewrite in_itv /= -real_lter_distl subrr // normr0. - apply: (subset_trans _ xeU) => z /=. - by rewrite in_itv /= -real_lter_distl //= distrC. + by rewrite in_itv/= -lter_distl subrr normr0. + apply: subset_trans xeU => z /=. + by rewrite in_itv /= -lter_distl distrC. case => [][[[]l|[]]] [[]r|[]] [[]]//= _. - move=> xlr lrU; exists (Order.min (x - l) (r - x)). by rewrite /= lt_min ?lterBDr ?add0r ?(itvP xlr). @@ -103,12 +102,12 @@ case => [][[[]l|[]]] [[]r|[]] [[]]//= _. - move=> xl lU; exists (x - l) => /=; first by rewrite lterBDr add0r (itvP xl). apply/(subset_trans _ lU)/subset_ball_prop_in_itv. suff : (`]x - (x - l), x + (x - l)[ <= `]l, +oo[)%O. - by move/subitvP => H ?; exact: H. + by move/subitvP => + ?; exact. by rewrite subitvE lteBSide/= subKr lexx. - move=> xr rU; exists (r - x) => /=; first by rewrite lterBDr add0r (itvP xr). apply/(subset_trans _ rU)/subset_ball_prop_in_itv. suff : (`]x - (r - x), x + (r - x)[ <= `]-oo, r[)%O. - by move/subitvP => H ?; exact: H. + by move/subitvP => + ?; exact. by rewrite subitvE lteBSide/= addrC subrK. - by move=> _; rewrite set_itvE subTset => ->; exists 1 => /=. Qed. @@ -131,12 +130,16 @@ HB.instance Definition _ (R : realFieldType) := PseudoPointedMetric.copy R R^o. HB.instance Definition _ (R : numClosedFieldType) := PseudoPointedMetric.copy R R^o. +#[export, non_forgetful_inheritance] +HB.instance Definition _ (R : numFieldType) := PseudoPointedMetric.copy R R^o. + #[export, non_forgetful_inheritance] HB.instance Definition _ (R : realFieldType) := Order_isNbhs.Build _ R (@real_order_nbhsE R). #[export, non_forgetful_inheritance] -HB.instance Definition _ (R : numFieldType) := PseudoPointedMetric.copy R R^o. +HB.instance Definition _ (R : realType) := + Order_isNbhs.Build _ R (@real_order_nbhsE R). Module Exports. HB.reexport. End Exports. diff --git a/theories/topology_theory/uniform_structure.v b/theories/topology_theory/uniform_structure.v index 611643c7d..51c439a41 100644 --- a/theories/topology_theory/uniform_structure.v +++ b/theories/topology_theory/uniform_structure.v @@ -284,6 +284,18 @@ rewrite !near_simpl near_withinE near_simpl => Pf; near=> y. by have [->|] := eqVneq y x; [by apply: nbhs_singleton|near: y]. Unshelve. all: by end_near. Qed. +Lemma continuous_injective_withinNx + (T U : topologicalType) (f : T -> U) (x : T) : + {for x, continuous f} -> + (forall y, f y = f x -> y = x) -> f @ x^' --> (f x)^'. +Proof. +move=> cf fI A; rewrite /nbhs /= /dnbhs !withinE/= => -[V Vfx AV]. +exists (f @^-1` V); first exact: cf Vfx. +by apply/seteqP; split=> y/=; + move/predeqP : AV => /(_ (f y))/= AV [AVfy yx]; + have /contra_neq /(_ yx) := fI y; tauto. +Qed. + (* This property is primarily useful for metrizability on uniform spaces *) Definition countable_uniformity (T : uniformType) := exists R : set_system (T * T), [/\