fix definition of concat

Sadol/Automatic.lean

@@ -102,11 +102,9 @@ def concat {α: Type u} {P Q: Language.Lang α} (p: Lang P) (q: Lang Q): Lang (L
   -- δ (p ⋆ q) a = δ⋆ ◂ (ν p · δ q a ∪ δ p a ⋆ q)
   (derive := fun (a: α) =>
     (iso Calculus.derive_concat
-      (scalar (null p)
-        (or
-          (derive q a)
-          (concat (derive p a) q)
-        )
+      (or
+        (scalar (null p) (derive q a))
+        (concat (derive p a) q)
       )
     )
   )

Sadol/Calculus.lean

@@ -276,7 +276,7 @@ def derive_scalar {α: Type u} {a: α} {s: Type u} {P: Lang α}:
 --   (λ { (([] , .(a ∷ w)) , refl , νP , Qaw) → refl
 --      ; ((.a ∷ u , v) , refl , Pu , Qv) → refl })
 def derive_concat {α: Type u} {a: α} {P Q: Lang α} {w: List α}:
-  (derive (concat P Q) a) w <=> (scalar (null P) (or (derive Q a) (concat (derive P a) Q))) w := by
+  (derive (concat P Q) a) w <=> (or (scalar (null P) (derive Q a)) (concat (derive P a) Q)) w := by
   refine TEquiv.mk ?toFun ?invFun ?leftInv ?rightInv
   case toFun =>
     -- TODO: The proof is complicated enough in Agda to warrant the liberal use of tactics in Lean

Sadol/Language.lean

@@ -70,7 +70,7 @@ inductive All {α: Type u} (P : α -> Type u) : (List α -> Type u) where
 -- (P ☆) w = ∃ λ ws → (w ≡ concat ws) × All P ws
 def star {α: Type u} (P : Lang α) : Lang α :=
   fun (w : List α) =>
-    Σ' (ws : List (List α)), (_pws: All P ws) ×' w = (List.join ws)
+    Σ' (ws : List (List α)), (_pws: All P ws) ×' w = (List.flatten ws)
 
 -- attribute [simp] allows these definitions to be unfolded when using the simp tactic.
 attribute [simp] universal emptyset emptystr char scalar or and concat star

Sadol/Symbolic.lean

@@ -86,11 +86,9 @@ def derive [Decidability.DecEq α] (l: Lang P) (a: α): Lang (Calculus.derive P
   -- δ (p ⋆ q) a = δ⋆ ◂ (ν p · δ q a ∪ δ p a ⋆ q)
   | concat p q =>
     (iso Calculus.derive_concat
-      (scalar (null p)
-        (or
-          (derive q a)
-          (concat (derive p a) q)
-        )
+      (or
+        (scalar (null p) (derive q a))
+        (concat (derive p a) q)
       )
     )
   -- δ (p ☆) a = δ☆ ◂ (ν p ✶‽ · (δ p a ⋆ p ☆))

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.11.0-rc2
+leanprover/lean4:v4.14.0