feat(ModelTheory): Set.Definable is transitive #19695
Conversation
github-actions
bot
added
the
large-import
PR summary 4ff2da0ee9Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.ModelTheory.Definability | 692 | 736 | +44 (+6.36%) |
| Mathlib.ModelTheory.Semantics | 691 | 719 | +28 (+4.05%) |
| Mathlib.ModelTheory.Syntax | 690 | 717 | +27 (+3.91%) |
Import changes for all files
| Files | Import difference |
|---|---|
3 filesMathlib.ModelTheory.Algebra.Field.CharP Mathlib.ModelTheory.Algebra.Field.IsAlgClosed Mathlib.ModelTheory.Algebra.Ring.FreeCommRing |
1 |
Mathlib.FieldTheory.AxGrothendieck Mathlib.ModelTheory.Algebra.Ring.Definability |
16 |
Mathlib.ModelTheory.Order |
17 |
Mathlib.ModelTheory.Fraisse Mathlib.ModelTheory.Graph |
19 |
4 filesMathlib.ModelTheory.Complexity Mathlib.ModelTheory.Equivalence Mathlib.ModelTheory.Satisfiability Mathlib.ModelTheory.Types |
20 |
Mathlib.ModelTheory.Encoding |
22 |
8 filesMathlib.ModelTheory.Bundled Mathlib.ModelTheory.DirectLimit Mathlib.ModelTheory.ElementaryMaps Mathlib.ModelTheory.ElementarySubstructures Mathlib.ModelTheory.FinitelyGenerated Mathlib.ModelTheory.PartialEquiv Mathlib.ModelTheory.Skolem Mathlib.ModelTheory.Substructures |
23 |
Mathlib.ModelTheory.Ultraproducts |
25 |
Mathlib.ModelTheory.Algebra.Field.Basic |
26 |
Mathlib.ModelTheory.Syntax |
27 |
3 filesMathlib.ModelTheory.Algebra.Ring.Basic Mathlib.ModelTheory.Quotients Mathlib.ModelTheory.Semantics |
28 |
Mathlib.ModelTheory.Definability |
44 |
Declarations diff
+ BoundedFormula.subst_definitions
+ Definable.trans
+ Formula.subst_definitions
+ Functions.term
+ LEquiv.onTerm
+ LEquiv.onTerm_symm
+ Term.subst_definitions
+ TermDefinable
+ TermDefinable.Definable
+ TermDefinable.TermDefinable₁
+ TermDefinable.map_expansion
+ TermDefinable.mono
+ TermDefinable.trans
+ TermDefinable₁
+ TermDefinable₁.Definable₂
+ TermDefinable₁_comp
+ TermDefinable₁_comp_TermDefinable
+ TermDefinable₁_const
+ TermDefinable₁_id
+ TermDefinable₁_iff_TermDefinable
+ empty_termDefinable_iff
+ realize_foldr_imp
+ realize_function_term
+ substFunc
+ subst_definitions_extraVals
+ subst_definitions_extraVals_X
+ subst_definitions_extraVals_spec
+ termDefinable_iff_empty_termDefinable_with_params
+ tupleGraph
+++ subst_definitions_eq
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
Timeroot
added
the
blocked-by-other-PR
|
Some of the parts are not written in the Mathlib style. Do you want pointers to concrete places that need to be changed? |
Yes please! I tried to adhere to the style but I'm sure I missed some things. |
| /-- Equivalence between the Sigma type `(i : Fin m) × Fin (n i)` and `Fin (∑ i : Fin m, n i)`. -/ | ||
| def finSigmaFinEquiv {m : ℕ} {n : Fin m → ℕ} : (i : Fin m) × Fin (n i) ≃ Fin (∑ i : Fin m, n i) := | ||
| match m with | ||
| | 0 => @Equiv.equivOfIsEmpty _ _ _ (by simp; exact Fin.isEmpty') |
There was a problem hiding this comment.
Yes, the one argument I'm providing (and it seems necessary to manually provide) is an instance parameter which doesn't have name. An alternative would be to write
let _ : IsEmpty (Fin (∑ i, n i)) := by simpa using Fin.isEmpty'
Equiv.equivOfIsEmpty _ _
which works, if you think that's cleaner.
Mathlib/ModelTheory/Semantics.lean
Outdated
| } | ||
| · intro h xs is | ||
| have ht₁ := t₁.subst_definitions_eq hFs _ (by | ||
| simp at is |
There was a problem hiding this comment.
Happy to change it if you tell me an equivalent/better way to write it. The actual statement of the have is quite long and ugly. I tried := t₁.subst_definitions_eq hFs _ ?_ so that I could fill in the missing proof as another goal, but the it can't infer the value of the underscore and it gives errors.
mathlib4-dependent-issues-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
leanprover-community-bot-assistant
added
the
merge-conflict
github-actions
bot
removed
the
merge-conflict
leanprover-community-bot-assistant
added
the
merge-conflict
github-actions
bot
removed
the
merge-conflict
|
|
||
| ## Main Results | ||
|
|
||
| - `L.DefinableSet A α` forms a `BooleanAlgebra` | ||
| - `Set.Definable.image_comp` shows that definability is closed under projections in finite | ||
| dimensions. | ||
| - `Set.Definable_trans` shows that `Set.Definable` is transitive, in the sense that if `S` can be | ||
| defined in `L` and all of `L`'s functions and relations can be defined in `L'`, then `S` is | ||
| also definanble in `L'`. |
There was a problem hiding this comment.
| also definanble in `L'`. | |
| also definable in `L'`. |
| * the realizations of all L.Functions have tupleGraph that's Definable on S, | ||
| * the realizations of all L.Relations are Definable on S, | ||
| then S is Definable on T, as well. -/ | ||
| theorem Definable.trans {S : Set (α → M)} (h₁ : A.Definable L S) |
There was a problem hiding this comment.
The assumptions on this theorem are very close to some more-commonly used logic definitions, and it would be worth considering whether it's appropriate to do this through one of those.
- If L extends the language L', then this is basically an extension-by-definition.
- This is also very close to interpretability
There was a problem hiding this comment.
I poked at this a while (when I first wrote it) and this was the best set of assumptions I could come up with. I would not be all surprised though if you have something better. :)
Consider maybe, this as the "basic" statement, but then some specializations of this theorem with hypotheses that fit more naturally into certain uses...? I don't know.
Co-authored-by: Aaron Anderson <[email protected]>
|
|
||
| /-- A `TermDefinable` function postcomposed with `TermDefinable₁` is `TermDefinable`. -/ | ||
| @[fun_prop] | ||
| theorem TermDefinable₁_comp_TermDefinable {f : M → M} {g : (α → M) → M} |
There was a problem hiding this comment.
We could also compose a higher-arity (term-)definable function with a tuple of (term-)definable functions.
| rfl | ||
|
|
||
| /-- Maps a term's symbols along a language equivalence. Deprecated in favor of `LEquiv.onTerm`. -/ | ||
| @[deprecated LEquiv.onTerm (since := "2024-12-02")] |
There was a problem hiding this comment.
This whole PR seems quite big, and I expect it will help to split it up - if you do, it may be good to have one preliminary PR to just fix this nomenclature.
There was a problem hiding this comment.
Sure, that's a good point. I guess there are a few small lemmas/defs I have in this PR that I can also pull out separately (making explicit note of the names here also for myself):
realize_function_termrealize_foldr_impFunctions.termsubstFunc
Then, I can pull out the TermDefinable stuff into a separate PR.
That leaves something like 60% of this PR left, which is the various forms of subst_definitions_eq that all kind of need to coexist, describing how to substitute first-order formula (not just terms) into each other. That's the bulk here -- "substituting" formulas is a lot messier, since you really need to build them at the formula level but then pass the information through when you go in and recurse down the terms. If that makes sense.
Anyway, that would probably split the PR decently well.
leanprover-community-bot-assistant
added
the
merge-conflict
Upstreamed from the EquationalTheories project.
The main new theorem in this PR is
Set.Definable_trans, which is that definability of sets in first order logic is transitive. The other work (in Syntax/Semantics) is pretty much all to facilitate that statement and proof.