Add Extensional isomorphism

Katydid.lean

@@ -11,6 +11,7 @@ import Katydid.Expr.Desc
 import Katydid.Expr.Regex
 
 import Katydid.Conal.Decidability
+import Katydid.Conal.Function
 import Katydid.Conal.Language
 import Katydid.Conal.Calculus
 import Katydid.Conal.Examples

Katydid/Conal/Calculus.lean

@@ -1,6 +1,7 @@
 -- A translation to Lean from Agda
 -- https://github.com/conal/paper-2021-language-derivatives/blob/main/Calculus.lagda
 
+import Katydid.Conal.Function
 import Katydid.Conal.Language
 import Mathlib.Logic.Equiv.Defs -- ≃
 import Katydid.Std.Tipe
@@ -236,12 +237,16 @@ def derivative_universal:
 
 -- δ𝟏  : δ 𝟏 a ⟷ ∅
 -- δ𝟏 = mk↔′ (λ ()) (λ ()) (λ ()) (λ ())
--- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
-def derivative_emptyStr:
-  ∀ (a: α),
-    (δ' ε a) ≡ ∅ := by
-  -- TODO
-  sorry
+def derivative_emptyStr: ∀ (w: List α), (δ' ε a) w <=> ∅ w := by
+  intro w
+  constructor
+  · intro D
+    simp at D
+    cases D
+    next D =>
+    contradiction
+  · intro E
+    contradiction
 
 -- δ`  : δ (` c) a ⟷ (a ≡ c) · 𝟏
 -- δ` = mk↔′

Katydid/Conal/Function.lean

@@ -0,0 +1,85 @@
+-- An approximation of the Function module in the Agda standard library.
+
+import Katydid.Std.Tipe
+
+-- A ↔ B = Inverse A B
+
+-- mk↔′ : ∀ (f : A → B) (f⁻¹ : B → A) → Inverseˡ f f⁻¹ → Inverseʳ f f⁻¹ → A ↔ B
+
+-- record Inverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+--   field
+--     to        : A → B
+--     from      : B → A
+--     to-cong   : Congruent _≈₁_ _≈₂_ to
+--     from-cong : Congruent _≈₂_ _≈₁_ from
+--     inverse   : Inverseᵇ _≈₁_ _≈₂_ to from
+
+-- Congruent : (A → B) → Set _
+-- Congruent f = ∀ {x y} → x ≈₁ y → f x ≈₂ f y
+
+-- Inverseᵇ : (A → B) → (B → A) → Set _
+-- Inverseᵇ f g = Inverseˡ f g × Inverseʳ f g
+
+-- Inverseˡ : (A → B) → (B → A) → Set _
+-- Inverseˡ f g = ∀ {x y} → y ≈₁ g x → f y ≈₂ x
+
+-- Inverseʳ : (A → B) → (B → A) → Set _
+-- Inverseʳ f g = ∀ {x y} → y ≈₂ f x → g y ≈₁ x
+
+-- (_≈₁_ : Rel A ℓ₁) -- Equality over the domain
+-- (_≈₂_ : Rel B ℓ₂) -- Equality over the codomain
+
+-- Rel : Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
+-- Rel A ℓ = REL A A ℓ
+
+-- REL : Set a → Set b → (ℓ : Level) → Set (a ⊔ b ⊔ suc ℓ)
+-- REL A B ℓ = A → B → Set ℓ
+
+def Congruent (f: A -> B): Type :=
+  ∀ {x y}, x ≡ y -> f x ≡ f y
+
+def Inverse (f: A -> B) (g: B -> A): Type :=
+  ∀ {x y}, y ≡ g x -> f y ≡ x
+
+inductive Inverses (f: A -> B) (g: B -> A): Type (u + 1) where
+  | mk
+    (congF : Congruent f)
+    (congG : Congruent g)
+    (inverseL : Inverse f g)
+    (inverseR : Inverse g f): Inverses f g
+
+-- Lean has Bi-implication
+-- If and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa. By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a` is equivalent to the corresponding expression with `b` instead.
+-- structure Iff (a b : Prop) : Prop where
+  -- If `a → b` and `b → a` then `a` and `b` are equivalent. -/
+  -- intro ::
+  -- Modus ponens for if and only if. If `a ↔ b` and `a`, then `b`. -/
+  -- mp : a → b
+  -- Modus ponens for if and only if, reversed. If `a ↔ b` and `b`, then `a`. -/
+  -- mpr : b → a
+
+-- We use this weaker form of Inverses, but redefine it work Type
+
+structure TIff (a b: Type u): Type (u + 1) where
+  intro ::
+    mp : a → b
+    mpr : b → a
+
+infixr:100 " <=> " => TIff
+
+-- Extensional (or “pointwise”) isomorphism relates predicates isomorphic on every argument: P ←→ Q = ∀ {w} → P w ↔ Q w
+
+def EIff {w: List α} (a b: List α -> Type u) := (a w) <=> (b w)
+
+-- blackslash <-->
+infixr:100 " ⟷ " => EIff
+
+-- Note: We see that proofs that need ⟷ are typically proven using mk↔′
+-- δ𝟏  : δ 𝟏 a ⟷ ∅
+-- δ𝟏 = mk↔′ (λ ()) (λ ()) (λ ()) (λ ())
+
+-- Lean struggles to synthesize w sometimes, for example
+--   (δ' ε a) ⟷ ∅
+-- results in the error: "don't know how to synthesize implicit argument 'w'"
+-- Then we need to explicitly provide 'w', as such
+--   ∀ (w: List α), (δ' ε a) w <=> ∅ w

Katydid/Conal/Symbolic.lean

@@ -2,18 +2,30 @@
 -- https://github.com/conal/paper-2021-language-derivatives/blob/main/Symbolic.lagda
 
 import Katydid.Conal.Decidability
+import Katydid.Conal.Function
 import Katydid.Conal.Language
 
 variable {P Q : dLang α}
 variable {s : Type u}
 
 inductive Lang : (List α -> Type u) -> Type (u + 1) where
+  -- ∅ : Lang ◇.∅
   | emptySet : Lang dLang.emptyset
-  | universal : Lang (fun _ => PUnit)
+  -- 𝒰 : Lang ◇.𝒰
+  | universal : Lang dLang.universal
+  -- 𝟏 : Lang ◇.𝟏
   | emptyStr : Lang dLang.emptystr
+  -- ` : (a : A) → Lang (◇.` a)
   | char {a: Type u}: (a: α) -> Lang (dLang.char a)
+  -- _∪_ : Lang P → Lang Q → Lang (P ◇.∪ Q)
   | or : Lang P -> Lang Q -> Lang (dLang.or P Q)
+  -- _∩_ : Lang P → Lang Q → Lang (P ◇.∩ Q)
   | and : Lang P -> Lang Q -> Lang (dLang.and P Q)
+  -- _·_ : Dec s → Lang P → Lang (s ◇.· P)
   | scalar {s: Type u}: (Dec s) -> Lang P -> Lang (dLang.scalar s P)
+  -- _⋆_ : Lang  P → Lang Q → Lang (P ◇.⋆ Q)
   | concat : Lang P -> Lang Q -> Lang (dLang.concat P Q)
+  -- _☆  : Lang P → Lang (P ◇.☆)
   | star : Lang P -> Lang (dLang.star P)
+  -- _◂_  : (Q ⟷ P) → Lang P → Lang Q
+  | iso: (Q ⟷ P) -> Lang P -> Lang Q