diff --git a/.github/workflows/nix-action-8.20.yml b/.github/workflows/nix-action-8.20.yml new file mode 100644 index 0000000..ae88475 --- /dev/null +++ b/.github/workflows/nix-action-8.20.yml @@ -0,0 +1,276 @@ +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@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@v30 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v15 + 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.20\" --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.20" --argstr + job "coq" + mathcomp: + 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@v30 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.20\" --argstr job \"mathcomp\" \\\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 previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "stdlib" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "mathcomp-fingroup" + - 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.20" --argstr + job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-solvable' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "mathcomp-solvable" + - 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.20" --argstr + job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-character' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "mathcomp-character" + - 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.20" --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.20" --argstr + job "mathcomp" + mathcomp-finmap: + 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@v30 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-finmap + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.20\" --argstr job \"mathcomp-finmap\" \\\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 previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "mathcomp-ssreflect" + - 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.20" --argstr + job "mathcomp-finmap" + multinomials: + needs: + - coq + - mathcomp-finmap + 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@v30 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target multinomials + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.20\" --argstr job \"multinomials\" \\\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 previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "mathcomp-ssreflect" + - 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.20" --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.20" --argstr + job "mathcomp-finmap" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "mathcomp-fingroup" + - 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.20" --argstr + job "mathcomp-bigenough" + - 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.20" --argstr + job "multinomials" +name: Nix CI for bundle 8.20 +on: + pull_request: + paths: + - .github/workflows/nix-action-8.20.yml + pull_request_target: + paths-ignore: + - .github/workflows/nix-action-8.20.yml + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.nix/config.nix b/.nix/config.nix index f2d16f2..01d96fc 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -75,6 +75,9 @@ "8.19".coqPackages = common-bundles // { coq.override.version = "8.19"; }; + "8.20".coqPackages = common-bundles // { + coq.override.version = "8.20"; + }; "master".coqPackages = { coq.override.version = "master"; coq-elpi.override.version = "coq-master"; diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f928dd8..0dae9da 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -5,7 +5,8 @@ ### Added - in `finmap.v`: - + lemmas `bigfcup_imfset`, `fbig_pred1_inj` + + lemmas `fset_seq1`, `imfset0`, `imfset_fset1`, `imfset_fset2`, `imfsetU`, + `imfsetU1`, `imfsetI`, `bigfcup_imfset` ### Changed diff --git a/finmap.v b/finmap.v index 67dc590..3911b52 100644 --- a/finmap.v +++ b/finmap.v @@ -5,7 +5,7 @@ From HB Require Import structures. Set Warnings "-notation-incompatible-format". From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq. Set Warnings "notation-incompatible-format". -From mathcomp Require Import choice path finset finfun fintype bigop. +From mathcomp Require Import choice finset finfun fintype bigop. (*****************************************************************************) (* This file provides representations for finite sets over a choiceType K, *) @@ -1606,6 +1606,11 @@ Proof. by apply/fsetP=> x; rewrite in_fset_cons !inE. Qed. Lemma fset_nil : [fset[key] x in [::] : seq K] = fset0. Proof. by apply/fsetP=> x; rewrite in_fset_nil. Qed. +Lemma fset_seq1 a : [:: a] = [fset a]. +Proof. +by rewrite (@perm_small_eq _ [fset a] [:: a])//; apply: uniq_perm=>// ? /[!inE]. +Qed. + Lemma fset_cat s s' : [fset[key] x in s ++ s'] = [fset[key] x in s] `|` [fset[key] x in s']. Proof. by apply/fsetP=> x; rewrite !inE !in_fset_cat. Qed. @@ -2131,7 +2136,7 @@ End Enum. Section ImfsetTh. Variables (key : unit) (K V V' : choiceType). -Implicit Types (f : K -> V) (g : V -> V') (A V : {fset K}). +Implicit Types (f : K -> V) (g : V -> V') (A B : {fset K}). Lemma imfset_id (A : {fset K}) : id @` A = A. Proof. by apply/fsetP=> a; rewrite in_fset. Qed. @@ -2159,6 +2164,39 @@ move=> eq_f eqP; apply/fsetP => x; apply/imfsetP/imfsetP => /= [] [k Pk ->]; by exists k => //=; rewrite ?eq_f ?eqP in Pk *. Qed. +Lemma imfsetU f A B : f @` (A `|` B) = f @` A `|` f @` B. +Proof. +apply/fsetP => v; apply/imfsetP/fsetUP. + by move=> [k /fsetUP [? ->|? ->]]; [left|right]; apply/imfsetP; exists k. +by move=> [|] /imfsetP /= [k kin ->]; exists k => //; rewrite inE kin ?orbT. +Qed. + +Lemma imfset0 f : f @` fset0 = fset0. +Proof. by apply/fsetP => v; apply/imfsetP; rewrite inE => -[k /[!inE]]. Qed. + +Lemma imfset_fset1 f x : f @` [fset x] = [fset f x]. +Proof. +apply/fsetP => y. +by apply/imfsetP/fset1P => [[x' /fset1P -> //]|->]; exists x; rewrite ?fset11. +Qed. + +Lemma imfset_fset2 f k1 k2 : f @` [fset k1; k2] = [fset f k1; f k2]. +Proof. by rewrite imfsetU 2!imfset_fset1. Qed. + +Lemma imfsetU1 f a A : f @` (a |` A) = f a |` (f @` A). +Proof. by rewrite imfsetU imfset_fset1. Qed. + +Lemma imfsetI f A B : + {in A & B, injective f} -> f @` (A `&` B) = f @` A `&` f @` B. +Proof. +move=> injf; apply/fsetP => v. +apply/imfsetP/fsetIP => /=. + by move=> [k /fsetIP [kinA kinB] ->]; split; apply/imfsetP; exists k. +move=> [/imfsetP /= [ka kainA eqka] /imfsetP /= [kb kbinB eqkb]]. +have eqk : ka = kb by apply: injf => //; rewrite -eqka -eqkb. +by exists ka => //; apply/fsetIP; split=> //; rewrite eqk. +Qed. + End ImfsetTh. Section PowerSetTheory. @@ -2477,15 +2515,29 @@ Qed. End BigFOpsSeq. -Lemma bigfcup_imfset1 (I T : choiceType) (P : {fset I}) (f : I -> T) : - \bigcup_(i <- P) [fset f i] = f @` P. +Section BigFOps. + +Variables (I T : choiceType). +Implicit Types (f : I -> T). + +Lemma bigfcup_imfset1 (P : {fset I}) f : \bigcup_(i <- P) [fset f i] = f @` P. Proof. apply/eqP; rewrite eqEfsubset; apply/andP; split; apply/fsubsetP => x. -- by case/bigfcupP=> i /andP [] iP _; rewrite inE => /eqP ->; apply/imfsetP; exists i. +- by case/bigfcupP=> i /andP [] iP _ /[!inE] /eqP ->; apply/imfsetP; exists i. - case/imfsetP => i /= iP ->; apply/bigfcupP; exists i; rewrite ?andbT //. by apply/imfsetP; exists (f i); rewrite ?inE. Qed. +Lemma bigfcup_imfset (V : choiceType) f (F : V -> {fset I}) (A : {fset V}): + \bigcup_(a <- A) f @` F a = f @` (\bigcup_(a <- A) F a). +Proof. +apply/fsetP => t; apply/bigfcupP/imfsetP. + by move=> [v ? /imfsetP [i ? ->]]; exists i => //; apply/bigfcupP; exists v. +by move=> [i /bigfcupP [v ? ?] ->]; exists v => //; apply/imfsetP; exists i. +Qed. + +End BigFOps. + Section fbig_pred1_inj. Variables (R : Type) (idx : R) (op : Monoid.com_law idx). diff --git a/multiset.v b/multiset.v index a665284..4107eb0 100644 --- a/multiset.v +++ b/multiset.v @@ -7,7 +7,7 @@ Set Warnings "-notation-incompatible-format". From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq. Set Warnings "notation-incompatible-format". -From mathcomp Require Import choice path finset finfun fintype bigop tuple. +From mathcomp Require Import choice finset finfun fintype bigop tuple. Require Import finmap. (*****************************************************************************)