better support for section implicit parameter

[leodemoura]

This morning Soonho and I found an annoying behavior in sections. In the current implementation, when we type

   section 
       parameter A : Type
       definition id (a : A) := a
       theorem eq_id (a : A) : id a = a := refl
  end

The type of id is Pi (A : Type), A -> A, and every occurrence of id in the section is actually notation for id A. We use the same convention if A is an implicit parameter. We think this produces counter-intuitive behavior. If A is implicit, id should be notation for id _ inside and outside of the section. Here is the example that triggered this discussion. We were playing with connectives.lean, and added a section

            section
            parameters {a b c d : Prop}
            theorem inl (Ha : a) : a ∨ b :=  intro_left b Ha
            theorem inr (Hb : b) : a ∨ b := intro_right a Hb
            theorem elim (H₁ : a ∨ b) (H₂ : a → c) (H₃ : b → c) : c := rec H₂ H₃ H₁
            theorem elim3 (H : a ∨ b ∨ c) (Ha : a → d) (Hb : b → d) (Hc : c → d) : d :=
            elim H Ha (assume H₂, elim H₂ Hb Hc)   <<<<< Error 
            …

In the current approach, every occurrence of elim (in the section) is elim a b c, and this breaks all theorems that use elim in this section. The only workarounds are: do not use sections; close/reopen the section. Both are bad. Here is the “close/reopen” one. It looks really weird for outsiders.

            section
            parameters {a b c d : Prop}
            theorem inl (Ha : a) : a ∨ b :=  intro_left b Ha
            theorem inr (Hb : b) : a ∨ b := intro_right a Hb
            theorem elim (H₁ : a ∨ b) (H₂ : a → c) (H₃ : b → c) : c := rec H₂ H₃ H₁
            end

            section
            parameters {a b c d : Prop}
            theorem elim3 (H : a ∨ b ∨ c) (Ha : a → d) (Hb : b → d) (Hc : c → d) : d :=
            elim H Ha (assume H₂, elim H₂ Hb Hc)   <<<<< Error 
            …
            End

[leodemoura]

@fpvandoorn, I was implementing this feature, and found a problem with category.lean. In the old approach, the declaration

  abbreviation ID (A : ob) : mor A A := @id A

is parsed as

  abbreviation ID (A : ob) : @category.mor ob Cat A A := @id ob Cat A

In the new approach (described above), it is parsed as

  abbreviation ID (A : ob) : @category.mor _ _ A A := @id _ _ A

and lean complains that it can't synthesize the second placeholder : category ob. This seems to be an instance of a more fundamental problem, there is no way to make Cat available for class instance resolution without explicitly including it as an argument for ID.

  abbreviation ID {Cat : category ob} (A : ob) : @category.mor _ _ A A := @id _ _ A

I realize this is not a nice solution. @soonhokong and I discussed about having a section-level including command, where we would be able to say

including Cat

in a section, and all declarations in the section would have Cat as an argument even if it is was not explicitly referenced. @avigad: any thoughts?

[avigad]

It is starting to sound a little baroque. A section is supposed to temporarily fix the parameters to the definitions, but then we make an exception where it doesn't, and then we give the user a way to work around that when it causes problems.

The alternative would be to make the user type or.elim in your original example. That seems more intuitive: because you want to apply a local definition with parameters other than the ones you have fixed, you have to explicitly go outside the section. I think that is easier to understand. (But if it turns out that one day I will have to do that all the time, maybe I will find it annoying.)

[leodemoura]

I agree, it is starting to sound too complicated.

The alternative would be to make the user type or.elim in your original example.

This sounds reasonable to me.

It is easier to explain: "A section is supposed to temporarily fix the parameters to the definitions" (there are no exceptions).

[fpvandoorn]

I see your point, Jeremy. Especially since my first thought of a reaction to Leo would be among the lines of "the command including foo would be nice, but what if you also want some definition in your section which does not depend on foo?" (that is, another layer of work-around).

I think there are three decisions about what a section does:

• when are parameters used as argument for a definition/theorem? (are they always used as argument, or only when they occur in the theorem)
• what is the semantics of definitions inside the section? (is "mor" an abbreviation for "mor ob Cat" or for "mor ", or not an abbreviation at all)
• what information do we discard when closing the section? (do we forget about local notation?)

