Zulip Chat Archive

Stream: lean4

Topic: Notation in structures


view this post on Zulip Kevin Buzzard (Mar 15 2021 at 11:21):

variables (G M : Type)

structure cocycle (G M : Type) :=
(to_fun : G  M)
-- I understand the reasons why I can't just call the function "f", but
-- this next line still looks ugly. Can I immediately replace
-- the computer science "to_fun" with the mathematician's "f" notation?
(spec :  g h, to_fun (g * h) = to_fun g + g  to_fun h) -- this looks ugly

I understand that it's a really good idea that the underlying function is always called to_fun.
Can I do something like this in Lean 4?

structure Cocycle (G M : Type) :=
(f : G  M)
(spec :  g h, f (g * h) = f g + g  f h)

Right now in mathlib we use these stupid primed notation structure fields and then
never use them again because they're full of explicit to_funs. We then instantly
define a coercion to function and prove all the unprimed lemmas all rewritten
with the coercions.

view this post on Zulip Sebastian Ullrich (Mar 15 2021 at 11:28):

You could define a PreCocycle with the first field, then the coercion, then extend it with the second field :upside_down:
edit: That doesn't really help

view this post on Zulip Kevin Buzzard (Mar 15 2021 at 11:36):

variables (G M : Type) [monoid G]
  [monoid G] [add_comm_group M] [distrib_mul_action G M]

