Zulip Chat Archive

Stream: new members

Topic: Is a namespace a type?


view this post on Zulip Lars Ericson (Dec 11 2020 at 16:49):

Regarding this:

namespace quot
variable {β : quot r  Sort v}

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

view this post on Zulip Eric Wieser (Dec 11 2020 at 16:50):

No, it just shares a name with a type

view this post on Zulip Kevin Buzzard (Dec 11 2020 at 16:51):

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?

view this post on Zulip Eric Wieser (Dec 11 2020 at 16:51):

docs#quot should be the definition

view this post on Zulip Eric Wieser (Dec 11 2020 at 16:52):

Huh, I was expecting a meta constant or something

view this post on Zulip Kevin Buzzard (Dec 11 2020 at 16:55):

go to definition also fails in VS Code

view this post on Zulip Reid Barton (Dec 11 2020 at 16:57):

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

view this post on Zulip Reid Barton (Dec 11 2020 at 16:57):

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

view this post on Zulip Kevin Buzzard (Dec 11 2020 at 16:57):

init_quotient in core.lean

view this post on Zulip Kevin Buzzard (Dec 11 2020 at 16:58):

/-
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

view this post on Zulip Adam Topaz (Dec 11 2020 at 16:59):

Will quot still be magic in lean4?

view this post on Zulip Chris B (Dec 11 2020 at 17:02):

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

view this post on Zulip Kevin Buzzard (Dec 11 2020 at 17:10):

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

view this post on Zulip Reid Barton (Dec 11 2020 at 17:13):

I wonder why it wanted to use the equation compiler

view this post on Zulip Reid Barton (Dec 11 2020 at 17:13):

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

view this post on Zulip Eric Wieser (Dec 11 2020 at 17:24):

Found this nice error message while trying that:

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

view this post on Zulip Eric Wieser (Dec 11 2020 at 17:24):

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

view this post on Zulip Reid Barton (Dec 11 2020 at 17:25):

nope, Lean is just onto you and your tricky ways

view this post on Zulip Eric Wieser (Dec 11 2020 at 17:26):

Actually def Prop breaks it

view this post on Zulip Eric Wieser (Dec 11 2020 at 17:26):

It requires it to be notation

view this post on Zulip Eric Wieser (Dec 11 2020 at 17:27):

But yes, check_eq_type looks fairly robust

view this post on Zulip Lars Ericson (Dec 11 2020 at 17:59):

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

view this post on Zulip Lars Ericson (Dec 11 2020 at 20:33):

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

view this post on Zulip Eric Wieser (Dec 11 2020 at 20:39):

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

view this post on Zulip Chris B (Dec 11 2020 at 23:29):

@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

view this post on Zulip Lars Ericson (Dec 11 2020 at 23:46):

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


Last updated: May 15 2021 at 02:11 UTC