Zulip Chat Archive

Stream: general

Topic: transport and parametricity


view this post on Zulip Simon Hudon (May 01 2019 at 13:02):

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.

view this post on Zulip Simon Hudon (May 01 2019 at 13:05):

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 ;-)

view this post on Zulip Simon Hudon (May 01 2019 at 13:07):

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

view this post on Zulip Patrick Massot (May 01 2019 at 13:08):

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

view this post on Zulip Patrick Massot (May 01 2019 at 13:08):

I can only repeat what Kevin wrote hundreds of times

view this post on Zulip Simon Hudon (May 01 2019 at 13:08):

Maybe I should talk to @Cyril Cohen again

view this post on Zulip Patrick Massot (May 01 2019 at 13:09):

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

view this post on Zulip Patrick Massot (May 01 2019 at 13:22):

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

view this post on Zulip Simon Hudon (May 01 2019 at 13:35):

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

view this post on Zulip Keeley Hoek (May 01 2019 at 13:38):

@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!)

view this post on Zulip Simon Hudon (May 01 2019 at 13:43):

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

view this post on Zulip Kevin Buzzard (May 01 2019 at 15:13):

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 :-/

view this post on Zulip Kevin Buzzard (May 01 2019 at 15:14):

(deleted)

view this post on Zulip Kevin Buzzard (May 06 2019 at 11:05):

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 TT; this obviously induces a reflexive binary relation on SS; 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 rr was a reflexive binary relation on a set SS with two elements, then rr was transitive. @Abhimanyu Pallavi Sudhir wrote up the solutions in Lean and he assumed that SS was fin 2. In a solution to such a question a mathematician would not think twice if a student wrote "WLOG S={0,1}S=\{0,1\}"; it is indistinguishable from "let the elements of SS be called xx and yy". In fact assuming SS is bool makes life even easier, but then one is faced with the question above.

view this post on Zulip Chris Hughes (May 06 2019 at 11:21):

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

view this post on Zulip Johan Commelin (May 06 2019 at 11:25):

Now Kenny golfs it (-;

view this post on Zulip Kenny Lau (May 06 2019 at 11:26):

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

view this post on Zulip Johan Commelin (May 06 2019 at 11:27):

Also, you missed the chance to use projection notation

view this post on Zulip Johan Commelin (May 06 2019 at 11:27):

You clearly didn't run that one

view this post on Zulip Kenny Lau (May 06 2019 at 11:28):

I haven't fired up Lean since a long time

view this post on Zulip Johan Commelin (May 06 2019 at 11:28):

And your internal type checker is rusty (-;

view this post on Zulip Johan Commelin (May 06 2019 at 11:29):

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

view this post on Zulip Kenny Lau (May 06 2019 at 11:30):

I'm staying off Lean until after the exam

view this post on Zulip Johan Commelin (May 06 2019 at 11:31):

Too bad that your exam is also staying off Lean

view this post on Zulip Kevin Buzzard (May 06 2019 at 15:54):

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.

view this post on Zulip Jesse Michael Han (May 06 2019 at 16:50):

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

view this post on Zulip Jesse Michael Han (May 06 2019 at 17:05):

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"

view this post on Zulip Mario Carneiro (May 06 2019 at 22:14):

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

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 20:15):

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?

view this post on Zulip Johan Commelin (Jun 11 2019 at 20:26):

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

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 20:33):

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

view this post on Zulip Chris Hughes (Jun 11 2019 at 21:29):

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

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 22:08):

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.

view this post on Zulip Fabian Glöckle (Jun 12 2019 at 06:16):

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.

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 06:46):

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.

view this post on Zulip Fabian Glöckle (Jun 12 2019 at 07:12):

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?

view this post on Zulip Fabian Glöckle (Jun 12 2019 at 07:21):

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.

view this post on Zulip Chris Hughes (Jun 12 2019 at 08:00):

So if a monotonic function is xyf(x)f(y)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)d(f(x),f(y))d(x,y) \le d(f(x),f(y))

view this post on Zulip Fabian Glöckle (Jun 12 2019 at 08:03):

Yes, somehow prop gets special treatment..

view this post on Zulip Fabian Glöckle (Jun 12 2019 at 08:04):

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

view this post on Zulip Fabian Glöckle (Jun 12 2019 at 08:09):

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

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 08:17):

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.

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 08:19):

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 XX plus a subset of X×P(X)X\times\mathcal{P}(X) (the product of XX 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.

view this post on Zulip Johan Commelin (Jun 12 2019 at 15:30):

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 fOX=OYf_* \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.

view this post on Zulip Johan Commelin (Jun 12 2019 at 15:32):

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".

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 15:56):

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.

view this post on Zulip Johan Commelin (Jun 12 2019 at 16:49):

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

view this post on Zulip Johan Commelin (Jun 12 2019 at 16:50):

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.

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 17:16):

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)