Especially the first two questions cannot be decided independently, as Leo's comment shows. Changing the semantics of definitions makes the current implementation on when parameters are used unfeasible (at least, I think that we would have to add "including Cat" in almost every theorem, because I never explicitly refer to "Cat").

However, I'm also not a fan of Jeremy's suggestion. Currently, I don't use parameters for the definitions I use afterwards in the section. For example, the current definition of morphism is abbreviation mor : ob → ob → Type := rec (λ mor compose id assoc idr idl, mor) Cat instead of abbreviation mor : Type := rec (λ mor compose id assoc idr idl, mor A B) Cat In the second definition I use the parameters A and B. If I would do that under the current implementation, I would have to write category.mor a lot in the rest of the file. I use mor B C, mor A A, mor B B, ... very frequently. The way to work around this is to either define mor outside the section, or to not use the parameters in the definition of mor. I currently use the second work-around. But I need to do this for a lot of definitions and theorems (and sometimes forgetting one also gives problems, which we saw with id_compose in another issue).

I'm don't know what the best solution is. It's easy to add a lot of bells and whistles to give exactly the functionality we want, but I agree that it's also good to keep things simple. My current preference would be something like the following (which might have too much bells and whistles): have two kind of parameters, "strong parameters" and "weak parameters" (these names need to be changed). -strong parameters would always go into the arguments of a definition foo (even if not mentioned by foo), and in that section foo will be an alias for foo <strong arguments> -weak parameters will only go into the arguments of a definition foo if mentioned by foo, and would not go into the alias, even if the parameter is explicit (so if they're explicit, I have to write these weak parameters every time I use foo)

In category.lean I would call ob, Cat strong parameters, and A B C D : ob weak parameters. Then I get exactly what I want: when I define abbreviation mor : Type := rec (λ mor compose id assoc idr idl, mor A B) Cat inside the section, mor will be an abbreviation for category.mor ob Cat, but I can still use mor B C and mor A A and so on. Also, every definition will depend on Cat, but not all of them will depend on D : ob.

Inside a math book, you sometimes see "For this section, fix group G" or something. That would correspond to defining a strong parameter. A weak parameter corresponds to the convention of using the letters g and h for group elements.

Maybe this is too much bells and whistles, but I think it provides some useful functionality not available with simpler proposals.

[avigad]

But in this example, is it really so much of a burden to fix just Cat and and write this?

abbreviation mor (A B : ob) : Type := rec (λ mor compose id assoc idr idl, mor A B) Cat

It seems much clearer than calling A and B "parameters" and then using them as ordinary variables within the section.

In your formalization of the natural numbers, most of your theorems begin

theorem foo (m n k : nat) ....

Would you really want to make m n and k "parameters" here too? It seems confusing. If, within the section, the theorem depends on arbitrary m, n, k, I feel like it is best to just state it that way.

I suppose the alternative is to have, as you say, another type of "parameters" -- like "general variables". I am not strongly against it, but I think I would personally prefer not to use them.

[fpvandoorn]

I thought that was the point of parameters. If every theorem of a file starts with declaring the same kind of objects, like theorem foo (m n k : nat) .... then instead you can just declare them once at the start of your file. I was indeed using parameters as general variables.

It is not a big problem to not be able to do that, but I think it's convenient.

If we're only using parameters in the restricted sense then I don't see the use for the feature to not include them in every definition in that section (even if not mentioned). Because then the idea is that every object in that section depends on the parameters, right?

[avigad]

On reflection, maybe it is not such a bad idea. It still seems strange to me to have

theorem comm: m * n = n * m

but I can imagine that it would be convenient once I got used to it. One small downside is that the order of the arguments is fixed by the order of the parameters, which is far from the definition. But usually we could declare parameters like m, n, k or a, b, c.

Leo, what do you think? I could be convinced either way. We could call them "defaults", as in

defaults m n k : nat

or something like that.

[avigad]

... or we could use "parameters" for strong parameters and "variables" for weak parameters.

[leodemoura]

I like the idea of strong and weak parameters, and use parameters … (for strong) and variables … (for weak). I think Floris justification for them is very convincing, and will look good in the user manual. We would also be able to avoid the section including command proposed in issue #178.

The strong parameters are a must have for “class-instance” resolution. It allows us to conveniently set a local instance for a class inside of a section. This was the main motivation for the including command in issue #178.

It still seems strange to me to have theorem comm: m * n = n * m

It is up to the user whether she will use this style or not. BTW, the following one looks reasonable to me

  theorem and.elim : a ∧ b → (a → b → c) → c :=
  assume H₁ H₂, rec H₂ H₁

[fpvandoorn]

I agree that the names parameter(s) and variable(s) are good.

[avigad]

You have both convinced me that it is a nice feature.

Note that the distinction also makes sense at the top level, outside any section. The intuition is: variables are generalized immediately, parameters are generalized when the section is closed. At the top level, a parameter is just a constant, since it is never generalized.

If you don't implement it that way, then the user has to write

namespace nat

section

variables (m n k : nat)

theorem foo : ...

end

If you give variables the same behavior at the top level, the user can omit "section / end", though presumably m n k go out of scope at the end of the file.

I don't have a strong preference either way, but I thought I would mention this.

[leodemoura]

Additional details.

• We also have the alternative syntax hypothesis, conjecture and axiom for parameter/variable. I think all of them should be "strong" parameters. Do you agree?
• A "strong" parameter cannot depend on a "weak" one. The following sequence triggers an error

section
   variable n : nat
   parameter v : vec int n    <<< v depends on n

• The signature of a declaration is composed of all "strong" parameters (in the order they were declared, followed by all used weak parameters (in the order they were declared), followed by explicitly given parameters. Example

section
   parameter {A : Type}
   variable a : A
   parameter b : A
   variable c : A
   variable d : A
   definition foo (x : A) := x = a \/ x = c

produces

definition foo {A : Type} (b : A) (a : A) (c : A) : Prop := x = a \/ x = c

Moreover, after the declaration, the symbol foo is an alias for foo A b in the section.

• Notation declarations in sections can only contain implicit strong parameters.

[leodemoura]

@avigad Regarding top-level strong/weak parameters, I'm on the fence. I can see it is useful, but on the other hand I think it is nice to have a clear scope for strong/weak parameters. Otherwise, the scope is going to be the whole file. We can relax things a little bit, and allow namespaces to be "scope delimiters" for strong/weak parameters. That is, we would be able to avoid the section and write

namespace nat
  variables (m n k : nat)
  theorem foo : ...
  ...  
end nat

Another issue is that sometimes we really want to add the axiom to the environment, or assert that some type A is inhabited. For example, we assert

axiom prop_complete : forall (a : Prop) : a = true \/ a = false

at classical.lean. In the current version, we can also assert that some type A is inhabited using

variable a : A

in the top level. Remark: we never really used this feature. Since in the proposal above variable is for declaring a weak parameter, what should we use instead? parameter is also not good. The following alternative is also not ideal

axiom H : inhabited A

[avigad]

Regarding the additional details, they all seem right to me.

I had to think about the third one for a minute. If we wanted to keep the user's order (with variable a before parameter b), we would have to have foo an alias for (fun a, foo A a b). On the other hand, if the user were to write

definition foo (a : A) (x : A) := x = a \/ x = c

the parameters A b would come before a. So Leo's proposal seems more consistent with the intuition that "variables (a : A)" does the same thing as insert (a : A) after the definition.

Regarding variables at the top level: I am also on the fence. In answer to the last question, the natural declaration seems to me to be

constant a : A

for the strong parameter. Using variable there always seemed misleading to me. And axiom would be a strong parameter, so that would do the right thing, wouldn't it?

But it does feel awkward to me to have "variable (a b : A)" floating around at the top level without a scope. It is intuitive and reasonable to make the user create a section. For example, the idiom

section nat_variables

variables (m n k: nat)

end nat_variables

makes the scope crystal clear. So I suppose I am leaning towards only having the strong / weak distinction inside a section.

Using namespace nat as scope delimiters seems to confuse the namespace / section distinction in a way that is problematic. For example, the user may want to write

namespace foo

axiom bar : ...
constant baz : ...

end foo

to have axiom foo.bar and foo.baz as new constants, not to make them parameters.

Summary: I think it is best to have the strong / weak distinction only in a section.

[leodemoura]

I had to think about the third one for a minute. If we wanted to keep the user's order (with variable a before parameter b), we would have to have foo an alias for (fun a, foo A a b).

I also considered using lambdas, but there are issues with dependent types. For example:

section
   parameter A : Type
   variable n : nat
   parameter v : vec A n
   ...
end

We are "fixing" v, but its type "varies". So, v is not really fixed. That is, it breaks the idea that a strong parameter v is fixed in the section. Moreover, v would have to be something like: v : Pi n, vec A n, and the alias for

definition foo := ... v ...

would be

(fun n, foo A n (v n))

[leodemoura]

Summary: I think it is best to have the strong / weak distinction only in a section.

Great for me. BTW, I'm assuming the command variable(s) should only be allowed in section. That is, lean will generate an error if it is used in the top level.

Just to make sure that everyone is on the same page, here are the "rules"

• Strong/fixed parameters are defined using parameter, axiom, conjecture, hypothesis, constant. The variant parameter can only be used inside sections.
• Weak parameters are defined inside sections using variable.
• At the top level, the commands axiom, conjecture, hypothesis, constant are postulating that a type is inhabited, and can make the environment inconsistent.

[avigad]

Very good. So "variable" can only be used in a section, and I think it will be easy to explain to users. Variables come after parameters in the order of arguments, and are implicitly generalized right away.

I thought of another fiddly point. What if the user does

section one
  parameter a : nat
  variable b : nat

  section two
    parameters c : nat
    variable d : nat

    definition foo := a + b + c + d

  end two
end one

The real "foo" has to be foo (a c b d). Inside section two, "foo" is an alias for "foo a c". After section two closes, and we are back in section one, "foo" is an alias for "foo a".

I don't see any problem with this, but we have to make this clear to users: in a nested section, we have all the parameters in scope, and all the variables in scope, but all the parameters come before all the variables.

Anyhow, this seems like the right way to go. The story is straightforward, and the functionality is useful.

[fpvandoorn]

This looks good. I agree with these rules.

[leodemoura]

BTW, in the proposal above, we don't have a way to simulate Coq's behavior for parameters. In Coq, all parameters are strong, but only the used ones are included in a definition. Coq's behavior is closer to the current one.

[avigad]

Sorry, I was focusing on the issue of whether or not the argument is added to the alias ("generalize immediately" rather than "generalize when the section is closed"). I forgot about the other issue, "insert whether or not the parameter is used".

The two issues are really orthogonal. With respect to the second issue, for both parameters and variables, I find the Coq behavior more natural: only include the ones that are used. I think it would happen fairly often that someone would fix a number of parameters in a section, but not every theorem should use all of them.

I suppose, then, that would require an explicit "including" command to include the parameter in the context. I just looked at issue #178. I don't see an "including" in category.lean. Could you remind me what the issue is? Is it really that common that we will need a parameter in a context, even though it is not mentioned even implicitly in the theorem?

[leodemoura]

Could you remind me what the issue is? Is it really that common that we will need a parameter in a context, even though it is not mentioned even implicitly in the theorem?

We need this feature for the class-instance resolution. For example, we have

parameter myInstance : classA

and we want myInstance to be used whenever we need an element of type classA. Right now, there is no way to do it. We have to include myInstance as an explicit parameter of every declaration where we want this behavior.

If all strong parameters are included in declarations, then the problem is solved, but we cannot simulate the current (and Coq) behavior anymore: only used parameters are added. A possible fix is to add the including command.

[avigad]

I see.

I think there will be situations where it will be annoying to have every parameter included by default, but maybe the problem can be avoided by making these parameters into "variables". I am tired now and having a hard time coming up with examples where we don't want to use a variable (because we don't want to keep writing the parameter) but don't want to include the parameter in every instance.

For inspiration, I looked at a file in the SSreflect library:

http://ssr.msr-inria.inria.fr/~jenkins/annotated/fingroup.v

There are certainly sections with theorems where not every variables / hypothesis is used in every theorem, but I don't see that any serious harm would arise by making them "variables" in our sense.

By the way, notice all the instances of the "Implicit Types" command. I think that is the same as our "variables". I had forgotten about that feature in Coq.

[avigad]

Correction: "Implicit Types" is not like our "variables". You still have to list them as arguments to the function. You just don't have to indicate the types.

[leodemoura]

I think there will be situations where it will be annoying to have every parameter included by default, but maybe the problem can be avoided by making these parameters into "variables". I am tired now and having a hard time coming up with examples where we don't want to use a variable (because we don't want to keep writing the parameter) but don't want to include the parameter in every instance.

