Zulip Chat Archive
Stream: new members
Topic: Omitting section variables inside the same section
Youngju Song (Jan 01 2025 at 01:43):
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 (Jan 01 2025 at 02:32):
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 (Jan 01 2025 at 02:32):
That won't help much with parametrized types though!
Eric Wieser (Jan 01 2025 at 02:33):
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 (Jan 01 2025 at 05:12):
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 (Jan 02 2025 at 18:02):
@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 (Jan 02 2025 at 18:05):
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 (Jan 02 2025 at 18:09):
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 (Jan 02 2025 at 18:19):
@Sebastian Ullrich Can you elaborate on the "module class approach"?
Eric Wieser (Jan 02 2025 at 18:28):
I think Sebastian Ullrich is describing the one that pandaman blogged about above
Youngju Song (Jan 02 2025 at 21:02):
@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 (Jan 03 2025 at 04:58):
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 (Jan 07 2025 at 17:49):
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.
Last updated: May 02 2025 at 03:31 UTC