From 564ae2227faffd80e21089bcb98c011839183c8d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 17 Nov 2023 11:38:39 +0900 Subject: [PATCH] rebase wrt 0.6.6 --- .github/workflows/docker-action.yml | 4 - .github/workflows/nix-action-8.14.yml | 201 -------------------------- .github/workflows/nix-action-8.15.yml | 201 -------------------------- coq-mathcomp-classical.opam | 2 +- theories/lang_syntax.v | 10 +- theories/lang_syntax_examples.v | 51 ++++--- theories/lang_syntax_toy.v | 2 +- theories/prob_lang.v | 24 +-- theories/prob_lang_wip.v | 6 +- 9 files changed, 47 insertions(+), 454 deletions(-) delete mode 100644 .github/workflows/nix-action-8.14.yml delete mode 100644 .github/workflows/nix-action-8.15.yml diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index efe7aa0b9..1590dc370 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -15,11 +15,7 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:1.15.0-coq-8.14' - - 'mathcomp/mathcomp:1.15.0-coq-8.15' - 'mathcomp/mathcomp:1.15.0-coq-8.16' - - 'mathcomp/mathcomp:1.16.0-coq-8.14' - - 'mathcomp/mathcomp:1.17.0-coq-8.15' - 'mathcomp/mathcomp:1.17.0-coq-8.16' - 'mathcomp/mathcomp:1.17.0-coq-8.17' fail-fast: false diff --git a/.github/workflows/nix-action-8.14.yml b/.github/workflows/nix-action-8.14.yml deleted file mode 100644 index fc1f56e3d..000000000 --- a/.github/workflows/nix-action-8.14.yml +++ /dev/null @@ -1,201 +0,0 @@ -jobs: - coq: - needs: [] - 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@v3 - 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@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.14\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ - s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "coq" - mathcomp-analysis: - 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@v3 - 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@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-analysis - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.14\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-classical' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "mathcomp-classical" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "mathcomp-bigenough" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "mathcomp-analysis" - mathcomp-analysis-single: - 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@v3 - 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@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-analysis-single - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.14\" --argstr job \"mathcomp-analysis-single\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "mathcomp-finmap" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "mathcomp-bigenough" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "mathcomp-analysis-single" -name: Nix CI for bundle 8.14 -'on': - pull_request: - paths: - - .github/workflows/** - pull_request_target: - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-8.15.yml b/.github/workflows/nix-action-8.15.yml deleted file mode 100644 index 379319f42..000000000 --- a/.github/workflows/nix-action-8.15.yml +++ /dev/null @@ -1,201 +0,0 @@ -jobs: - coq: - needs: [] - 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@v3 - 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@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.15\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ - s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.15" --argstr - job "coq" - mathcomp-analysis: - 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@v3 - 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@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-analysis - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.15\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.15" --argstr - job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-classical' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.15" --argstr - job "mathcomp-classical" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.15" --argstr - job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.15" --argstr - job "mathcomp-bigenough" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.15" --argstr - job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.15" --argstr - job "mathcomp-analysis" - mathcomp-analysis-single: - 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@v3 - 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@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-analysis-single - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.15\" --argstr job \"mathcomp-analysis-single\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.15" --argstr - job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.15" --argstr - job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.15" --argstr - job "mathcomp-finmap" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.15" --argstr - job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.15" --argstr - job "mathcomp-bigenough" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.15" --argstr - job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.15" --argstr - job "mathcomp-analysis-single" -name: Nix CI for bundle 8.15 -'on': - pull_request: - paths: - - .github/workflows/** - pull_request_target: - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/coq-mathcomp-classical.opam b/coq-mathcomp-classical.opam index 463a8dfa5..0e0bc72a6 100644 --- a/coq-mathcomp-classical.opam +++ b/coq-mathcomp-classical.opam @@ -18,7 +18,7 @@ the Coq proof-assistant and using the Mathematical Components library.""" build: [make "-C" "classical" "-j%{jobs}%"] install: [make "-C" "classical" "install"] depends: [ - "coq" { (>= "8.14" & < "8.19~") | (= "dev") } + "coq" { (>= "8.16" & < "8.19~") | (= "dev") } "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.19~") | (= "dev") } "coq-mathcomp-fingroup" "coq-mathcomp-algebra" diff --git a/theories/lang_syntax.v b/theories/lang_syntax.v index ac3c32e4f..a00996cb8 100644 --- a/theories/lang_syntax.v +++ b/theories/lang_syntax.v @@ -1,8 +1,8 @@ Require Import String. From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. -From mathcomp.classical Require Import mathcomp_extra boolp classical_sets. -From mathcomp.classical Require Import functions cardinality fsbigop. +From mathcomp Require Import mathcomp_extra boolp classical_sets. +From mathcomp Require Import functions cardinality fsbigop. Require Import signed reals ereal topology normedtype sequences esum measure. Require Import lebesgue_measure numfun lebesgue_integral kernel prob_lang. Require Import lang_syntax_util. @@ -89,7 +89,7 @@ Proof. done. Qed. Let mswap_sigma_additive x : semi_sigma_additive (mswap x). Proof. exact: measure_semi_sigma_additive. Qed. -HB.instance Definition _ x := isMeasure.Build _ R _ +HB.instance Definition _ x := isMeasure.Build _ _ R (mswap x) (mswap0 x) (mswap_ge0 x) (@mswap_sigma_additive x). Definition mkswap : _ -> {measure set Z -> \bar R} := @@ -185,7 +185,7 @@ Let T0 z : (T' z) set0 = 0. Proof. by []. Qed. Let T_ge0 z x : 0 <= (T' z) x. Proof. by []. Qed. Let T_semi_sigma_additive z : semi_sigma_additive (T' z). Proof. exact: measure_semi_sigma_additive. Qed. -HB.instance Definition _ z := @isMeasure.Build _ R X (T' z) (T0 z) (T_ge0 z) +HB.instance Definition _ z := @isMeasure.Build _ X R (T' z) (T0 z) (T_ge0 z) (@T_semi_sigma_additive z). Let sfinT z : sfinite_measure (T' z). Proof. exact: sfinite_kernel_measure. Qed. @@ -197,7 +197,7 @@ Let U0 z : (U' z) set0 = 0. Proof. by []. Qed. Let U_ge0 z x : 0 <= (U' z) x. Proof. by []. Qed. Let U_semi_sigma_additive z : semi_sigma_additive (U' z). Proof. exact: measure_semi_sigma_additive. Qed. -HB.instance Definition _ z := @isMeasure.Build _ R Y (U' z) (U0 z) (U_ge0 z) +HB.instance Definition _ z := @isMeasure.Build _ Y R (U' z) (U0 z) (U_ge0 z) (@U_semi_sigma_additive z). Let sfinU z : sfinite_measure (U' z). Proof. exact: sfinite_kernel_measure. Qed. diff --git a/theories/lang_syntax_examples.v b/theories/lang_syntax_examples.v index d4262f995..4be13e9c5 100644 --- a/theories/lang_syntax_examples.v +++ b/theories/lang_syntax_examples.v @@ -59,7 +59,7 @@ Lemma letin'_sample_bernoulli d d' (T : measurableType d) Proof. rewrite letin'E/=. rewrite ge0_integral_measure_sum// 2!big_ord_recl/= big_ord0 adde0/=. -by rewrite !ge0_integral_mscale//= !integral_dirac//= indicT 2!mul1e. +by rewrite !ge0_integral_mscale//= !integral_dirac//= !diracT 2!mul1e. Qed. Section letin'_return. @@ -81,7 +81,7 @@ Lemma letin'_retk (f : X -> Y) (mf : measurable_fun setT f) (k : R.-sfker Y * X ~> Z) x U : measurable U -> letin' (ret mf) k x U = k (f x, x) U. Proof. -move=> mU; rewrite letin'E retE integral_dirac ?indicT ?mul1e//. +move=> mU; rewrite letin'E retE integral_dirac ?diracT ?mul1e//. exact: (measurableT_comp (measurable_kernel k _ mU)). Qed. @@ -218,9 +218,9 @@ Proof. rewrite !execP_letin !execP_sample !execD_bernoulli execP_return /=. rewrite execD_pair !exp_var'E (execD_var_erefl "x") (execD_var_erefl "y") /=. rewrite letin'E integral_measure_add//= !ge0_integral_mscale//= /onem. -rewrite !integral_dirac//= !indicE !in_setT/= !mul1e. +rewrite !integral_dirac//= !diracT !mul1e. rewrite !letin'E !integral_measure_add//= !ge0_integral_mscale//= /onem. -by rewrite !integral_dirac//= !indicE !in_setT/= !mul1e !diracE. +by rewrite !integral_dirac//= !diracT !mul1e. Qed. Lemma exec_sample_pair0_TandT : @@ -266,9 +266,9 @@ Proof. rewrite !execP_letin !execP_sample !execD_bernoulli execP_return /=. rewrite (@execD_bin _ _ binop_and) !exp_var'E (execD_var_erefl "x") (execD_var_erefl "y") /=. rewrite letin'E integral_measure_add//= !ge0_integral_mscale//= /onem. -rewrite !integral_dirac//= !indicE !in_setT/= !mul1e. +rewrite !integral_dirac//= !diracT !mul1e. rewrite !letin'E !integral_measure_add//= !ge0_integral_mscale//= /onem. -rewrite !integral_dirac//= !indicE !in_setT/= !mul1e !diracE. +rewrite !integral_dirac//= !diracT !mul1e. rewrite muleDr// -addeA; congr (_ + _)%E. by rewrite !muleA; congr (_%:E); congr (_ * _); field. rewrite -muleDl// !muleA -muleDl//. @@ -289,11 +289,11 @@ rewrite !execP_letin !execP_sample !execD_bernoulli execP_return /=. rewrite !(@execD_bin _ _ binop_and) !exp_var'E. rewrite (execD_var_erefl "x") (execD_var_erefl "y") (execD_var_erefl "z") /=. rewrite letin'E integral_measure_add//= !ge0_integral_mscale//= /onem. -rewrite !integral_dirac//= !indicE !in_setT/= !mul1e. +rewrite !integral_dirac//= !diracT !mul1e. rewrite !letin'E !integral_measure_add//= !ge0_integral_mscale//= /onem. -rewrite !integral_dirac//= !indicE !in_setT/= !mul1e. +rewrite !integral_dirac//= !diracT !mul1e. rewrite !letin'E !integral_measure_add//= !ge0_integral_mscale//= /onem. -rewrite !integral_dirac//= !indicE !in_setT/= !mul1e !diracE. +rewrite !integral_dirac//= !diracT !mul1e. rewrite !muleDr// -!addeA. by congr (_ + _)%E; rewrite ?addeA !muleA -?muleDl//; congr (_ * _)%E; congr (_%:E); field. @@ -336,24 +336,23 @@ rewrite !integral_measure_add //=; last by move=> b _; rewrite integral_ge0. rewrite !ge0_integral_mscale //=; last 2 first. by move=> b _; rewrite integral_ge0. by move=> b _; rewrite integral_ge0. -rewrite !integral_dirac// !indicE !in_setT !mul1e. +rewrite !integral_dirac// !diracT !mul1e. rewrite iteE/= !ge0_integral_mscale//=. rewrite ger0_norm//. rewrite !integral_indic//= !iteE/= /mscale/=. -rewrite setTI diracE !in_setT !mule1. +rewrite setTI !diracT !mule1. rewrite ger0_norm//. rewrite -EFinD/= eqe ifF; last first. by apply/negbTE/negP => /orP[/eqP|//]; rewrite /onem; lra. rewrite !letin'E/= !iteE/=. rewrite !ge0_integral_mscale//=. rewrite ger0_norm//. -rewrite !integral_dirac//= !indicE !in_setT /= !mul1e ger0_norm//. +rewrite !integral_dirac//= !diracT !mul1e ger0_norm//. rewrite exp_var'E (execD_var_erefl "x")/=. rewrite /bernoulli/= measure_addE/= /mscale/= !mul1r. -rewrite muleDl//; congr (_ + _)%E; - rewrite -!EFinM; - congr (_%:E); - by rewrite indicE /onem; case: (_ \in _); field. +by rewrite muleDl//; congr (_ + _)%E; + rewrite -!EFinM; congr (_%:E); + rewrite !indicT !indicE /onem /=; case: (_ \in _); field. Qed. Definition bernoulli12_score := [Normalize @@ -379,11 +378,11 @@ rewrite !integral_measure_add //=; last by move=> b _; rewrite integral_ge0. rewrite !ge0_integral_mscale //=; last 2 first. by move=> b _; rewrite integral_ge0. by move=> b _; rewrite integral_ge0. -rewrite !integral_dirac// !indicE !in_setT !mul1e. +rewrite !integral_dirac// !diracT !mul1e. rewrite iteE/= !ge0_integral_mscale//=. rewrite ger0_norm//. rewrite !integral_indic//= !iteE/= /mscale/=. -rewrite setTI diracE !in_setT !mule1. +rewrite setTI !diracT !mule1. rewrite ger0_norm//. rewrite -EFinD/= eqe ifF; last first. apply/negbTE/negP => /orP[/eqP|//]. @@ -391,13 +390,13 @@ rewrite -EFinD/= eqe ifF; last first. rewrite !letin'E/= !iteE/=. rewrite !ge0_integral_mscale//=. rewrite ger0_norm//. -rewrite !integral_dirac//= !indicE !in_setT /= !mul1e ger0_norm//. +rewrite !integral_dirac//= !diracT !mul1e ger0_norm//. rewrite exp_var'E (execD_var_erefl "x")/=. rewrite /bernoulli/= measure_addE/= /mscale/= !mul1r. rewrite muleDl//; congr (_ + _)%E; rewrite -!EFinM; congr (_%:E); - by rewrite indicE /onem; case: (_ \in _); field. + by rewrite !indicT !indicE /onem /=; case: (_ \in _); field. Qed. (* https://dl.acm.org/doi/pdf/10.1145/2933575.2935313 (Sect. 4) *) @@ -428,11 +427,11 @@ rewrite !integral_measure_add //=; last by move=> b _; rewrite integral_ge0. rewrite !ge0_integral_mscale //=; last 2 first. by move=> b _; exact: integral_ge0. by move=> b _; exact: integral_ge0. -rewrite !integral_dirac// !indicE !in_setT !mul1e. +rewrite !integral_dirac// !diracT !mul1e. rewrite iteE/= !ge0_integral_mscale//=. rewrite ger0_norm//. -rewrite !integral_indic//= !iteE/= /mscale/=. -rewrite setTI diracE !in_setT !mule1. +rewrite !integral_cst//= !diracT !(mule1,mul1e). +rewrite !iteE/= /mscale/= !diracT !mule1. rewrite ger0_norm//. rewrite -EFinD/= eqe ifF; last first. apply/negbTE/negP => /orP[/eqP|//]. @@ -440,12 +439,12 @@ rewrite -EFinD/= eqe ifF; last first. rewrite !letin'E/= !iteE/=. rewrite !ge0_integral_mscale//=. rewrite ger0_norm//. -rewrite !integral_dirac//= !indicE !in_setT /= !mul1e ger0_norm//. +rewrite !integral_dirac//= !diracT !mul1e ger0_norm//. rewrite /bernoulli/= measure_addE/= /mscale/= !mul1r. rewrite muleDl//; congr (_ + _)%E; rewrite -!EFinM; congr (_%:E); - by rewrite indicE /onem; case: (_ \in _); field. + by rewrite !indicT !indicE /onem /=; case: (_ \in _); field. Qed. End bernoulli_examples. @@ -473,7 +472,7 @@ Proof. apply/eq_sfkernel => x U. rewrite letin'E/= /sample; unlock. rewrite integral_measure_add//= ge0_integral_mscale//= ge0_integral_mscale//=. -rewrite integral_dirac//= integral_dirac//= !indicT/= !mul1e. +rewrite !integral_dirac//= !diracT/= !mul1e. by rewrite /mscale/= iteE//= iteE//= fail'E mule0 adde0 ger0_norm. Qed. diff --git a/theories/lang_syntax_toy.v b/theories/lang_syntax_toy.v index a328ea1cd..9e0bdfd84 100644 --- a/theories/lang_syntax_toy.v +++ b/theories/lang_syntax_toy.v @@ -1,7 +1,7 @@ Require Import String Classical. From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg. -From mathcomp.classical Require Import mathcomp_extra boolp. +From mathcomp Require Import mathcomp_extra boolp. Require Import signed reals topology normedtype. Require Import lang_syntax_util. diff --git a/theories/prob_lang.v b/theories/prob_lang.v index d870d5072..bfd5adfba 100644 --- a/theories/prob_lang.v +++ b/theories/prob_lang.v @@ -2,10 +2,10 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import rat. -From mathcomp.classical Require Import mathcomp_extra boolp classical_sets. -From mathcomp.classical Require Import functions cardinality fsbigop. +From mathcomp Require Import mathcomp_extra boolp classical_sets. +From mathcomp Require Import functions cardinality fsbigop. Require Import reals ereal signed topology normedtype sequences esum measure. -Require Import lebesgue_measure numfun lebesgue_integral exp kernel. +Require Import lebesgue_measure numfun lebesgue_integral exp kernel. (******************************************************************************) (* Semantics of a probabilistic programming language using s-finite kernels *) @@ -116,7 +116,7 @@ Lemma integral_bernoulli {R : realType} Proof. move=> f0. rewrite ge0_integral_measure_sum// 2!big_ord_recl/= big_ord0 adde0/=. -by rewrite !ge0_integral_mscale//= !integral_dirac//= indicT 2!mul1e. +by rewrite !ge0_integral_mscale//= !integral_dirac//= !diracT !mul1e. Qed. Section uniform_probability. @@ -131,7 +131,7 @@ HB.instance Definition _ := Measure.on uniform_probability. Let uniform_probability_setT : uniform_probability [set: _] = 1. Proof. rewrite /uniform_probability /mscale/= /mrestr/=. -rewrite setTI lebesgue_measure_itv hlength_itv/= lte_fin. +rewrite setTI lebesgue_measure_itv/= lte_fin. by rewrite -subr_gt0 ab0 -EFinD -EFinM mulVf// gt_eqF// subr_gt0. Qed. @@ -528,7 +528,7 @@ Proof. apply/eq_measure/funext => U. rewrite /ite; unlock => /=. rewrite /kcomp/= integral_dirac//=. -rewrite indicT mul1e. +rewrite diracT mul1e. rewrite -/(measure_add (ITE.kiteT k1 (x, f x)) (ITE.kiteF k2 (x, f x))). rewrite measure_addE. rewrite /ITE.kiteT /ITE.kiteF/=. @@ -588,7 +588,7 @@ Lemma letin_retk x U : measurable U -> letin (ret mf) k x U = k (x, f x) U. Proof. -move=> mU; rewrite letinE retE integral_dirac ?indicT ?mul1e//. +move=> mU; rewrite letinE retE integral_dirac ?diracT ?mul1e//. exact: (measurableT_comp (measurable_kernel k _ mU)). Qed. @@ -893,7 +893,7 @@ Let kcomp_scoreE d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (score mf \; g) r U = `|f r|%:E * g (r, tt) U. Proof. rewrite /= /kcomp /kscore /= ge0_integral_mscale//=. -by rewrite integral_dirac// indicT mul1e. +by rewrite integral_dirac// diracT mul1e. Qed. Lemma scoreE d' (T' : measurableType d') (x : T * T') (U : set T') (f : R -> R) @@ -926,7 +926,7 @@ Proof. apply/eq_sfkernel => x U. rewrite letinE/= /sample; unlock. rewrite integral_measure_add//= ge0_integral_mscale//= ge0_integral_mscale//=. -rewrite integral_dirac//= integral_dirac//= !indicT/= !mul1e. +rewrite integral_dirac//= integral_dirac//= !diracT/= !mul1e. by rewrite /mscale/= iteE//= iteE//= failE mule0 adde0 ger0_norm. Qed. @@ -1004,7 +1004,7 @@ Let T0 z : (T z) set0 = 0. Proof. by []. Qed. Let T_ge0 z x : 0 <= (T z) x. Proof. by []. Qed. Let T_semi_sigma_additive z : semi_sigma_additive (T z). Proof. exact: measure_semi_sigma_additive. Qed. -HB.instance Definition _ z := @isMeasure.Build _ R X (T z) (T0 z) (T_ge0 z) +HB.instance Definition _ z := @isMeasure.Build _ X R (T z) (T0 z) (T_ge0 z) (@T_semi_sigma_additive z). Let sfinT z : sfinite_measure (T z). Proof. exact: sfinite_kernel_measure. Qed. @@ -1016,7 +1016,7 @@ Let U0 z : (U z) set0 = 0. Proof. by []. Qed. Let U_ge0 z x : 0 <= (U z) x. Proof. by []. Qed. Let U_semi_sigma_additive z : semi_sigma_additive (U z). Proof. exact: measure_semi_sigma_additive. Qed. -HB.instance Definition _ z := @isMeasure.Build _ R Y (U z) (U0 z) (U_ge0 z) +HB.instance Definition _ z := @isMeasure.Build _ Y R (U z) (U0 z) (U_ge0 z) (@U_semi_sigma_additive z). Let sfinU z : sfinite_measure (U z). Proof. exact: sfinite_kernel_measure. Qed. @@ -1145,7 +1145,7 @@ Lemma letin_sample_bernoulli d d' (T : measurableType d) Proof. rewrite letinE/=. rewrite ge0_integral_measure_sum// 2!big_ord_recl/= big_ord0 adde0/=. -by rewrite !ge0_integral_mscale//= !integral_dirac//= indicT 2!mul1e. +by rewrite !ge0_integral_mscale//= !integral_dirac//= !diracT 2!mul1e. Qed. Section sample_and_return. diff --git a/theories/prob_lang_wip.v b/theories/prob_lang_wip.v index 9ab73014b..cdc372e59 100644 --- a/theories/prob_lang_wip.v +++ b/theories/prob_lang_wip.v @@ -1,8 +1,8 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import rat. -From mathcomp.classical Require Import mathcomp_extra boolp classical_sets. -From mathcomp.classical Require Import functions cardinality fsbigop. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality fsbigop. Require Import signed reals ereal topology normedtype sequences esum measure. Require Import lebesgue_measure numfun lebesgue_integral exp kernel trigo. Require Import prob_lang. @@ -142,7 +142,7 @@ transitivity (\int[@mgauss01 R]_(y in U) (f1 y)%:E). apply: eq_integral => //= r. rewrite letinE/= ge0_integral_mscale//= ger0_norm//; last first. by rewrite invr_ge0// gauss_density_ge0. - by rewrite integral_dirac// indicT mul1e diracE indicE. + by rewrite integral_dirac// diracT mul1e diracE indicE. rewrite integral_mgauss01//. transitivity (\int[lebesgue_measure]_(x in U) (\1_U x)%:E). apply: eq_integral => /= y yU.