From bfe0e6d9b65187144996f0ce02954885769b4167 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Mon, 22 Jul 2024 12:44:37 +0200
Subject: [PATCH 1/3] add definition and result about regexp derivatives,
 rename cat-based residual to avoid name shadowing

---
 theories/dfa.v    | 16 ++++++-------
 theories/regexp.v | 61 +++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 69 insertions(+), 8 deletions(-)

diff --git a/theories/dfa.v b/theories/dfa.v
index e855872..b7eb16c 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_cat 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_catP (f : nat -> word char) (L : lang char) :
+    (forall n1 n2, residual_cat L (f n1) =p residual_cat 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_cat !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_catP 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.

From 6b1a61bb289994ca1d9ed58073740cfe1764b891 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Mon, 22 Jul 2024 13:00:26 +0200
Subject: [PATCH 2/3] remove nix-action-master CI for now

---
 .github/workflows/nix-action-master.yml | 309 ------------------------
 1 file changed, 309 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

From eb70236e98b83b9409ff0a7a70abccfb71f8ee14 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Mon, 22 Jul 2024 13:14:27 +0200
Subject: [PATCH 3/3] rename residual_cat to residual_lang

---
 theories/dfa.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/dfa.v b/theories/dfa.v
index b7eb16c..cff26a9 100644
--- a/theories/dfa.v
+++ b/theories/dfa.v
@@ -421,10 +421,10 @@ Section NonRegular.
 
   Implicit Types (L : lang char).
 
-  Definition residual_cat L x := fun y => L (x ++ y).
+  Definition residual_lang L x := fun y => L (x ++ y).
 
-  Lemma residual_catP (f : nat -> word char) (L : lang char) :
-    (forall n1 n2, residual_cat L (f n1) =p residual_cat 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]].
@@ -432,7 +432,7 @@ Section NonRegular.
     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_cat !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: (@residual_catP 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.