remove some unsafe, but not all

Thank you @arthur-adjedj

README.md

@@ -100,18 +100,51 @@ We use explicit parameters and almost no module level parameters, for example `L
 
 ## The Non-Trivial difference from the Agda implementation
 
-[Automatic.lean](./Sodal/Automatic.lean) requires the use of `unsafe` to define `Automatic.Lang`:
+[Automatic.lean](./Sodal/Automatic.lean) has a lot of termination checking issues.
+We can safely define Automatic.Lang:
 
 ```lean
-unsafe
-inductive Lang {α: Type u} (R: Language.Lang α): Type (u) where
+inductive Lang {α: Type u} : Language.Lang α -> Type (u+1) where
   | mk
-   (null: Decidability.Dec (Calculus.null R))
-   (derive: (a: α) -> Lang (Calculus.derive R a))
-   : Lang R
+    (null: Decidability.Dec (Calculus.null R))
+    (derive: (a: α) -> Lang (Calculus.derive R a))
+    : Lang R
 ```
 
-Without `unsafe`, we get the following error: `"(kernel) arg #4 of 'Automatic.Lang.mk' contains a non valid occurrence of the datatypes being declared"`
+But when we try to instantiate it using any operator, we get termination checking issues, for example given `emptyset`:
+```
+-- ∅ : Lang ◇.∅
+def emptyset {α: Type u}: Lang (@Language.emptyset.{u} α) := Lang.mk
+  -- ν ∅ = ⊥‽
+  (null := Decidability.empty)
+  -- δ ∅ a = ∅
+  (derive := fun _ => emptyset)
+```
+
+We get the following error:
+```
+fail to show termination for
+  Automatic.emptyset
+with errors
+failed to infer structural recursion:
+Not considering parameter α of Automatic.emptyset:
+  it is unchanged in the recursive calls
+no parameters suitable for structural recursion
+
+well-founded recursion cannot be used, 'Automatic.emptyset' does not take any (non-fixed) arguments
+```
+
+Getting around this issue requires the use of `unsafe`:
+
+```
+-- ∅ : Lang ◇.∅
+unsafe -- failed to infer structural recursion
+def emptyset {α: Type u}: Lang (@Language.emptyset.{u} α) := Lang.mk
+  -- ν ∅ = ⊥‽
+  (null := Decidability.empty)
+  -- δ ∅ a = ∅
+  (derive := fun _ => emptyset)
+```
 
 This was probably inevitable, given that the Agda version of Lang in [Automatic.lagda](https://github.com/conal/paper-2021-language-derivatives/blob/main/Automatic.lagda#L40-L44) required coinduction, which is not a feature of Lean:
 
@@ -123,7 +156,7 @@ record Lang (P : ◇.Lang) : Set (suc ℓ) where
     δ : (a : A) → Lang (◇.δ P a)
 ```
 
