transport tactic

Stream: metaprogramming / tactics

[Bryan Wang]

This question is more out of curiosity than anything, but I noticed that in mathlib3 there was a transport tactic, but it seems not in mathlib4 - is there any specific reason why?

[Johan Commelin]

I think it was almost never used in the Lean 3 days, and hence nobody bothered porting it.

[Kevin Buzzard]

The reason transport is used far less often than you think is the following observation (which I learnt from Mario). Mathematicians are presumably going to want the theorem that says that if X and Y are homeomorphic, and X is compact, then Y is compact, and it would be not hard to imagine a machine proving such a theorem for us. But in fact there's a stronger theorem, which is slightly less easy to imagine a computer proving, that if X is compact and X surjects onto Y then Y is compact, and this is a theorem you want in your API, so if you need the theorem that something homeomorphic to a compact thing is compact then you may as well just use that homeomorphisms are continuous surjections and get it that way.

A surprisingly large number of statements of the form "if X has property P and there's an isomorphism X \iso Y in the appropriate category then Y has property P" are special cases of "if X has property P and X -> Y is monic/epic then Y has property P", and in practice this is what gets used.

[Shreyas Srinivas]

Shouldn’t generalised rewriting be able to handle this in principle?

[Jovan Gerbscheid]

It looks to me like grw wouldn't be able to do this, because the relevent gcongr lemma doesn't exist in the library (and the transport tactic generates this kind of lemma on the fly).

Besides, I have only tested grw for rewriting with relations, not with for rewriting with data, like an Equiv, but feel free to try if that seems useful :)

[Shreyas Srinivas]

Fwiw, this kind of a tactic will be super useful in theoretical CS

[Shreyas Srinivas]

We often deal with isomorphic structures which are just different ways to talk about the same thing, but are computationally very different. For example adjacency matrices, adjacency lists, incidence matrices, and simplegraph, or different but equivalent computation models.

[Shreyas Srinivas]

@Jovan Gerbscheid : Would it help if we simply generated and tagged Prop variants of Equiv?

[Shreyas Srinivas]

Because to a point it already exists :https://github.com/leanprover/lean4/blob/919e297292280cdb27598edd4e03437be5850221/src/Init/Core.lean#L1307-L1323

[Jovan Gerbscheid]

@Shreyas Srinivas I don't think that it being in Type is a fundamental problem. However it seems to me that the main difficulty here is in generating the @[gcongr] lemmas.

Can you say in more detail what you would want from this tactic? I'm not familiar with the original transport tactic. I might be interested in implementing this kind of tactic

[Chris Henson]

Shreyas Srinivas said:

We often deal with isomorphic structures which are just different ways to talk about the same thing, but are computationally very different. For example adjacency matrices, adjacency lists, incidence matrices, and simplegraph, or different but equivalent computation models.

Note the similarity to motivations for HoTT, a type theory in which isomorphism implies equality. So I would be curious to see the implementation and scope of a transport tactic.

[Jovan Gerbscheid]

Do people have explicit examples of tactic steps for this tactic to do that aren't easy to do otherwise?

[Jireh Loreaux]

This recent paper is quite relevant. Cyril gave a talk about it at LftCM 2024 at CIRM.

[Christian Merten]

cc @Vincent Kuhlmann

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

I would think of examples from this paper

[Shreyas Srinivas]

They just pick a different case of different data structures representing the same abstract data type. If you map Ordered sets to balanced search trees, you might want properties of ordered set operations to translate to their AVL tree representations.

[Shreyas Srinivas]

And then from that to other search tree structures which have the ordering property for the children of each node.

[Vincent Kuhlmann]

Jireh Loreaux said:

This recent paper is quite relevant. Cyril gave a talk about it at LftCM 2024 at CIRM.

Yes it is quite an interesting framework regarding transport. I am currently writing an implementation for Lean, as part of my MSc thesis.

[Jovan Gerbscheid]

One reason why I'm interested in this is that I think that such a framework could be used to implement to_additive. Have you considered testing your implementation on some basic examples that to_additive handles?

[Vincent Kuhlmann]

Good suggestion! I haven't yet, but will try how far I get. At first glance, I'm a bit unsure of how I could encode the heuristics that to_additive needs (i.e. it shouldn't blindly replace all multiplications with additions). Looking at the code of to_additive, it seems that most code is about the heuristics and the frontend/configuration. So this would only become more elegant if my implementation for Lean has plenty of powerful knobs to tweak its behaviour, and can hence replace a lot of that code. This will probably fall out of scope for my thesis project however, my goal is a proof of concept, with spare time spent on improving ergonomics and pretty printing.

The strength of the Trocq framework lies more in transporting data types, with correspondence properties being modular so you only need to prove the minimum about them for what you need. Aside from equivalent and quotient types, this modular systems also allows for correspondences like WithBot Nat with Nat, so statements can be guarded against junk values with little administrational overhead. The paper has an example of doing this with infinite sums, transporting ∀ (f g : seq_xnnR), Σ (f + g) = Σ f + Σ g where summations yield infinity-aware values (think WithBot Nat) to ∀ (f g : summable), Σ (f + g) = Σ f + Σ g where summations yield plain naturals.

[Jovan Gerbscheid]

Yes, I absolutely agree that actually integrating such a tool into to_additive would be a lot of extra work. But it could be interesting to see if it the tool also works in this context. There is indeed this issue in to_additive that we need a heuristic to figure out what to translate and what not, which is implemented in the additiveTest function that tells whether the type should be translated or not.

I look forward to seeing what is possible with this kind of framework!

One more example I have in mind, for which I also don't know if this is in scope, is in Euclidean geometry. The typical setup is

variable {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (finrank ℝ V = 2)]

But proving things in this setup is equivalent to proving things with V = P = ℝ × ℝ, so it would be neat if you could replace V and P with ℝ × ℝ (using some equivalence like the one given by finDimVectorspaceEquiv)