# How to reason with notations directly?

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?

• Can you add an example of what having "to deal with their desugarings" looks like to you?
– Eric
Commented Dec 21, 2023 at 14:54
• Are you talking about purely syntactic notations? Commented Dec 21, 2023 at 17:36
• 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. Commented Dec 21, 2023 at 19:54
• @Eric I have updated the problem description, thanks for the suggestion. Commented Dec 22, 2023 at 4:53
• 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? Commented Dec 22, 2023 at 5:54

• 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. Commented Dec 29, 2023 at 12:30