Perhaps we should have a command to say that some parameter should not be included by default. That is, by default, all parameters are added, but we can have a ondemand x command that says that x must be included only if it is explicitly referenced.

Correction: "Implicit Types" is not like our "variables". You still have to list them as arguments to the function. You just don't have to indicate the types.

PVS also has this feature. I think it is useful.

[fpvandoorn]

Jeremy and I just had a meeting and we talked about section parameters. Here is a summary.

There are basically two questions we need to answer for section parameters:

• When are they used? (only when mentioned in the theorem or always)
• When are they generalized? (immediately or when closing the section) (so inside the section, does foo mean foo A B or are A and B immediately generalized and does foo just mean foo)

There are four possible combinations, and it's hard to see in advance whether there is a combination we definitely don't need. So we should support them all.

We suggest the following:

• parameter foo1 declares a parameter which will be generalized at the end of the section
• variable foo2 declares a parameter which will be generalized immediately

Both will only be included when they are mentioned. If we want to change this, we can write including foo1 or including foo2, which means they will be always included in the following theorems/definitions. If we've written including foo and want to state theorems later in the section which do not use foo, then we can write omitting foo (which - if I understand correctly - is the same as the ondemand foo you suggested) to toggle the "always include"-behavior off for foo.

Jeremy made the argument that it's probably easier for the user to understand if both parameter and variable are not always included by default, and this only happens when you explicitly use the command including.

