Accessing/making use of automatic variables

Stream: lean4

[Robert Maxton]

Just started playing with Lean 4, with some but not much experience with Lean 3. I notice that the new proof environment automatically makes a number of variable definitions for things like instances or implicits; I also notice that the variable names aren't actually valid tokens, so they can't be invoked. I can generally define my own copy, but then I have my own copy of, say, the typeclass instance for a Category, and the compiler needs me to prove something with reference to its own, automatically generated instance.

[Robert Maxton]

I assume I'm doing something wrong, but what?

[Robert Maxton]

Concrete example: I'm implementing bits of CategoryTheory for practice.

import Mathlib.CategoryTheory.Category.Init
import Mathlib.Combinatorics.Quiver.Basic
import Mathlib.Tactic.PPWithUniv
import Mathlib.Tactic.Common


universe v u

namespace CategoryTheory

--Base scaffolding is copypasta'd from mathlib

  @[pp_with_univ]
  class CategoryStruct (obj : Type u) extends Quiver.{v + 1} obj : Type max u (v + 1) where
    /--Axiom: Identity-/
    id: ∀ X: obj, X ⟶ X
    /--Axiom: Composition of morphisms, written f ≫ g-/
    comp: ∀ {X Y Z: obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)

  initialize_simps_projections CategoryStruct (-toQuiver_Hom)

  /--Notation-/
  scoped notation "𝟙" => CategoryStruct.id
  scoped infixr:80 " ≫ " => CategoryStruct.comp

  @[pp_with_univ]
  class Category (obj : Type u) extends CategoryStruct.{v} obj : Type (max u (v + 1)) where
    id_comp : ∀ {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f
    comp_id : ∀ {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f
    assoc : ∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ (g ≫ h)

  initialize_simps_projections Category (-toCategoryStruct)

  attribute [simp] Category.id_comp Category.comp_id Category.assoc
  attribute [trans] CategoryStruct.comp

  abbrev LargeCategory (C : Type (u + 1)) : Type (u + 1) := Category.{u} C
  abbrev SmallCategory (C : Type u) : Type (u + 1) := Category.{u} C

  section

  instance UnitCategoryStruct (α: Type u) [Unique α]: CategoryStruct α where
    Hom := λ _ _ ↦ {f: α → α // f = id}
    id := λ _ ↦ ⟨id, rfl⟩
    comp := λ _ _ ↦ ⟨id, rfl⟩

  instance UnitCategory (α: Type u) [Unique α]: Category α := { UnitCategoryStruct α with
    id_comp := λ {X Y} (f: X ⟶ Y) ↦ by
      have h : X = Y := by rw [Unique.eq_default X]; exact Unique.default_eq Y
      subst h
      have h : f = 𝟙 X := by ...

[Robert Maxton]

At the end of that instance-in-progress, Lean reports a state that contains the variable src✝: CategoryStruct.{u, u} α := UnitCategoryStruct α. I need to prove id_comp with reference to src✝'s definition of Hom X Y; but I don't know how to access that definition, so I'm stuck. I could define my own src: CategoryStruct.{u, u} α := UnitCategoryStruct α, but proving id_comp against src.Hom does not prove id_comp against src✝.Hom.

[Robert Maxton]

(I ended up solving this specific problem by realizing that there was a good reason the mathlib definition does the proof of the composition lemmas as defaults in the original Category definition and bypassing the problem entirely that way; but I'd still like to have an answer here in case it comes up again. Unless that is the standard fix?)

[James Gallicchio]

Generally, you should name any variables that you need to refer to. This is part of Lean's macro hygiene features; if you didn't explicitly give it a name, you shouldn't be accessing it by name later on, since that would make your proofs break if the autogenerated names ever changed in the future.

Most tactics that introduce hypotheses have a way to name hypotheses, e.g. case takes a list of hypothesis names. You can also use the next a b c => tactic to name the most recent inaccessible hypotheses (in this case giving them names a, b, c in that order). You can also use the rename tactic to "look up" an inaccessible value by its type and rename it.

[Robert Maxton]

Most tactics that introduce hypotheses have a way to name hypotheses, e.g. case takes a list of hypothesis names.

You say that, but if Foo is a structure with multiple fields, cases foo with | h gives me a red squiggle under h with the error invalid aIternative name 'h' (sic) no matter what I use for h; presumably there's a way of providing a list of a name for each field but it's not clear how?

[Robert Maxton]

Ah, I see. mk to match the constructor case, and then names for the variables. Still doesn't let me access inherited fields, though...

[Timo Carlin-Burns]

This isn't exactly your question, but the standard way to add an instance for a new class that extends a class you already added an instance for is with where. This way there will only be one instance of UnitCategoryStruct in scope, the one registered in the previous declaration.

instance UnitCategory (α: Type u) [Unique α]: Category α where
  id_comp := λ {X Y} (f: X ⟶ Y) ↦ by
    have h : X = Y := by rw [Unique.eq_default X]; exact Unique.default_eq Y
    subst h
    have h : f = 𝟙 X := by sorry
    sorry
  comp_id := sorry
  assoc := sorry

[James Gallicchio]

Robert Maxton said:

presumably there's a way of providing a list of a name for each field but it's not clear how?

for structures you can use lots of different syntaxes in a tactic block:

• match myVal with | {field1, field2} => ... (whitespace sensitive)
• let {field1, field2} := myVal
• rcases myVal with \< field1, field2 \>
• cases myVal; case mk field 1 field2 => ...

[James Gallicchio]

you might wonder why so many different notations for the same thing, but they all have their place...