structure cocycle :=
(to_fun : G  M)
-- I do not really understand why you need to have a definition.
(spec' :  g h, to_fun (g * h) = to_fun g + g  to_fun h) -- this looks ugly

-- This next line looks a bit scary in Lean code written for mathematicians.
-- I also do not even know whether I'm supposed to run it within the namespace
-- or outside
instance : has_coe_to_fun (cocycle G M) := _,cocycle.to_fun

namespace cocycle
variables {G M} (c : cocycle G M)
-- finally fix the mess
def spec :  (g h : G), c (g * h) = c g + g  c h := c.spec'
end cocycle
-- rm -rf cocycle.*'

view this post on Zulip Sebastian Ullrich (Mar 15 2021 at 11:41):

Kevin Buzzard said:

-- I understand the reasons why I can't just call the function "f"

Why is that, exactly? Because fields cannot be marked protected in Lean 3? In Lean4 they can.

view this post on Zulip Kevin Buzzard (Mar 15 2021 at 11:42):

because of all this stupid fuss about old and new structure commands

view this post on Zulip Kevin Buzzard (Mar 15 2021 at 11:42):

you are forcing structures which we don't like on us and we are going to have to write automation to build them I think. Our structures grow in complex ways.

view this post on Zulip Eric Wieser (Mar 15 2021 at 11:45):

I think we are already in dire need of automation for structures whose first member is to_fun

view this post on Zulip Eric Wieser (Mar 15 2021 at 11:47):

Once we have that, dealing with new-style structures would be hidden away anyway

view this post on Zulip Eric Wieser (Mar 15 2021 at 11:48):

Although it would be nice if lean could establish a canonical "self reference" name in structure fields

view this post on Zulip Eric Wieser (Mar 15 2021 at 11:48):

Doc-gen uses c (as in, c.to_fun):

view this post on Zulip Eric Wieser (Mar 15 2021 at 11:48):

docs#monoid_hom

view this post on Zulip Sebastian Ullrich (Mar 15 2021 at 11:52):

What is the advantage of doing that over printing the actually-correct to_fun?

view this post on Zulip Eric Wieser (Mar 15 2021 at 12:02):

I take it back, it's not doc-gen; #print does it too in lean 3

view this post on Zulip Sebastian Ullrich (Mar 15 2021 at 12:03):

Sure, it's just not correct to present that output as the definition of the field

view this post on Zulip Gabriel Ebner (Mar 15 2021 at 12:04):

I'm not sure if everybody realizes this, but Lean 4 doesn't have or . The coercion is immediately eliminated after/during elaboration:

instance : CoeFun Nat (fun _ => Nat  Nat) where
  coe a b := a + b

#check (4 : Nat) 8
-- (fun (b : Nat) => 4 + b) 8 : Nat

view this post on Zulip Gabriel Ebner (Mar 15 2021 at 12:05):

So you can just use to_fun in the definition of the structure. You only miss the nice notation, but it's the same result you'd get later with the coercion.

view this post on Zulip Scott Morrison (Mar 15 2021 at 12:19):

Does this mean that all our simp lemmas which relying on "seeing" the coercion in order to match are no longer viable?

view this post on Zulip Gabriel Ebner (Mar 15 2021 at 12:25):

You still see the to_fun function.

view this post on Zulip Sebastien Gouezel (Mar 15 2021 at 12:48):

Do you know the reason for this design choice? Coercions are not only a feature for user-input, but also extremely important for pretty-printing readability. Is there a way to enable a default pretty-printing using ? I mean, if e is an equiv and there is e.to_fun in an expression to be pretty-printed, can one make sure that ⇑e is pretty-printed instead (where I don't care about the internals of what the arrow means to Lean)?

view this post on Zulip Leonardo de Moura (Mar 15 2021 at 16:27):

@Sebastien Gouezel There is no short answer here. I will try to summarize

  • Lean 3 coercion system contains a few hacks. Example: the coercion from Prop to Bool is a hard-coded hack in the elaborator. We wanted to eliminate this hack in Lean 4.
  • We need dependent coercions for expressing the coercion from Prop to Bool since only decidable propositions can be coerced.
instance decPropToBool (p : Prop) [Decidable p] : CoeDep Prop p Bool where
  coe := decide p
  • Thus, the coe type is
coe : {α : Sort u_1}  {β : Sort u_2}  (a : α)  [inst : CoeT α a β]  β

This function is quite messy to handle at simp because of the dependency. So, we have considered the following alternatives:
1- Remove dependent coercions, and use the Lean 3 hack. Discarded because it is hackish and has limitations.
2- Require the user to show that CoeDep α a β types are subsingletons (CoeT is just a layer on top of CoeDep). Then, we would be able to have a congruence lemma of the form [CoeT α a β] -> [CoeT α a' β] -> (h : a = a') -> coe a = coe a'. Discarded because it would increase the complexity even more.
3- Distinguish regular coercions from dependent coercions, and expand eagerly only dependent ones. Discarded because it is not a uniform solution.
4- Expand coercions eagerly. (selected this one). Moreover, after the expansion, the terms were way simpler to manipulate in proofs.
I can see this may be inconvenient when generating documentation (e.g., HTML pages from elaborated declarations).

That all being said. We are willing to put hooks on the system to allow users to customize this kind of behavior. There are many possibilities, and I have realized that it is impossible to make everybody happy :) For my goals, alternative 4 is great.

view this post on Zulip Sebastien Gouezel (Mar 15 2021 at 16:47):

I also think that alternative 4 is great, for clarity and everything. I would be perfectly happy with this alternative together with a system to register some notations in the pretty-printer, like when e is an equiv, print e.to_fun as e (or e with a weird arrow or whatever is nicer than e.to_fun). Of course, I don't have any idea if/how this can be implemented, and if/how it creates problems for roundtrips, and so on, so you may safely discard this as wishful thinking :-)

view this post on Zulip Mario Carneiro (Mar 15 2021 at 16:47):

By the way, there is was a long standing issue in lean 3 that may be related. Currently, it's not possible for simp to rewrite inside the function part of a coe_fn application, like coe_fn (f + 0) x, because coe_fn allows coercion to dependent functions (even if the particular instance in question is not dependent). This means that often (f + 0).to_fun x will simplify where coe_fn (f + 0) x will not, which has been used to argue against using function coercions in spite of their other advantages. (I remember this coming up in category theory)

view this post on Zulip Sebastien Gouezel (Mar 15 2021 at 16:48):

This has been solved a long time ago by @Gabriel Ebner in the case of non-dependent coercions, I think.

view this post on Zulip Mario Carneiro (Mar 15 2021 at 16:49):

well we'll be revisiting this issue in lean 4 I think

view this post on Zulip Sebastien Gouezel (Mar 15 2021 at 16:55):

This was lean#209, if I'm not mistaken. It made a huge difference for simp usability together with coercions. If coercions are gone in Lean 4 (apart from user input), I don't see why we should get problems with this in Lean 4.

view this post on Zulip Mario Carneiro (Mar 15 2021 at 16:57):

I'm on board with coercions getting eliminated at parse time; less syntax to recognize and pattern match on is always a good thing. We probably want to keep the coercion functions themselves recognizable, but that's a problem that can be solved by code quality and review stuff

view this post on Zulip Mario Carneiro (Mar 15 2021 at 16:59):

for example if coe x expands to nat.cast x then the simp lemmas will talk about nat.cast, but if coe x expands to nat.recOn x 0 (+1) then that would be bad for automation and probably also for the printer

view this post on Zulip Leonardo de Moura (Mar 15 2021 at 17:13):

Kevin Buzzard said:

you are forcing structures which we don't like on us and we are going to have to write automation to build them I think. Our structures grow in complex ways.

I think it is a bit much to say we are forcing anything on you. From my point of view, we are just not implementing what you want :)
We also took the time to explain why. Finally, as I pointed out over and over again, Lean is extensible, users may implement their own structure command and be happy.

