From 4effa43d57f4cf0fdcae87f6ecbd2034ebd12af0 Mon Sep 17 00:00:00 2001
From: Walter Schulze <awalterschulze@gmail.com>
Date: Sun, 28 Jan 2024 13:04:33 +0000
Subject: [PATCH] Hott alternatives for Language and Calculus

---
 Katydid.lean                            |  23 +-
 Katydid/Conal/CalculusHott.lean         | 315 ++++++++++++++++++++++++
 Katydid/Conal/LanguageHott.lean         |  88 +++++++
 Katydid/Conal/LanguageNotationHott.lean |  37 +++
 4 files changed, 453 insertions(+), 10 deletions(-)
 create mode 100644 Katydid/Conal/CalculusHott.lean
 create mode 100644 Katydid/Conal/LanguageHott.lean
 create mode 100644 Katydid/Conal/LanguageNotationHott.lean

diff --git a/Katydid.lean b/Katydid.lean
index 9223fe9..6f20c28 100644
--- a/Katydid.lean
+++ b/Katydid.lean
@@ -1,11 +1,14 @@
-import Katydid.Std.Lists
-import Katydid.Std.Ltac
-import Katydid.Std.Balistic
-import Katydid.Std.TDecidable
-import Katydid.Std.Tipe
+-- import Katydid.Std.Lists
+-- import Katydid.Std.Ltac
+-- import Katydid.Std.Balistic
+-- import Katydid.Std.TDecidable
+-- import Katydid.Std.Tipe
 
