Skip to content

refactor: Language as a one-field structure#36934

Open
Parcly-Taxel wants to merge 15 commits intoleanprover-community:masterfrom
Parcly-Taxel:language1fs
Open

refactor: Language as a one-field structure#36934
Parcly-Taxel wants to merge 15 commits intoleanprover-community:masterfrom
Parcly-Taxel:language1fs

Conversation

@Parcly-Taxel
Copy link
Copy Markdown
Collaborator

@Parcly-Taxel Parcly-Taxel commented Mar 21, 2026

I came across definitional equality problems when trying to prove the following as part of a challenge from my PhD advisor:

import Mathlib.Computability.Language

variable {α : Type*}

/-- `IsSingleton y` states that `y` consists of only one word, and that word is not empty. -/
def IsSingleton (y : Language α) : Prop :=
  (∀ z ≤ y, z = y ∨ z = 0) ∧ y ≠ 1 ∧ y ≠ 0

lemma isSingleton_iff {y : Language α} : IsSingleton y ↔ ∃ w ≠ [], y = {w} := by
  sorry

This refactor resolves said defeq problems by making Language into a one-field structure with toSet and ofSet.


@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 21, 2026

PR summary 7555c791b1

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ bot_def
+ compl_def
+ equiv
+ inf_def
+ instance : CompleteAtomicBooleanAlgebra (Language α)
+ instance : Insert (List α) (Language α)
+ instance : KStar (Language α)
+ instance : Membership (List α) (Language α)
+ instance : Singleton (List α) (Language α)
+ le_def
+ mem_def
+ mem_singleton_iff
+ ofSet_toSet
+ sInf_def
+ sSup_def
+ sup_def
+ toSet_accepts_comap
+ toSet_ofSet
+ top_def
- accepts_comap
- ext
- instance : Inhabited (Language α) := ⟨(∅ : Set _)⟩
- instance : Insert (List α) (Language α) := ⟨Set.insert⟩
- instance : KStar (Language α) := ⟨fun l ↦ {x | ∃ L : List (List α), x = L.flatten ∧ ∀ y ∈ L, y ∈ l}⟩
- instance : Membership (List α) (Language α) := ⟨Set.Mem⟩
- instance : Singleton (List α) (Language α) := ⟨Set.singleton⟩
-+-+ acceptsFrom

You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.


Decrease in tech debt: (relative, absolute) = (9.00, 0.00)
Current number Change Type
6795 -9 backward.isDefEq.respectTransparency

Current commit 3ee298d586
Reference commit 7555c791b1

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions bot added the t-computability Computability theory (TMs, DFAs, languages, grammars, etc) label Mar 21, 2026
@Parcly-Taxel Parcly-Taxel requested a review from vihdzp March 21, 2026 06:10
@eric-wieser
Copy link
Copy Markdown
Member

An alternative I tried and failed to do in the past would be to make SetSemiring a structure and Language an abbrev for it.

@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 30, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

This pull request has conflicts, please merge master and resolve them.

@Parcly-Taxel Parcly-Taxel removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 1, 2026
@YaelDillies
Copy link
Copy Markdown
Contributor

An alternative I tried and failed to do in the past would be to make SetSemiring a structure and Language an abbrev for it.

This will only work if List is equipped with multiplication as
concatenation, right? Do we want this?

Comment thread Mathlib/Computability/ContextFreeGrammar.lean
Comment on lines +334 to +336
@[simp] lemma language_reverse : g.reverse.language = g.language.reverse := by
ext
simp [language, Language.reverse_eq_image, List.reverse_eq_iff]
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If you've set things up correctly, then this proof shouldn't need changing

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't know how to do this.

Comment thread Mathlib/Computability/DFA.lean
Comment thread Mathlib/Computability/DFA.lean Outdated
Comment thread Mathlib/Computability/Language.lean Outdated
Comment thread Mathlib/Computability/Language.lean Outdated
Comment thread Mathlib/Computability/Language.lean Outdated
Comment thread Mathlib/Computability/Language.lean Outdated
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 3, 2026
@eric-wieser
Copy link
Copy Markdown
Member

An alternative I tried and failed to do in the past would be to make SetSemiring a structure and Language an abbrev for it.

This will only work if List is equipped with multiplication as concatenation, right? Do we want this?

I meant SetSemiring (FreeMonoid X)

@YaelDillies
Copy link
Copy Markdown
Contributor

I tend to agree then. @Parcly-Taxel, could you investigate this solution?

@Parcly-Taxel
Copy link
Copy Markdown
Collaborator Author

I tend to agree then. @Parcly-Taxel, could you investigate this solution?

#37603

@Parcly-Taxel Parcly-Taxel removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 6, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 8, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 8, 2026
@mathlib-dependent-issues mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 8, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

This PR/issue depends on:

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-computability Computability theory (TMs, DFAs, languages, grammars, etc)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants