Encapsulation in Lean

Stream: new members

[Dan Abramov]

What faculties does Lean provide for encapsulation?

In traditional software engineering, encapsulation is very important. How you do it precisely depends on the language and/or framework. But generally there’s some way to specify the boundaries of what’s an API and what’s an implementation detail, and to enforce those boundaries.

In Lean there’s a notion of API (lemmas related to definitions) but it feels more “by convention”. For example, you have to “learn” that unfolding is bad. Or that when you have an unfamiliar definition in the goal, you need to click into it and look for lemmas around it that seem like an API.

To some extent I think it’s nice that you can still “hack around it” even if the API is missing or not the best. But I’m wondering if there are first-class primitives I’m not aware of (existing or planned) that would make API a more first-class concept. For example I’d expect to have these abilities:

• Prevent a definition from being unfolded outside of the file it’s defined in.

• A way to find all lemmas that constitute a public API for a definition or a set of definitions. In other words, a way to bundle definitions with “their” lemmas. (Having to open the internals and scroll does not constitute such a way. I mean something more deterministic and intentional — for example, something VS Code would be able to enumerate based on a goal.)

Do these tools exist? If yes, are they common in Mathlib? Lean in the wild? Should their usage be promoted more?

[Kyle Miller]

Dan Abramov said:

Prevent a definition from being unfolded outside of the file it’s defined in.

People sometimes add the @[irreducible] attribute for this. You can add it after you've made the lemmas that characterize a definition.

It has some issues though: if you're not careful then those lemmas' types might now be type-incorrect, since they may have depended on unfolding.

Sebastian Ullrich has been hard at work at a better solution, that lets you do fine-grained exposure of internal definitions, while making sure everything is type correct in the public API. It's also work toward avoiding rebuilds of downstream files if all that changed is non-exposed details. https://lean-lang.org/doc/reference/latest/The-Module-System/

[Dan Abramov]

Ah, fantastic, I've seen glimpses here and there but wasn't sure if there's any writeup.

[Dan Abramov]

I wonder if this can also help "guessing" tactics like apply? to be more accurate

[Kyle Miller]

It's not clear to me yet to what extent the new module system will be embraced for mathematical definitions. It can be hard to predict which aspects are implementation details and which are fundamental structure that you need for some theory.

Still, there are plenty of definitions that are sort of arbitrary, where it'd be good to encourage not unfolding them.

There's also another independent concept, "universal properties". That's where you don't define the object directly, and instead you say what it means if you had such an object, with enough to say that such an object is essentially unique. Once you show such an object exists, you avoid working with that specific one. It prevents you from unfolding definitions since you're never talking about anything specific. This is the mathematician's version of API, and there's a certain beauty to it because you've eliminated arbitrariness too.

[Kyle Miller]

In case you'd find this interesting @Dan Abramov, here's an implementation of abstract product types using this universal property concept.

The idea is that one could in principle work with arbitrary types that can serve as the product (without mentioning Prod in the definition). It'd be really annoying though, since using Prod directly is very convenient!

There's also an unfinished exercise at the end to show that Kuratowski pairs can serve as a product type, and that β × α can serve as a product (why must the first element of a pair come first, right?). The Kuratowski example is meant to emphasize that whether or not you use Kuratowski pairs is an implementation detail.

import Mathlib.Tactic

universe u v

/--
Represents that `p` is an abstract type that can serve as `α × β`.

API:
- `IsProd.fst` and `IsProd.snd` are the component projections.
- `IsProd.canon` is the "canonical function", which is how you can create functions
  into the product.
- `IsProd.mkPair` is the constructor for the product type.
- `IsProd.unique` is the uniqueness property. Any type that serves as a product type `α × β`
  serves as well as any other one.

