From aa171da88bdcde710adadf7c473c438f30e7dcd8 Mon Sep 17 00:00:00 2001
From: Walter Schulze <awalterschulze@gmail.com>
Date: Fri, 15 Mar 2024 14:58:02 +0000
Subject: [PATCH] Lang and dLang

---
 Katydid/Conal/Calculus.lean         |  71 +++++++--------
 Katydid/Conal/Examples.lean         |  12 ++-
 Katydid/Conal/Language.lean         | 130 +++++++++++++++++++++++++---
 Katydid/Conal/LanguageNotation.lean |  18 ++--
 4 files changed, 170 insertions(+), 61 deletions(-)

diff --git a/Katydid/Conal/Calculus.lean b/Katydid/Conal/Calculus.lean
index 4ae0b0e..67ce595 100644
--- a/Katydid/Conal/Calculus.lean
+++ b/Katydid/Conal/Calculus.lean
@@ -3,7 +3,8 @@
 
 import Katydid.Conal.LanguageNotation
 import Mathlib.Logic.Equiv.Defs -- ≃
-open Lang
+import Katydid.Std.Tipe2
+open dLang
 open List
 open Char
 open String
@@ -53,21 +54,21 @@ def example_of_proof_relevant_parse2 : (char 'a', (char 'b' ⋃ char 'c')) (toLi
 
 -- ν⇃ : Lang → Set ℓ      -- “nullable”
 -- ν⇃ P = P []
-def ν (P : Lang α) : Type u := -- backslash nu
+def ν' (P : dLang α) : Type u := -- backslash nu
   P []
 
 -- δ⇃ : Lang → A → Lang   -- “derivative”
 -- δ⇃ P a w = P (a ∷ w)
-def δ (P : Lang α) (a : α) : Lang α := -- backslash delta
+def δ' (P : dLang α) (a : α) : dLang α := -- backslash delta
   fun (w : List α) => P (a :: w)
 
-attribute [simp] ν δ
+attribute [simp] ν' δ'
 
 -- ν∅  : ν ∅ ≡ ⊥
 -- ν∅ = refl
 theorem nullable_emptySet:
   ∀ (α: Type),
-    @ν α ∅ ≡ PEmpty := by
+    @ν' α ∅ ≡ PEmpty := by
   intro α
   constructor
   rfl
@@ -76,7 +77,7 @@ theorem nullable_emptySet:
 -- ν𝒰 = refl
 theorem nullable_universal:
   ∀ (α: Type),
-    @ν α 𝒰 ≡ PUnit := by
+    @ν' α 𝒰 ≡ PUnit := by
   intro α
   constructor
   rfl
@@ -89,7 +90,7 @@ theorem nullable_universal:
 --   (λ { refl → refl })
 theorem nullable_emptyStr:
   ∀ (α: Type),
-    @ν α ε ≃ PUnit := by
+    @ν' α ε ≃ PUnit := by
   intro α
   refine Equiv.mk ?a ?b ?c ?d
   intro _
@@ -105,7 +106,7 @@ theorem nullable_emptyStr:
 
 theorem nullable_emptyStr':
   ∀ (α: Type),
-    @ν α ε ≃ PUnit :=
+    @ν' α ε ≃ PUnit :=
     fun _ => Equiv.mk
       (fun _ => PUnit.unit)
       (fun _ => by constructor; rfl)
@@ -116,7 +117,7 @@ theorem nullable_emptyStr':
 -- ν` = mk↔′ (λ ()) (λ ()) (λ ()) (λ ())
 theorem nullable_char:
   ∀ (c: α),
-    ν (char c) ≃ PEmpty := by
+    ν' (char c) ≃ PEmpty := by
   intro α
   simp
   apply Equiv.mk
@@ -131,7 +132,7 @@ theorem nullable_char:
 
 theorem nullable_char':
   ∀ (c: α),
-    ν (char c) -> PEmpty := by
+    ν' (char c) -> PEmpty := by
   intro
   refine (fun x => ?c)
   simp at x
@@ -145,8 +146,8 @@ theorem nullable_char':
 -- ν∪  : ν (P ∪ Q) ≡ (ν P ⊎ ν Q)
 -- ν∪ = refl
 theorem nullable_or:
-  ∀ (P Q: Lang α),
-    ν (P ⋃ Q) ≡ (Sum (ν P) (ν Q)) := by
+  ∀ (P Q: dLang α),
+    ν' (P ⋃ Q) ≡ (Sum (ν' P) (ν' Q)) := by
   intro P Q
   constructor
   rfl
@@ -154,8 +155,8 @@ theorem nullable_or:
 -- ν∩  : ν (P ∩ Q) ≡ (ν P × ν Q)
 -- ν∩ = refl
 theorem nullable_and:
-  ∀ (P Q: Lang α),
-    ν (P ⋂ Q) ≡ (Prod (ν P) (ν Q)) := by
+  ∀ (P Q: dLang α),
+    ν' (P ⋂ Q) ≡ (Prod (ν' P) (ν' Q)) := by
   intro P Q
   constructor
   rfl
@@ -163,8 +164,8 @@ theorem nullable_and:
 -- ν·  : ν (s · P) ≡ (s × ν P)
 -- ν· = refl
 theorem nullable_scalar:
-  ∀ (s: Type) (P: Lang α),
-    ν (Lang.scalar s P) ≡ (Prod s (ν P)) := by
+  ∀ (s: Type) (P: dLang α),
+    ν' (dLang.scalar s P) ≡ (Prod s (ν' P)) := by
   intro P Q
   constructor
   rfl
@@ -176,8 +177,8 @@ theorem nullable_scalar:
 --   (λ { (νP , νQ) → refl } )
 --   (λ { (([] , []) , refl , νP , νQ) → refl})
 theorem nullable_concat:
-  ∀ (P Q: Lang α),
-    ν (P, Q) ≃ (Prod (ν Q) (ν P)) := by
+  ∀ (P Q: dLang α),
+    ν' (P, Q) ≃ (Prod (ν' Q) (ν' P)) := by
   -- TODO
   sorry
 
@@ -210,8 +211,8 @@ theorem nullable_concat:
 --     (ν P) ✶
 --   ∎ where open ↔R
 theorem nullable_star:
-  ∀ (P: Lang α),
-    ν (P *) ≃ List (ν P) := by
+  ∀ (P: dLang α),
+    ν' (P *) ≃ List (ν' P) := by
   -- TODO
   sorry
 
@@ -219,7 +220,7 @@ theorem nullable_star:
 -- δ∅ = refl
 theorem derivative_emptySet:
   ∀ (a: α),
-    (δ ∅ a) ≡ ∅ := by
+    (δ' ∅ a) ≡ ∅ := by
   intro a
   constructor
   rfl
@@ -228,7 +229,7 @@ theorem derivative_emptySet:
 -- δ𝒰 = refl
 theorem derivative_universal:
   ∀ (a: α),
-    (δ 𝒰 a) ≡ 𝒰 := by
+    (δ' 𝒰 a) ≡ 𝒰 := by
   intro a
   constructor
   rfl
@@ -238,7 +239,7 @@ theorem derivative_universal:
 -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
 theorem derivative_emptyStr:
   ∀ (a: α),
-    (δ ε a) ≡ ∅ := by
+    (δ' ε a) ≡ ∅ := by
   -- TODO
   sorry
 
@@ -251,9 +252,9 @@ theorem derivative_emptyStr:
 -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
 theorem derivative_char:
   ∀ (a: α) (c: α),
-    (δ (char c) a) ≡ Lang.scalar (a ≡ c) ε := by
+    (δ' (char c) a) ≡ dLang.scalar (a ≡ c) ε := by
     intros a c
-    unfold δ
+    unfold δ'
     unfold char
     unfold emptyStr
     unfold scalar
@@ -262,8 +263,8 @@ theorem derivative_char:
 -- δ∪  : δ (P ∪ Q) a ≡ δ P a ∪ δ Q a
 -- δ∪ = refl
 theorem derivative_or:
-  ∀ (a: α) (P Q: Lang α),
-    (δ (P ⋃ Q) a) ≡ ((δ P a) ⋃ (δ Q a)) := by
+  ∀ (a: α) (P Q: dLang α),
+    (δ' (P ⋃ Q) a) ≡ ((δ' P a) ⋃ (δ' Q a)) := by
   intro a P Q
   constructor
   rfl
@@ -271,8 +272,8 @@ theorem derivative_or:
 -- δ∩  : δ (P ∩ Q) a ≡ δ P a ∩ δ Q a
 -- δ∩ = refl
 theorem derivative_and:
-  ∀ (a: α) (P Q: Lang α),
-    (δ (P ⋂ Q) a) ≡ ((δ P a) ⋂ (δ Q a)) := by
+  ∀ (a: α) (P Q: dLang α),
+    (δ' (P ⋂ Q) a) ≡ ((δ' P a) ⋂ (δ' Q a)) := by
   intro a P Q
   constructor
   rfl
@@ -280,8 +281,8 @@ theorem derivative_and:
 -- δ·  : δ (s · P) a ≡ s · δ P a
 -- δ· = refl
 theorem derivative_scalar:
-  ∀ (a: α) (s: Type) (P: Lang α),
-    (δ (Lang.scalar s P) a) ≡ (Lang.scalar s (δ P a)) := by
+  ∀ (a: α) (s: Type) (P: dLang α),
+    (δ (dLang.scalar s P) a) ≡ (dLang.scalar s (δ' P a)) := by
   intro a s P
   constructor
   rfl
@@ -298,9 +299,9 @@ theorem derivative_scalar:
 --      ; ((.a ∷ u , v) , refl , Pu , Qv) → refl })
 -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
 theorem derivative_concat:
-  ∀ (a: α) (P Q: Lang α),
+  ∀ (a: α) (P Q: dLang α),
   -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
-    (δ (P , Q) a) ≡ Lang.scalar (ν P) ((δ Q a) ⋃ ((δ P a), Q)) := by
+    (δ' (P , Q) a) ≡ dLang.scalar (ν' P) ((δ' Q a) ⋃ ((δ' P a), Q)) := by
   -- TODO
   sorry
 
@@ -338,8 +339,8 @@ theorem derivative_concat:
 --   ∎ where open ↔R
 -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
 theorem derivative_star:
-  ∀ (a: α) (P: Lang α),
+  ∀ (a: α) (P: dLang α),
   -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
-    (δ (P *) a) ≡ Lang.scalar (List (ν P)) (δ P a, P *) := by
+    (δ' (P *) a) ≡ dLang.scalar (List (ν' P)) (δ' P a, P *) := by
   -- TODO
   sorry
diff --git a/Katydid/Conal/Examples.lean b/Katydid/Conal/Examples.lean
index 2c6104d..103f2c4 100644
--- a/Katydid/Conal/Examples.lean
+++ b/Katydid/Conal/Examples.lean
@@ -2,9 +2,9 @@
 -- https://github.com/conal/paper-2021-language-derivatives/blob/main/Examples.lagda
 
 import Katydid.Conal.LanguageNotation
-open Lang
+open dLang
 
-example: (Lang.char 'a') ['a'] := by
+example: (dLang.char 'a') ['a'] := by
   simp
   constructor
   rfl
@@ -15,7 +15,7 @@ example: (Lang.char 'a') ['a'] := by
 -- _ : a∪b [ 'b' ]
 -- _ = inj₂ refl
 example : (char 'a' ⋃ char 'b') ['b'] :=
-  Sum.inr (TEq.mk rfl)
+  Sum.inr trfl
 
 example : (char 'a' ⋃ char 'b') (String.toList "b") := by
   apply Sum.inr
@@ -42,6 +42,12 @@ example : (char 'a', char 'b') (String.toList "ab") := by
   refine PSigma.mk trfl ?d
   rfl
 
+example : (char 'a', char 'b') (String.toList "ab") :=
+  PSigma.mk ['a'] (PSigma.mk ['b'] (PSigma.mk trfl (PSigma.mk trfl rfl)))
+
+example : (char 'a', char 'b') (String.toList "ab") :=
+  PSigma.mk ['a'] (PSigma.mk ['b'] (PSigma.mk trfl (PSigma.mk trfl rfl)))
+
 example : ((char 'a')*) (String.toList "a") := by sorry
   -- TODO:
   -- simp
diff --git a/Katydid/Conal/Language.lean b/Katydid/Conal/Language.lean
index 2e3fc78..07a70e6 100644
--- a/Katydid/Conal/Language.lean
+++ b/Katydid/Conal/Language.lean
@@ -6,15 +6,14 @@ open List
 
 -- module Language {ℓ} (A : Set ℓ) where
 universe u
-variable (α : Type u)
 
 -- Lang : Set (suc ℓ)
 -- Lang = A ✶ → Set ℓ
-def Lang : Type (u + 1) :=
+def dLang (α : Type u) : Type (u + 1) :=
   List α -> Type u
 
 -- namespace Lang is required to avoid ambiguities with or, and, concat and star.
-namespace Lang
+namespace dLang
 
 -- variable α should be implicit to make sure examples do not need to also provide the parameter of α when constructing char, or, concat, since it usually can be inferred to be Char.
 variable {α : Type u}
@@ -26,50 +25,50 @@ variable {α : Type u}
 
 -- ∅ : Lang
 -- ∅ w = ⊥
-def emptySet : Lang α :=
+def emptySet : dLang α :=
   -- PEmpty is Empty, but allows specifying the universe
   -- PEmpty is a Sort, which works for both Prop and Type
   fun _ => PEmpty
 
 -- 𝒰 : Lang
 -- 𝒰 w = ⊤
-def universal : Lang α :=
+def universal : dLang α :=
   -- PUnit is Empty, but allows specifying the universe
   -- PUnit is a Sort, which works for both Prop and Type
   fun _ => PUnit
 
 -- 𝟏 : Lang
 -- 𝟏 w = w ≡ []
-def emptyStr : Lang α :=
+def emptyStr : dLang α :=
   fun w => w ≡ []
 
 -- ` : A → Lang
 -- ` c w = w ≡ [ c ]
-def char (a : α): Lang α :=
+def char (a : α): dLang α :=
   fun w => w ≡ [a]
 
 -- infixl 7 _·_
 -- _·_ : Set ℓ → Op₁ Lang
 -- (s · P) w = s × P w
-def scalar (s : Type u) (P : Lang α) : Lang α :=
+def scalar (s : Type u) (P : dLang α) : dLang α :=
   fun w => s × P w
 
 -- infixr 6 _∪_
 -- _∪_ : Op₂ Lang
 -- (P ∪ Q) w = P w ⊎ Q w
-def or (P : Lang α) (Q : Lang α) : Lang α :=
+def or (P : dLang α) (Q : dLang α) : dLang α :=
   fun w => P w ⊕ Q w
 
 -- infixr 6 _∩_
 -- _∩_ : Op₂ Lang
 -- (P ∩ Q) w = P w × Q w
-def and (P : Lang α) (Q : Lang α) : Lang α :=
+def and (P : dLang α) (Q : dLang α) : dLang α :=
   fun w => P w × Q w
 
 -- infixl 7 _⋆_
 -- _⋆_ : Op₂ Lang
 -- (P ⋆ Q) w = ∃⇃ λ (u ,  v) → (w ≡ u ⊙ v) × P u × Q v
-def concat (P : Lang α) (Q : Lang α) : Lang α :=
+def concat (P : dLang α) (Q : dLang α) : dLang α :=
   fun (w : List α) =>
     Σ' (x : List α) (y : List α), (_px: P x) ×' (_qy: Q y) ×' w = (x ++ y)
 
@@ -80,16 +79,119 @@ inductive All {α: Type u} (P : α -> Type u) : (List α -> Type u) where
 -- infixl 10 _☆
 -- _☆ : Op₁ Lang
 -- (P ☆) w = ∃ λ ws → (w ≡ concat ws) × All P ws
-def star (P : Lang α) : Lang α :=
+def star (P : dLang α) : dLang α :=
   fun (w : List α) =>
     Σ' (ws : List (List α)), (_pws: All P ws) ×' w = (List.join ws)
 
 -- TODO: What does proof relevance even mean for the `not` operator?
-def not (P: Lang α) : Lang α :=
+def not (P: dLang α) : dLang α :=
   fun (w: List α) =>
     P w -> Empty
 
 -- attribute [simp] allows these definitions to be unfolded when using the simp tactic.
 attribute [simp] universal emptySet emptyStr char scalar or and concat star
 
-end Lang
+-- 𝜈 :(A✶ → B) → B -- “nullable”
+-- 𝜈 f = f []
+-- nullable
+-- ν = backslash nu
+def ν (f: List α -> β): β :=
+  f []
+
+-- 𝒟: (A✶ → B) → A✶ → (A✶ → B) -- “derivative”
+-- 𝒟 f u = 𝜆 v → f (u + v)
+-- 𝒟 = backslash McD
+def 𝒟 (f: dLang α) (u: List α): (dLang α) :=
+  fun v => f (u ++ v)
+
+-- 𝛿 : (A✶ → B) → A → (A✶ → B)
+-- 𝛿 f a = 𝒟 f [a]
+-- δ = backslash delta or backslash Gd
+def δ (f: dLang α) (a: α): (dLang α) :=
+  𝒟 f [a]
+
+end dLang
+
+-- 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 α
+
+-- ⊥? : Dec ⊥
+-- ⊥? =no(𝜆())
+def empty? : Dec PEmpty :=
+  Dec.no (by intro; contradiction)
+
+def unit? : Dec PUnit :=
+  Dec.yes PUnit.unit
+
+def sum? (a: Dec α) (b: Dec β): Dec (α ⊕ β) :=
+  match (a, b) with
+  | (Dec.no a, Dec.no b) =>
+    Dec.no (fun ab =>
+      match ab with
+      | Sum.inl sa => a sa
+      | Sum.inr sb => b sb
+    )
+  | (Dec.yes a, Dec.no _) =>
+    Dec.yes (Sum.inl a)
+  | (_, Dec.yes b) =>
+    Dec.yes (Sum.inr b)
+
+def prod? (a: Dec α) (b: Dec β): Dec (α × β) :=
+  match (a, b) with
+  | (Dec.yes a, Dec.yes b) => Dec.yes (Prod.mk a b)
+  | (Dec.no a, Dec.yes _) => Dec.no (fun ⟨a', _⟩ => a a')
+  | (_, Dec.no b) => Dec.no (fun ⟨_, b'⟩ => b b')
+
+def list?: Dec α -> Dec (List α) := fun _ => Dec.yes []
+
+
+
+inductive Lang : (List α -> Type u) -> Type (u + 1) where
+  -- | emptySet : Lang dLang.emptySet
+  | universal : Lang (fun _ => PUnit)
+  -- | emptyStr : Lang dLang.emptyStr
+  -- | char {a: Type u}: (a: α) -> Lang (dLang.char a)
+  -- | or : Lang P -> Lang Q -> Lang (dLang.or P Q)
+  -- | and : Lang P -> Lang Q -> Lang (dLang.and P Q)
+  -- | scalar {s: Type u}: (Dec s) -> Lang P -> Lang (dLang.scalar s P)
+  -- | concat : Lang P -> Lang Q -> Lang (dLang.concat P Q)
+  -- | star : Lang P -> Lang (dLang.star P)
+
+#check @Lang.casesOn
+
+-- 𝜈 : Lang P → Dec (⋄.𝜈 P)
+theorem ν {α: Type u} {P: dLang α} (f: Lang P): Dec (dLang.ν P) := by
+  induction f with
+  | universal => exact unit?
+
+-- TODO: rewrite ν using casesOn
+-- def ν' {α: Type u} {P: dLang α} (f: Lang P): Dec (dLang.ν P) := by
+--   refine (Lang.casesOn ?a ?b ?c ?d ?e)
+--   match f with
+--   | universal => unit?
+
+-- def ν'' {α: Type u} {P: dLang α} (f: Lang P): Dec (dLang.ν P) := by
+--   induction f with
+--   | universal => exact unit?
+
+-- #print ν''
+
+
+
+
+
+
+
+
+
+
+
+
+
+  -- | lang_emptyset (str : List α):
+  --   False ->
+  --   Lang Regex.emptyset str
diff --git a/Katydid/Conal/LanguageNotation.lean b/Katydid/Conal/LanguageNotation.lean
index a73c471..b8ecdf9 100644
--- a/Katydid/Conal/LanguageNotation.lean
+++ b/Katydid/Conal/LanguageNotation.lean
@@ -1,26 +1,26 @@
 import Katydid.Conal.Language
 
 -- `(priority := high)` is required to avoid the error: "ambiguous, possible interpretations"
-notation (priority := high) "∅" => Lang.emptySet -- backslash emptyset
+notation (priority := high) "∅" => dLang.emptySet -- backslash emptyset
 
-notation "𝒰" => Lang.universal -- backslash McU
+notation "𝒰" => dLang.universal -- backslash McU
 
-notation "ε" => Lang.emptyStr -- backslash epsilon
+notation "ε" => dLang.emptyStr -- backslash epsilon
 
 -- TODO: fix scalar to work in Calculus.lean
-infixl:4 " · " => Lang.scalar -- backslash .
+infixl:4 " · " => dLang.scalar -- backslash .
 
-infixl:5 (priority := high) " ⋃ " => Lang.or -- backslash U
+infixl:5 (priority := high) " ⋃ " => dLang.or -- backslash U
 
-infixl:4 " ⋂ " => Lang.and -- backslash I
+infixl:4 " ⋂ " => dLang.and -- backslash I
 
-infixr:5 " , " => Lang.concat
+infixr:5 " , " => dLang.concat
 
-postfix:6 "*" => Lang.star
+postfix:6 "*" => dLang.star
 
 -- Tests for notation
 
-open Lang
+open dLang
 #check 𝒰
 #check ε
 #check (ε ⋃ 𝒰)