From 1c044caf047cb58049876b4db4ee93fcd33991b6 Mon Sep 17 00:00:00 2001
From: Walter Schulze <awalterschulze@gmail.com>
Date: Tue, 27 Aug 2024 12:18:27 +0100
Subject: [PATCH] Symbolic is now fully defined

---
 Katydid/Conal/Decidability.lean | 22 +++++++-
 Katydid/Conal/Symbolic.lean     | 97 ++++++++++++++++-----------------
 2 files changed, 65 insertions(+), 54 deletions(-)

diff --git a/Katydid/Conal/Decidability.lean b/Katydid/Conal/Decidability.lean
index 2a1245f..a429c10 100644
--- a/Katydid/Conal/Decidability.lean
+++ b/Katydid/Conal/Decidability.lean
@@ -8,9 +8,25 @@ namespace Decidability
 -- data Dec (A: Set l):Set l where
 --   yes: A → Dec A
 --   no :¬A → Dec A
-inductive Dec (α: Type u): Type u where
-  | yes: α -> Dec α
-  | no: (α -> PEmpty.{u}) -> Dec α
+class inductive Dec (P: Type u): Type u where
+  | yes: P -> Dec P
+  | no: (P -> PEmpty.{u}) -> Dec P
+
+@[inline_if_reduce, nospecialize] def Dec.decide (P : Type) [h : Dec P] : Bool :=
+  h.casesOn (fun _ => false) (fun _ => true)
+
+abbrev DecPred {α : Type u} (r : α → Type) :=
+  (a : α) → Dec (r a)
+
+abbrev DecRel {α : Type u} (r : α → α → Type) :=
+  (a b : α) → Dec (r a b)
+
+abbrev DecEq (α : Type u) :=
+  (a b : α) → Dec (a ≡ b)
+
+-- module Symbolic {ℓ} {A : Set ℓ} (_≟_ : Decidable₂ {A = A} _≡_) where
+def decEq {α : Type u} [inst : DecEq α] (a b : α) : Dec (a ≡ b) :=
+  inst a b
 
 -- ⊥? : Dec ⊥
 -- ⊥? = no(𝜆())
diff --git a/Katydid/Conal/Symbolic.lean b/Katydid/Conal/Symbolic.lean
index 3a39e5b..6e48658 100644
--- a/Katydid/Conal/Symbolic.lean
+++ b/Katydid/Conal/Symbolic.lean
@@ -9,7 +9,7 @@ import Katydid.Conal.Calculus
 namespace Symbolic
 
 -- data Lang : ◇.Lang → Set (suc ℓ) where
-inductive Lang: Language.Lang.{u} α -> Type (u + 1) where
+inductive Lang: {α: Type u} -> Language.Lang.{u} α -> Type (u + 1) where
   -- ∅ : Lang ◇.∅
   | emptyset : Lang Language.emptyset
   -- 𝒰 : Lang ◇.𝒰
@@ -17,7 +17,7 @@ inductive Lang: Language.Lang.{u} α -> Type (u + 1) where
   -- 𝟏 : Lang ◇.𝟏
   | emptystr : Lang Language.emptystr
   -- ` : (a : A) → Lang (◇.` a)
-  | char {a: Type u}: (a: α) -> Lang (Language.char a)
+  | char: (a: α) -> Lang (Language.char a)
   -- _∪_ : Lang P → Lang Q → Lang (P ◇.∪ Q)
   | or : Lang P -> Lang Q -> Lang (Language.or P Q)
   -- _∩_ : Lang P → Lang Q → Lang (P ◇.∩ Q)
@@ -28,16 +28,13 @@ inductive Lang: Language.Lang.{u} α -> Type (u + 1) where
   | concat : Lang P -> Lang Q -> Lang (Language.concat P Q)
   -- _☆  : Lang P → Lang (P ◇.☆)
   | star : Lang P -> Lang (Language.star P)
-  -- TODO: complete definition of Lang by adding the last operator:
   -- _◂_  : (Q ⟷ P) → Lang P → Lang Q
-  -- We tried this definition in Lean:
-  -- | iso {P Q: Language.Lang α}: (Q ⟷ P) -> Lang P -> Lang Q
-  -- But we got the following error:
-  -- "(kernel) declaration has free variables 'Symbolic.Lang.iso'"
-  -- The paper says: "The reason _◀_ must be part of the inductive representation is the same as the other constructors, namely so that the core lemmas (Figure 3) translate into an implementation in terms of that representation."
+  -- "The reason _◀_ must be part of the inductive representation is the same as the other constructors, namely so that the core lemmas (Figure 3) translate into an implementation in terms of that representation."
+  -- This is also used in the definition derive as the result of various operators.
+  | iso {P Q: Language.Lang α}: (∀ {w: List α}, Q w <=> P w) -> Lang P -> Lang Q
 
 -- ν  : Lang P → Dec (◇.ν P)
-def null (l: Lang P): Decidability.Dec (Calculus.null P) :=
+def null (l: Lang R): Decidability.Dec (Calculus.null R) :=
   match l with
   -- ν ∅ = ⊥‽
   | Lang.emptyset => Decidability.empty?