The `Prod.IsProd` definition demonstrates that products exist. It uses `Prod` as the product type.
-/
structure IsProd (α : Type u) (β : Type v) (p : Type (max u v)) where
  fst : p → α
  snd : p → β
  /-- Products are "terminal". Given any type `p'` with functions to `α` and `β`,
  then there's a function `f : p' → p` to the product. The values can then be
  obtained by applying the product's `fst` and `snd` functions. -/
  terminal : ∀ (p' : Type (max u v)) (fst' : p' → α) (snd' : p' → β),
    ∃! (f : p' → p), fst' = fst ∘ f ∧ snd' = snd ∘ f

protected def Prod.IsProd (α : Type u) (β : Type v) : IsProd α β (α × β) where
  fst := Prod.fst
  snd := Prod.snd
  terminal p' fst' snd' := by
    -- Implement the function `f` by constructing a pair with the results of applying
    -- `fst'` and `snd'`.
    use fun x => (fst' x, snd' x)
    refine ⟨⟨?_, ?_⟩, ?_⟩
    · rfl
    · rfl
    · rintro f' ⟨rfl, rfl⟩
      rfl

variable {α : Type u} {β : Type v}

/--
The canonical function into the product, given functions to each type.
```
        p'
     /  |  \
    /   |   \
   /    |can.\
  v     v     v
 α <--- p ---> β
    fst   snd
