From 8b6b8a31f396b2ed88b314bb0c0373c4964d16df Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Mon, 22 Jul 2024 15:29:32 +0200 Subject: [PATCH] add definition and result about regexp derivatives (#73) * add definition and result about regexp derivatives, rename cat-based residual to avoid name shadowing * remove nix-action-master CI for now * rename residual_cat to residual_lang --- .github/workflows/nix-action-master.yml | 309 ------------------------ theories/dfa.v | 16 +- theories/regexp.v | 61 +++++ 3 files changed, 69 insertions(+), 317 deletions(-) delete mode 100644 .github/workflows/nix-action-master.yml diff --git a/.github/workflows/nix-action-master.yml b/.github/workflows/nix-action-master.yml deleted file mode 100644 index b22092a..0000000 --- a/.github/workflows/nix-action-master.yml +++ /dev/null @@ -1,309 +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 coq-community - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, math-comp - name: coq-community - - 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 \"master\" --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 "master" - --argstr job "coq" - coq-elpi: - 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 coq-community - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, math-comp - name: coq-community - - id: stepCheck - name: Checking presence of CI target coq-elpi - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"master\" --argstr job \"coq-elpi\" \\\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 "master" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" - --argstr job "coq-elpi" - hierarchy-builder: - needs: - - coq - - coq-elpi - 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 coq-community - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, math-comp - name: coq-community - - id: stepCheck - name: Checking presence of CI target hierarchy-builder - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"master\" --argstr job \"hierarchy-builder\" \\\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 "master" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq-elpi' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" - --argstr job "coq-elpi" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" - --argstr job "hierarchy-builder" - mathcomp: - needs: - - coq - - hierarchy-builder - 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 coq-community - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, math-comp - name: coq-community - - 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 \"master\" --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 "master" - --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 "master" - --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 "master" - --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 "master" - --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 "master" - --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 "master" - --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 "master" - --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 "master" - --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 "master" - --argstr job "mathcomp" - reglang: - 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 coq-community - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, math-comp - name: coq-community - - id: stepCheck - name: Checking presence of CI target reglang - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"master\" --argstr job \"reglang\" \\\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 "master" - --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 "master" - --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 "master" - --argstr job "reglang" -name: Nix CI for bundle master -'on': - pull_request: - paths: - - .github/workflows/nix-action-master.yml - pull_request_target: - paths-ignore: - - .github/workflows/nix-action-master.yml - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/theories/dfa.v b/theories/dfa.v index e855872..cff26a9 100644 --- a/theories/dfa.v +++ b/theories/dfa.v @@ -421,18 +421,18 @@ Section NonRegular. Implicit Types (L : lang char). - Definition residual L x := fun y => L (x ++ y). + Definition residual_lang L x := fun y => L (x ++ y). - Lemma residualP (f : nat -> word char) (L : lang char) : - (forall n1 n2, residual L (f n1) =p residual L (f n2) -> n1 = n2) -> + Lemma residual_langP (f : nat -> word char) (L : lang char) : + (forall n1 n2, residual_lang L (f n1) =p residual_lang L (f n2) -> n1 = n2) -> ~ inhabited (regular L). Proof. move => f_spec [[A E]]. - pose f' (n : 'I_#|A|.+1) := delta_s A (f n). - suff: injective f' by move/leq_card; rewrite card_ord ltnn. - move => [n1 H1] [n2 H2]. rewrite /f' /delta_s /= => H. + pose g (n : 'I_#|A|.+1) := delta_s A (f n). + suff: injective g by move/leq_card; rewrite card_ord ltnn. + move => [n1 H1] [n2 H2]. rewrite /g /delta_s /= => H. apply/eqP; change (n1 == n2); apply/eqP. apply: f_spec => w. - by rewrite /residual !E !inE /dfa_accept !delta_cat H. + by rewrite /residual_lang !E !inE /dfa_accept !delta_cat H. Qed. Hypothesis (a b : char) (Hab : a != b). @@ -457,7 +457,7 @@ Section NonRegular. Lemma Lab_not_regular : ~ inhabited (regular Lab). Proof. pose f n := nseq n a. - apply: (@residualP f) => n1 n2. move/(_ (nseq n2 b)) => H. + apply: (@residual_langP f) => n1 n2. move/(_ (nseq n2 b)) => H. apply: Lab_eq. apply/H. by exists n2. Qed. diff --git a/theories/regexp.v b/theories/regexp.v index 43aefc5..f5c1caf 100644 --- a/theories/regexp.v +++ b/theories/regexp.v @@ -485,3 +485,64 @@ Qed. Lemma regular_rev (char : finType) (L : lang char) : regular L -> regular (fun x => L (rev x)). Proof. case/regularP => e H. apply/regularP. exists (Rev e) => x. by rewrite Rev_correct. Qed. + +(** ** Derivative of a regular expression *) + +Fixpoint has_eps (char : eqType) (e : regexp char) := + match e with + | Void => false + | Eps => true + | Atom x => false + | Star e1 => true + | Plus e1 e2 => has_eps e1 || has_eps e2 + | Conc e1 e2 => has_eps e1 && has_eps e2 + end. + +Lemma has_epsE (char : eqType) (e : regexp char) : + has_eps e = ([::] \in e). +Proof. + elim: e => //= [r hc1 c2 hc2|r hc1 c2 hc2]; first by rewrite hc1 hc2. + rewrite hc1 hc2 => //. rewrite -[xx in _ = xx] topredE /=. + by apply/idP/existsP; [exists ord0| case]. +Qed. + +Fixpoint der (char: eqType) x (e : regexp char) := + match e with + | Void => Void + | Eps => Void + | Atom y => if x == y then Eps else Void + | Star e1 => Conc (der x e1) (Star e1) + | Plus e1 e2 => Plus (der x e1) (der x e2) + | Conc e1 e2 => if has_eps e1 + then Plus (Conc (der x e1) e2) (der x e2) + else Conc (der x e1) e2 + end. + +Lemma derE (char : finType) (x : char) (e : regexp char) : + der x e =i residual x (mem e). +Proof. + elim: e => //= [y|e IHe|e1 IHe1 e2 IHe2|e1 IHe1 e2 IHe2] u. + - by rewrite 2!fun_if /=. + - by apply/concP/concP=> [] [v e_v]; exists v; rewrite // IHe in e_v *. + - by rewrite !inE IHe1 IHe2. + - case he: (has_eps e1). + + apply/orP/concP=> [[] | [[|y v]]] /=; rewrite -/re_lang. + * move/concP=> [w1 [w2 uw]]. + move: uw; rewrite IHe1 in_residual; move => [uw [w1e w2e]]. + by exists (x :: w1), w2; rewrite uw. + * move => hu. exists [::]. rewrite -has_epsE. + exists (x::u) => //. by rewrite -in_residual -IHe2. + * case=> w [def_w [_ e2w]]; right. + by rewrite IHe2 !inE def_w. + * case=> w [[xy uvw] [e1w e2w]]; left; apply/concP. + by exists v, w; rewrite IHe1 xy in_residual. + + apply/concP/concP => [[v] | ] /=; rewrite -/re_lang. + case=> w [uw [e1w e2w]]. + by exists (x :: v), w; rewrite uw -in_residual -IHe1. + + case; case => [|y v]; case => /= w [hv [he1 he2]]. + by move: he; rewrite has_epsE he1. + move/eqP: hv. + rewrite eqseq_cons. case/andP. + move/eqP => hx. move/eqP => hu. exists v. + by rewrite IHe1 in_residual hx; exists w. +Qed.