Omitting section variables inside the same section

Stream: new members

[Youngju Song]

I wish the following code type checks:

section
  variable (A: Type)
  variable (a: A)
  def M := A
  def m: M := a -- this does not typecheck
  -- def m: M A := a -- this typechecks
end

where the definition M inside the section uses a section variable A, and when this definition is used "inside" the same section, I don't have to provide A again.
Would it be already possible to do this in Lean? I relied a lot on and loved this feature when I was using Coq, which not just reduced few keystrokes but also made the code shorter and more elegant.
This is especially useful when you later add a new parameter to a series of functions (that can call each other) without devastatingly modifying the code.

[Eric Wieser]

One way to add a parameter to a large collection of functions at once is to move them all within a Reader monad, and then you can have a structure with all the configuration that you can add fields to in just one place.

[Eric Wieser]

That won't help much with parametrized types though!

[Eric Wieser]

The feature you're asking for existed in Lean 3 as parameter instead of variable, but it was not inherited by Lean 4: presumably due to a combination of lack of interest and surprising behavior

[pandaman]

What I did in a similar situation was to declare a structure (or a class) that holds inputs as fields, and define stuff like M as a function that takes structure.
https://zenn.dev/pandaman64/articles/lean-proof-data-en

[Youngju Song]

@Eric Wieser @pandaman Thank you for the suggestions! I agree that these workarounds could be useful, but that does not cover my cases.

[Youngju Song]

As a person who really loves this feature, it is interesting that this feature existed before and got dropped. It would be great if one can at least reimplement "parameter" as a user library in Lean4.

[Sebastian Ullrich]

In what way does it not cover your use case? The "module" class approach should be strictly more powerful and convenient, crucially it also allows for reopening the section and accessing declarations instantiated for a given set of parameters

[Youngju Song]

@Sebastian Ullrich Can you elaborate on the "module class approach"?

[Eric Wieser]

I think Sebastian Ullrich is describing the one that pandaman blogged about above

[Youngju Song]

@Sebastian Ullrich Am I correct that we are discussing something like the following?

inductive A: Type
inductive B: Type

class Params :=
  a: A
  b: B

section
  variable [Params]
  def useA: Unit := let _: A := Params.a; () -- "a" does not typecheck - why?
  def useB: Unit := let _: B := Params.b; ()
  def useAB: Unit := let _: A := Params.a; let _: B := Params.b; ()
end
#print useA

I have been using this pattern when the set of parameters form a clear semantic unit and they always go together. But in most other cases, I ended up using variable (a: A) (b: B). In my recollection, the reasons are as follows:
(1) There is an additional obligation to define such a class (Params).
(2) I would want useA to rely on parameter A but not B. In this simple case, it should be possible to split these into different sections, but I have cases where I quantify over multiple variables and then define and prove multiple auxiliary derived definitions on top of them in the same section. I want each of these auxiliary definitions and theorems around them to quantify over just the needed ones, automatically (without me needing to figure those out).
(3) I don't want my final definitions to have typeclass quantification (too much typeclass caused tricky unexpected performance issues). It should be possible to achieve this but I am afraid it will be tedious.

This is a question: I think a and b (instead of Params.a and Params.b) should work in the above code snippet, but it doesn't. Apparently I made some stupid mistake - do you have any idea?

[pandaman]

I'm not quite satisfied with my approach either and I hope there is a better guide than mine. For me, there are some usability issues like

• the interaction with case analysis is manual, and I needed to introduce separate classes for each branch by hand
• the fields of the "module" class are definitionally equal to variables in my theorem statements, but not equal-that-rw-and-simp-recognize so manipulations of the terms were less than ideal
• Classes don't work well with nested dot notations: #general > Nested dot notation fails with type classes

Still, it at least allows some proof reuse that is crucial for my project.

[Youngju Song]

I also found that, in my mental model, the behavior of parameter is more natural and gives me less cognitive compared to variable. In my mental model, parameter and def in the top-level command roughly corresponds to function arguments and let binding in the kernel term:

section parameter (A: Type)
chunk_of_code
end
===>
(fun (A: Type) => chunk_of_code)

Here, the behavior of parameter is congruent the behavior of the function arguments (e.g., #check (fun (A: Type) (a: A) => let M := A; let m: M := a; (M, m)) typechecks), and it is easy for me to understand. If you want to access chunk_of_code outside the section, you need to provide the section parameters just as the user of the function provides arguments - this behavior is also congruent.

section def (A: Type) := body
chunk_of_code
end
===>
(let A: Type := body; chunk_of_code)

Also, chunk_of_code typechecks the same way regardless of whether A is parameter or def, just like chunk_of_code typechecks the same way regardless of whether A is a function argument or let-bound. I think this is a desirable property and definitely lessens my cognitive overhead.