```
-/
noncomputable def IsProd.canon {p : Type (max u v)} (s : IsProd α β p)
    {p' : Type (max u v)} (fst' : p' → α) (snd' : p' → β) : p' → p :=
  (s.terminal p' fst' snd').choose

/--
The canonical function is unique. (Rephrased from `IsProd.terminal`.)
-/
theorem IsProd.canon_unique {p : Type (max u v)} (s : IsProd α β p)
    {p' : Type (max u v)} (fst' : p' → α) (snd' : p' → β)
    (f : p' → p) (hfst : fst' = s.fst ∘ f) (hsnd : snd' = s.snd ∘ f) :
    f = s.canon fst' snd' :=
  (s.terminal p' fst' snd').choose_spec.2 f ⟨hfst, hsnd⟩

/--
Composing with `fst` gives `fst'`. (Rephrased from `IsProd.terminal`.)
-/
@[simp] theorem IsProd.fst_comp_canon {p : Type (max u v)} (s : IsProd α β p)
    {p' : Type (max u v)} (fst' : p' → α) (snd' : p' → β) :
    s.fst ∘ s.canon fst' snd' = fst' :=
  (s.terminal p' fst' snd').choose_spec.1.1.symm

/--
Composing with `snd` gives `snd'`. (Rephrased from `IsProd.terminal`.)
-/
@[simp] theorem IsProd.snd_comp_canon {p : Type (max u v)} (s : IsProd α β p)
    {p' : Type (max u v)} (fst' : p' → α) (snd' : p' → β) :
    s.snd ∘ s.canon fst' snd' = snd' :=
  (s.terminal p' fst' snd').choose_spec.1.2.symm

@[simp] theorem IsProd.fst_canon_apply {p : Type (max u v)} (s : IsProd α β p)
    {p' : Type (max u v)} (fst' : p' → α) (snd' : p' → β) (x : p') :
    s.fst (s.canon fst' snd' x) = fst' x :=
  congr_fun (s.fst_comp_canon fst' snd') x

@[simp] theorem IsProd.snd_canon_apply {p : Type (max u v)} (s : IsProd α β p)
    {p' : Type (max u v)} (fst' : p' → α) (snd' : p' → β) (x : p') :
    s.snd (s.canon fst' snd' x) = snd' x :=
  congr_fun (s.snd_comp_canon fst' snd') x

/--
The canonical map `p → p` for a product's own projections is the identity function.
-/
@[simp] theorem IsProd.canon_self {p : Type (max u v)} (s : IsProd α β p) :
    s.canon s.fst s.snd = id :=
  (s.canon_unique s.fst s.snd id rfl rfl).symm

/--
Checking that the canonical function `p' → α × β` is indeed `fun x => (fst' x, snd' x)`.
-/
theorem Prod.IsProd.canon_apply (p' : Type (max u v)) (fst' : p' → α) (snd' : p' → β) (x : p') :
    (Prod.IsProd α β).canon fst' snd' x = (fst' x, snd' x) := by
  have := IsProd.canon_unique (Prod.IsProd α β) fst' snd' (fun x => (fst' x, snd' x)) rfl rfl
  rw [← this]

/--
Given two types `p` and `p'` that are products of `α` and `β`, there is a bijection between them.

Not proved here: the bijection preserves the `fst`/`snd` structure.
These are immediate consequences of `IsProd.fst_comp_canon` and `IsProd.snd_comp_canon`.
-/
@[simps]
noncomputable def IsProd.unique {α : Type u} {β : Type v} {p p' : Type (max u v)}
    (s : IsProd α β p) (s' : IsProd α β p') : p ≃ p' where
  toFun := s'.canon s.fst s.snd
  invFun := s.canon s'.fst s'.snd
  left_inv := by
    intro x
    -- This composition of canonical maps is `p → p`. Apply uniqueness.
    have := s.canon_unique _ _ (s.canon s'.fst s'.snd ∘ s'.canon s.fst s.snd) rfl rfl
    have := congr_fun this x
    rw [Function.comp_apply] at this
    rw [this]
    simp [← Function.comp_assoc]
  right_inv := by
    intro x
    -- This composition of canonical maps is `p' → p'`. Apply uniqueness.
    have := s'.canon_unique _ _ (s'.canon s.fst s.snd ∘ s.canon s'.fst s'.snd) rfl rfl
    have := congr_fun this x
    rw [Function.comp_apply] at this
    rw [this]
    simp [← Function.comp_assoc]

/--
Constructing pairs from values.
The constructor satisfies the correct lemmas: `IsProd.fst_mkPair` and `IsProd.snd_mkPair`.

This makes use of the native `Prod` type.
-/
noncomputable def IsProd.mkPair {p : Type (max u v)} (s : IsProd α β p) (x : α) (y : β) : p :=
  s.canon Prod.fst Prod.snd (x, y)

@[simp]
theorem IsProd.fst_mkPair {p : Type (max u v)} {s : IsProd α β p} {x : α} {y : β} :
    s.fst (s.mkPair x y) = x := by
  simp [IsProd.mkPair]

@[simp]
theorem IsProd.snd_mkPair {p : Type (max u v)} {s : IsProd α β p} {x : α} {y : β} :
    s.snd (s.mkPair x y) = y := by
  simp [IsProd.mkPair]

/-- Kuratowski pairs. -/
def KPair (α : Type u) : Type u :=
  { p : Set (Set α) // ∃ (x y : α), p = {{x}, {x, y}}}

/-- The Kuratowski pairs for `α` works as the type `α × α`. -/
noncomputable def KPair.IsProd (α : Type u) : IsProd α α (KPair α) where
  fst := sorry
  snd := sorry
  terminal := by
    sorry

/--
The reversed `Prod` also serves as a product.
-/
def Prod.IsProd' (α : Type u) (β : Type v) : IsProd α β (β × α) where
  fst := Prod.snd
  snd := Prod.fst
  terminal := by
    sorry

[Aaron Liu]

unfortunately you have to quantify over all types

[Aaron Liu]

there's probably a way there is a way to not do that and be more universe polymorphic

[Kyle Miller]

Prod.rec quantifies over all types too, so what's the issue?

Anyway, let's not derail this with whether or not this is universe polymorphic enough. It's meant to illustrate that there are design patterns in math that go beyond making definitions opaque.

[Aaron Liu]

Kyle Miller said:

Prod.rec quantifies over all types too, so what's the issue?

The problem is that IsProd.terminal takes p' : Type (max u v) instead of p' : Type w (and you can't solve this by making IsProd take an extra parameter w)

[Aaron Liu]

Kyle Miller said:

Anyway, let's not derail this with whether or not this is universe polymorphic enough. It's meant to illustrate that there are design patterns in math that go beyond making definitions opaque.

of course but this is a problem with lots of universal properties

[Kyle Miller]

Yes, I'm aware that it has limitations. Let's consider the fact that Dan is probably not super interested in the finer details of universe polymorphism here.

I considered putting it all in Type just to avoid the extra complication and potential discussion.