coercions in TPL3

Stream: new members

[Mike Shulman]

The section on coercions in Theorem Proving in Lean (3) says that the output sort and function type are fields of the typeclasses has_coe_to_sort and has_coe_to_fun. However, it seems that (now?) they are actually parameters:

@[class]
structure has_coe_to_sort : Sort u → out_param (Sort v) → Sort (max (max 1 u) v)
fields:
has_coe_to_sort.coe : Π {a : Sort u} {S : Sort v} [self : has_coe_to_sort a S], a → S

@[class]
structure has_coe_to_fun : Π (a : Sort u), out_param (a → Sort v) → Sort (max (max 1 u) v)
fields:
has_coe_to_fun.coe : Π {a : Sort u} {F : a → Sort v} [self : has_coe_to_fun a F] (x : a), F x

In particular, the "try it!" boxes in this section do not work, unless I edit them to move the fields to parameters, e.g.

instance Semigroup_to_sort : has_coe_to_sort Semigroup (Type u) :=
{coe := λ S, S.carrier}

instance morphism_to_fun (S1 S2 : Semigroup) :
  has_coe_to_fun (morphism S1 S2) (λ _, S1 → S2) :=
{ coe := λ m, m.mor }

Is this something that can be fixed in TPL3, for those of us still using and teaching with Lean 3?

[Johan Commelin]

Hmm, the easy fix would be to pin TPL to an older version of Lean. Would that be acceptible?

[Mike Shulman]

That would make the "try it!" boxes work, but it would reduce the usefulness of TPL for people who want to learn Lean 3. Shouldn't they want to learn the most recent version?

[Johan Commelin]

Well, the hope is that ~ 6 months from now they should want to learn Lean 4.

[Johan Commelin]

So it's not clear whether it's worth it to try to bump TPL to recent Lean.

[Patrick Massot]

I think @Jeremy Avigad is still willing to maintain TPIL 3.

[Jeremy Avigad]

Yes, hopefully it won't be hard to fix. I'll take a look tomorrow.

[Mike Shulman]

Thanks!

[Mike Shulman]

Also: exercise 7.10.1 says

you should work within a namespace named hide, or something like that, in order to avoid name clashes.

but it appears that namespaces are not allowed to be named hide:

invalid namespace declaration, identifier expected
invalid 'hide' command, identifier expected

[Mike Shulman]

And it might be more helpful for section 1.2 to link to https://leanprover-community.github.io/ instead of https://github.com/leanprover/lean/.

[Jeremy Avigad]

Thanks! Will do.

[Jeremy Avigad]

I can't seem to build TPIL any more with Sphinx. TPIL uses a Python extension, lean_sphinx, by Gabriel. It handles the lean code blocks. I am getting the following error:

Could not import extension lean_sphinx (exception: cannot import name 'CodeBlock' from 'sphinx.directives' (/home/avigad/projects/theorem_proving_in_lean/.venv/lib/python3.10/site-packages/sphinx/directives/__init__.py))
make: *** [Makefile:27: leantest] Error 2

Does anyone have any ideas what to do? Maybe something has changed in recent versions of Sphinx? I also have Python 3.9 lying around, but that doesn't seem to work either.

[Jeremy Avigad]

O.k., the good news is that form this page,
https://www.sphinx-doc.org/en/master/extdev/deprecated.html
I discovered that I should change from sphinx.directives import CodeBlock to from sphinx.directives.code import CodeBlock.

The bad news is updating mathlib and testing showed that dozens of things have broken. It will be a while before I'll have time to do this, and I am not sure it is worth it. @Mike Shulman , if you have the time and energy, you could give it a try. The README file is pretty self explanatory, and if you can get a version to build, I can deploy it. It will mostly be a matter of fixing imports for filenames that have changed, fixing theorem names that have changed, etc.

[Mike Shulman]

Ah, all right; maybe it isn't worth it then. I certainly don't have the time and energy. What about pinning it to an earlier version of Lean, as Johan suggested, but adding comments noting that some things have changed since it was written?

[Jeremy Avigad]

@Bryan Gin-ge Chen Is there a way to access a web version of an earlier version of Lean?

[Bryan Gin-ge Chen]

Unfortunately not at the moment, we don't have different versions of the web editor. The community web editor is also frozen at the moment since the ZIP file containing mathlib oleans has gotten too big for GitHub pages.

[Jeremy Avigad]

O.k., thanks. Anyhow, it would be nice to update TPIL. I'll put it on my todo list and wait for a lazy Sunday afternoon to spend a couple of hours making all the little fixes.