-import Katydid.Conal.Language
-import Katydid.Conal.LanguageNotation
-import Katydid.Conal.RegexNotation
-import Katydid.Conal.Calculus
-import Katydid.Conal.Examples
+-- import Katydid.Conal.Language
+-- import Katydid.Conal.LanguageNotation
+-- import Katydid.Conal.RegexNotation
+-- import Katydid.Conal.Calculus
+-- import Katydid.Conal.Examples
+import Katydid.Conal.LanguageHott
+import Katydid.Conal.LanguageNotationHott
+import Katydid.Conal.CalculusHott
diff --git a/Katydid/Conal/CalculusHott.lean b/Katydid/Conal/CalculusHott.lean
new file mode 100644
index 0000000..900bb42
--- /dev/null
+++ b/Katydid/Conal/CalculusHott.lean
@@ -0,0 +1,315 @@
+-- A translation to Lean from Agda
+-- https://github.com/conal/paper-2021-language-derivatives/blob/main/Calculus.lagda
+
+import Katydid.Conal.LanguageNotationHott
+import GroundZero.Types.Id
+import GroundZero.Types.Equiv
+open Lang
+open Id
+
+-- ν⇃ : Lang → Set ℓ      -- “nullable”
+-- ν⇃ P = P []
+def ν (P : Lang α) : Type u := -- backslash nu
+  P []
+
+-- δ⇃ : Lang → A → Lang   -- “derivative”
+-- δ⇃ P a w = P (a ∷ w)
+def δ (P : Lang α) (a : α) : Lang α := -- backslash delta
+  fun (w : List α) => P (a :: w)
+
+attribute [simp] ν δ
+
+-- ν∅  : ν ∅ ≡ ⊥
+-- ν∅ = refl
+hott theorem nullable_emptySet:
+  ∀ (α: Type),
+    @ν α ∅ = PEmpty := by
+  intro α
+  reflexivity
+
+-- ν𝒰  : ν 𝒰 ≡ ⊤
+-- ν𝒰 = refl
+hott theorem nullable_universal:
+  ∀ (α: Type),
+    @ν α 𝒰 = PUnit := by
+  intro α
+  reflexivity
+
+-- ν𝟏  : ν 𝟏 ↔ ⊤
+-- ν𝟏 = mk↔′
+--   (λ { refl → tt })
+--   (λ { tt → refl })
+--   (λ { tt → refl })
+--   (λ { refl → refl })
+theorem nullable_emptyStr:
+  ∀ (α: Type),
+    @ν α ε ≃ PUnit := by
+  sorry
+  -- intro α
+  -- refine Equiv.intro ?a ?b ?c ?d
+  -- intro
+  -- exact PUnit.unit
+  -- intro
+  -- exact trifle
+  -- intro
+  -- exact trifle
+  -- simp
+  -- intro x
+  -- cases x with
+  -- | _ => exact trifle
+
+theorem nullable_emptyStr':
+  ∀ (α: Type),
+    @ν α ε ≃ PUnit :=
+    sorry
+    -- fun _ => Tiso.intro
+    --   (fun _ => PUnit.unit)
+    --   (fun _ => trifle)
+    --   (sorry)
+    --   (sorry)
+
+-- ν`  : ν (` c) ↔ ⊥
+-- ν` = mk↔′ (λ ()) (λ ()) (λ ()) (λ ())
+theorem nullable_char:
+  ∀ (c: α),
+    ν (char c) ↔ PEmpty := by
+  sorry
+  -- intro α
+  -- simp
+  -- apply Tiso.intro
+  -- intro
+  -- contradiction
+  -- intro
+  -- contradiction
+  -- sorry
+  -- sorry
+
+theorem nullable_char':
+  ∀ (c: α),
+    ν (char c) -> PEmpty := by
+  intro
+  refine (fun x => ?c)
+  simp at x
+  contradiction
+
+-- set_option pp.all true
+-- #print nullable_char'
+
+theorem t : 1 = 2 -> False := by
+  intro
+  contradiction
+
+theorem t'' : 1 = 2 -> False := by
+  intro
+  contradiction
+
+-- theorem t''' : 1 = 2 → False :=
+-- fun a => absurd a (of_decide_eq_false (Eq.refl (decide (1 = 2))))
+
+-- theorem t' : 1 = 2 → False :=
+-- fun a =>
+--   (TEq.casesOn (motive := fun a_1 x => 2 = a_1 → HEq a x → False) a
+--       (fun h => Nat.noConfusion h fun n_eq => Nat.noConfusion n_eq) (Eq.refl 2) (HEq.refl a)).elim
+
+-- theorem nullable_char'''.{u_2, u_1} : {α : Type u_1} → (c : α) → ν.{u_1} (Lang.char.{u_1} c) → PEmpty.{u_2} :=
+-- fun {α : Type u_1} (c : α) (x : ν.{u_1} (Lang.char.{u_1} c)) =>
+--   False.elim.{u_2}
+--     (False.elim.{0}
+--       (TEq.casesOn.{0, u_1} (motive := fun (a : List.{u_1} α) (x_1 : TEq.{u_1} List.nil.{u_1} a) =>
+--         Eq.{u_1 + 1} (List.cons.{u_1} c List.nil.{u_1}) a → HEq.{u_1 + 1} x x_1 → False) x
+--         (fun (h : Eq.{u_1 + 1} (List.cons.{u_1} c List.nil.{u_1}) List.nil.{u_1}) => List.noConfusion.{0, u_1} h)
+--         (Eq.refl.{u_1 + 1} (List.cons.{u_1} c List.nil.{u_1})) (HEq.refl.{u_1 + 1} x)))
+
+-- ν∪  : ν (P ∪ Q) ≡ (ν P ⊎ ν Q)
+-- ν∪ = refl
+theorem nullable_or:
+  ∀ (P Q: Lang α),
+    ν (P ⋃ Q) = (Sum (ν P) (ν Q)) := by
+  intro P Q
+  reflexivity
+
+-- ν∩  : ν (P ∩ Q) ≡ (ν P × ν Q)
+-- ν∩ = refl
+theorem nullable_and:
+  ∀ (P Q: Lang α),
+    ν (P ⋂ Q) = (Prod (ν P) (ν Q)) := by
+  intro P Q
+  reflexivity
+
+-- ν·  : ν (s · P) ≡ (s × ν P)
+-- ν· = refl
+theorem nullable_scalar:
+  ∀ (s: Type) (P: Lang α),
+    ν (Lang.scalar s P) = (Prod s (ν P)) := by
+  intro P Q
+  reflexivity
+
+-- ν⋆  : ν (P ⋆ Q) ↔ (ν P × ν Q)
+-- ν⋆ = mk↔′
+--   (λ { (([] , []) , refl , νP , νQ) → νP , νQ })
+--   (λ { (νP , νQ) → ([] , []) , refl , νP , νQ })
+--   (λ { (νP , νQ) → refl } )
+--   (λ { (([] , []) , refl , νP , νQ) → refl})
+theorem nullable_concat:
+  ∀ (P Q: Lang α),
+    ν (P, Q) ≃ (Prod (ν Q) (ν P)) := by
+  -- TODO
+  sorry
+
+-- ν✪  : ν (P ✪) ↔ (ν P) ✶
+-- ν✪ {P = P} = mk↔′ k k⁻¹ invˡ invʳ
+--  where
+--    k : ν (P ✪) → (ν P) ✶
+--    k zero✪ = []
+--    k (suc✪ (([] , []) , refl , (νP , νP✪))) = νP ∷ k νP✪
+
+--    k⁻¹ : (ν P) ✶ → ν (P ✪)
+--    k⁻¹ [] = zero✪
+--    k⁻¹ (νP ∷ νP✶) = suc✪ (([] , []) , refl , (νP , k⁻¹ νP✶))
+
+--    invˡ : ∀ (νP✶ : (ν P) ✶) → k (k⁻¹ νP✶) ≡ νP✶
+--    invˡ [] = refl
+--    invˡ (νP ∷ νP✶) rewrite invˡ νP✶ = refl
+
+--    invʳ : ∀ (νP✪ : ν (P ✪)) → k⁻¹ (k νP✪) ≡ νP✪
+--    invʳ zero✪ = refl
+--    invʳ (suc✪ (([] , []) , refl , (νP , νP✪))) rewrite invʳ νP✪ = refl
+
+-- ν☆  : ν (P ☆) ↔ (ν P) ✶
+-- ν☆ {P = P} =
+--   begin
+--     ν (P ☆)
+--   ≈˘⟨ ✪↔☆ ⟩
+--     ν (P ✪)
+--   ≈⟨ ν✪ ⟩
+--     (ν P) ✶
+--   ∎ where open ↔R
+theorem nullable_star:
+  ∀ (P: Lang α),
+    ν (P *) ≃ List (ν P) := by
+  -- TODO
+  sorry
+
+-- δ∅  : δ ∅ a ≡ ∅
+-- δ∅ = refl
+theorem derivative_emptySet:
+  ∀ (a: α),
+    (δ ∅ a) = ∅ := by
+  intro a
+  reflexivity
+
+-- δ𝒰  : δ 𝒰 a ≡ 𝒰
+-- δ𝒰 = refl
+theorem derivative_universal:
+  ∀ (a: α),
+    (δ 𝒰 a) = 𝒰 := by
+  intro a
+  reflexivity
+
+-- δ𝟏  : δ 𝟏 a ⟷ ∅
+-- δ𝟏 = mk↔′ (λ ()) (λ ()) (λ ()) (λ ())
+-- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
+theorem derivative_emptyStr:
+  ∀ (a: α),
+    (δ ε a) = ∅ := by
+  -- TODO
+  sorry
+
+-- δ`  : δ (` c) a ⟷ (a ≡ c) · 𝟏
+-- δ` = mk↔′
+--   (λ { refl → refl , refl })
+--   (λ { (refl , refl) → refl })
+--   (λ { (refl , refl) → refl })
+--   (λ { refl → refl })
+-- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
+theorem derivative_char:
+  ∀ (a: α) (c: α),
+    (δ (char c) a) = Lang.scalar (a = c) ε := by
+    intros a c
+    unfold δ
+    unfold char
+    unfold emptyStr
+    unfold scalar
+    sorry
+
+-- δ∪  : δ (P ∪ Q) a ≡ δ P a ∪ δ Q a
+-- δ∪ = refl
+theorem derivative_or:
+  ∀ (a: α) (P Q: Lang α),
+    (δ (P ⋃ Q) a) = ((δ P a) ⋃ (δ Q a)) := by
+  intro a P Q
+  reflexivity
+
+-- δ∩  : δ (P ∩ Q) a ≡ δ P a ∩ δ Q a
+-- δ∩ = refl
+theorem derivative_and:
+  ∀ (a: α) (P Q: Lang α),
+    (δ (P ⋂ Q) a) = ((δ P a) ⋂ (δ Q a)) := by
+  intro a P Q
+  reflexivity
+
+-- δ·  : δ (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
+  intro a s P
+  reflexivity
+
+-- δ⋆  : δ (P ⋆ Q) a ⟷ ν P · δ Q a ∪ δ P a ⋆ Q
+-- δ⋆ {a = a} {w = w} = mk↔′
+--   (λ { (([] , .(a ∷ w)) , refl , νP , Qaw) → inj₁ (νP , Qaw)
+--      ; ((.a ∷ u , v) , refl , Pu , Qv) → inj₂ ((u , v) , refl , Pu , Qv) })
+--   (λ { (inj₁ (νP , Qaw)) → ([] , a ∷ w) , refl , νP , Qaw
+--      ; (inj₂ ((u , v) , refl , Pu , Qv)) → ((a ∷ u , v) , refl , Pu , Qv) })
+--   (λ { (inj₁ (νP , Qaw)) → refl
+--      ; (inj₂ ((u , v) , refl , Pu , Qv)) → refl })
+--   (λ { (([] , .(a ∷ w)) , refl , νP , Qaw) → refl
+--      ; ((.a ∷ u , v) , refl , Pu , Qv) → refl })
+-- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
+theorem derivative_concat:
+  ∀ (a: α) (P Q: Lang α),
+  -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
+    (δ (P , Q) a) = Lang.scalar (ν P) ((δ Q a) ⋃ ((δ P a), Q)) := by
+  -- TODO
+  sorry
+
+-- δ✪  : δ (P ✪) a ⟷ (ν P) ✶ · (δ P a ⋆ P ✪)
+-- δ✪ {P}{a} {w} = mk↔′ k k⁻¹ invˡ invʳ
+--  where
+--    k : δ (P ✪) a w → ((ν P) ✶ · (δ P a ⋆ P ✪)) w
+--    k (suc✪ (([] , .(a ∷ w)) , refl , (νP , P✪a∷w))) with k P✪a∷w
+--    ... |            νP✶  , etc
+--        = νP ∷ νP✶ , etc
+--    k (suc✪ ((.a ∷ u , v) , refl , (Pa∷u , P✪v))) = [] , (u , v) , refl , (Pa∷u , P✪v)
+
+--    k⁻¹ : ((ν P) ✶ · (δ P a ⋆ P ✪)) w → δ (P ✪) a w
+--    k⁻¹ ([] , (u , v) , refl , (Pa∷u , P✪v)) = (suc✪ ((a ∷ u , v) , refl , (Pa∷u , P✪v)))
+--    k⁻¹ (νP ∷ νP✶ , etc) = (suc✪ (([] , a ∷ w) , refl , (νP , k⁻¹ (νP✶ , etc))))
+
+--    invˡ : (s : ((ν P) ✶ · (δ P a ⋆ P ✪)) w) → k (k⁻¹ s) ≡ s
+--    invˡ ([] , (u , v) , refl , (Pa∷u , P✪v)) = refl
+--    invˡ (νP ∷ νP✶ , etc) rewrite invˡ (νP✶ , etc) = refl
+
+--    invʳ : (s : δ (P ✪) a w) → k⁻¹ (k s) ≡ s
+--    invʳ (suc✪ (([] , .(a ∷ w)) , refl , (νP , P✪a∷w))) rewrite invʳ P✪a∷w = refl
+--    invʳ (suc✪ ((.a ∷ u , v) , refl , (Pa∷u , P✪v))) = refl
+
+-- δ☆  : δ (P ☆) a ⟷ (ν P) ✶ · (δ P a ⋆ P ☆)
+-- δ☆ {P = P}{a} {w} =
+--   begin
+--     δ (P ☆) a w
+--   ≈˘⟨ ✪↔☆ ⟩
+--     δ (P ✪) a w
+--   ≈⟨ δ✪ ⟩
+--     ((ν P) ✶ · (δ P a ⋆ P ✪)) w
+--   ≈⟨ ×-congˡ (⋆-congˡ ✪↔☆) ⟩
+--     ((ν P) ✶ · (δ P a ⋆ P ☆)) w
+--   ∎ where open ↔R
+-- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
+theorem derivative_star:
+  ∀ (a: α) (P: Lang α),
+  -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
+    (δ (P *) a) = Lang.scalar (List (ν P)) (δ P a, P *) := by
+  -- TODO
+  sorry
diff --git a/Katydid/Conal/LanguageHott.lean b/Katydid/Conal/LanguageHott.lean
new file mode 100644
index 0000000..6a18af6
--- /dev/null
+++ b/Katydid/Conal/LanguageHott.lean
@@ -0,0 +1,88 @@
+-- A translation to Lean from Agda
+-- https://github.com/conal/paper-2021-language-derivatives/blob/main/Language.lagda
+
+import GroundZero.Types.Id
+
+open List
+
+-- module Language {ℓ} (A : Set ℓ) where
+universe u
+variable (α : Type u)
+
+-- Lang : Set (suc ℓ)
+-- Lang = A ✶ → Set ℓ
+def Lang: Type (u + 1) :=
+  List α -> Type u
+
+-- namespace Lang is required to avoid ambiguities with or, and, concat and star.
+namespace Lang
+
+-- 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}
+
+-- ∅ : Lang
+-- ∅ w = ⊥
+def emptySet : Lang α :=
+  -- 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 α :=
+  -- 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 α :=
+  fun w => w = []
+
+-- ` : A → Lang
+-- ` c w = w ≡ [ c ]
+def char (a : α): Lang α :=
+  fun w => w = [a]
+
+-- infixl 7 _·_
+-- _·_ : Set ℓ → Op₁ Lang
+-- (s · P) w = s × P w
+def scalar (s : Type u) (P : Lang α) : Lang α :=
+  fun w => s × P w
+
+-- infixr 6 _∪_
+-- _∪_ : Op₂ Lang
+-- (P ∪ Q) w = P w ⊎ Q w
+def or (P : Lang α) (Q : Lang α) : Lang α :=
+  fun w => P w ⊕ Q w
+
+-- infixr 6 _∩_
+-- _∩_ : Op₂ Lang
+-- (P ∩ Q) w = P w × Q w
+def and (P : Lang α) (Q : Lang α) : Lang α :=
+  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 α :=
+  fun (w : List α) =>
+    Σ (x : List α) (y : List α), (w = (x ++ y)) × P x × Q y
+
+-- Only the Prop version is available in mathlib https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/List/Defs.html#List.Forall
+-- so we have to create our own version for Type
+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)
+
+-- infixl 10 _☆
+-- _☆ : Op₁ Lang
+-- (P ☆) w = ∃ λ ws → (w ≡ concat ws) × All P ws
+def star (P : Lang α) : Lang α :=
+  fun (w : List α) =>
+    Σ (ws : List (List α)), (w = (List.join ws)) × All P ws
+
+-- 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
diff --git a/Katydid/Conal/LanguageNotationHott.lean b/Katydid/Conal/LanguageNotationHott.lean
new file mode 100644
index 0000000..4ba7d6b
--- /dev/null
+++ b/Katydid/Conal/LanguageNotationHott.lean
@@ -0,0 +1,37 @@
+import Katydid.Conal.LanguageHott
+
+-- `(priority := high)` is required to avoid the error: "ambiguous, possible interpretations"
+notation (priority := high) "∅" => Lang.emptySet -- backslash emptyset
+
+notation "𝒰" => Lang.universal -- backslash McU
+
+notation "ε" => Lang.emptyStr -- backslash epsilon
+
+notation:6 (priority := high) "{" c "}" => Lang.char c
+
+-- TODO: fix scalar to work in Calculus.lean
+infixl:4 " · " => Lang.scalar -- backslash .
+
+infixl:5 (priority := high) " ⋃ " => Lang.or -- backslash U
+
+infixl:4 " ⋂ " => Lang.and -- backslash I
+
+infixr:5 " , " => Lang.concat
+
+postfix:6 "*" => Lang.star
+
+-- Tests for notation
+
+-- #check 𝒰
+-- #check ε
+-- #check (ε ⋃ 𝒰)
+-- #check (ε ⋂ 𝒰)
+-- #check ∅
+-- #check (∅*)
+-- #check {'a'}
+-- #check {'b'}
+-- #check ({'a'} ⋂ ∅)
+-- #check ({'a'} ⋂ {'b'})
+-- #check ({1} ⋂ {2})
+-- #check (PUnit · {2})
+-- #check ({1}, {2})