Lean Automata

monoid_recognizers.lean

import data.fintype

structure dfa (alphabet : Type) [fintype alphabet] :=
 (qq : Type) {is_finite : fintype qq} {has_decidable_eq : decidable_eq qq}
 (δ : qq → alphabet → qq)
 (init : qq)
 (fin : qq → bool)

def language (alphabet : Type) [fintype alphabet] := list alphabet → bool

def δ' {alphabet : Type} [fintype alphabet] {Δ : dfa alphabet} : 
    Δ.qq → list alphabet → Δ.qq 
    | i [] := i
    | i (x :: xs) := δ' (Δ.δ i x) xs

def language_of {alphabet : Type} [fintype alphabet] : 
    (dfa alphabet) → language alphabet
    | Δ  l := Δ.fin (δ' Δ.init l)

instance {α : Type} : monoid (list α) := ⟨list.append, list.append_assoc, list.nil, list.nil_append, list.append_nil⟩

structure monoid_recognizer (alphabet : Type) [fintype alphabet] :=
 (m : Type) {is_finite : fintype m} {is_monoid: monoid m} {has_decidable_eq : decidable_eq m}
 (fin : m → bool)
 (h : monoid_hom (list alphabet) m)

instance is_monoid_recognizer {A} [fintype A] (M : monoid_recognizer A) : monoid M.m := M.is_monoid

def recognized_by {alphabet : Type} [fintype alphabet] : 
    (monoid_recognizer alphabet) → language alphabet
    | M l := M.fin (M.h l)

instance monoid_of_endofunctions {α : Type} : monoid (α → α) := 
    ⟨ function.comp , function.comp.assoc, id, function.comp.left_id, function.comp.right_id ⟩

def dfa_to_recognizer {alphabet : Type} [fintype alphabet]  (Δ : dfa alphabet) : monoid_recognizer alphabet := 
@monoid_recognizer.mk _ _ 
    (Δ.qq → Δ.qq) (@pi.fintype Δ.qq _ Δ.is_finite Δ.has_decidable_eq (λ _, Δ.is_finite)) _ (@fintype.decidable_pi_fintype Δ.qq _ Δ.is_finite (λ _, Δ.has_decidable_eq))
    (λ f, Δ.fin (f Δ.init))
    ⟨(λ xs q, δ' q xs), sorry, sorry⟩

def recognizer_to_dfa {alphabet : Type} [fintype alphabet] (M : monoid_recognizer alphabet) : dfa alphabet := 
@dfa.mk _ _ 
    M.m M.is_finite M.has_decidable_eq
    (λ q a, q * (M.h [a]))
    (M.h []) 
    M.fin


theorem recognizer_to_dfa_works {alphabet : Type} [fintype alphabet] (l : language alphabet) : 
    ∀ (M : monoid_recognizer alphabet), ∃ (Δ : dfa alphabet), ∀ σ, recognized_by M σ = language_of Δ σ := 
begin
    intros,
    use (recognizer_to_dfa M),
    intros,
    sorry
end 

theorem dfa_to_recognizer_works {alphabet : Type} [fintype alphabet] (l : language alphabet) : 
    ∀ (Δ : dfa alphabet), ∃ (M : monoid_recognizer alphabet), ∀ σ, recognized_by M σ = language_of Δ σ := 
begin
    intros,
    use (dfa_to_recognizer Δ),
    intros,
    induction σ,
    sorry
end