view this post on Zulip Kevin Buzzard (Mar 16 2021 at 08:35):

Leonardo de Moura said:

I think it is a bit much to say we are forcing anything on you. From my point of view, we are just not implementing what you want :)

Thanks a lot for the answer Leo. I'm beginning to understand the philosophy better now.

I might have ideas about how to use coercions to functions in a slick manner within some structure format to make Lean code look more comprehensible to mathematicians, and I came here asking whether this should be part of Lean's default structure command, but you're pointing out (something which is probably obvious to all the programming people) that you have made structures already and the point is that Lean 4 has the flexibility for me to be able to make what I want myself (e.g. an entire new structure command or an old-structure-cmd emulator) rather than asking you to change anything at your end.

Sorry for being so slow :-) I have not yet really properly understood the consequences of the change from Lean 3 to Lean 4.

view this post on Zulip Jason Gross (Mar 16 2021 at 13:21):

Is there anything special about fields in structures, or is it entirely configurable? That is, suppose I want to define a variant of a structure command that lets me mix defs and instances and even other structures in the middle (closer to Agda's record/data declarations), such that later fields are allowed to refer to these in their types. Is there a way to set things up so that the . notation and record builder notation, etc, work with whatever these fields desugar to?

view this post on Zulip Sebastian Ullrich (Mar 16 2021 at 13:36):

These features categorize some inductives as "structure-like" or "structures", see https://github.com/leanprover/lean4/blob/master/src/Lean/Structure.lean
In principle, you can define your own inductive and projection functions that fulfill these predicates. I'm not completely sure what desugaring you have in mind, but if you can compile it down to an inductive, it seems likely you can also do so down to a (simpler) structure, in which case you would not have to worry about this aspect.

view this post on Zulip Jason Gross (Mar 16 2021 at 13:50):

The compilation scheme I have in mind is to compile it down to a structure where all of the definitions and instances (and also structures, though this will be harder) have been inlined into the field types. Then I can define new constructors and fields which just adjust the type signatures (or in the case of inlined structures, adjust the data presentation).

That is, something like

stucture Cat where
  Obj : Type
  Arr : Obj -> Obj -> Type
  instance : HasArr Obj := { arr := Arr }
  id : \forall {a : Obj}, HasArr.arr a a

would be compiled into something like

stucture Cat where
  Obj' : Type
  Arr' : Obj -> Obj -> Type
  id ': \forall {a : Obj}, @HasArr.arr Obj' { arr := Arr' } a a
def Obj : Cat -> Type := Obj'
def Arr : ... := Arr'
instance inst : HasArr Arr := ...
def id : \forall {a : Obj}, @HasArr.arr Obj inst a a := ...

Hm, I guess retyping the constructor here is quite tricky, but this should give a sense of what I'm thinking of

view this post on Zulip Sebastian Ullrich (Mar 16 2021 at 14:01):

I see. Defining a custom constructor would be a problem for the current structure instance notation ({...}), though custom fields are less of an issue since dot notation will work for any declaration that is inside the namespace of the given term's type. The only thing you currently lose is access to inherited custom fields.


Last updated: May 07 2021 at 13:21 UTC