feat: proof of Myhill-Nerode theorem for DFAs#491

Open

akhilesh-balaji wants to merge 26 commits into

leanprover:mainfrom

akhilesh-balaji:myhill-nerode

Commits on Apr 3, 2026

feat: prove myhill-nerode equivalence classes
akhilesh-balaji
committed

Commits on Apr 7, 2026

feat: proof of number of states of minimal DFA for a language
akhilesh-balaji
committed

Commits on Apr 8, 2026

Commits on Apr 13, 2026

Commits on Apr 14, 2026

Merge branch 'leanprover:main' into myhill-nerode
akhilesh-balaji
authored

Commits on Apr 15, 2026

Commits on Apr 20, 2026

fix linter errors and remove some unnecessary @[simp]
ctchou
committed

Commits on Apr 21, 2026

Merge remote-tracking branch 'upstream/main' into myhill-nerode
ctchou
committed

Commits on Apr 25, 2026

Commits on May 13, 2026

Commits on May 21, 2026

Merge remote-tracking branch 'upstream/main' into myhill-nerode
ctchou
committed

Commits on May 26, 2026

Merge remote-tracking branch 'upstream/main' into myhill-nerode
ctchou
committed

Commits on May 27, 2026

Merge remote-tracking branch 'upstream/main' into myhill-nerode
ctchou
committed

Commits on May 29, 2026

Merge remote-tracking branch 'upstream/main' into myhill-nerode
ctchou
committed

Commits on May 30, 2026

Fix a failure caused by toolchain update
ctchou
committed