transport and parametricity

Stream: general

[Simon Hudon]

I could put some time on transfer and parametricity. I'll have to get a refresher on parametricity though. But this project is still useful. Although it will likely be replaced in Lean 4, when we do have a FFI, we can start building CS applications that themselves may be more portable.

[Simon Hudon]

The math is moving forward pretty nicely. Meanwhile the CS side of mathlib and other Lean packages is still under furnished. Please forgive us for spending time on it ;-)

[Simon Hudon]

Btw, do you have any time for parametricity and transfer? We could pick it up today if you like

[Patrick Massot]

I have time today, but I don't have the required knowledge

[Patrick Massot]

I can only repeat what Kevin wrote hundreds of times

[Simon Hudon]

Maybe I should talk to @Cyril Cohen again

[Patrick Massot]

We need Lean to understand that isomorphic stuff have the same properties, for any property that makes sense

[Patrick Massot]

Simon, if you want a nice project for today, you could redo my leancrawler correctly. The goal is to be able to display the graph of all concepts in a Lean project, where each declaration is a node, and each edge means a declaration uses another declaration. Mine is unfortunately really bad, many edges are missing

[Simon Hudon]

You misunderstand me. I'm not looking for new projects. I'm trying to find help for the projects I already have

[Keeley Hoek]

@Patrick Massot a bit of an aside, but a fellow one of Scott's students has just started working on iso_induction, using an isomorphism X ≅ Y to replace every object Y that's in your goal with an X (and hopefully changing nothing else). At the moment it can show that for X and Y isomorphic types, to prove inhabited Y it suffices to show inhabited X! But this is done with some very general typeclass instances pertaining to functoriality. Not too long from now you should be able to add a command after the definition of e.g. local_ring which generates a proof of functoriality of the construction, and then be done with transporting such structure. (At least that's the plan, anyway!)

[Simon Hudon]

Interesting. I got a fair amount of push back when I tried focusing on isomorphisms for transport. That seemed like a good goal to me but Johannes didn't seem to like that idea

[Kevin Buzzard]

I wish I understood all of this better. I still keep coming back to the same idea -- if R is a local ring and S is isomorphic to R then S is local, and I cannot see why Lean can't auto-generate this theorem using some sequence of equivs. R and S are ring-equiv, so the lattice of ideals of R and of S are lattice-equiv, and the definition of local ring is some predicate on these lattices which only depends on the lattice structure so commutes with the equiv. If someone wants to update https://github.com/leanprover-community/mathlib/issues/408 so I understand better the plan for implementing this in Lean, maybe I would get less frustrated by this issue :-/

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

I have two fintypes S and T, an equiv S \equiv T, a proof that all reflexive binary relations on S are transitive, and I want to deduce that all reflexive binary relations on T are transitive. I am adding this to my list of transport complaints ;-) The maths proof is: "consider a reflexive binary relation on $T$; this obviously induces a reflexive binary relation on $S$; the induced relation is transitive; hence obviously the original relation is transitive".

How to do this in Lean in a clean and clear way?

---

