Proof assistants with dynamic scope/local instances/etc.?

Question

Say I'm formalizing something in group theory, and I'm working with some action $\cdot$ of $(G, +)$ on a set. In my math textbook, the identity of $\cdot$ is explicitly mentioned once (if that), and then left implicit. In my formalization, do I have to constantly keep specifying $(G, \cdot)$, or can I temporarily set $\cdot$ as the default?

In my limited experience, mathematical writing uses "dynamic scope" like this a lot. Does this actually correspond to a computer scientist's definition of dynamic scope, and if so, do any proof assistants support this?

Answer 1

Agda has generalization of declared variables. In short, you can leave a variable block of variables that are appearing often.

Example:

variable
  g : Grammar

first-item : symbol g -> Item g

It implicitly adds the {g:Grammar} -> in front of the first-item.

There's another system that lets you do this on variables, called modules. And here's an example of using that:

module FinMap (k : Set)
              (size : ℕ) where
   maxSize : ℕ
   maxSize = size

You can later open this kind of a module and fill in the pieces. Possibly within another module, if your fill-up depends on implicits.

module ItemSet {g : Grammar} {n : ℕ} where
  open FinMap.FinMap (EIM g n) (eim-size g n) public
    using (maxSize)

These are syntactic-sugar features relying on implicits. It behaves a lot like a dynamic scope in practice.

Answer 2

In Isabelle/Isar locale can be used to specify implicit assumptions and notation conventions that are limited in scope. The assumptions are then added to each theorem proven in the locale. With the sublocale keyword one can define how notation maps from one context (locale) to another so that theorems can be reused in a different context.