Dependent type runtime

Stream: new members

[Nicolò Cavalleri]

I have an abstract question which arises from a concrete problem which is complicated to transform into an #mwe, so I will try to ask it in words (I can link a branch though). If I have a dependent type, say Π a : α, A, and x : A a, y : A b, where a and b are equal but not definitionally equal (I need to use an easy simp lemma to show that a = b), the proposition x = y will not be accepted by Lean. If I need to impose this proposition as a condition in a structure, what can I do? I kind of managed to produce an accepted proposition in tactic mode (by rewriting the simp lemma and then using exact), but it is extremely slow to compile, so I wonder if there is a better way or what is in general a good solution to this kind of problem. Also, although it typechecks, I did not manage to test it yet to see if it is what I want because the goal when trying to prove things is just prop so I cannot say it works yet (it could be that I should use exact with something of Type the prop I want but I don't really know how to do this)

[Kenny Lau]

you can write x == y and end up in heq hell

[Kenny Lau]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/heq.20hell.20again

[Nicolò Cavalleri]

Do you have any resource about ==? I mean to understand better what it is and what it does

[Nicolò Cavalleri]

I cannot find a way to search for "==" in Zulip, it tells me no results when at least this chat should clearly appear in the results

[Alex J. Best]

== is the notation for heterogeneous equality, its in https://leanprover.github.io/tutorial/tutorial.pdf at least

[Patrick Massot]

docs#heq

[Kevin Buzzard]

You can define a function from A a to A b and show it maps x to y

[Kenny Lau]

maybe we should prove that eq.rec is a ring hom etc

[Nicolò Cavalleri]

Would you suggest trying to avoid using heq at all costs? It actually seems to be designed exactly for my problem

[Nicolò Cavalleri]

But I already encountered the first problem: how do I apply extensionality results to heq?

[Mario Carneiro]

don't use heq

[Mario Carneiro]

that's really the best advice I can give; if you are using heq you are either doing something really specialized or something has gone wrong earlier

[Mario Carneiro]

Do you have a #mwe?

[Nicolò Cavalleri]

No things departed from mathlib too much time ago, I have a big branch

[Mario Carneiro]

you should link a branch then

[Nicolò Cavalleri]

I am using it to define left invariant vector fields. I kind of need to use it naturally as two different tangent vectors at two different tangent spaces have different types

[Mario Carneiro]

You can still sorry things out for the purpose of an #mwe you know

[Nicolò Cavalleri]

Yeah but there is many PRs in between, I feel my problem can be discussed philosophically first

[Mario Carneiro]

well I want to #xy your problem and I can't do that without more context

[Mario Carneiro]

I want to know what problem got you to this stage

[Nicolò Cavalleri]

Ok I'll link a branch tomorrow as there are many things I need to write to explain what is going on: there's really a lot of code in between. In any case I implemented everything as in standard maths. Tangent spaces are spaces of derivations at that point, so it feels natural that to impose the condition of left invatiant vector field I need to use heq. Lean cannot know in advance the tangent space of the vector field evaluated at g and the tangent space of the vector field evaluated at the identity and then transported to g are the same space

[Nicolò Cavalleri]

There is a lemma that proves it but lean cannot know it

[Nicolò Cavalleri]

But just to sleep well tonight and finish off what I started: there is no standard way to apply extensionality to heq right?

[Mario Carneiro]

You really don't need all the code here

[Mario Carneiro]

just snip out the part that contains the heq, the stuff needed to understand the types of those objects, and then just axiomatize all the things needed to make those things typecheck

[Mario Carneiro]

I have never seen an issue that needs an #mwe of more than 50 lines unless it is actually a code review question

[Mario Carneiro]

even if it doesn't compile, could you post the code that says

so it feels natural that to impose the condition of left invatiant vector field I need to use heq

[Mario Carneiro]

Lean cannot know in advance the tangent space of the vector field evaluated at g and the tangent space of the vector field evaluated at the identity and then transported to g are the same space

