[Merged by Bors] - refactor(data/pi/lex): Use lex, provide notation
#14164
Conversation
YaelDillies
added
the
awaiting-review
| ∃ i, (∀ j, r j i → x j = y j) ∧ s (x i) (y i) | ||
|
|
||
| /-- The cartesian product of an indexed family, equipped with the lexicographic order. -/ | ||
| def pilex (α : Type*) (β : α → Type*) : Type* := Π a, β a | ||
| notation `Πₗ` binders `, ` r:(scoped p, lex (Π i, p i)) := r |
There was a problem hiding this comment.
Should this be
| notation `Πₗ` binders `, ` r:(scoped p, lex (Π i, p i)) := r | |
| notation `Πₗ ` binders `, ` r:(scoped p, lex (Π i, p i)) := r |
or does lean add the space automaticaly?
There was a problem hiding this comment.
It seems like it does. This is the infoview on line 147 of data.sigma.order.
_x : Σₗ (i : ι), α i
and this is the notation declaration
notation `Σₗ` binders `, ` r:(scoped p, _root_.lex (sigma p)) := r
However my new notation gets torn in the infoview.
a b : lex (Π (i : ι), (λ (i : ι), β i) i)
Is there an equivalent of sigma p (as opposed to Σ i, p i) for Π i, p i?
There was a problem hiding this comment.
Is there an equivalent of
sigma p(as opposed toΣ i, p i) forΠ i, p i?
No, because if there were it would need two copies of itself in its own type!
There was a problem hiding this comment.
Ah yeah of course 😕
There was a problem hiding this comment.
Maybe best to not actually use the notation in this file then, so that the instances and lemmas are fully delta-reduced.
There was a problem hiding this comment.
Should I even introduce the notation then? There's no point in having it if we can't use it. An alternative would be the rather less practical Πₗ β.
There was a problem hiding this comment.
I think the notation could still be useful within a proof if you're constructing some big nested lex object; the delta reductions are probably mostly harmless, but keeping them out of the basic API lemmas is worth the trouble.
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
delegated
|
You should probably add the lemmas that |
|
bors merge |
Delete `pilex ι β` in favor of `lex (Π i, β i)` which we provide `Πₗ i, β i` notation for.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
lex, provide notationlex, provide notation
Delete
pilex ι βin favor oflex (Π i, β i)which we provideΠₗ i, β inotation for.