From d83586b74e10b1926ce21dabaad990996e9501d3 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Mon, 13 Nov 2023 20:18:41 +0000
Subject: [PATCH] Work from session on 2023-11-13

---
 Katydid/Conal/Lang.lean | 46 +++++++++++++++++++++++++++++++++++++----
 1 file changed, 42 insertions(+), 4 deletions(-)

diff --git a/Katydid/Conal/Lang.lean b/Katydid/Conal/Lang.lean
index 6bea9ee..9419490 100644
--- a/Katydid/Conal/Lang.lean
+++ b/Katydid/Conal/Lang.lean
@@ -1,9 +1,47 @@
 open List
 
-def Lang : Type (u + 1) := {α : Type u} -> List α -> Type u
+/--
+The equality relation. We use this instead of Lean's `Eq` because
+we need it to be defined on Type instead of Prop.
+-/
+inductive REq {α : Type u} (x : α) : α -> Type u where
+  | rrefl : REq x x
 
-def emptySet : Lang := fun _ => Empty
+inductive All {α: Type u} (P : α -> Type u) : (List α -> Type u)  where
+  | nil : All P []
+  | cons : ∀ {x xs} (_px : P x) (_pxs : All P xs), All P (x :: xs)
 
-def universal : Lang := fun _ => Unit
+def Lang (α : Type u) : Type (u + 1) :=  List α -> Type u
 
--- def emptyStr : Lang := fun w => w = []
+def emptySet : Lang α := fun _ => Empty
+
+def universal : Lang α := fun _ => Unit
+
+def emptyStr : Lang α := fun w => REq w []
+
+def char (a : α) := fun w => REq w [a]
+
+def scalar (s : Type u) (P : Lang α) : Lang α  := fun w => s × P w
+
+def or_ (P : Lang α) (Q : Lang α) : Lang α := fun w => P w ⊕ Q w
+
+def and_ (P : Lang α) (Q : Lang α) : Lang α := fun w => P w × Q w
+
+def concat (P : Lang α) (Q : Lang α) : Lang α :=
+  fun (w : List α) =>
+    Σ (x : List α) (y : List α), (REq w (x ++ y)) × P x × Q y
+
+def star (P : Lang α) : Lang α :=
+  fun (w : List α) =>
+    Σ (ws : List (List α)), (REq w (List.join ws)) × All P ws
+
+def ν (P : Lang α) : Type u := P []
+
+def δ (P : Lang α) (a : α) : Lang α := fun (w : List α) => P (a :: w)
+
+example : (or_ (char 'a') (char 'b')) ['a'] :=
+  Sum.inl REq.rrefl
+
+example : (or_ (char 'a') (char 'b')) ['a'] := by
+  apply Sum.inl
+  constructor