Variables and sections

[fizruk]

To reduce boilerplate in formalisations, it makes sense to introduce some simple organisational features, such as sections and variables (shared assumptions). I've implemented a version of these in develop, getting inspired by Lean and Coq. I ended up with Coq-style variables, but I'm not sure which one is better and why. Below are some examples and some of my thoughts.

Lean

Lean4 has Variables which can be used to automatically add bound variables to the following definitions:

variable (α β γ : Type)
variable (g : β → γ) (f : α → β) (h : α → α)
variable (x : α)

def compose := g (f x)
def doTwice := h (h x)
def doThrice := h (h (h x))
def plus4 := compose _ _ _ (fun x => x + 2) (fun x => x + 2)

Important properties of variable declaration in Lean4:

1. A given variable is added as a bound variable only if it is actually used in the definition (explicitly or implicitly). E.g. compose will not have h as its bound variable, but will have α, β, γ, g, f, and x bound variables. On the other hand, doTwice and doThrice only depend on α, h, and x.
2. Variables added in this way are explicit (they can be implicit if we use curly braces, e.g. variable {α β γ : Type}), even inside the same section. This is why plus4 calls compose with all 5 arguments.

Coq

Coq has Assumptions, including Variable and Hypothesis commands (which are equivalent).

Section example.
  Variable (α β γ : Type).
  Section compose.
    Variable (g : β → γ) (f : α → β) (h : α → α).
    Variable (x : α).

    Define compose := g (f x).
    Define doTwice := h (h x).
    Define doThrice := h (h (h x)).
    (* Define plus4 := compose. PROBLEM: compose is already saturated (fully applied). *)
  End compose.

  (* Type variables are already in scope. *)
  (* But g, f, and x become explicit arguments. *)
  Def plus4 := compose (fun x => x + 2) (fun x => x + 2).
End example.

(* Outside of section "example", type variables become explicit arguments. *)
Def plus4' := compose _ _ _ (fun x => x + 2) (fun x => x + 2).

Important properties of Variable command in Coq:

1. Similarly to Lean, only variables that are actually used in a definition are introduced as parameter upon exiting a section.

2. In contrast to Lean, variables are implicit in applications of definitions in the same section (this means that sometimes you need to exit section before you can properly use it).

Rzk (experimental)

There is an implementation of Coq-style variables and sections (see 469cde53554e882ad697c187c9b89c089023afbc, or develop branch at the time of writing). You can see an example use of this here: https://github.com/fizruk/rzk/blob/37708d49aa50fe866a4c54370b827b9ff0c6b1ca/docs/docs/rzk-1/recId.md?plain=1#L80-L187.

Originally, this seemed to be a nice approach, however, I now think this is setting up an issue: it is too easy to accidentally use an extra assumption. For example, it is tempting to set #variable AisSegal : isSegal A to make the proof assistant automatically figure out when it is used, even when it is implicit. In particular, it would make it easy to use conclusion as assumption (e.g. when proving that A is Segal using a lemma that indirectly uses AisSegal).

This is less of a problem if we use Lean-style variables, since we would have to write AisSegal explicitly in the proof and will probably notice it. However, this might still become a problem once we add term inference and write _ instead of AisSegal (or a similar argument), or when it is introduced indirectly somehow (I would have to think of an example).

This suggests to me two things:

1. There is a strong need in a language server (see #31) to make sure users have easy access to see explicitly all assumptions of a definition.

2. It might make sense to add some extra checks/warnings when an assumption matches (exactly?) the conclusion in a definition.

[fizruk]

38 is now merged and implements Coq-style variables and sections, with extra checks for implicitly used variables and uses (...) annotations to suppress errors. This should work well enough in practice, I think. If something goes wrong, we will open another issue.