I think @Sebastien Gouezel has dealt with a problem similar to this for defining tangent spaces in manifolds

[Mario Carneiro]

Nicolò Cavalleri said:

But just to sleep well tonight and finish off what I started: there is no standard way to apply extensionality to heq right?

The theorem f == g -> x == y -> f x == g y is not a theorem in lean (it is consistent but not provable from lean's axioms), but f = g -> x1 == y1 -> ... -> xn == yn -> f x1 ... xn == g y1 ... yn is provable (and I believe congr will prove it). Maybe this answers your question?

[Nicolò Cavalleri]

Well this is gonna take me at least two hours haha I promise there's like 1500 lines of code between the current state of mathlib and my branch! When I'll link the branch if someone will be able to write a 50 lines #mwe I'll be extremely surprised. The structure is

def Lb (I : model_with_corners 𝕜 E H)
  (G : Type*) [topological_space G] [charted_space H G] [smooth_manifold_with_corners I G]
  [group G] [topological_group G] [lie_group I G] (g : G) : C∞(I, G; I, G) :=
⟨(L g), smooth_mul_left⟩

def fdifferential (f : C∞(I, M; I', M')) (x : M) (v : point_derivation I M x): (point_derivation I' M' (f x))

def eval (X : vector_field_derivation I M) (x : M) : point_derivation I M x

structure left_invariant_vector_field (I : model_with_corners 𝕜 E H)
  (G : Type*) [topological_space G] [charted_space H G] [smooth_manifold_with_corners I G]
  [group G] [topological_group G] [lie_group I G] extends vector_field_derivation I G :=
(left_invariant : ∀ g : G, to_vector_field_derivation.eval g == (fd (Lb I G g)) (1 : G) (to_vector_field_derivation.eval (1 : G)))

[Nicolò Cavalleri]

Now I try to define something

[Nicolò Cavalleri]

Names are temporary not at all what I plan to push

[Mario Carneiro]

So you can just delete the typeclasses, they look irrelevant to the example. But the types of fd and Lb look important, put them in the mwe

[Nicolò Cavalleri]

fd is the differential in this context, Lb left multiplication for bundled smooth maps

[Mario Carneiro]

also to_vector_field_derivation.eval

[Nicolò Cavalleri]

eval is a function that evaluates a vector field at a point

[Mario Carneiro]

sure, I mean the types of all those functions should be in the mwe

[Mario Carneiro]

My guess is, you need a function that maps the type of to_vector_field_derivation.eval g (see here I need to see the type of to_vector_field_derivation.eval to say the right words) to the type of (fd (Lb I G g))

[Mario Carneiro]

this type is a map from P x to P y where x = y, although usually you can say something weaker than just x = y

[Mario Carneiro]

So point_derivation I M x for different values of x are different vector spaces?

[Nicolò Cavalleri]

Yes

[Mario Carneiro]

I guess P here is point_derivation I M

[Mario Carneiro]

Yeah the easy thing is to just make a function point_derivation_eq : x = y -> point_derivation I M x -> point_derivation I M y

[Mario Carneiro]

and apply it here to perform the type juggling

[Mario Carneiro]

with a bit of soul searching you might find a more appropriate assumption than x = y, like x <= y for some sense of <=

[Nicolò Cavalleri]

Ok but so just for general culture heq should not exist right? I cannot really immagine a more natural situation for it to be used than this one, so I guess you think it should never be used

[Mario Carneiro]

I mean you could use it here, it's equivalent, but it will not be as nice to work with

[Mario Carneiro]

if you choose to put it in the structure you will want lemmas saying how to get from it to various other versions using explicit coercion between types

[Nicolò Cavalleri]

Ok then I'll link a branch tomorrow so to get help to remove it cause I am not sure I am able to do it now

[Nicolò Cavalleri]

Just to write the code to show my purpose though do you know how to use extensionality rules with it? I promise I'll remove it I just want to test the machinery I wrote before people can help me removing it

[Mario Carneiro]

You will have to be more specific. Many basic tactics don't work on heq

[Mario Carneiro]

ext doesn't work on any heq goal that I can think of

[Mario Carneiro]

what kind of extensionality theorem are you talking about? again, #mwe even if the W comes later

[Reid Barton]

If the question is only to define left invariant vector fields then you should be able to define the action of G on vector fields and then take the vector fields fixed by this action

[Reid Barton]

Alternatively can you just change the left hand side to evaluation at g * 1 or something?

[Mario Carneiro]

or evaluation at _ to dodge the problem

[Reid Barton]

or another way (which is basically expanding out the action on vector fields approach to something similar to what you have) is to require an equation with g * x on the left, for all g x : G

[Reid Barton]

Have you constructed examples of left invariant vector fields yet?

[Sebastien Gouezel]

The mathlib tangent space is designed so that the type of the tangent space at all points is the same, to avoid precisely this issue. Are you trying to define another tangent space? (I don't think we want to have several instantiations of the tangent space in mathlib, the one we have should be general enough)

[Patrick Massot]

Yes, I was very confused by @Nicolò Cavalleri 's messages. Sébastien went out of his way to avoid exactly this issue, at the cost of an extremely unnatural construction of the tangent bundle. I think you are currently proving he was right. What you can probably do is building a function turning a derivation into a tangent vector, but you shouldn't make a new tangent bundle.

[Nicolò Cavalleri]

The point is that I tried for about a week to define it with the current tangent bundle but I am really not able to understand how am I supposed to use it and I hence I cannot really work with it. My initial strategy was to define vector bundles and then define vector fields as sections of a vector bundle. I was not able to do it and I tried to ask for help to do this, in the topic "Vector bundles" in new members and in the topic "Lie algebras and Lie groups" in maths, but I did not receive any answer to any of the two, and that was just the initial problem, then I had many others. So I looked for a workaround on which I could be more independent, without the need to ask for too much help, which is harder to get for more specific sections of the library, and I came up with an idea that is in the end purely algebraic: using derivations both for vector fields and to define Lie brackets. I am not redefining the tangent bundle, I am just doing everything in terms of derivations: I do not plan to work on any smooth structures on them, just dealing with the algebra. When I talked about tangent spaces before I meant point derivations, not a proper substitution to the current tangent space. I believe this solution looks extremely natural and proofs with these definition are short and easy. It is just that it does present this problem of heq, for which it looks though that there are solutions (I am thinking in particular to that of Mario) that would allow me to keep using just algebra. In any case I do not necessarily plan to upload all of this to mathlib, I just need to prove some results on my own, so if people have suggestions about how to use heq with extensionality rules I'm happy to hear them all the same

[Reid Barton]

What's your definition of point_derivation?

[Nicolò Cavalleri]

variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
{E : Type*} [normed_group E] [normed_space 𝕜 E]
{H : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
(M : Type*) [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M]

open_locale manifold

def module_point_derivation (x : M) : module C∞(I, M; 𝕜) 𝕜 :=
{ smul := λ f k, f x * k,
  one_smul := λ k, one_mul k,
  mul_smul := λ f g k, mul_assoc _ _ _,
  smul_add := λ f g k, mul_add _ _ _,
  smul_zero := λ f, mul_zero _,
  add_smul := λ f g k, add_mul _ _ _,
  zero_smul := λ f, zero_mul _ }

def compatible_semimodule_tangent_space (x : M) :
  @compatible_semimodule 𝕜 C∞(I, M; 𝕜) _ _ _ 𝕜 _ (module_point_derivation I M x) _ :=
{ compatible_smul := λ h k, rfl, }

@[reducible] def point_derivation (x : M) :=
  @derivation 𝕜 C∞(I, M; 𝕜) _ _ _ 𝕜 _ (module_point_derivation I M x) _
  (compatible_semimodule_tangent_space I M x)

the derivation part is in the derivation PR but I can include it here if you want

[Reid Barton]

Yet another way to avoid heq is to work with the type \Sigma x, point_derivation I M x -- this is the total space of the tangent bundle in these terms

[Nicolò Cavalleri]

Ok cool this would be nice as well I'll give it a try

[Nicolò Cavalleri]

Do you have in mind any particular point in mathlib where a similar solution was used and which I could look for inspiration?

[Reid Barton]

just experiment

[Reid Barton]

the drawback is now you cannot easily e.g. add two tangent vectors that you know are based at the same point

[Reid Barton]

Mario Carneiro said:

Yeah the easy thing is to just make a function point_derivation_eq : x = y -> point_derivation I M x -> point_derivation I M y

At some point, you will probably be forced to do this :this: in any case

[Nicolò Cavalleri]

Ok thanks

[Reid Barton]

So ultimately, a v : point_derivation I M x is a function from C∞(I, M; 𝕜) that satisfies a long list of properties. The key point is that C∞(I, M; 𝕜) doesn't depend on x any more. You want to prove that if x = y, then the properties for point_derivation I M x are the same (equivalent) to the ones for point_derivation I M y, and therefore you can convert point_derivation I M x to point_derivation I M y by using the same function.

[Nicolò Cavalleri]

Ok you meant something like this:

def point_derivation_eq {I : model_with_corners 𝕜 E H}
  {M : Type*} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {x y : M}
  (h : x = y) (v : point_derivation I M x) : point_derivation I M y :=
by{ rw h at v, exact v }

lemma Lb_apply_one (I : model_with_corners 𝕜 E H) (G : Type*) [topological_space G]
  [charted_space H G] [smooth_manifold_with_corners I G] [group G] [topological_group G]
  [lie_group I G] (g : G) : (Lb I G g) 1 = g := by rw [Lb_apply, mul_one]

structure left_invariant_vector_field (I : model_with_corners 𝕜 E H)
  (G : Type*) [topological_space G] [charted_space H G] [smooth_manifold_with_corners I G]
  [group G] [topological_group G] [lie_group I G] extends vector_field_derivation I G :=
(left_invariant : ∀ g : G, to_vector_field_derivation.eval g = point_derivation_eq
  (Lb_apply_one I G g) ((fd (Lb I G g)) (1 : G) (to_vector_field_derivation.eval (1 : G))) )

right? This kind of works

[Nicolò Cavalleri]

All the same I wonder if it were possible to write a tactic hext that transforms extensionality rules for = into extensionality rules for ==. This would make woking with heq totally possible in my situation

[Nicolò Cavalleri]

I mean just for the sake of elegance, and not to write lemmas that have to make things work with point_derivation_eq

[Sebastien Gouezel]

A simple way to define the Lie algebra using the current tangent space in mathlib is just to define Ad by deriving conjugacy, and then ad by deriving Ad (see https://en.wikipedia.org/wiki/Adjoint_representation if you're not familiar with this).

[Nicolò Cavalleri]

Sebastien Gouezel said:

A simple way to define the Lie algebra using the current tangent space in mathlib is just to define Ad by deriving conjugacy, and then ad by deriving Ad (see https://en.wikipedia.org/wiki/Adjoint_representation if you're not familiar with this).

Well sure I do know what the adjoint representation is. The problem with this approach is that I am not really able to prove even basic stuff about the current tangent bundle, such as functoriality of the differential (if it has been proved I can't find it, the words functor composition and inverse are not in the documentation). Unless I have a stable help to use this tangent bundle I am not really able to use it...

[Sebastien Gouezel]

Hopefully everything you need on the derivative should be in the file mfderiv.lean, see https://leanprover-community.github.io/mathlib_docs/geometry/manifold/mfderiv.html. The fact that the derivative of the composition is the composition of derivatives should be there, probably under the name mfderiv_comp that you can guess once you know that the name for the derivative is mfderiv, as explained in the file-level docstring. If you want to use the full tangent map, then the file level docstring tells you that it is called tangent_map, and then the statement on the composition on the tangent maps is probably called tangent_map_comp (I haven't checked, but I hope this is it). If you have ideas on how we could improve the documentation to make this easier to find, your thoughts are most welcome!

[Sebastien Gouezel]

All this should also be covered at length in the tutorial for manifolds I gave at lftcm2020.

[Nicolò Cavalleri]

Ops right I do not know why I did not find it before, probably I looked for composition instead of comp thinking there would have been a documentation string above. I cannot find mfderiv_inv but that I should be able to prove it probably, I'll give it a try. Well I guess it is because that would require diffeomorphisms

[Nicolò Cavalleri]

I'd need to implement a version of mfderiv for diffeomorphism as I need the fact that the mfderiv of a diffeo is an isomorphism. Is it a good idea, how should it be called? I mean was this problem faced for fderiv already?

[Mario Carneiro]

Nicolò Cavalleri said:

All the same I wonder if it were possible to write a tactic hext that transforms extensionality rules for = into extensionality rules for ==. This would make woking with heq totally possible in my situation

I'm still confused by what exactly you mean by this. Could you write down the statement of the extensionality theorem you expect?

[Nicolò Cavalleri]

variables {I} {M} {x y : M} {v w : point_derivation I M x}

@[hext] theorem hext (h1 : point_derivation I M x = point_derivation I M y) (h2 : ∀ f, v f == w f) : v == w

[Reid Barton]

I think this might not be provable, but it should be fine if you change h1 to h1 : x = y

[Nicolò Cavalleri]

Reid Barton said:

I think this might not be provable, but it should be fine if you change h1 to h1 : x = y

That's totally fine! Just out of curiosity what is the strategy to prove it?

[Reid Barton]

cases h1, then rewrite heq to eq

[Reid Barton]

docs#heq_iff_eq

[Reid Barton]

(also, I'm assuming the type of w is wrong--should have y)

[Nicolò Cavalleri]

Reid Barton said:

(also, I'm assuming the type of w is wrong--should have y)

Yep sure sorry

[Nicolò Cavalleri]

Yeah it works even if h2 needs to be changed to only one equal, which is better and cases h1 seems a bit magic to me

[Nicolò Cavalleri]

In any case I wonder whether this kind of theorem can be generated automatically from ext theorems or they are specific to each case

[Sebastien Gouezel]

I think the closest we have to this is local_homeomorph.mfderiv (see the section /-! ### Differentiable local homeomorphisms -/ starting at line 1151 in mfderiv.lean). There are two possible paths:

• define homeomorph.differentiable, and homeomorph.mfderiv and so on, following the local_homeomorph API. So, the main objects would be homeomorphisms, and there would be predicates on them
• introduce bundled diffeomorphisms.

Both paths make sense. If you want to go the bundled route (which I think I like a little bit more), it would be important to have it in intermediate smoothness (i.e., be able to talk of a C^k-diffeomorphism between smooth manifolds, for any $0 \leq k \leq \infty$, where for k=0 this would just be homeomorphisms).

For local homeomorphisms, the bundled way isn't good because we want to be able to talk about the smoothness of the charts, and the charts are given as local homeos already. But this constraint does not apply to the global objects, so I think I would go for bundled.

[Nicolò Cavalleri]

Well I actually have a ready PR in cue with bundled diffeos which I was waiting to push after bundled maps, but I did the C^\infty case only. What do you wanna call C^k diffeomoerphisms?

[Sebastien Gouezel]

Something like (to be copy-pasted as the end of times_cont_mdiff.lean, but it would probably deserve its own file)

variables (I I' M M' n)
structure diffeomorph extends M ≃ M' :=
(times_cont_mdiff_symm : times_cont_mdiff I' I n inv_fun)
(times_cont_mdiff : times_cont_mdiff I I' n to_fun)

@[refl] def diffeomorph.refl : diffeomorph I M I M n :=
{ times_cont_mdiff := times_cont_mdiff_id,
  times_cont_mdiff_symm := times_cont_mdiff_id,
  ..equiv.refl M }

and so on, with a whole API to be written, with symm, trans, mono (to say that a C^n diffeo induces a C^m diffeo when m \leq n), coercions to functions, to homeos and to bundled continuous functions...