Yury G. Kudryashov (Dec 06 2020 at 22:44):
Currently I use a
local notation for docs#circle_deg1_lift.translation_number
In the future I'm going to need at least the following maps and their lifts to the real line:
circle_homeo: an order-preserving homeomorphism of the circle ;
circle_diffeo: an order-preserving -smooth diffeomorphism of the circle;
circle_break_homeo: a circle homeomorphism which is smooth at all points but one, and has a given ratio of left/right derivatives at this point;
circle_smooth_critical: a smooth homeomorphism of the circle with one (or finitely many) critical point(s).
In each case I'll need to talk about translation number of the lift and about the rotation number of the circle self-map. I have two questions:
- How can I avoid repeating all basic lemmas? Coercions? Typeclasses instead of structures? Something else?
- I need at least two symbols, one for the translation number and one for the rotation number. Any suggestions?
Yury G. Kudryashov (Dec 06 2020 at 22:51):
@Sebastien Gouezel :up:
Sebastien Gouezel (Dec 07 2020 at 08:06):
I think I would go for coercions. This could be painful if you had to rewrite along lemmas (because they would not syntactically be of the right form), but since you will mostly apply lemmas this should be fine.
You could even exercise your tactic skills if you have lemmas along which you want to rewrite. Assume you have a class
foo, a coercion to functions, and a bunch of lemmas involving
f x where
f : foo, for instance
foo.lemma2. And then you define a class
foo. Very often, one registers the function coercion for
bar, a coercion from
foo, the fact that the composition of the coercions is the function coercion, and one restates the lemma for
bar, in terms of the function coercion for
bar. I feel a small tactic
restate_function_lemmas foo bar [lemma1, lemma2] registering all the coercions and restating
bar.lemma2 would be extremely handy.
What about rho for the rotation number and tau for the translation number?
Sebastien Gouezel (Dec 07 2020 at 09:17):
While I'm dreaming, let me dream bigger. Is it possible that, whenever one declares a structure with a
to_fun field, then a function coercion is automatically declared? An even nicer magic would be if all the fields of the structure involving
to_fun and whose name ends with a prime would be restated without the prime and in terms of the function coercion.
And when one extends a structure
foo with a
to_fun field to a structure
bar, then a function coercion could be registered for
bar, and all lemmas of the form
foo.lemma1 in the namespace
foo and involving the function coercion for
foo are restated in the
bar namespace with the function coercion for
I have the impression this would simplify a lot of boilerplate code we have to write for every new function-like structure we introduce.
Eric Wieser (Dec 07 2020 at 10:48):
That would definitely be a useful thing to happen, and would eliminate much of
Johan Commelin (Dec 07 2020 at 11:09):
@Sebastien Gouezel I completely agree. We just need someone with good meta skills to write the automation for us.
Eric Wieser (Dec 07 2020 at 13:13):
I think we could do similar automation for things with a
carrier : set A member too
Eric Wieser (Dec 07 2020 at 13:20):
Would we get this inheritance automatically if we replaced
monoid_hom A B with
fun_subtype A B is_monoid_hom, where
fun_subtype is defeq to subtype?
Eric Wieser (Dec 07 2020 at 13:21):
Then we could just stick all the generic ext/for/mk lemmas on
Yury G. Kudryashov (Dec 07 2020 at 13:41):
This is a workaround which is not free (e.g., it doesn't work for
equivs) and doesn't give you automation for
map_* and more advanced lemmas.
Sebastien Gouezel (Dec 07 2020 at 14:02):
You're right that for
equiv it would do the wrong thing (a lemma for
f (f.symm x) would be extended with the naive procedure I sketched to a lemma for which
f.symm x would become
f.to_foo.symm x, which is not what we want). What about an attribute
@[extend_fun] if we want to extend the function lemmas from
bar automatically, and something else for equiv-like structures? An attribute
@[extend_equiv] would not work, as the
symm is meaningless when defining the structure, but a tactic that one would call once
bar.refl have been defined would be an option.
Yury G. Kudryashov (Dec 07 2020 at 14:10):
@Sebastien Gouezel Sorry for not being clear. I was trying to say that @Eric Wieser's approach with
subtype will not work in many cases.
Sebastien Gouezel (Dec 07 2020 at 14:11):
ok, thanks for the clarification. Still, there is indeed a problem with my initial proposal!
Yury G. Kudryashov (Dec 07 2020 at 14:12):
equivs we need to define
Yury G. Kudryashov (Dec 07 2020 at 14:12):
homs we need to define
Eric Wieser (Dec 07 2020 at 14:21):
it doesn't work for equivs
I hadn't thought of that
And for homs we need to define id and comp manually.
If we had
fun_subtype A B is_monoid_hom, could we create a
preserves_comp (is_monoid_hom A B) (is_monoid_hom B C) typeclass that can produce a
is_monoid_hom A C instance, and then define
fun_subtype.comp in terms of that typeclass?
Last updated: May 09 2021 at 10:11 UTC