Last active
January 14, 2020 13:39
-
-
Save Agnishom/426552564fd1a235ac7c009c24b11c09 to your computer and use it in GitHub Desktop.
Lean Automata
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment