refine_struct

Stream: mathlib4

[Thomas Murrills]

So, I have an idea for how to port the functionality of refine_struct, but I'm not sure if it's a good idea. (it seems good to me, though!) Thought I'd suggest it here.

It seems that refine in lean 4 relies on holes of the form ?_ or ?x instead of _. So, instead of using .. to refine structures, then, to be consistent, the lean 4 analogue of .. in this context should be ?...

As such...I think we might be able to avoid using refine_struct at all. Instead, we can define a term elaboration for any structure-like syntax that contains ?... This would elaborate the given syntax into one with an explicit named hole for each field. For example, given a structure with x, y, and z as fields, { x := 1, ?.. } would elaborate to { x := 1, y := ?y, z := ?z } (or some equivalent expression). We can then feed this directly to refine instead of using refineStruct at all.

Given the existing use of .. and _, the use of ?.. in refine seems like it would fill a niche in refine's functionality. It might also get used more than refine_struct is used in mathlib3 if it's simply "part of how refine works" instead of being shelved under a separate name. (To alert people to this functionality, maybe the docstring for refine could be added to in mathlib? I'm not familiar with how documentation is managed yet, though, so I don't know.)

As for how to implement the interaction with haveField, the idea would be to attach the necessary information as metadata to each of the metavariables created by ?... Then haveField could (I hope) inspect the metadata on the given goal to figure out what field should be.

Anyway, let me know if this is a good idea (or if it would break something/is not as feasible as it seems)!

(I've already started trying to implement it just to see if I can get it to work, but if it turns out we'd rather shift this functionality to an explicit refineStruct or a port of pi_instance_derive_field instead, it shouldn't be too hard.)

[Thomas Murrills]

Ok, so given that ?.. would be a new sigil, which is nontrivial, I want to make the case for it properly! For whenever that decision gets made, here are the reasons I think it would fit nicely. (If you're wondering why I wrote all this, it's just that I like thinking about notation. :smile:)

[Thomas Murrills]

The case for ?..

Context
We need functionality for automatically filling unspecified fields in structures with synthetic holes, such that the holes are named by the field. For example, given a structure with two fields x, y, we need a convenient way to produce { x := ?x, y := ?y }. The question is: what should the syntax be? In Lean 3, we use { .. } (with refine_struct) to do this. In Lean 4, { .. } fills the fields with natural holes. Do we rewrite StructInst.lean to make it use synthetic holes?

My proposal is that we instead use the syntax { ?.. } for this task. Ultimately, the idea is that it enforces a certain conceptual metaphor.

(see bottom for tl;dr)

In Lean, there’s a close relationship between _ and ... _ can be used as a discarded pattern and as a natural hole; .. can be used as a sequence of discarded patterns and as a sequence of natural holes. Conceptually, we come to think of .. as a variadic form of _.

So what's the variadic form of a synthetic hole ?_? The concept for moving from _ to ?_ is "prefix a blank or an ident with ?, and it becomes synthetic instead of natural". As such, ?.. fits into the metaphor nicely as the synthetic form of .. and the variadic form ?_.

The distinction between synthetic and natural holes is important in general, of course, but particularly so in the context of refine: we demand that all new goals in refine be marked with ?. Why, then, should the programmer expect that something not marked with ? in refine should create a goal? The use of ? as a visual marker of syntheticness becomes, in the context of refine, a shorthand for something else: an indicator of what goals will be produced. Using .. for synthetic holes in refine would break this conceptual consistency, and might feel ad hoc. It would require "extra knowledge" to know that .. would be ?-like, whereas ?.. signals the occurrence of synthetic goals transparently. Even someone who hadn't encountered ?.. before could reasonably guess that it had something to do with ?_ and ?x, given that this is the only use of a prefixed ?.

This is arguably more important than the bare indicator of whether something is synthetic or not: ? indicates how a given hole will relate to the rest of our code, and, in particular, whether we need to continue to interact with it or not. We tend not to care about occurrences of _ and .. later on, but we do continue to care about occurrences of ?_ (and ?..).

To address the point that .. is already in use within refine_struct in Lean 3, and so we should maintain that usage: I would argue that replacing it in these contexts with ?.. is consistent with the move from Lean 3 to Lean 4. Holes used as goals in refine tactics should become synthetic holes, and in so doing, acquire a ? in Lean 4 (whether they're _ or .. holes).

(Note: refine_struct should simply become refine—after all, there's no need for refining a structure to be a special activity!)

Further, using .. in structures currently already works as one would expect in Lean 4. { .. } produces natural holes for unspecified fields, and can be used with refine' (the version that allows natural holes). (Some might find the ability to create natural holes like this useful—I'm not sure.) { ?.. } would create named synthetic holes for each field, named by the given field; e.g. if we had two fields x, y, { ?.. } would become { x := ?x, y := ?y }.

If we changed the behavior such that { .. } created synthetic holes, it would in principle be possible for the programmer to deduce that { .. } used in the context of refine is analogous to multiple ?_s instead of multiple _. But the metaphor of ? ⇔ "synthetic hole"/"goal to address" would be broken; further, the metaphor of .. corresponding to multiple _'s would be broken, as sometimes .. it would correspond to multiple ?_'s which remain relevant while still corresponding to multiple _'s which get discarded in other situations.

Likewise, ?_ can technically be used as a pattern in place of _—but we never do so in practice, in part because we intuitively get (and voluntarily enforce) the metaphor that _ and .. are for things we don't need to worry about, and ? is for things we do.

In general, my view is that syntax should communicate semantics and usage-roles as transparently as possible by relying on visual metaphors that are as transparent as possible—and there's some content that can be very transparently communicated by the presence of a single ?.

So, tl;dr:

• ?.. transparently signals a synthetic quality (and a goal quality) via the presence of ? and bolsters the analogy with ?_/?x.
• the role of the "synthetic ?_"/"natural _" distinction has an important intuitive meaning: _ and .. are for things we don't need to continue worry about, while ?_ (and ?..) is for things we do. ? signals not only a formal property of our code, but an aspect of how we think about and plan to interact with it. (Especially so in refine.)
• using .. for synthetic holes instead would muddy the conceptual waters for .., as sometimes it would mean multiple _'s, and sometimes it would mean multiple ?_'s; moreover, sometimes it would represent something discarded, whereas sometimes it would represent something with continued relevance.
• { .. } has an already-existing role to play by filling in unspecified fields with natural holes.
• { .. } is only ever used in refinement contexts in Lean 3; in moving to Lean 4, we should prepend all holes that we want to be goals in the context of refine with ?.

[Mario Carneiro]

This should be moved to #lean4 as a [RFC] thread