Scope of section variables

Stream: general

[Bodo Igler]

Is there a way to influence the scope of section variables?

Example:

section Example
  variable (a : ℕ)
  def p := a = a

  theorem t1: p a := by
    unfold p
    rfl

  theorem t1_fail: p := by
    unfold p
    rfl
end Example

Objective: I would like to use p within the scope of this section without having to explicitly bind pwith a, i.e. keep this dependency implicitly bound within all of the section. This objective is demonstrated in theorem t1_fail.

However, Lean reports a type error on the occurence of p in theorem t1_fail:

type expected, got  (p : ?m.44 → Prop)

I understand that p depends - as expected - on a variable of type \N, but I would like it to be dependent on the section variable a. (This is the way that section variables work in e.g. Coq.)

Is there any way to achieve this in Lean?

[Damiano Testa]

This is mostly irrelevant to your question, but ℕ in your code is an arbitrary TypeSort, not the natural numbers.

[Damiano Testa]

I do not have any knowledge of Coq, so I cannot really comment on the actual question that you are asking.

[Kyle Miller]

Lean 3 used to have a feature called "section parameters" which seem to be what you would want, but Lean 4 only has section variables. It's only for saving needing to duplicate argument lists in declarations.

[Daniel Weber]

There is local notation, which lets you use variables like that, but I'm not sure if it's exactly what you want:

section Example
  variable (a : ℕ)
  local notation "p" => a = a

  theorem t1_not_fail: p := by
    rfl

  #check t1_not_fail
end Example

[Bodo Igler]

Thank you very much for your quick and helpful responses. I gather that there is no direct way to achieve "Coq-style section variables", but that you can use local notations to achieve a similar effect.

The local notation approach seems to have one drawback: It omits identifier information. This is neither obvious from nor relevant to my above example. However, this consequence gets relevant, if the identifier is necessary for e.g. recognizing a given function by name (and not by its function body).

The only way that comes to my mind to save the identifier information is a variation on the local notation approach, e.g.:

namespace Example
  variable (a : Nat)
  def p := a = a
end Example