-Also this representation encountered issues with Agda's termination checker, when defining the derivative of the concat operator, which was fixed using a sized version of the record:
+Also this representation encountered issues with Agda's termination checker, but only when defining the derivative of the concat operator, not all operators as in Lean, which was fixed using a sized version of the record:
 
 ```agda
 record Lang i (P : ◇.Lang) : Set (suc ℓ) where

Sadol/Automatic.lean

@@ -23,83 +23,79 @@ namespace Automatic
 --     ν : Dec (◇.ν P)
 --     δ : (a : A) → Lang (◇.δ P a)
 
-unsafe
--- we need "unsafe" otherwise we get the following error:
--- "(kernel) arg #4 of 'Automatic.Lang.mk' contains a non valid occurrence of the datatypes being declared"
-inductive Lang {α: Type u} (R: Language.Lang α): Type (u) where
+inductive Lang {α: Type u} : Language.Lang α -> Type (u+1) where
   | mk
-   (null: Decidability.Dec (Calculus.null R))
-   (derive: (a: α) -> Lang (Calculus.derive R a))
-   : Lang R
+    (null: Decidability.Dec (Calculus.null R))
+    (derive: (a: α) -> Lang (Calculus.derive R a))
+    : Lang R
 
-unsafe -- we need unsafe, since Automatic.Lang requires unsafe
 def null (l: Lang R): Decidability.Dec (Calculus.null R) :=
   match l with
   | Lang.mk n _ => n
 
-unsafe -- we need unsafe, since Automatic.Lang requires unsafe
 def derive {α: Type u} {R: Language.Lang α} (l: Lang R) (a: α): Lang (Calculus.derive R a) :=
   match l with
   | Lang.mk _ d => d a
 
 -- ∅ : Lang ◇.∅
-unsafe -- we need unsafe, since Automatic.Lang requires unsafe
+unsafe -- failed to infer structural recursion
 def emptyset {α: Type u}: Lang (@Language.emptyset.{u} α) := Lang.mk
   -- ν ∅ = ⊥‽
   (null := Decidability.empty)
   -- δ ∅ a = ∅
   (derive := fun _ => emptyset)
 
 -- 𝒰    : Lang  ◇.𝒰
-unsafe -- we need unsafe, since Automatic.Lang requires unsafe
+unsafe -- failed to infer structural recursion
 def universal {α: Type u}: Lang (@Language.universal.{u} α) := Lang.mk
   -- ν 𝒰 = ⊤‽
   (null := Decidability.unit)
   -- δ 𝒰 a = 𝒰
   (derive := fun _ => universal)
 
+
 -- _∪_  : Lang  P  → Lang Q  → Lang (P  ◇.∪  Q)
-unsafe -- we need unsafe, since Automatic.Lang requires unsafe
+unsafe -- fail to show termination for Automatic.or
 def or {α: Type u} {P Q: Language.Lang α} (p: Lang P) (q: Lang Q): Lang (Language.or P Q) := Lang.mk
   -- ν (p ∪ q) = ν p ⊎‽ ν q
   (null := Decidability.sum (null p) (null q))
   -- δ (p ∪ q) a = δ p a ∪ δ q a
   (derive := fun (a: α) => or (derive p a) (derive q a))
 
 -- _∩_  : Lang  P  → Lang Q  → Lang (P  ◇.∩  Q)
-unsafe -- we need unsafe, since Automatic.Lang requires unsafe
+unsafe -- fail to show termination for Automatic.and
 def and {α: Type u} {P Q: Language.Lang α} (p: Lang P) (q: Lang Q): Lang (Language.and P Q) := Lang.mk
   -- ν (p ∩ q) = ν p ×‽ ν q
   (null := Decidability.prod (null p) (null q))
   -- δ (p ∩ q) a = δ p a ∩ δ q a
   (derive := fun (a: α) => and (derive p a) (derive q a))
 
 -- _·_  : Dec   s  → Lang P  → Lang (s  ◇.·  P)
-unsafe -- we need unsafe, since Automatic.Lang requires unsafe
+unsafe -- fail to show termination for Automatic.scalar
 def scalar {α: Type u} {P: Language.Lang α} (s: Decidability.Dec S) (p: Lang P): Lang (Language.scalar S P) := Lang.mk
   -- ν (s · p) = s ×‽ ν p
   (null := Decidability.prod s (null p))
   -- δ (s · p) a = s · δ p a
   (derive := fun (a: α) => scalar s (derive p a))
 
 -- _◂_  : (Q ⟷ P) → Lang P → Lang Q
-unsafe -- we need unsafe, since Automatic.Lang requires unsafe
+unsafe -- fail to show termination for Automatic.iso
 def iso {α: Type u} {P Q: Language.Lang α} (f: ∀ {w: List α}, Q w <=> P w) (p: Lang P): Lang Q := Lang.mk
   -- ν (f ◂ p) = f ◃ ν p
   (null := Decidability.apply' f (null p))
   -- δ (f ◂ p) a = f ◂ δ p a
   (derive := fun (a: α) => iso f (derive p a))
 
 -- 𝟏    : Lang ◇.𝟏
-unsafe -- we need unsafe, since Automatic.Lang requires unsafe
+unsafe -- dependent on iso which uses unsafe
 def emptystr {α: Type u}: Lang (@Language.emptystr α) := Lang.mk
   -- ν 𝟏 = ν𝟏 ◃ ⊤‽
   (null := Decidability.apply' Calculus.null_emptystr Decidability.unit)
   -- δ 𝟏 a = δ𝟏 ◂ ∅
   (derive := fun _ => iso Calculus.derive_emptystr emptyset)
 
 -- _⋆_  : Lang  P  → Lang Q  → Lang (P  ◇.⋆  Q)
-unsafe -- we need unsafe, since Automatic.Lang requires unsafe
+unsafe -- fail to show termination for Automatic.concat
 def concat {α: Type u} {P Q: Language.Lang α} (p: Lang P) (q: Lang Q): Lang (Language.concat P Q) := Lang.mk
   -- ν (p ⋆ q) = ν⋆ ◃ (ν p ×‽ ν q)
   (null := Decidability.apply' Calculus.null_concat (Decidability.prod (null p) (null q)))
@@ -116,7 +112,7 @@ def concat {α: Type u} {P Q: Language.Lang α} (p: Lang P) (q: Lang Q): Lang (L
   )
 
 -- _☆   : Lang  P → Lang (P ◇.☆)
-unsafe -- we need unsafe, since Automatic.Lang requires unsafe
+unsafe -- fail to show termination for Automatic.star
 def star {α: Type u} {P: Language.Lang α} (p: Lang P): Lang (Language.star P) := Lang.mk
   -- ν (p ☆) = ν☆ ◃ (ν p ✶‽)
   (null := Decidability.apply' Calculus.null_star (Decidability.list (null p)))
@@ -131,7 +127,7 @@ def star {α: Type u} {P: Language.Lang α} (p: Lang P): Lang (Language.star P)
   )
 
 -- `    : (a : A) → Lang (◇.` a)
-unsafe -- we need unsafe, since Automatic.Lang requires unsafe
+unsafe -- dependent on iso which uses unsafe
 def char {α: Type u} [Decidability.DecEq α] (c: α): Lang (Language.char c) := Lang.mk
   -- ν (` a) = ν` ◃ ⊥‽
   (null := Decidability.apply' Calculus.null_char Decidability.empty)
@@ -146,7 +142,6 @@ def char {α: Type u} [Decidability.DecEq α] (c: α): Lang (Language.char c) :=
 -- ⟦_⟧‽ : Lang P → Decidable P
 -- ⟦ p ⟧‽     []    = ν p
 -- ⟦ p ⟧‽ (a  ∷ w)  = ⟦ δ p a ⟧‽ w
-unsafe -- we need unsafe, since Automatic.Lang requires unsafe
 def decDenote (p: Lang P): Decidability.DecPred P :=
   fun w =>
     match w with
@@ -155,7 +150,6 @@ def decDenote (p: Lang P): Decidability.DecPred P :=
 
 -- ⟦_⟧ : Lang P → ◇.Lang
 -- ⟦_⟧ {P} _ = P
-unsafe -- we need unsafe, since Automatic.Lang requires unsafe
 def denote (_: @Lang α P): Language.Lang α := P
 
 end Automatic