Is a namespace a type?

Stream: new members

[Lars Ericson]

Regarding this:

namespace quot
variable {β : quot r → Sort v}

It appears that a namespace defines a class. Is that correct?

[Eric Wieser]

No, it just shares a name with a type

[Kevin Buzzard]

You can read about namespaces in #tpil, a book which you are probably now in a position to get to the end of. Your code doesn't run for me. quot is already a thing in core Lean -- is this what is confusing you?

[Eric Wieser]

docs#quot should be the definition

[Eric Wieser]

Huh, I was expecting a meta constant or something

[Kevin Buzzard]

go to definition also fails in VS Code

[Reid Barton]

quot and its associated constants are magically declared to exist by the kernel

[Reid Barton]

there's some command which triggers their construction which I forget

[Kevin Buzzard]

init_quotient in core.lean

[Kevin Buzzard]

/-
Initialize the quotient module, which effectively adds the following definitions:

constant quot {α : Sort u} (r : α → α → Prop) : Sort u

constant quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : quot r

constant quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
  (∀ a b : α, r a b → eq (f a) (f b)) → quot r → β

constant quot.ind {α : Sort u} {r : α → α → Prop} {β : quot r → Prop} :
  (∀ a : α, β (quot.mk r a)) → ∀ q : quot r, β q

Also the reduction rule:

quot.lift f _ (quot.mk a) ~~> f a

-/
init_quotient

[Adam Topaz]

Will quot still be magic in lean4?

[Chris B]

Yes. https://github.com/leanprover/lean4/blob/3682e3b9938a3dd0b3c64ce72f7fd9f3fe5118fb/src/kernel/quot.cpp#L47

[Kevin Buzzard]

prelude

init_quotient

gives the rather tasty error message

failed to initialize quot module, environment does not have 'eq' type

One could maybe redefine eq and prove false somehow?

prelude

universe u

def Prop := Sort 0

inductive false : Prop

def eq : Π {α : Sort u}, α → α → Prop := λ α a b, false
/-
equation compiler failed to create auxiliary declaration 'eq.equations._eqn_1'
nested exception message:
unknown declaration 'eq.refl'
-/

kind of annoying. I'm not sure what the rules are in prelude

[Reid Barton]

I wonder why it wanted to use the equation compiler

[Reid Barton]

What if you just make an inductive type like eq but empty

[Eric Wieser]

Found this nice error message while trying that:

https://github.com/leanprover-community/lean/blob/ec1613aef1eee72e601f192b16740629c6d49690/src/kernel/quotient/quotient.cpp#L63

[Eric Wieser]

Looks like it was meant to say "unexpected" not "expected"?

[Reid Barton]

nope, Lean is just onto you and your tricky ways

[Eric Wieser]

Actually def Prop breaks it

[Eric Wieser]

It requires it to be notation

[Eric Wieser]

But yes, check_eq_type looks fairly robust

[Lars Ericson]

Thanks for the clarification. So:

static environment init_quotient_cmd(parser & p) {
    return module::declare_quotient(p.env());
}

or in other words :

namespace hidden
universes u v
constant quot : Π {α : Sort u}, (α → α → Prop) → Sort u
end hidden

[Lars Ericson]

The application was that I was trying to trace out the types involved in a couple of representations of the set {0,1,2}, and quot came up as a blank spot, but that's OK. Here is the picture I came up with:
Screenshot-from-2020-12-11-15-32-05.png

[Eric Wieser]

Lars, if you like dependency graphs about lean, you might find https://observablehq.com/@eric-wieser/lean-ga-imports interesting

[Chris B]

@Lars Ericson

It also adds quot.mk, quot.lift, and quot.ind. They get assembled 'by hand' and then added to the environment without any checks as soon as the eq inductive has been admitted. If you print an export file from Lean 3, it will be a couple of name declarations, an #IND for eq, and then just #QUOT which tells the verifier to add the quotient stuff to the environment.

This file has comments with lean annotations showing what's actually being put together.
https://github.com/ammkrn/nanoda_lib/blob/master/src/quot.rs

[Lars Ericson]

@Eric Wieser that's really great visualization, thanks.