variable (x : Nat)
macro "p" : term => `(@Example.p x)

theorem t1 : p := by
  unfold Example.p
  rfl

Now, whenever p is used,

• the variable p is bound to a given variable
• the identifier information remains.

Unfortunately, you have to know that p actually has two names: p and Example.p.

[Kyle Miller]

Do you have an application of this? Perhaps if you shared it in more detail, there'd be something that's more Lean-idiomatic.

[Bodo Igler]

Yes, there is. I will create a minimal example and post it here.

[Bodo Igler]

What I would actually like to do is to partition specifications/theories into several self-contained modules with "clean" interfaces between them, like e.g. a (simplified) theory of sets (-> module1) and a module that adds some predicates, propositions and proofs to it (-> module2):

Example1 "cluttered"

class module1 (α : Type) :=
  equal: α → α → Prop
  subset: α → α → Prop
  isect: α → α → α
  union: α → α → α
  equal_ext (a b : α):
    (∀ (x : α), (subset x a) ↔ (subset x b)) ↔ (equal a b)
  union_comm (a b : α): equal (union a b) (union b a)
  isect_comm (a b : α): equal (isect a b) (isect b a)

infixl:63 " ≡ " => module1.equal
infixl:64 " ⊂ " => module1.subset
infixl:65 " ∪ " => module1.union
infixl:65 " ∩ " => module1.isect

section module2
  variable (T : Type) [module1 T]
  variable (a b : T)

  def equal_to_a (x : T) : Prop := a ≡ x
  def equal_to_b (x : T) : Prop := b ≡ x

  def subset_of_both (x y z : T) := x ⊂ y ↔ x ⊂ z
-- this definition fails
  def subset_iff_equal' := (∀ (x : T), equal_to_a x ↔ equal_to_b x) ↔
    (∀ (x : T), subset_of_both x a b)
-- this definition typechecks
  def subset_iff_equal := (∀ (x : T), equal_to_a T a x ↔ equal_to_b T b x) ↔
    (∀ (x : T), subset_of_both T x a b)
-- this fails
  theorem t1' : subset_iff_equal := by sorry
-- this typechecks
  theorem t1 : subset_iff_equal T a b := by sorry
end module2

#check t1
-- t1 (T : Type) [module1 T] (a b : T) : subset_iff_equal T a b

#print subset_iff_equal
-- def subset_iff_equal : (T : Type) → [inst : module1 T] → T → T → Prop :=
-- fun T [module1 T] a b ↦ (∀ (x : T), equal_to_a T a x ↔ equal_to_b T b x) ↔ ∀ (x : T), subset_of_both T x a b

(This example is not supposed to be particularly meaningful in itself, i.e. w.r.t. proposition on sets. It is just supposed to illustrate the idea of structuring a theory in this way.)

The expressions that the type checker accepts get, in my opinion, quite cluttered with details that could in principle be inferred from the context. (Implicit variables {a b : Type} do not solve this problem.)

Applying local notation gets rid of the clutter:

Example 2: local notations

class module1 (α : Type) :=
  equal: α → α → Prop
  subset: α → α → Prop
  isect: α → α → α
  union: α → α → α
  equal_ext (a b : α):
    (∀ (x : α), (subset x a) ↔ (subset x b)) ↔ (equal a b)
  union_comm (a b : α): equal (union a b) (union b a)
  isect_comm (a b : α): equal (isect a b) (isect b a)

infixl:63 " ≡ " => module1.equal
infixl:64 " ⊂ " => module1.subset
infixl:65 " ∪ " => module1.union
infixl:65 " ∩ " => module1.isect

section module2
  variable (T : Type) [module1 T]
  variable (a b : T)

  local notation "equal_to_a" "(" x ")" => a ≡ x
  local notation "equal_to_b" "(" x ")" => a ≡ x

  local notation "subset_of_both" "(" x "," y "," z ")" => x ⊂ y ↔ x ⊂ z

  local notation "subset_iff_equal" =>
    (∀ (x : T), equal_to_a ( x ) ↔ equal_to_b ( x )) ↔
-- no macro or `[quot_precheck]` instance for syntax kind 'Lean.Parser.Term.forall' found
--  ∀ (x : T), equal_to_a(x) ↔ equal_to_b(x)
    (∀ (x : T), subset_of_both (x, a, b))

  theorem t1 : subset_iff_equal := by sorry
end module2

#check t1 -- unknown identifier 't1'
#print subset_iff_equal -- unknown constant 'subset_iff_equal'

However, this approach adds new problems:

1. the parameters of the notation cannot be type-checked
2. this gives errors, when applying the notation with e.g. ∀
3. the notations cannot be used outside the section
4. "normal" (non-local) notations cannot be used as they would point to variables that only live inside the section

Another approach could be to specifiy module2 with a typeclass, too:

Example 3: typeclass

class module1 (α : Type) :=
  equal: α → α → Prop
  subset: α → α → Prop
  isect: α → α → α
  union: α → α → α
  equal_ext (a b : α):
    (∀ (x : α), (subset x a) ↔ (subset x b)) ↔ (equal a b)
  union_comm (a b : α): equal (union a b) (union b a)
  isect_comm (a b : α): equal (isect a b) (isect b a)

infixl:63 " ≡ " => module1.equal
infixl:64 " ⊂ " => module1.subset
infixl:65 " ∪ " => module1.union
infixl:65 " ∩ " => module1.isect

class module2 (T : Type) [module1 T] :=
  a : T
  b : T
  equal_to_a (x : T) := a ≡ x
  equal_to_b (x : T) := b ≡ x
  subset_of_both (x y z : T) := x ⊂ y ↔ x ⊂ z
  subset_iff_equal :=
    (∀ (x : T), equal_to_a x ↔ equal_to_b x) ↔
    (∀ (x : T), subset_of_both x a b)

variable (T : Type) [module1 T] [module2 T]
theorem t1 : @module2.subset_iff_equal T _ _ := by
-- 1 goal
-- T : Type
-- inst✝¹ : module1 T
-- inst✝ : module2 T
-- ⊢ module2.subset_iff_equal T
  unfold module2.subset_iff_equal
-- 1 goal
-- T : Type
-- inst✝¹ : module1 T
-- inst✝ : module2 T
-- ⊢ inst✝.6
  sorry

#check t1 -- t1 (T : Type) [module1 T] [module2 T] : module2.subset_iff_equal T
#print module2.subset_iff_equal
-- def module2.subset_iff_equal : (T : Type) → [inst : module1 T] → [self : module2 T] → Prop :=
-- fun T [module1 T] [self : module2 T] ↦ self.6

This solves some of the above problems but seems to make it at least difficult to use some of the typeclass elements. It is for instance difficult to unfold module2.subset_iff_equal.

Probably, as Kyle pointed out, there is a "Lean way" of partitioning a theory/specification in a way similar to these examples. I would be grateful for any hints. :smile:

[Bodo Igler]

The best way I could come up with uses a container (structure or class) for the interdependent variables. This gives you one "handle" to access the complete set of variables.

The "variable container" in the following example is module2.vars. The variables and preds of module2 are then used in module3. As module2.vars is a type class, each time a variable (e.g. a) from module2.varsis used, only one parameter - the corresponding type class parameter (here: T) - has to be provided. This can be made a bit more convenient by using local notations.

class module1 (α : Type) :=
  equal: α → α → Prop
  subset: α → α → Prop
  isect: α → α → α
  union: α → α → α
  equal_ext (a b : α):
    (∀ (x : α), (subset x a) ↔ (subset x b)) ↔ (equal a b)
  union_comm (a b : α): equal (union a b) (union b a)
  isect_comm (a b : α): equal (isect a b) (isect b a)

infixl:63 " ≡ " => module1.equal
infixl:64 " ⊂ " => module1.subset
infixl:65 " ∪ " => module1.union
infixl:65 " ∩ " => module1.isect

namespace module2
  class vars (T : Type) [module1 T] where
    a : T
    b : T

  namespace preds
    variable (T : Type) [module1 T] [vars T]
    local notation "a" => @vars.a T _ _
    local notation "b" => @vars.b T _ _
    def equal_to_a (x : T) : Prop := a ≡ x
    def equal_to_b (x : T) : Prop := b ≡ x
    def subset_of_both (x y z : T) := x ⊂ y ↔ x ⊂ z
  end preds
end module2

namespace module3
  variable (T : Type) [module1 T] [module2.vars T]

  local notation "a" => @module2.vars.a T _ _
  local notation "b" => @module2.vars.b T _ _
  local notation "equal_to_a" => @module2.preds.equal_to_a T _
  local notation "equal_to_b" => @module2.preds.equal_to_b T _
  local notation "subset_of_both" => @module2.preds.subset_of_both T _

  namespace preds
    def subset_iff_equal := (∀ (x : T), equal_to_a x ↔ equal_to_b x) ↔
      (∀ (x : T), subset_of_both x a b)
  end preds

  local notation "subset_iff_equal" => @preds.subset_iff_equal T _ _
  theorem t1 : subset_iff_equal := by
    unfold  preds.subset_iff_equal
            module2.preds.equal_to_a
            module2.preds.equal_to_b
            module2.preds.subset_of_both
    sorry
end module3

#check module3.t1
-- module3.t1 (T : Type) [module1 T] [module2.vars T] :
--    module3.preds.subset_iff_equal T

#print module3.preds.subset_iff_equal
-- def module3.preds.subset_iff_equal : (T : Type) → [inst : module1 T] → [inst : module2.vars T] → Prop :=
-- fun T [module1 T] [module2.vars T] ↦
--   (∀ (x : T), module2.preds.equal_to_a T x ↔ module2.preds.equal_to_b T x) ↔
--     ∀ (x : T), module2.preds.subset_of_both T x module2.vars.a module2.vars.b

Is there any way to make this more convenient and/or more Lean-idiomatic?

[Kyle Miller]

It seems that you don't need to use local notation here. One feature you can use to make it convenient is open/export. For example, in the following I can open vars and get access to a and b. It uses the expected type to resolve what these are supposed to mean. In subset_iff_equal it gets an expected type from the other side of the ≡, but in general you could write (a : T) and (b : T) to say which a and b these are.

Note that in subset_iff_equal I added some parentheses since I was having some parsing trouble (perhaps because I have import Mathlib and it's conflicting with the ModEq notation).

class module1 (α : Type) :=
  equal: α → α → Prop
  subset: α → α → Prop
  isect: α → α → α
  union: α → α → α
  equal_ext (a b : α):
    (∀ (x : α), (subset x a) ↔ (subset x b)) ↔ (equal a b)
  union_comm (a b : α): equal (union a b) (union b a)
  isect_comm (a b : α): equal (isect a b) (isect b a)

infixl:63 " ≡ " => module1.equal
infixl:64 " ⊂ " => module1.subset
infixl:65 " ∪ " => module1.union
infixl:65 " ∩ " => module1.isect

namespace module2
  class vars (T : Type) [module1 T] where
    a : T
    b : T

  namespace preds
    variable {T : Type} [module1 T] [vars T]
    def subset_of_both (x y z : T) := x ⊂ y ↔ x ⊂ z
  end preds
end module2

namespace module3
  variable (T : Type) [module1 T] [module2.vars T]

  open module2.vars

  namespace preds
    def subset_iff_equal := (∀ (x : T), (a ≡ x) ↔ (b ≡ x)) ↔
      (∀ (x : T), module2.preds.subset_of_both x a b)
  end preds

  theorem t1 : preds.subset_iff_equal T := by
    unfold preds.subset_iff_equal
           module2.preds.subset_of_both
    sorry
end module3

[Kyle Miller]

I didn't see what the purpose of equal_to_a/equal_to_b were, so I deleted them. Instead of equal_to_a x you can just as well write a ≡ x.

[Bodo Igler]

In the end, we decided to use typeclasses and namespaces to mimick the desired module concept. If this is of interest, I could give a minimal example to explain our approach.