add universes to Calculus

Katydid/Conal/Automatic.lean

@@ -13,12 +13,17 @@ namespace Automatic
 
 -- 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 declaredLean 4
 unsafe
-inductive Lang {α: Type u} (R: List α -> Type u): Type u where
+inductive Lang {α: Type u} (R: Language.Lang α): Type (u + 1) where
   | mk
-   (null: Decidability.Dec (Language.null R))
-   (derive: (a: α) -> Lang (Language.derive R a))
+   (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
+
 -- ∅ : Lang ◇.∅
 unsafe -- we need unsafe, since Automatic.Lang requires unsafe
 def emptyset {α: Type u}: Lang (@Language.emptyset.{u} α) := Lang.mk
@@ -29,41 +34,41 @@ def emptyset {α: Type u}: Lang (@Language.emptyset.{u} α) := Lang.mk
 
 -- 𝒰    : Lang  ◇.𝒰
 unsafe -- we need unsafe, since Automatic.Lang requires unsafe
-def universal {a: Type u}: Lang (@Language.universal.{u} α) := Lang.mk
+def universal {α: Type u}: Lang (@Language.universal.{u} α) := Lang.mk
   -- ν 𝒰 = ⊤‽
-  (null := by sorry)
+  (null := Decidability.unit?)
   -- δ 𝒰 a = 𝒰
-  (derive := by sorry)
+  (derive := fun _ => universal)
 
 -- _∪_  : Lang  P  → Lang Q  → Lang (P  ◇.∪  Q)
 unsafe -- we need unsafe, since Automatic.Lang requires unsafe
-def or {a: Type u} (p: @Lang α P) (q: @Lang α Q): Lang (@Language.or.{u} α P Q) := Lang.mk
+def or (p: Lang P) (q: Lang Q): Lang (Language.or P Q) := Lang.mk
   -- ν (p ∪ q) = ν p ⊎‽ ν q
-  (null := sorry)
+  (null := Decidability.sum? (null p) (null q))
   -- δ (p ∪ q) a = δ p a ∪ δ q a
   (derive := sorry)
 
 -- _∩_  : Lang  P  → Lang Q  → Lang (P  ◇.∩  Q)
 unsafe -- we need unsafe, since Automatic.Lang requires unsafe
-def and {a: Type u} (p: @Lang α P) (q: @Lang α Q): Lang (@Language.and.{u} α P Q) := Lang.mk
+def and (p: Lang P) (q: Lang Q): Lang (Language.and P Q) := Lang.mk
   -- ν (p ∩ q) = ν p ×‽ ν q
-  (null := sorry)
+  (null := Decidability.prod? (null p) (null q))
   -- δ (p ∩ q) a = δ p a ∩ δ q a
   (derive := sorry)
 
 -- _·_  : Dec   s  → Lang P  → Lang (s  ◇.·  P)
 unsafe -- we need unsafe, since Automatic.Lang requires unsafe
-def scalar {a: Type u} (_: Decidability.Dec s) (p: @Lang α P): Lang (@Language.scalar.{u} α s Q) := Lang.mk
+def scalar (s': Decidability.Dec S) (p: Lang P): Lang (Language.scalar S P) := Lang.mk
   -- ν (s · p) = s ×‽ ν p
-  (null := sorry)
+  (null := Decidability.prod? s' (null p))
   -- δ (s · p) a = s · δ p a
   (derive := sorry)
 
 -- 𝟏    : Lang ◇.𝟏
 unsafe -- we need unsafe, since Automatic.Lang requires unsafe
 def emptystr {α: Type u}: Lang (@Language.emptystr.{u} α) := Lang.mk
   -- ν 𝟏 = ν𝟏 ◃ ⊤‽
-  (null := sorry)
+  (null := Decidability.apply' Calculus.null_emptystr Decidability.unit?)
   -- δ 𝟏 a = δ𝟏 ◂ ∅
   (derive := sorry)
 

Katydid/Conal/Calculus.lean

@@ -67,36 +67,32 @@ def derive' (P : Lang α) (a : α) : Lang α := -- backslash delta
 
 -- ν : (A ✶ → B) → B                -- “nullable”
 -- ν f = f []
-def null (f: List α -> β): β :=
+def null {α: Type u} {β: Type v} (f: List α -> β): β :=
   f []
 
 -- 𝒟 : (A ✶ → B) → A ✶ → (A ✶ → B)  -- “derivative”
 -- 𝒟 f u = λ v → f (u ⊙ v)
-def derives (f: List α -> β) (u: List α): (List α -> β) :=
+def derives {α: Type u} {β: Type v} (f: List α -> β) (u: List α): (List α -> β) :=
   λ v => f (u ++ v)
 
 -- δ : (A ✶ → B) → A → (A ✶ → B)
 -- δ f a = 𝒟 f [ a ]
-def derive (f: Lang α) (a: α): (Lang α) :=
+def derive {α: Type u} {β: Type v} (f: List α -> β) (a: α): (List α -> β) :=
   derives f [a]
 
 attribute [simp] null' derive'
 
 -- ν∅  : ν ∅ ≡ ⊥
 -- ν∅ = refl
-def null_emptyset:
-  ∀ {α: Type},
-    @null α _ emptyset ≡ PEmpty := by
-  intro α
+def null_emptyset {α: Type u}:
+  @null α _ emptyset ≡ PEmpty := by
   constructor
   rfl
 
 -- ν𝒰  : ν 𝒰 ≡ ⊤
 -- ν𝒰 = refl
-def null_universal:
-  ∀ {α: Type},
-    @null α _ universal ≡ PUnit := by
-  intro α
+def null_universal {α: Type u}:
+  @null α _ universal ≡ PUnit := by
   constructor
   rfl
 
@@ -106,10 +102,8 @@ def null_universal:
 --   (λ { tt → refl })
 --   (λ { tt → refl })
 --   (λ { refl → refl })
-def null_emptystr:
-  ∀ {α: Type},
-    @null α _ emptystr <=> PUnit := by
-  intro α
+def null_emptystr {α: Type u}:
+  @null α _ emptystr <=> PUnit := by
   refine TEquiv.mk ?a ?b ?c ?d
   · intro _
     exact PUnit.unit
@@ -125,18 +119,17 @@ def null_emptystr:
     simp
 
 -- An alternative "proof" of null_emptystr not using tactics
-def null_emptystr':
-  ∀ {α: Type},
-    @null α _ emptystr <=> PUnit :=
-    TEquiv.mk
-      (fun _ => PUnit.unit)
-      (fun _ => by constructor; rfl)
-      (sorry)
-      (sorry)
+def null_emptystr' {α: Type u}:
+  @null α _ emptystr <=> PUnit :=
+  TEquiv.mk
+    (fun _ => PUnit.unit)
+    (fun _ => by constructor; rfl)
+    (sorry)
+    (sorry)
 
 -- ν`  : ν (` c) ↔ ⊥
 -- ν` = mk↔′ (λ ()) (λ ()) (λ ()) (λ ())
-def null_char:
+def null_char {α: Type u}:
   ∀ {c: α},
     null (char c) <=> PEmpty := by
   intro c
@@ -152,7 +145,7 @@ def null_char:
 
 -- ν∪  : ν (P ∪ Q) ≡ (ν P ⊎ ν Q)
 -- ν∪ = refl
-def null_or:
+def null_or {α: Type u}:
   ∀ {P Q: Lang α},
     null (or P Q) ≡ (Sum (null P) (null Q)) := by
   intro P Q
@@ -161,7 +154,7 @@ def null_or:
 
 -- ν∩  : ν (P ∩ Q) ≡ (ν P × ν Q)
 -- ν∩ = refl
-def null_and:
+def null_and {α: Type u}:
   ∀ {P Q: Lang α},
     null (and P Q) ≡ (Prod (null P) (null Q)) := by
   intro P Q
@@ -170,8 +163,8 @@ def null_and:
 
 -- ν·  : ν (s · P) ≡ (s × ν P)
 -- ν· = refl
-def null_scalar:
-  ∀ {s: Type} {P: Lang α},
+def null_scalar {α: Type u}:
+  ∀ {s: Type u} {P: Lang α},
     null (scalar s P) ≡ (Prod s (null P)) := by
   intro P Q
   constructor
@@ -183,7 +176,7 @@ def null_scalar:
 --   (λ { (νP , νQ) → ([] , []) , refl , νP , νQ })
 --   (λ { (νP , νQ) → refl } )
 --   (λ { (([] , []) , refl , νP , νQ) → refl})
-def null_concat:
+def null_concat {α: Type u}:
   ∀ {P Q: Lang α},
     null (concat P Q) <=> (Prod (null P) (null Q)) := by
   -- TODO
@@ -217,15 +210,15 @@ def null_concat:
 --   ≈⟨ ν✪ ⟩
 --     (ν P) ✶
 --   ∎ where open ↔R
-def null_star:
+def null_star {α: Type u}:
   ∀ {P: Lang α},
     null (star P) <=> List (null P) := by
   -- TODO
   sorry
 
 -- δ∅  : δ ∅ a ≡ ∅
 -- δ∅ = refl
-def derive_emptyset:
+def derive_emptyset {α: Type u}:
   ∀ {a: α},
     (derive emptyset a) ≡ emptyset := by
   intro a
@@ -234,7 +227,7 @@ def derive_emptyset:
 
 -- δ𝒰  : δ 𝒰 a ≡ 𝒰
 -- δ𝒰 = refl
-def derive_universal:
+def derive_universal {α: Type u}:
   ∀ {a: α},
     (derive universal a) ≡ universal := by
   intro a
@@ -243,7 +236,7 @@ def derive_universal:
 
 -- δ𝟏  : δ 𝟏 a ⟷ ∅
 -- δ𝟏 = mk↔′ (λ ()) (λ ()) (λ ()) (λ ())
-def derive_emptystr:
+def derive_emptystr {α: Type u} {a: α}:
   ∀ {w: List α},
     (derive emptystr a) w <=> emptyset w := by
   intro w
@@ -268,7 +261,7 @@ def derive_emptystr:
 --   (λ { (refl , refl) → refl })
 --   (λ { (refl , refl) → refl })
 --   (λ { refl → refl })
-def derive_char:
+def derive_char {α: Type u}:
   ∀ {w: List α} {a: α} {c: α},
     (derive (char c) a) w <=> (scalar (a ≡ c) emptystr) w := by
     intros a c
@@ -280,7 +273,7 @@ def derive_char:
 
 -- δ∪  : δ (P ∪ Q) a ≡ δ P a ∪ δ Q a
 -- δ∪ = refl
-def derive_or:
+def derive_or {α: Type u}:
   ∀ {a: α} {P Q: Lang α},
     (derive (or P Q) a) ≡ (or (derive P a) (derive Q a)) := by
   intro a P Q
@@ -289,7 +282,7 @@ def derive_or:
 
 -- δ∩  : δ (P ∩ Q) a ≡ δ P a ∩ δ Q a
 -- δ∩ = refl
-def derive_and:
+def derive_and {α: Type u}:
   ∀ {a: α} {P Q: Lang α},
     (derive (and P Q) a) ≡ (and (derive P a) (derive Q a)) := by
   intro a P Q
@@ -298,8 +291,8 @@ def derive_and:
 
 -- δ·  : δ (s · P) a ≡ s · δ P a
 -- δ· = refl
-def derive_scalar:
-  ∀ {a: α} {s: Type} {P: Lang α},
+def derive_scalar {α: Type u}:
+  ∀ {a: α} {s: Type u} {P: Lang α},
     (derive (scalar s P) a) ≡ (scalar s (derive P a)) := by
   intro a s P
   constructor
@@ -315,7 +308,7 @@ def derive_scalar:
 --      ; (inj₂ ((u , v) , refl , Pu , Qv)) → refl })
 --   (λ { (([] , .(a ∷ w)) , refl , νP , Qaw) → refl
 --      ; ((.a ∷ u , v) , refl , Pu , Qv) → refl })
-def derive_concat:
+def derive_concat {α: Type u}:
   ∀ {w: List α} {a: α} {P Q: Lang α},
     (derive (concat P Q) a) w <=> (scalar (null P) (or (derive Q a) (concat (derive P a) Q))) w := by
   -- TODO
@@ -353,7 +346,7 @@ def derive_concat:
 --   ≈⟨ ×-congˡ (⋆-congˡ ✪↔☆) ⟩
 --     ((ν P) ✶ · (δ P a ⋆ P ☆)) w
 --   ∎ where open ↔R
-def derive_star:
+def derive_star {α: Type u}:
   ∀ {w: List α} {a: α} {P: Lang α},
     (derive (star P) a) w <=> (scalar (List (null P)) (concat (derive P a) (star P))) w := by
   -- TODO

Katydid/Conal/Decidability.lean

@@ -10,7 +10,7 @@ namespace Decidability
 --   no :¬A → Dec A
 class inductive Dec (P: Type u): Type u where
   | yes: P -> Dec P
-  | no: (P -> PEmpty.{u}) -> Dec P
+  | no: (P -> PEmpty.{u + 1}) -> Dec P
 
 @[inline_if_reduce, nospecialize] def Dec.decide (P : Type) [h : Dec P] : Bool :=
   h.casesOn (fun _ => false) (fun _ => true)
@@ -42,7 +42,7 @@ def unit? : Dec PUnit :=
 -- no ¬a  ⊎‽ no ¬b  = no [ ¬a , ¬b ]
 -- yes a  ⊎‽ no ¬b  = yes (inj₁ a)
 -- _      ⊎‽ yes b  = yes (inj₂ b)
-def sum? (a: Dec α) (b: Dec β): Dec (α ⊕ β) :=
+def sum? {α β: Type u} (a: Dec α) (b: Dec β): Dec (α ⊕ β) :=
   match (a, b) with
   | (Dec.no a, Dec.no b) =>
     Dec.no (fun ab =>
@@ -59,21 +59,21 @@ def sum? (a: Dec α) (b: Dec β): Dec (α ⊕ β) :=
 -- yes a  ×‽ yes b  = yes (a , b)
 -- no ¬a  ×‽ yes b  = no (¬a ∘ proj₁)
 -- _      ×‽ no ¬b  = no (¬b ∘ proj₂)
-def prod? (a: Dec α) (b: Dec β): Dec (α × β) :=
+def prod? {α β: Type u} (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')
 
 -- _✶‽ : Dec A → Dec (A ✶)
 -- _ ✶‽ = yes []
-def list?: Dec α -> Dec (List α) :=
+def list? {α: Type u}: Dec α -> Dec (List α) :=
   fun _ => Dec.yes []
 
 -- map′ : (A → B) → (B → A) → Dec A → Dec B
 -- map′ A→B B→A (yes a) = yes (A→B a)
 -- map′ A→B B→A (no ¬a) = no (¬a ∘ B→A)
-def map' (ab: A -> B) (ba: B -> A) (deca: Dec A): Dec B :=
+def map' {α β: Type u} (ab: α -> β) (ba: β -> α) (deca: Dec α): Dec β :=
   match deca with
   | Dec.yes a =>
     Dec.yes (ab a)
@@ -82,17 +82,17 @@ def map' (ab: A -> B) (ba: B -> A) (deca: Dec A): Dec B :=
 
 -- map‽⇔ : A ⇔ B → Dec A → Dec B
 -- map‽⇔ A⇔B = map′ (to ⟨$⟩_) (from ⟨$⟩_) where open Equivalence A⇔B
-def map? (ab: A <=> B) (deca: Dec A): Dec B :=
+def map? {α β: Type u} (ab: α <=> β) (deca: Dec α): Dec β :=
   map' ab.toFun ab.invFun deca
 
 -- _▹_ : A ↔ B → Dec A → Dec B
 -- f ▹ a? = map‽⇔ (↔→⇔ f) a?
-def apply (f: A <=> B) (deca: Dec A): Dec B :=
+def apply {α β: Type u} (f: α <=> β) (deca: Dec α): Dec β :=
   map? f deca
 
 -- _◃_ : B ↔ A → Dec A → Dec B
 -- g ◃ a? = ↔Eq.sym g ▹ a?
-def apply' (f: B <=> A) (deca: Dec A): Dec B :=
+def apply' {α β: Type u} (f: β <=> α) (deca: Dec α): Dec β :=
   map? f.sym deca
 
 end Decidability

Katydid/Conal/Language.lean

@@ -93,23 +93,4 @@ example: Lang Nat := (and (char 1) (char 2))
 example: Lang Nat := (scalar PUnit (char 2))
 example: Lang Nat := (concat (char 1) (char 2))
 
--- 𝜈 :(A✶ → B) → B -- “nullable”
--- 𝜈 f = f []
--- nullable
--- ν = backslash nu
-def null {α: Type u} {β: Type v} (f: List α -> β): β :=
-  f []
-
--- 𝒟: (A✶ → B) → A✶ → (A✶ → B) -- “derivative”
--- 𝒟 f u = 𝜆 v → f (u + v)
--- 𝒟 = backslash McD
-def derives {α: Type u} {β: Type v} (f: List α -> β) (u: List α): (List α -> β) :=
-  fun v => f (u ++ v)
-
--- 𝛿 : (A✶ → B) → A → (A✶ → B)
--- 𝛿 f a = 𝒟 f [a]
--- δ = backslash delta or backslash Gd
-def derive {α: Type u} {β: Type v} (f: List α -> β) (a: α): (List α -> β) :=
-  derives f [a]
-
 end Language