Notation in structures

Stream: lean4

[Kevin Buzzard]

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.

[Sebastian Ullrich]

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

[Kevin Buzzard]

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

[Sebastian Ullrich]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

docs#monoid_hom

[Sebastian Ullrich]

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

[Eric Wieser]

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

[Sebastian Ullrich]

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

[Gabriel Ebner]

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

[Gabriel Ebner]

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.

[Scott Morrison]

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

[Gabriel Ebner]

You still see the to_fun function.

[Sebastien Gouezel]

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

[Leonardo de Moura]

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

[Sebastien Gouezel]

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

[Mario Carneiro]

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)

[Sebastien Gouezel]

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

[Mario Carneiro]

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

[Sebastien Gouezel]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Leonardo de Moura]

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.

[Kevin Buzzard]

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.

[Jason Gross]

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?

[Sebastian Ullrich]

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.

[Jason Gross]

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

[Sebastian Ullrich]

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.