0
$\begingroup$

Intuitive notations are always a big boost when stating and proving things. Modern interactive theorem provers usually have some way of building syntactic sugars aside from their ordinary abstraction mechanisms, such as macros in Lean, notations in Coq, etc.

However, as far as I know, when using these sugared forms, the users of these provers are forced to deal with their desugarings.

My question is: is there a way to systematically abstract away the definition of these newly-defined notations, and reason with them directly?

Update: Specifically, when using sugared forms, such as do-notations in Lean, users often have to deal with desugarings when proving theorems. As an example, consider the following Lean theorem (arbitrarily taken from Sebastian Ullrich's dissertation):

theorem simple [Monad m] [LawfulMonad m] (b : Bool) (ma ma' : m α)
  : (do let mut x ← ma;
        if b then { x ← ma' };
        pure x)
      = (ma >>= fun x => if b then ma' else pure x)

When proving this theorem, one needs to reason with the term after elaboration. Is there a systematic approach to proving theorems using do-notations without relying on elaboration, perhaps by establishing several lemmas beforehand?

$\endgroup$
5
  • 1
    $\begingroup$ Can you add an example of what having "to deal with their desugarings" looks like to you? $\endgroup$
    – Eric
    Commented Dec 21, 2023 at 14:54
  • $\begingroup$ Are you talking about purely syntactic notations? $\endgroup$ Commented Dec 21, 2023 at 17:36
  • $\begingroup$ As for Coq, I think the question makes sense for Definitions, which are akin to just abbreviations, yet the need for unfolding in order to "use" those definitions. Notations in Coq are a further layer and are (mostly) plain transparent. $\endgroup$ Commented Dec 21, 2023 at 19:54
  • $\begingroup$ @Eric I have updated the problem description, thanks for the suggestion. $\endgroup$
    – yiyuan-cao
    Commented Dec 22, 2023 at 4:53
  • $\begingroup$ I’m confused by your example. In the dissertation, the proof is simply by cases b <;> simp. I don’t see how that is “reasoning with the term after elaboration”. Are you saying the relevant simp lemmas only apply since they apply to the elaborated term? Do you want notations which are opaque in the sense one can’t automatically use lemmas which apply to the elaborated form? $\endgroup$
    – Jason Rute
    Commented Dec 22, 2023 at 5:54

1 Answer 1

2
$\begingroup$

This is a general problem, not just with notations: you always have to deal with the elaborated code, not the "one you wrote". This applies to notations, but also to type-classes resolution (in most systems), equations compilation (in Lean or if you use Equations in Coq), insertion of coercions (which is done via type-classes in Lean, but is a separate mechanism in Coq), or even more extreme, terms that were built through tactics. There is no way to avoid this: in the end, the proof assistant only knows about the elaborated term, the sugared one is not much more than a string of characters.

This being said, notations are a rather mild part of elaboration, as the output of desugaring/elaboration is very predictable (compare with type-class search or, worse, tactics). I do not know how things are in Lean, but Coq usually does a good job at re-sugaring notations when presenting a term to the user, so you are usually able to reason "at the notation level", although this is not what the system really "sees".

As you remark, something that is usually useful to encapsulate the notation properly and reason at the more abstract level is to establish a bunch of lemmas beforehand, typically by "opening up" the abstraction. Note that this is not really specific to notations, but is a general good way to organise formal developments: each time you introduce a new abstraction layer, you develop its "theory" connecting it to other notions, and then you try and reason as much as possible at the new abstraction level, without having to go back to the lower one.

$\endgroup$
2
  • $\begingroup$ Thank you for your answer! After further thought, I think a deeper question I am seeking an answer to is: Can we integrate syntactic abstractions like macros and notations into the core logic level, so that we can reason with them directly, analogous to reasoning about function definitions? $\endgroup$
    – yiyuan-cao
    Commented Dec 23, 2023 at 12:20
  • $\begingroup$ Simple macros/notations are only a nice way to present a certain definition: a mathematician might write $\int_{a}^{b} x^2 \,dx$ where a proof assistant without notations would rather write something like integral lebesgue_measure (fun x => (prod x x)) a b. The notation is then just a display artefact, but has no fundamental status, simply reducing to definitions. And definitions usually have a fundamental status, at the core logic level. If you go for more elaborated notations, that might be doing more work behind the scene, well… I guess it is much less clear. $\endgroup$ Commented Dec 29, 2023 at 12:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.