refactor: Language as a one-field structure

[Parcly-Taxel]

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]

PR summary 2e36a1dbb4

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
+ inf_def
+ instance : BooleanAlgebra (Language α)
+ instance : CompleteAtomicBooleanAlgebra (Language α)
+ instance : Insert (List α) (Language α)
+ instance : KStar (Language α)
+ instance : Lattice (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
6892	-9	backward.isDefEq.respectTransparency

Current commit a03de4066b
Reference commit 2e36a1dbb4

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).

[eric-wieser]

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]

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

[YaelDillies]

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?

[YaelDillies]

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

[YaelDillies]

Can you please Equiv.distribLattice here?

[YaelDillies]

or even Equiv.completeAtomicBooleanAlgebra right away?

[Parcly-Taxel]

Equiv.completeAtomicBooleanAlgebra doesn't exist…

[YaelDillies]

Can you add it then? See Equiv.group for a model