Background: I asked my students (in last year's exam) to prove that if $r$ was a reflexive binary relation on a set $S$ with two elements, then $r$ was transitive. @Abhimanyu Pallavi Sudhir wrote up the solutions in Lean and he assumed that $S$ was fin 2. In a solution to such a question a mathematician would not think twice if a student wrote "WLOG $S=\{0,1\}$"; it is indistinguishable from "let the elements of $S$ be called $x$ and $y$". In fact assuming $S$ is bool makes life even easier, but then one is faced with the question above.

[Chris Hughes]

I don't think this is the answer you wanted but

import data.equiv.basic

example {α β : Type*} (e : α ≃ β) (h : ∀ r : α → α → Prop, (∀ x, r x x) →
  (∀ x y z, r x y → r y z → r x z)) : ∀ r : β → β → Prop, (∀ x, r x x) →
  (∀ x y z, r x y → r y z → r x z) :=
λ r hrefl x y z hxy hyz, begin
  rw [← equiv.apply_symm_apply e x, ← equiv.apply_symm_apply e z],
  rw [← equiv.apply_symm_apply e x, ← equiv.apply_symm_apply e y] at hxy,
  rw [← equiv.apply_symm_apply e y, ← equiv.apply_symm_apply e z] at hyz,
  exact h (λ x y, r (e x) (e y)) (λ _, hrefl _) _ _ _ hxy hyz
end

[Johan Commelin]

Now Kenny golfs it (-;

[Kenny Lau]

import data.equiv.basic

example {α β : Type*} (e : α ≃ β) (h : ∀ r : α → α → Prop, (∀ x, r x x) →
  (∀ x y z, r x y → r y z → r x z)) : ∀ r : β → β → Prop, (∀ x, r x x) →
  (∀ x y z, r x y → r y z → r x z) :=
λ r hrefl x y z hxy hyz, begin
  rw [← equiv.apply_symm_apply e x, ← equiv.apply_symm_apply e z] at \|- hxy hyz,
  exact h (λ x y, r (e x) (e y)) (λ _, hrefl _) _ _ _ hxy hyz
end

[Johan Commelin]

Also, you missed the chance to use projection notation

[Johan Commelin]

You clearly didn't run that one

[Kenny Lau]

I haven't fired up Lean since a long time

[Johan Commelin]

And your internal type checker is rusty (-;

[Johan Commelin]

You're still running Lean 3.4.1, aren't you?

[Kenny Lau]

I'm staying off Lean until after the exam

[Johan Commelin]

Too bad that your exam is also staying off Lean

[Kevin Buzzard]

Yeah, I can prove it too; but I just know deep down that this is a special case of a general principle; given e and h, a mathematician knows in their soul that the goal is true, and doesn't want to prove it. The question, I think, is how to prove it with a tactic. I have more time for this now; Mario posted something a month or two ago but I was completely focussed on the perfectoid project at the time and didn't want to get distracted; now I am interested again.

My proof was more mundane: given rb on beta I literally built ra on alpha using the equiv, proved that the relationship on beta one can build from ra is rb again, and then just transferred everything manually.

But my point is that this should somehow be a one-liner.

[Jesse Michael Han]

essentially Kevin's approach, but big_bertha style:

import data.equiv.basic

example {α β : Type*} (e : α ≃ β) (h : ∀ r : α → α → Prop, (∀ x, r x x) →
  (∀ x y z, r x y → r y z → r x z)) : ∀ r : β → β → Prop, (∀ x, r x x) →
  (∀ x y z, r x y → r y z → r x z) :=
begin
  intros r H x y z _ _,
  let r' := λ a b, r (e.1 a) (e.1 b),
  specialize h r' (by finish) (e.2 x) (e.2 y) (e.2 z),
  {[smt] eblast_using[e.4, (by simp : ∀ a b, r (e.1 a) (e.1 b) ↔ r' a b)]}
end

[Jesse Michael Han]

this doesn't quite do what Kevin wants, but we can see that proving the transfer is automatic; we just have to state it. all the constructed data/lemmas in the above proof are very follow-your-nose, so it's conceivable that one could whip up a tactic that attempts to use equiv.to_fun and equiv.inv_fun to produce the requisite data when it sees a lemma in context like h which is applicable "modulo equivalence"

[Mario Carneiro]

There is a transfer style proof of this theorem. Floris mentioned wanting to get working on adding more transfer lemmas; I should PR equiv.rel if it hasn't made it in yet, it's pretty important for these kinds of proofs

[Kevin Buzzard]

In this old paper by MacLane he sketches on p179 what he says Bourbaki calls a "type" of "structure". His definition of structure is sufficiently general to allow topological spaces.

What is confusing me is the claim on p180 that a type of structure leads to the notion of morphism from one model of the structure to another; I'm not sure these words mean the same thing nowadays but what he's saying is that the axioms for a group give you a structure and now you can figure out what a homomorphism of groups is. But he's also saying that the axioms for a topological space give you a structure and now you can figure out what a homomorphism of topological spaces is. I did not know this. Is it true? MacLane offers no proof. I am fine with the idea that you can figure out what an isomorphism of structures is, but I don't see how to guess what a morphism of topological spaces is. There are some vague comments about how the power set can be covariant or contravariant, but I am confused about whether this co/contravariance is supposed to be part of the structure. Is this just a load of old codswallop or is there something here which can be made rigorous?

[Johan Commelin]

@Fabian Glöckle :up: This might be relevant to what you are implementing

[Kevin Buzzard]

Does anyone know the reference to Bourbaki where they define these "types of structures"?

[Chris Hughes]

https://link-springer-com.iclibezp1.cc.ic.ac.uk/content/pdf/10.1007%2F978-3-540-34035-5.pdf I think.
Chaiptre IV is called structures. It's in Théorie des ensembles

[Kevin Buzzard]

Thanks Chris. I've found it. Bourbaki don't just define a morphism between two structures, they have some additional data (basically the axioms that the map has to satisfy!). They explicitly give the example of topological spaces and how morphisms can either be open maps or continuous maps depending on the additional data (denoted $\sigma$), on p215 of the pdf, section 2.1 of chapter IV. In fact they explicitly flag with a bendy road sign the fact that given just a structure, you don't have enough information to define morphisms of structures.

[Fabian Glöckle]

I have some thoughts on this.
1) I already implemented the easy case: https://github.com/faabian/mathlib/blob/3.5/meta.lean
Take a structure definition (like ordered_ring) and generate the corresponding type of homomorphisms (of maps compatible with all additional structure). I will now head for generating the category instances, forgetful functors etc.
2) I didn't know about this before, but think MacLane may be correct about being able to find out what a continuous map is:

In logic/model theory, there are two types of homomorphisms, weak ones (respecting relations as in R(x_1, ..., x_n) \implies R(f x_1, ..., f x_n)) and strong ones (the same with Iff). Which one would one choose in category theory? Answer: weak ones, as they correspond to precomposition with f if we view relations as maps X \times ... \times X \to Prop.
Then a subset of X is the same as a predicate (unary relation) on X or Y, and for a map f : X \to Yand a subset U \subset Y, the composition "characteristic function of U \comp f" is the characteristic function of the preimage of U under f.
Then topologies are subsets of the powersets, so predicates on the power sets. We already found out that the natural map between the powersets is taking preimages. So a weak homomorphism means: "open U \subset Y \implies open (f^{-1} U) \subset X", the definition of a continuous map. (Or: the preimage of the topology of X under the map "take preimage under f" is the topology on Y).

I didn't check in the paper, but hope this is what he meant.

[Kevin Buzzard]

The issue is that Bourbaki's definition of "structure" allows more things than functions and relations -- it allows things like "functions from the power set of the power set of X to the product of X and the power set of X". It seems to me that MacLane just throws comments around like "let's say power set is contravariant" when talking about topologies, but without making it clear what he means in the general case. Is the thing I just mentioned covariant or contravariant? I'm not sure what I asked there even makes sense. Bourbaki avoid this by simply writing down the things they want to remain invariant first, calling them sigma, and then defining a sigma-morphism to be something that preserves sigma. They make it expressly clear that there is no "abstract nonsense" definition of a morphism between structures which does not involve choosing a sigma first.

[Fabian Glöckle]

But does this contradict the statement that in some cases there is a canonical way of finding sigma? I think MacLane says taking powerset to be contravariant is natural, and thus continuous maps are (unlike open maps) the natural choice. Do we know structures where this "canonical" choice of morphisms is not correct?

[Fabian Glöckle]

Concerning your example, the X part should be covariant, the (X to Prop) part contravariant. I think this is fully algorithmical as the only rule is "whenever the structure X itself appears, use f to get to Y". This can mean both pre- or postcomposition. Then draw a diagram and say it must commute.

[Chris Hughes]

So if a monotonic function is $x \le y \implies f(x) \le f(y)$, we're using the order on Prop somehow, or we're just saying an order is a category, so a morphism is a functor? What's the canonical "weak" morphism on a metric space? Is it $d(x,y) \le d(f(x),f(y))$

[Fabian Glöckle]

Yes, somehow prop gets special treatment..

[Fabian Glöckle]

The metric spaces though are a great example showing that there are more than just the algebraic structures.

[Fabian Glöckle]

The algebraic version of a metric space map would be d(x,y) = d(f(x),f(y)) (called isometry?)

[Kevin Buzzard]

Locally ringed spaces are a great example showing that a structure in the sense of Bourbaki is not everything that a mathematician cares about. It is surely impossible to automatically generate the definition of a morphism of locally ringed spaces. But I am not sure that a locally ringed space falls into this whole structure definition at all. On the other hand it is clearly possible to define an isomorphism of locally ringed spaces, even though they are a more complex structure than what I think is allowed by Bourbaki.

[Kevin Buzzard]

Concerning your example, the X part should be covariant, the (X to Prop) part contravariant.

Does this make sense? Let's define a structure called foo, and a foo is a type $X$ plus a subset of $X\times\mathcal{P}(X)$ (the product of $X$ and its power set). How are you going to define morphisms? How can you be covariant in part of the data and contravariant in the other part? I just don't understand how to make this precise.

[Johan Commelin]

Locally ringed spaces are a great example showing that a structure in the sense of Bourbaki is not everything that a mathematician cares about. It is surely impossible to automatically generate the definition of a morphism of locally ringed spaces. But I am not sure that a locally ringed space falls into this whole structure definition at all. On the other hand it is clearly possible to define an isomorphism of locally ringed spaces, even though they are a more complex structure than what I think is allowed by Bourbaki.

A naive autogenerated type-theoretic isom of locally ringed spaces would probably be wrong. Because the isom is a 2-categorical thing. HoTT would automatically get it right, I guess.
But if you aren't careful, the autogenerated thing would ask for the $f_* \mathcal{O}_X = \mathcal{O}_Y$ (with equality on the nose). Of course the isom should actually include extra data, namely an isom between those two sheaves.

[Johan Commelin]

But how could Lean ever figure out that it should automatically include such an isom in the autogenerated definition of an iso of LRS's? This only seems plausible if we tightly couple the categorical nature of sheaves to the definition of a sheaf. Otherwise it will just treat sheaf X as a discrete thing. But we want to consider them "up to homotopy".

[Kevin Buzzard]

I am not sure that locally ringed spaces are covered by this Bourbaki definition of structure, so probably you have to put extra allowances in for all the extra types kicking around; terms have to be equal but types just have to be isomorphic.

[Johan Commelin]

@Kevin Buzzard I'm not yet convinced that one can automagically produce the definition of isoms of LRS's...

[Johan Commelin]

If we endow everything with category instances... then maybe. Otherwise you either need to give the system a helping hand, or something clever has to be done.

[Kevin Buzzard]

The isomorphism of topological spaces enables you to push one sheaf over to the other space and now we want an isomorphism of sheaves. I don't see the problem but given that transfer seems to be such a key issue I'm still listening. I still believe that given any structure that Lean could make, it should be able to construct the notion of isomorphism between two instances of that structure (modulo possible universe issues)

[Johan Commelin]

How should the transfer tactic realise that an isomorphism of LRS requires an isomorphism between $f_* \mathcal{O}_X$ and $\mathcal{O}_Y$, instead of an equality?

[Johan Commelin]

I've got (X Y : LRS). I'm a robot. I need to figure out what is an isomorphism between X and Y. Well... an LRS consists of a topological space, a sheaf on that space, and some other junk.
Great, I figure out what is an isomorphism of topological spaces. So I decide that an isom of LRSs consists of a topological isom f : X.carrier \iso Y.carrier. Using generic transfer blabla, this allows me to transfer the sheaf X.sheaf from X.carrier to Y.carrier along f. Now, I've got two terms of type sheaf Y.carrier. I decide that it is very reasonable that these two terms should be equal.
Finally, this equality trivially preserves all the other junk. I have figured out what an isomorphism between X and Y is.
I'm a robot.

[Reid Barton]

Well there are Types inside sheaf, so presumably you would need to construct a notion of "equal" that doesn't involve literal equality of types

[Reid Barton]

by induction over the syntax of the structure

[Johan Commelin]

This very much feels like reinventing HoTT's transport.

[Reid Barton]

That is kind of the goal, right?

[Johan Commelin]

Hmmm... maybe it does work.

[Johan Commelin]

@Fabian Glöckle How hard would it be for you to automatically generate such an equiv for an arbitrary structure using the framework that you have so far?

[Reid Barton]

A difference is that in HoTT the equality is an intrinsic part of the theory, while here we're trying to emulate it by meta-level considerations, building up by induction on the structure what we expect the right interpretation of "equality" to be.

[Reid Barton]

Equality of types in HoTT is not defined to be isomorphism any more than equality of ordered pairs is defined to be equality of each component

[Cyril Cohen]

@Simon Hudon did someone progress on this while I was away?

[Simon Hudon]

I didn't. I think it's at the same point it was before

[Kevin Buzzard]

OK so we have Bochner integration in Lean! This work has helped me to formalise a question which might be related to this transfer/transport stuff.

Let's say I have a smart computer scientist undergrad who is intested in analysis and logic, and wants to do something cool in Lean. Say they read this thread and then say to me "This Bochner integral definition -- it mentions the real numbers, and in Lean the real numbers are defined to be the Cauchy reals. Do you think it would be interesting to port the entire Bochner integral definition over to the Dedekind reals? Here's my plan. First I write an interface with Dedekind reals at the back end, providing an interface to exactly those functions and definitions and other things that are in the real namespace the moment the real numbers are defined in Lean (as Cauchy reals). The proofs should then barely need modifying, and everything should just port over". And I say "sounds great, go ahead" and I think "I knew this transport stuff was easy". A week later the student comes back and says that they have run into trouble. Turns out that some of the maps between Cauchy and Dedekind reals were noncomputable, the API for the Cauchy reals built with the Dedekind reals as backend is also noncomputable, all the proofs have ported beautifully but then loads of them don't work because sometimes computer scientists used simp which used to work but didn't any more because of some computability issue. We then come onto the chat asking how we can fix the proof and deduce our Bochner integral thing for the Dedekind reals. We are fine if everything is noncomputable by the way -- we are mathematicians. Feel free to use all your axioms.

[Kevin Buzzard]

@Simon Hudon @Floris van Doorn does the above post make any sense?

[Simon Hudon]

I don't get why computability becomes an issue. I see why the transport might be non-computable but since you're accepting that, what's the problem?

[Kevin Buzzard]

Could this approach actually work to port the Bochner stuff over to Dedekind reals?

[Kevin Buzzard]

Surely some of the functions defined in the API for data.real.basic will allow some kind of computational reductions which the analogous objects in the Dedekind-backend reals would not satisfy, so some rfl proofs might break? Or am I talking nonsense?

[Kevin Buzzard]

I'm no logician

[Mario Carneiro]

Your concern is theoretically justified, but you should replace simp in the example with rfl or dsimp

[Mario Carneiro]

The proofs that were going to break did break, and were fixed, when real was made irreducible

[Mario Carneiro]

it basically makes it impossible to prove facts about real numbers by rfl

[Mario Carneiro]

so now (in theory) you could completely swap out the definition of reals with something else and fix the API theorems and nothing further should break

[Kevin Buzzard]

How do I know that some rogue proof didn't unfold real?

[Mario Carneiro]

you have to write some really horrible looking tactic code to unfold real

[Kevin Buzzard]

I'll get Chris onto it.

[Mario Carneiro]

So it's not impossible, but a proof that does this is visibly ugly

[Kevin Buzzard]

You have to write some really horrible looking maths to say anything about the real numbers for which the answer would be different for Dedekind cuts and Cauchy sequences.

[Kevin Buzzard]

A proof that did that would be visibly weird.

[Kevin Buzzard]

In fact a proof which used anything other than the Officially Mathematically Sanctioned Axioms For The Real Numbers, which is something about them being some complete archimedean field, would be visibly ugly.

[Kevin Buzzard]

So it's not impossible, but a proof that does this is visibly ugly

I think that you should then replace real by a constant and just provide an API to the proof that they satisfy those complete archimedean field axioms.

[Kevin Buzzard]

Then you'd know that you could not fall off the straight and narrow.

[Kevin Buzzard]

Computer-generated tactics of the future might unfold real

[Mario Carneiro]

Yes, it would be nice if we could do this in lean. Unfortunately the only way to truly be bulletproof is to use a constant and that pollutes the #print axioms list (and requires people to be careful not to introduce unsoundness)

[Andrew Ashworth]

Isn't the bulletproof way just to define a complete archimedean field typeclass? the reals would just be an alias for a declaration of a type and the associated instance

[Andrew Ashworth]

maybe not. I just googled the topic and came up with a paper where people have all sorts of axioms for the real numbers

[Andrew Ashworth]

https://arxiv.org/pdf/1402.6645.pdf

[Kevin Buzzard]

Should we make the construction of the localization of a ring at a submonoid irreducible as well?

[Simon Hudon]

There's another approach. You could make real into a structure that contains it's construction. Then, you have to use introduction and elimination rules to work on the construction

[Kevin Buzzard]

Let's say that this summer I get a beginner Lean student to formalise the statement of the Birch and Swinnerton-Dyer conjecture (BSD), which says that for every cubic equation in two variables with rational coefficients, the behaviour of the set of rational solutions of the equation is related to a value of a certain complex function which depends on the equation. The student certainly doesn't write any weird meta code and doesn't unfold any definitions of real. Note that they do use the complex numbers though, so they do use real. And let's say that I get a second student working on a Dedekind real library for Lean and they get some kind of regular expression going which automatically ports a bunch of mathlib over to the Dedekind reals, including the statement of BSD.

Let's then say that in 2020 some team led by Christian Szegedy at Google announces a fully formalised AI-generated incomprehensible long Lean 3.4.2 proof of BSD as formalised by my Cauchy student. My Dedekind student attempts to apply the regex to port the proof over to the Dedekind reals, but the port fails because it turns out that Szegedy has unfolded the reals in his proof for performance reasons.

Do we know for sure in this situation that there is a Lean proof of BSD for Dedekind reals?

[Keeley Hoek]

Isn't your last statement Kevin an essentially purely "conventional" mathematical question? something like "(All with normal set-theory): If there exists a proof of a particular proposition P involving real numbers:

• but whose statement requires only certain axiomatised properties of the reals which we can write down in a list and agree on,
• and whose proof proceeds by using Cauchy-reals (meant just as some definition in terms of sets),

does there exist a proof of the same fact which uses Dedekind-reals?"

In which case, surely the answer is "it depends on the strength of the list of axioms which we can agree on".

[Kevin Buzzard]

My question is completely precise and does not depend on conventions. I completely agree that there is an analogous question in ZFC.

[Kevin Buzzard]

In particular we don't have to have any sort of debate beforehand. For the Lean question I'm talking about a Lean proof and for the ZFC question I'm talking about a proof in eg Mizar. The basic question is whether a conjecture whose statement can be written using only the usual interface but whose proof might not follow this rule can always be ported to the Dedekind case because of some general theorem of logic

[Kevin Buzzard]

I can envisage how the ZFC proof might go but I'm less good at type theory

[Mario Carneiro]

Yes, provided the statement itself falls within the "mathematically acceptable" subset, you can translate the "BSD for cauchy reals" statement to "BSD for dedekind reals", and they will be provably equivalent using transfer theorems

[Mario Carneiro]

For comparison, the proof of dirichlet's theorem in lean via metamath has a similar flavor. The proof uses some crazy techniques using some completely different notion of reals, natural numbers, etc, but because the statement is comprehensible you can just translate the predicates across until you get the conventional lean statement.

[Kevin Buzzard]

For the transfer tactic to work one needs to ensure that every single thing you can do for the Cauchy reals has some sort of analogue for the Dedekind reals. Does the proof of this start something like "we replace Cauchy reals with Dedekind reals, we replace the constructor with a function which takes a Cauchy sequence and returns the corresponding Dedekind limit, and we replace the eliminator with the function which takes the same inputs as the Cauchy eliminator and returns a function from the Dedekind reals instead". But then how do you prove that the proof still works? Switching out the constructor and eliminator so they work for Dedekind reals instead is easy, you just use the equiv between Cauchy and Dedekind reals. But now there must be something to do to check that the corresponding term has the appropriate type.

[Andrew Ashworth]

I don't follow - why can't you rely on Lean to typecheck the transferred expression for you?

[Andrew Ashworth]

Maybe my understanding of what transfer does is flawed. I think about it in terms of a specialized source-to-source transpiler. What comes out is just another Lean expr that will by typechecked by Lean itself.

[Mario Carneiro]

For the transfer tactic to work one needs to ensure that every single thing you can do for the Cauchy reals has some sort of analogue for the Dedekind reals.

No, what is needed is only that everything mathematically reasonable that you can do to the Cauchy reals has an analogue. If in this Szegedy fictional proof other things that aren't mathematically reasonable are exploited, it doesn't matter for the transfer. Since the resulting theorem (BSD) is a mathematically reasonable proposition, you should be able to translate it

[Mario Carneiro]

You aren't transferring the proof, you are transferring the statement

[Mario Carneiro]

Does the proof of this start something like "we replace Cauchy reals with Dedekind reals, we replace the constructor with a function which takes a Cauchy sequence and returns the corresponding Dedekind limit, and we replace the eliminator with the function which takes the same inputs as the Cauchy eliminator and returns a function from the Dedekind reals instead". But then how do you prove that the proof still works?

For simple proofs, where the proof itself is entirely mathematically reasonable, then this works. But it's not foolproof, and can break proofs that unfold real.

For complicated proofs, we aren't shifting anything under the foundation of the proof itself at all. We just use the statement "BSD is true for cauchy reals" as is, without inspecting or modifying the proof in any way. The idea is to prove statements of the form "P is true for cauchy iff P' is true for dedekind" where P and P' are analogous

[Kevin Buzzard]

I am currently a bit confused about what the straight answer is to my straight question. If I have a Lean-formalised mathematical conjecture about complete ordered archimedean fields (i.e. about all constructions of the real numbers) and if I have a possibly "mathematically unreasonable" but Lean-accepted proof of this conjecture in the special case of the Cauchy reals, it is a theorem that there exists a Lean-accepted proof of the special case of Dedekind reals? If so, what is the proof? Secondly, were I to present such a conjecture and (1000 line long) proof for the Cauchy reals, what needs to be done in practice to get a proof for the Dedekind reals?

[Kevin Buzzard]

Here's another question. The Bochner integral is defined in Lean using the Cauchy reals. What if I want a version for Dedekind reals? The analogous function but in the Dedekind situation. Again this is a very precise question -- as far as I can see -- I would like to generate the term which would have been made if real had been defined using the Dedekind reals.

[Mario Carneiro]

If so, what is the proof?

We can prove today that "BSD for cauchy reals holds iff BSD for dedekind reals holds", so if we get any proof, even an unreasonable one, of BSD for cauchy reals, by composing it with this we get a proof of BSD for dedekind reals.

Here's another question. The Bochner integral is defined in Lean using the Cauchy reals. What if I want a version for Dedekind reals? The analogous function but in the Dedekind situation. Again this is a very precise question -- as far as I can see -- I would like to generate the term which would have been made if real had been defined using the Dedekind reals.

There are a few kinds of definitions based on reals. Some of them don't actually depend on it being any kind of reals, for example you can replace "real is an ordered field" with "real' is an ordered field" reusing the same predicate "ordered field". Other definitions have the reals embedded inside; for example the Bochner integral is defined for functions over a real vector space, and so you would need Bochner' integral defined for functions over a real' vector space. The only proofs that have to be translated are those that are involved in stating the theorem, and they can either be translated similarly by replacing real with real' everywhere, or they can be explicitly transferred by proving that all sub-formulas of the statement of the theorem hold for real' iff they hold of real.

[Kevin Buzzard]

We can prove today that "BSD for cauchy reals holds iff BSD for dedekind reals holds"

What is the proof of that?

You are talking again and again about transferring statements, but I want to see how to transfer a proof, especially a proof which we cannot guarantee is "normal". Regarding translating the Bochner integral function, I can see that this is possible in theory because no way will there be any weird real-unfolding, but I can't imagine how to do it in practice.

[Andrew Ashworth]

you can't give a 1-line explanation, the algorithm involved is hairy, but if you want to read a paper about it, try this one: <deleted, see below>

[Andrew Ashworth]

there are differences between the paper I linked which is in Coq and the transfer tactic from isabelle which we are trying to port to Lean, but I can't say what they are...

[Kevin Buzzard]

What is this random paper? It has no date or hint about where it was/will be published. Is it OK? By default I tend to be skeptical about random pdfs on the internet (I've seen a lot of crap maths). Just paranoid by default. I find computer science papers hard to read. I am looking for a theorem and a proof. The theorem says that something can always be done (X_for_Cauchy -> X_for_Dedekind), the paper says "we describe a new tactic". I guess our two cultures think about these things differently.

[Andrew Ashworth]

ahh, perhaps a better link would be to it's home in the Journal of Formalised Reasoning

[Andrew Ashworth]

apparently I linked a pre-print

[Andrew Ashworth]

https://jfr.unibo.it/article/view/1574

[Andrew Ashworth]

or something, weird

[Andrew Ashworth]

I am not sure where the theorem you want is stated, we'll just have to wait for a type theory specialist to chime in.

[Andrew Ashworth]

What would a proof look like, though? The basic idea of the tactic is: define an equivalence relation for the two isomorphic types you are interested in. For the reals, this relation would be based on the axioms of a complete ordered field. For the more advanced objects you work with, the "Strickland" predicates you have on defined on various unnamed types. Then, mechanically go through each proof. For each definition or proof used on one type, generate a proof obligation that it is a morphism and substitute.

[Andrew Ashworth]

If you write some definition or function that is not a morphism, this tactic will fail, and you'll be stuck.

[Andrew Ashworth]

X_for_Cauchy -> X_for_Dedekind is false in general

[Andrew Ashworth]

Under what circumstances is X_for_Cauchy -> X_for_Dedekind always true? Only if for each definition or function used in X, it is defined only in terms of the axioms of a complete archimedian field, which are the properties shared by both, or if we can derive complete_arch_field -> (X_for_Cauchy /\ X_for_Dedekind) . So for mathlib's reals, if we try and transfer a certain definition over the Cauchy reals to the Dedekind reals, that depends on construction details of the Cauchy reals, we won't be able to because we won't be able to prove that it is a morphism. It just won't type-check.

[Andrew Ashworth]

ps: this is extremely tedious. If you thought adding additional functions to your baby ring tactic was a pain, this dials it up to 11 if you are working with a complex, many-propertied object. This is a generalization of the method of how ring works.

[Andrew Ashworth]

If at all possible if you know you want to reason about many kinds of isomorphic objects, define the appropriate equivalence class and work with that instead as soon as possible.

[Kevin Buzzard]

I think you guys are always thinking about the details of the construction. I can quite believe it's difficult. I'm trying to understand this "Stricklandization" way of thinking. But there is also a theorem somewhere which says that if X is a true/false statement about compete ordered Archimedean fields then X is true for Cauchy reals iff it's true for Dedekind reals. I was hoping for a reference for this. There might be some analogous theorems about localisations or kaehler one forms, and these are the things I'm really interested in, but it's easier to talk about real numbers because more people know what they are

[Andrew Ashworth]

Yes? This is the Liskov substitution principle. https://en.wikipedia.org/wiki/Liskov_substitution_principle

[Andrew Ashworth]

summoning @Mario Carneiro because I have no idea if this has a formal proof in CIC

[Andrew Ashworth]

Ah, nevermind, that isn't the proof you're looking for. I haven't been able to find anything about the theorem as stated, except that it's unprovable by computers and equivalent to the halting problem in general, if you're willing to write a degenerate enough proposition that depends on the truth or falsity of, say, the Goldbach conjectures. But that says nothing about if it exists or not in all cases.

[Johan Commelin]

Is there already an established name for these sort of predicates? Otherwise I propose to call them characteristic predicates.

[Andrew Ashworth]

Apparently in type theory we call "complete archimedean field" a type and the cauchy, dedekind reals a "(strong) behavioral subtype".

[Andrew Ashworth]

The process of deducing isomorphism invariant properties is called "interface extraction" as in https://refactoring.guru/extract-interface . (I guess in Rust this would be "extract trait". In Python this would be defining an abstract base superclass.)

[Andrew Ashworth]

and I looked some more and I found people saying that the Liskov substitution principle is actually necessary and sufficient for the theorem Kevin wanted, but I can't find a formulation explicitly in the terms he gave (that is, getting rid of all the programming related statements and deriving it purely in proof-theoretical terms). I would be shocked if it wasn't in the type theory literature somewhere, though.

[Kevin Buzzard]

I couldn't work out how to get Liskov substitution to do it. There must be more details which I'm missing.

[Kevin Buzzard]

I might ask a more mathsy version of my question on mathoverflow to see what the logicians make of it. They speak a language closer to my own.

[Andrew Ashworth]

I can get behind characteristic predicate, it's shorter than "isomorphic invariant properties"

[Andrew Ashworth]

not by much, though

[Andrew Ashworth]

it's also less creepy than the category theory term "skeletonization"

[Johan Commelin]

Should we also have a "characteristic predicate" for constructions like mv_polynomial?

[Kevin Buzzard]

Do we need one? One thing (unrelated to transfer) about mv_polynomial is that I think someone should take a look at what instances are defined on it, and ask if they have sensible priorities

[Mario Carneiro]

The proof of X_for_Cauchy <-> X_for_Dedekind depends on X and is not always true. It is true for what I am calling "mathematically reasonable" propositions to mimic your claims about things mathematicians refuse to do with their language, but that term is also deliberately vague so that there is no general metatheorem being applied here

[Andrew Ashworth]

So the Liskov substitution principle is necessary and sufficient for Hoare logic according to Wikipedia. Is there something analogous for the calculus of inductive constructions?

[Andrew Ashworth]

I figure it ought to be simpler since there's no mutability, but I'm not a type theorist..

[Mario Carneiro]

The substitution principle in this generality is basically HoTT's domain. If you require it for all predicates then you can easily show it's equivalent to saying "Cauchy_reals = Dedekind_reals"

[Andrew Ashworth]

I can see how that makes sense. The only way to get 100% semantic equality would be for the two types to be exactly the same.

[Mario Carneiro]

I actually don't mean exactly the same, I mean equal according to the = predicate in DTT, which as you know is a more subtle thing

[Mario Carneiro]

And in HoTT the difference between = and defeq is center stage

[Kevin Buzzard]

But something funny is going on here because we're not using HoTT and it is true that for "mathematically reasonable statements" they're true for the Cauchy reals iff they're true for the Dedekind reals, so something is missing from my understanding. I asked at MO and, as is unfortunately sometimes the case with logic questions, I've caused a great deal of noise :-/ https://mathoverflow.net/questions/336191/cauchy-reals-and-dedekind-reals-satisfy-the-same-mathematical-theorems

[Andrew Ashworth]

I think the answer is buried there, though, in one comment. https://math.stackexchange.com/questions/437948/do-isomorphic-structures-always-satisfy-the-same-second-order-sentences. The answer is true for 1st-order propositions, and false for higher order.

[Kevin Buzzard]

I'm hoping I can get Noah Schweber to write more details. I feel like we're making progress in the sense that I'm learning something.

[Jesse Michael Han]

noah's sketch seems like the "just transfer the higher-order statements you need" approach (he's probably adding extra sorts so he can quantify over things like subsets) but with more bookkeeping (this is probably the path to a uniform transfer theorem for constructions of CAOFs)

amusingly, terry tao is essentially recommending that we just roll with a CAOF typeclass

[Kevin Buzzard]

What's a CAOF typeclass?

[Jesse Michael Han]

the hypothetical typeclass for complete archimedean ordered fields, so that every instance of it corresponds to an interpretation of the generic symbol R mentioned by terry in his comment

[François G. Dorais]

@Jesse Michael Han Why is the typeclass hypothetical? It's easy to write down several variants.

[Mario Carneiro]

The typeclass approach isn't quite flexible enough, because of the need to deal with n-ary predicates with a variety of different relations between objects at the same time

[Jesse Michael Han]

@François G. Dorais it's hypothetical because i don't think anyone's PR'd it to mathlib yet :^)

but indeed it shouldn't be difficult

[Mario Carneiro]

oops, spoke too soon. It's possible to have a typeclass for "real-like thing" but we are embedding it in definitions exactly because we are not anticipating to change the definition of the reals any time soon

[François G. Dorais]

Ah, got it. In that case, let me record my favorite version: R is the terminal object in the category of archimedean ordered fields.

class real_field (α : Type) extends linear_ordered_field α, archimedean α :=
(term (β : Type) [linear_ordered_field β] [archimedean β] : ∃ (f : β → α), is_field_hom f)

It's a bit harder to get off the ground with this one, but it's very entertaining to see how it works. (The restriction to Type is not a typo. Archimedean ordered fields are so fantastically rigid, this is enough to ensure that this is a terminal object for all universe levels.)

[François G. Dorais]

I answered @Kevin Buzzard's question on MO but in the context of ZFC. In the context of Lean, having a real typeclass is the best since that will make transfer happen automatically. That said, mathlib's current reals are essentially harmless. As I explained on MO, to transfer a theorem about reals (or whatever) the only key ingredient is that the _statement_ only mentions equality and external structure between real numbers and never looks under the hood at the innards. Because mathlib's reals are opaque, it's really hard to write anything that uses the innards of mathlib's reals. Nevertheless, opaque is quite a few shades lighter than pitch black... I am still very comfortable to assert that mathlib's reals are 99.9999% transferable. The main reason I feel so comfortable is that mathlib's reals are basically computationally useless, so I doubt anyone would have had the idea to breach the opaqueness barrier unless it was absolutely necessary.

The same kind of trick I mentioned on MO works for Lean but it's a much harder argument involving carefully crafted comma category-like stuff and such. I had a similar thing come up recently and I ran out of steam before I could even write down what needed to be done. This is really hard work but it's a one-time deal, so it might be worth it. (I do not have time to do it.)