@@ -57,51 +54,49 @@ def null (l: Lang P): Decidability.Dec (Calculus.null P) :=
   | Lang.star p => Decidability.apply' Calculus.null_star (Decidability.list? (null p))
   -- ν (` a) = ν` ◃ ⊥‽
   | Lang.char a => Decidability.apply' Calculus.null_char Decidability.empty?
-  -- TODO: Add the case for language iso morphism, once the Lang.iso operator is added:
   -- ν (f ◂ p) = f ◃ ν p
-  -- | Lang.iso f p => Decidability.apply' f (null p)
+  | Lang.iso f p => Decidability.apply' f (null p)
 
 -- δ  : Lang P → (a : A) → Lang (◇.δ P a)
--- def derive (l: @Lang α P) (a: α): Lang (Calculus.derive P a) :=
---   match l with
---   -- δ ∅ a = ∅
---   | Lang.emptyset => Lang.emptyset
---   -- δ 𝒰 a = 𝒰
---   | Lang.universal => Lang.universal
---   -- δ (p ∪ q) a = δ p a ∪ δ q a
---   | Lang.or p q => Lang.or (derive p a) (derive q a)
---   -- δ (p ∩ q) a = δ p a ∩ δ q a
---   | Lang.and p q => Lang.and (derive p a) (derive q a)
---   -- δ (s · p) a = s · δ p a
---   | Lang.scalar s p => Lang.scalar s (derive p a)
---   -- δ 𝟏 a = δ𝟏 ◂ ∅
---   | Lang.emptystr => (Lang.iso Calculus.derive_emptystr Lang.emptyset)
---   -- δ (p ⋆ q) a = δ⋆ ◂ (ν p · δ q a ∪ δ p a ⋆ q)
---   | Lang.concat p q =>
---     (Lang.iso Calculus.derive_concat
---       (Lang.scalar (null p)
---         (Lang.or
---           (derive q a)
---           (Lang.concat (derive p a) q)
---         )
---       )
---     )
---   -- δ (p ☆) a = δ☆ ◂ (ν p ✶‽ · (δ p a ⋆ p ☆))
---   | Lang.star p =>
---     (Lang.iso Calculus.derive_star
---       (Lang.scalar
---         (Decidability.list? (null p))
---         (Lang.concat (derive p a) (Lang.star p))
---       )
---     )
---   -- δ (` c) a = δ` ◂ ((a ≟ c) · 𝟏)
---   | Lang.char c =>
---     (Lang.iso Calculus.derive_char
---       -- TODO: not sure if ≟ is the same as ≡
---       (Lang.scalar (a ≡ c) Lang.emptystr)
---     )
-  -- TODO: Add the case for language iso morphism, once the Lang.iso operator is added:
+def derive [Decidability.DecEq α] (l: @Lang α P) (a: α): Lang (Calculus.derive P a) :=
+  match l with
+  -- δ ∅ a = ∅
+  | Lang.emptyset => Lang.emptyset
+  -- δ 𝒰 a = 𝒰
+  | Lang.universal => Lang.universal
+  -- δ (p ∪ q) a = δ p a ∪ δ q a
+  | Lang.or p q => Lang.or (derive p a) (derive q a)
+  -- δ (p ∩ q) a = δ p a ∩ δ q a
+  | Lang.and p q => Lang.and (derive p a) (derive q a)
+  -- δ (s · p) a = s · δ p a
+  | Lang.scalar s p => Lang.scalar s (derive p a)
+  -- δ 𝟏 a = δ𝟏 ◂ ∅
+  | Lang.emptystr => (Lang.iso Calculus.derive_emptystr Lang.emptyset)
+  -- δ (p ⋆ q) a = δ⋆ ◂ (ν p · δ q a ∪ δ p a ⋆ q)
+  | Lang.concat p q =>
+    (Lang.iso Calculus.derive_concat
+      (Lang.scalar (null p)
+        (Lang.or
+          (derive q a)
+          (Lang.concat (derive p a) q)
+        )
+      )
+    )
+  -- δ (p ☆) a = δ☆ ◂ (ν p ✶‽ · (δ p a ⋆ p ☆))
+  | Lang.star p =>
+    (Lang.iso Calculus.derive_star
+      (Lang.scalar
+        (Decidability.list? (null p))
+        (Lang.concat (derive p a) (Lang.star p))
+      )
+    )
+  -- δ (` c) a = δ` ◂ ((a ≟ c) · 𝟏)
+  | Lang.char c =>
+    let cmp: Decidability.Dec (a ≡ c) := Decidability.decEq a c
+    (Lang.iso Calculus.derive_char
+      (Lang.scalar cmp Lang.emptystr)
+    )
   -- δ (f ◂ p) a = f ◂ δ p a
-  -- | Lang.iso f p => Lang.iso f (derive p a)
+  | Lang.iso f p => Lang.iso f (derive p a)
 
 end Symbolic