view this post on Zulip Johan Commelin (Jun 12 2019 at 17:19):

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

view this post on Zulip Johan Commelin (Jun 12 2019 at 17:23):

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.

view this post on Zulip Reid Barton (Jun 12 2019 at 17:26):

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

view this post on Zulip Reid Barton (Jun 12 2019 at 17:26):

by induction over the syntax of the structure

view this post on Zulip Johan Commelin (Jun 12 2019 at 17:26):

This very much feels like reinventing HoTT's transport.

view this post on Zulip Reid Barton (Jun 12 2019 at 17:35):

That is kind of the goal, right?

view this post on Zulip Johan Commelin (Jun 12 2019 at 17:48):

Hmmm... maybe it does work.

view this post on Zulip Johan Commelin (Jun 12 2019 at 17:49):

@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?

view this post on Zulip Reid Barton (Jun 12 2019 at 18:36):

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.

view this post on Zulip Reid Barton (Jun 12 2019 at 18:36):

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

view this post on Zulip Cyril Cohen (Jun 21 2019 at 11:36):

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

view this post on Zulip Simon Hudon (Jun 21 2019 at 12:33):

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

view this post on Zulip Kevin Buzzard (Jul 12 2019 at 23:26):

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.

view this post on Zulip Kevin Buzzard (Jul 12 2019 at 23:31):

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

view this post on Zulip Simon Hudon (Jul 12 2019 at 23:37):

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?

view this post on Zulip Kevin Buzzard (Jul 12 2019 at 23:40):

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

view this post on Zulip Kevin Buzzard (Jul 12 2019 at 23:43):

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?

view this post on Zulip Kevin Buzzard (Jul 12 2019 at 23:43):

I'm no logician

view this post on Zulip Mario Carneiro (Jul 12 2019 at 23:44):

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

view this post on Zulip Mario Carneiro (Jul 12 2019 at 23:45):

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

view this post on Zulip Mario Carneiro (Jul 12 2019 at 23:45):

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

view this post on Zulip Mario Carneiro (Jul 12 2019 at 23:46):

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

view this post on Zulip Kevin Buzzard (Jul 12 2019 at 23:46):

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

view this post on Zulip Mario Carneiro (Jul 12 2019 at 23:47):

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

view this post on Zulip Kevin Buzzard (Jul 12 2019 at 23:47):

I'll get Chris onto it.

view this post on Zulip Mario Carneiro (Jul 12 2019 at 23:48):

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

view this post on Zulip Kevin Buzzard (Jul 12 2019 at 23:48):

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.

view this post on Zulip Kevin Buzzard (Jul 12 2019 at 23:48):

A proof that did that would be visibly weird.

view this post on Zulip Kevin Buzzard (Jul 12 2019 at 23:49):

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.

view this post on Zulip Kevin Buzzard (Jul 12 2019 at 23:54):

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.

view this post on Zulip Kevin Buzzard (Jul 12 2019 at 23:55):

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

view this post on Zulip Kevin Buzzard (Jul 12 2019 at 23:57):

Computer-generated tactics of the future might unfold real

view this post on Zulip Mario Carneiro (Jul 13 2019 at 00:00):

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)

view this post on Zulip Andrew Ashworth (Jul 13 2019 at 00:03):

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

view this post on Zulip Andrew Ashworth (Jul 13 2019 at 00:05):

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

view this post on Zulip Andrew Ashworth (Jul 13 2019 at 00:05):

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

view this post on Zulip Kevin Buzzard (Jul 13 2019 at 00:25):

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

view this post on Zulip Simon Hudon (Jul 13 2019 at 00:45):

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

view this post on Zulip Kevin Buzzard (Jul 13 2019 at 10:35):

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?

view this post on Zulip Keeley Hoek (Jul 13 2019 at 11:17):

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".

view this post on Zulip Kevin Buzzard (Jul 13 2019 at 11:43):

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

view this post on Zulip Kevin Buzzard (Jul 13 2019 at 14:07):

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

view this post on Zulip Kevin Buzzard (Jul 13 2019 at 16:20):

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

view this post on Zulip Mario Carneiro (Jul 13 2019 at 18:33):

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

view this post on Zulip Mario Carneiro (Jul 13 2019 at 18:35):

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.

view this post on Zulip Kevin Buzzard (Jul 13 2019 at 21:16):

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.

view this post on Zulip Andrew Ashworth (Jul 13 2019 at 22:16):

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

view this post on Zulip Andrew Ashworth (Jul 13 2019 at 22:37):

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.

view this post on Zulip Mario Carneiro (Jul 14 2019 at 00:42):

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

view this post on Zulip Mario Carneiro (Jul 14 2019 at 00:43):

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

view this post on Zulip Mario Carneiro (Jul 14 2019 at 01:48):

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

view this post on Zulip Kevin Buzzard (Jul 14 2019 at 14:29):

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?

