rename residual_cat to residual_lang

coq-community · Jul 22, 2024 · eb70236 · eb70236
1 parent 6b1a61b
commit eb70236
Showing 1 changed file with 5 additions and 5 deletions.
diff --git a/theories/dfa.v b/theories/dfa.v
@@ -421,18 +421,18 @@ 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]].
     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_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.