Stream: math-comp analysis

Topic: Using HB instances

Zachary Stone (Jul 12 2022 at 01:21):

Now that I've touched the functions.v file a bit, I'm starting to understand things better. This is definitely a dramatic improvement over the existing approach. I did have a handful of questions here

1. Applying theorems with HB based arguments was not what I was expecting. Several times I got opaque error messages. If I have a theorem

Lemma example (f : {bij A >-> B}) : P f

and I have an f : X -> Y in scope, and my goal is P f. I'd like to write just apply: example, and then have a remaining goal that says

f is a bijection

Unfortunately, I just get an error about how the tactic failed to apply. Is there an better way to do this? How would you even write the f is a bijection thing as a goal? I would be fine to create a bespoke HB instance for f in the middle of my proof. The difficulty is determining exactly what instance to create.

2. I've been thinking about extending this with mixins for continuity and homeomorphisms. Is that where you were planning on going with this approach? It's infeasible to change everything at once, so is there an existing technique for incrementally changes?

Cyril Cohen (Jul 12 2022 at 08:21):

Zachary Stone said:

Now that I've touched the functions.v file a bit, I'm starting to understand things better. This is definitely a dramatic improvement over the existing approach. I did have a handful of questions here

1. Applying theorems with HB based arguments was not what I was expecting. Several times I got opaque error messages. If I have a theorem

Lemma example (f : {bij A >-> B}) : P f

and I have an f : X -> Y in scope, and my goal is P f. I'd like to write just apply: example, and then have a remaining goal that says

f is a bijection

Unfortunately, I just get an error about how the tactic failed to apply. Is there an better way to do this? How would you even write the f is a bijection thing as a goal? I would be fine to create a bespoke HB instance for f in the middle of my proof. The difficulty is determining exactly what instance to create.

2. I've been thinking about extending this with mixins for continuity and homeomorphisms. Is that where you were planning on going with this approach? It's infeasible to change everything at once, so is there an existing technique for incrementally changes?

1. Local instances are indeed problematic right now, the current solution is to use the Pbij helper lemma, as in have /Pbij : set_bij A B f.. We have been and are going to work on lighter solutions though.
2. Yes! The plan is to extend this with various kinds of morphisms (continuity, etc), and stuff. The main problem right now is that it will soon interfere with a parallel hierarchy (namely additive, rmorphism, etc) which is built by hand instead of HB. When https://github.com/math-comp/math-comp/pull/733 is finally merged, we might finally have the ability to merge both hierarchy.

2'. Also, a longer term goal of mine is to make HB generate structures and morphisms simultaneously (when appropriate) and provide the common language (symbols) and theory of category theory to handle them.

Zachary Stone (Jul 14 2022 at 01:30):

1. Ah, that explains what those lemmas are doing. I figured I wasn't the first person to have the problem.
2. Ah, generating the morphism is a nice touch. I'm all for the automation. But I'm no category theory expert. Is that an existing category theory library you'd leverage?

Last updated: Oct 13 2024 at 01:02 UTC