Zulip Chat Archive

Stream: general

Topic: Kinds of declarations


view this post on Zulip Patrick Massot (Dec 02 2019 at 19:19):

Still coming back to meta-code, I'd like to clean up leancrawler a bit, and maybe PR part of it to mathlib for general use. The very first step is to triage declaration by kind (I would say type but that would be very confusing). Can anyone comment on https://gist.github.com/PatrickMassot/64167b3fce4b3f07c556328c1ffa683b? Would mathlib be interested in that?

view this post on Zulip Floris van Doorn (Dec 02 2019 at 20:17):

I think that could be useful.
Some comments:

  • Theorems can be instances when you write @[instance] theorem ...
  • Definitions can be classes when you write @[class] def .... I believe this actually happens in mathlib.
  • This is the first time that I see the declaration environment.structure_fields. That is useful. There are some declarations in meta.expr that mimic this built-in declaration. I will PR a change that removes those.

view this post on Zulip Floris van Doorn (Dec 02 2019 at 20:20):

Also, if you want to golf the function a bit, you can write return $ if (env.is_projection n).is_some then Structure_field else Definition

view this post on Zulip Patrick Massot (Dec 02 2019 at 20:26):

Thanks a lot! New version:

meta def environment.get_kind (env : environment) : declaration  tactic declaration.kind
| (thm n _ _ _) := do (tactic.has_attribute `class n >> return Instance) <|> return Lemma
| (defn n _ _ _ _ _) := do
    (has_attribute `class n >> return Class) <|>
    (has_attribute `instance n >> return Instance) <|>
    return (if (env.is_projection n).is_some then Structure_field else Definition)
| (cnst n _ _ _) := do
    (has_attribute `class n >> return Class) <|>
    return (if (env.structure_fields n).is_some then Structure
              else if is_ginductive env n then Inductive else Constant)
| (ax _ _ _) := return Axiom

view this post on Zulip Patrick Massot (Dec 02 2019 at 20:26):

Is it better?

view this post on Zulip Floris van Doorn (Dec 02 2019 at 20:28):

Line 2: `class -> `instance

Suggestion: maybe first case on whether it has certain attributes, and only then case on the declaration-constructor (using declaration.is_theorem and friends from meta.expr)

view this post on Zulip Patrick Massot (Dec 02 2019 at 20:29):

oops

view this post on Zulip Patrick Massot (Dec 02 2019 at 20:30):

Do we have a nice way to do case analysis not based on constructors of inductive types?

view this post on Zulip Patrick Massot (Dec 02 2019 at 20:30):

Already in my version the nested if/then/else look ugly, for lack of elif.

view this post on Zulip Floris van Doorn (Dec 02 2019 at 20:35):

Not really...

view this post on Zulip Patrick Massot (Dec 02 2019 at 20:36):

I'll still try, so we'll be able to compare.

view this post on Zulip Floris van Doorn (Dec 02 2019 at 20:36):

You can still do a match d with ... in the middle of the expression.

view this post on Zulip Patrick Massot (Dec 02 2019 at 20:39):

How do you like

meta def environment.get_kind' (env : environment) (decl : declaration) : tactic declaration.kind :=
do
  let n := decl.to_name,
  (has_attribute `instance n >> return Instance) <|>
  (has_attribute `class n >> return Class) <|>
  return (
    if (env.structure_fields n).is_some then Structure else
    if (env.is_projection n).is_some then Structure_field else
    if is_ginductive env n then Inductive else
    if decl.is_definition then Definition else
    if decl.is_theorem then Lemma else
    if decl.is_constant then Constant else Axiom

view this post on Zulip Patrick Massot (Dec 02 2019 at 20:40):

Writing a proof that it's the same function (or not, I guess there is 50% change) would be a fun challenge.

view this post on Zulip Patrick Massot (Dec 02 2019 at 20:40):

I think it's more readable. I hope it's the same result.

view this post on Zulip Floris van Doorn (Dec 02 2019 at 21:13):

I think this definition looks good.
What are you going to use this data for though? The datastructure declaration.kind assumes that the classes are disjoint, which is not true.
In addition to the previous mentioned cases (classes can be either structures or definitions, instances can be theorems or definitions), there are also structure fields that are instances. You lose this "secondary" information. This is fine, but depends on the application.

view this post on Zulip Patrick Massot (Dec 02 2019 at 21:19):

A version of this was used to create the graph at https://leanprover-community.github.io/lean-perfectoid-spaces/

view this post on Zulip Patrick Massot (Dec 02 2019 at 21:19):

But ideally I'd like a general purpose version.

view this post on Zulip Patrick Massot (Dec 02 2019 at 21:20):

So I don't want to lose anything I could keep.

view this post on Zulip Patrick Massot (Dec 02 2019 at 21:20):

So I choose probably use a more elaborate type.

view this post on Zulip Floris van Doorn (Dec 02 2019 at 21:22):

If you don't want to lose information, you indeed want a more elaborate type. You could have a type with 4 constructors, corresponding to the constructors of declaration and then some boolean values whether it is a field/structure/class/instance.


Last updated: May 11 2021 at 02:05 UTC