view this post on Zulip Kevin Buzzard (Jul 14 2019 at 14:48):

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.

view this post on Zulip Mario Carneiro (Jul 14 2019 at 15:45):

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.

view this post on Zulip Kevin Buzzard (Jul 14 2019 at 18:56):

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.

view this post on Zulip Andrew Ashworth (Jul 14 2019 at 19:12):

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>

view this post on Zulip Andrew Ashworth (Jul 14 2019 at 19:42):

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...

view this post on Zulip Kevin Buzzard (Jul 14 2019 at 20:09):

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.

view this post on Zulip Andrew Ashworth (Jul 14 2019 at 20:10):

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

view this post on Zulip Andrew Ashworth (Jul 14 2019 at 20:10):

apparently I linked a pre-print

view this post on Zulip Andrew Ashworth (Jul 14 2019 at 20:10):

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

view this post on Zulip Andrew Ashworth (Jul 14 2019 at 20:11):

or something, weird

view this post on Zulip Andrew Ashworth (Jul 14 2019 at 20:14):

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.

view this post on Zulip Andrew Ashworth (Jul 14 2019 at 20:21):

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.

view this post on Zulip Andrew Ashworth (Jul 14 2019 at 20:22):

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

view this post on Zulip Andrew Ashworth (Jul 14 2019 at 20:27):

X_for_Cauchy -> X_for_Dedekind is false in general

view this post on Zulip Andrew Ashworth (Jul 14 2019 at 20:28):

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.

view this post on Zulip Andrew Ashworth (Jul 14 2019 at 20:45):

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.

view this post on Zulip Andrew Ashworth (Jul 14 2019 at 20:50):

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.

view this post on Zulip Kevin Buzzard (Jul 14 2019 at 21:31):

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

view this post on Zulip Andrew Ashworth (Jul 14 2019 at 23:25):

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

view this post on Zulip Andrew Ashworth (Jul 14 2019 at 23:38):

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

view this post on Zulip Andrew Ashworth (Jul 15 2019 at 05:28):

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.

view this post on Zulip Johan Commelin (Jul 15 2019 at 15:46):

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

view this post on Zulip Andrew Ashworth (Jul 15 2019 at 16:15):

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

view this post on Zulip Andrew Ashworth (Jul 15 2019 at 16:15):

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.)

view this post on Zulip Andrew Ashworth (Jul 15 2019 at 16:18):

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.

view this post on Zulip Kevin Buzzard (Jul 15 2019 at 16:25):

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

view this post on Zulip Kevin Buzzard (Jul 15 2019 at 16:26):

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.

view this post on Zulip Andrew Ashworth (Jul 15 2019 at 16:48):

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

view this post on Zulip Andrew Ashworth (Jul 15 2019 at 16:49):

not by much, though

view this post on Zulip Andrew Ashworth (Jul 15 2019 at 16:52):

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

view this post on Zulip Johan Commelin (Jul 15 2019 at 18:14):

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

view this post on Zulip Kevin Buzzard (Jul 15 2019 at 18:46):

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

view this post on Zulip Mario Carneiro (Jul 15 2019 at 20:02):

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

view this post on Zulip Andrew Ashworth (Jul 15 2019 at 20:17):

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?

view this post on Zulip Andrew Ashworth (Jul 15 2019 at 20:18):

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

view this post on Zulip Mario Carneiro (Jul 15 2019 at 20:23):

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"

view this post on Zulip Andrew Ashworth (Jul 15 2019 at 20:25):

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.

view this post on Zulip Mario Carneiro (Jul 15 2019 at 20:28):

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

view this post on Zulip Mario Carneiro (Jul 15 2019 at 20:29):

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

view this post on Zulip Kevin Buzzard (Jul 15 2019 at 23:06):

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

view this post on Zulip Andrew Ashworth (Jul 15 2019 at 23:24):

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.

view this post on Zulip Kevin Buzzard (Jul 15 2019 at 23:28):

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.

view this post on Zulip Jesse Michael Han (Jul 15 2019 at 23:39):

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

view this post on Zulip Kevin Buzzard (Jul 15 2019 at 23:42):

What's a CAOF typeclass?

view this post on Zulip Jesse Michael Han (Jul 15 2019 at 23:44):

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

view this post on Zulip François G. Dorais (Jul 16 2019 at 00:19):

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

view this post on Zulip Mario Carneiro (Jul 16 2019 at 01:00):

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

view this post on Zulip Jesse Michael Han (Jul 16 2019 at 01:00):

@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

view this post on Zulip Mario Carneiro (Jul 16 2019 at 01:01):

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

view this post on Zulip François G. Dorais (Jul 16 2019 at 01:42):

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.)

view this post on Zulip François G. Dorais (Jul 16 2019 at 03:21):

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.)


Last updated: May 16 2021 at 21:11 UTC