---

Aside: do "Implicit Types" add much when we already have variable? I can't think of a concrete situation where I want to do something with Implicit Types which is impossible with variables.

[leodemoura]

I think the latest proposal is easier to explain to users, and it covers all possible cases.

Aside: do "Implicit Types" add much when we already have variable?

Operationally, I think it does not add any real power, but some may claim it is good for documentation because the signature is easier to understand. For example,

theorem comm m n : m * n = n * m

makes it clear that the first argument is m and the second n. If we omit them, then the user has to recall the order the variables were declared in the section. It is not a big deal, but this is the rationale in PVS.

[avigad]

I like the proposal too. It seems clearer and more intuitive to separate concerns, and it offers maximum flexibility.

By the way, Floris convinced me that a user might even want to "include" variables by default. For example, suppose we use the partially unbundled type classes to define homomorphisms between a group G and a group H, and then go on to define composition of homomorphisms, involving another group K. We might do it like this:

section 
  variables (G H : Type)
  variable {groupG : GroupStruc G}
  variable {groupH : GroupStruc H}
  definition homomorphism (f : A -> B) := forall a1 a1 : A, f (a1 * a2) = f a1 * f a2
  ...

  section
    variable (K : Type)
    variable {groupK : GroupStruc H}
    theorem (f : A -> B) (g : B -> C) : homomorphism f -> homomorphism g -> homomorphism (g o f)
    ...
  end
end

We need the variables groupG, groupH, groupK in the context for type inference. But they should be variables, because we want to change the arguments to "homomorphism".

As Floris points out, if it turns out that users will more often want to include parameters, there is a slight downside that this is not the default behavior. But it is easy to write

  include groupG groupH

especially since we do not have to write the types, and it makes it crystal clear that groupG and groupH will be an argument to every theorem.

By the way, I suggest using

  include groupG groupH

and

  omit groupG groupH

to set the behavior. We can do

  theorem foo ... := including groupG ...

  theorem foo ... := omitting groupG ...

to change the behavior for a single theorem.