RFC: command names

[leodemoura]

It is quite unfortunate that print, exit and eval cannot be used as identifiers because they are commands.
Moreover, they are "temporary/transient" commands that we only use while we are developing a library/project. I think we should rename them to:

1- #print
2- #exit
3- #eval (for the current vm_eval)
4- #reduce (for the current eval)
5- #run (short for run_command) Should we keep run_command?
6- #help

We also replace the following command with meta functions we execute using #run.
1- init_quotient becomes #run quot.init
2- declare_trace id becomes #run trace.declare id
3- add_key_equivalence id1 id2 becomes #run keyed_matching.add_equiv id1 id2

It would also be nice to remove command aliases that nobody uses:
1- definition (alias for def)
2- proposition (alias for theorem)
3- corollary (alias for theorem)
4- conjecture (alias for parameter)
5- record (alias for structure)

AFAIK, the following ones are used
1- lemma (alias for theorem)
2- premise (alias for variable)
3- hypothesis (alias for parameter)

[johoelzl]

+1

I also would remove hypothesis and premise. They are only used one or two times in lean/library and library_dev.

What about check and set_option? Has check another purpose than inspecting a type?

[leodemoura]

I also would remove hypothesis and premise.

I would be happy to remove them too :)

What about check and set_option? Has check another purpose than inspecting a type?

Good point! check is a "transient command" used for "debugging". We should use #check.
set_option is also rarely used when we are done with a module, and we could shorten it to #set.

[avigad]

I like these changes. I think distinguishing the transient commands is good. Alternative names are sometimes nice but often confusing.

I often use premise when teaching, but I can give it up.

We also use axiom as a syntactic equivalent for constant, which also gives the illusion that there is a difference between the two. Should we drop that? Would it then be strange to say print axioms foo to see the constants?

I'd even be willing to give up lemma. It is usually misused in our library to denote propositions, i.e. small straightforward facts, rather than things that are specifically stated to prove a theorem. If everything was theorem we would never have to think about which to use.

[leodemoura]

We also use axiom as a syntactic equivalent for constant, which also gives the illusion that there is a difference between the two

Yes, there is no difference between constant and axiom.

Should we drop that? Would it then be strange to say print axioms foo to see the constants?

I don't know. It is also weird that the current print axioms prints constant declarations.

I'd even be willing to give up lemma. It is usually misused in our library to denote propositions, i.e. small straightforward facts, rather than things that are specifically stated to prove a theorem. If everything was theorem we would never have to think about which to use.

I like to use lemma because it is shorter, but I'm also willing to give it up.

So, we would have only

• constant(s)
• def
• theorem
• variable(s)
• parameter(s)
• structure
• inductive
• class
• instance

theorem is needed because it affects how the definition is compiled.

[avigad]

We also have example.

In analogy to def, we could abbreviate theorem to thm. Of course, that would encourage us to abbreviate the others (const, var, param), but I like the longer names for those. The rationale is that there are many more theorems.

Still, theorem looks nicer, and I think my slight preference is to keep it like that. (But I could be talked out of it.)

[leodemoura]

We also have example.

Yes, I forgot to list it.
It is very useful, and we should keep it.

In analogy to def, we could abbreviate theorem to thm

I considered thm too, but I also think theorem looks nicer.

[spl]

I think it's a good idea to reduce the number of keywords in general. At first, the synonymous keywords (theorem/lemma, variable/premise, etc.) appear to be useful in documenting something, but later, it seems that they just add clutter and fill my head with more things that I'm forced to remember.

[Kha]

#run isn't exactly a transient command, is it? I would argue it is central enough that even just run would be defensible.

Somewhat related, I'd love it if transient commands could be used inside of (tactic) proofs.

[leodemoura]

#run isn't exactly a transient command, is it? I would argue it is central enough that even just run would be defensible.

You are right. #run is not transient. I agree it is a good idea to have the run keyword.

Somewhat related, I'd love it if transient commands could be used inside of (tactic) proofs.

After this change, we will be able to implement tactic.check, tactic.reduce, etc, and write

begin 
   ...
    check t,
    reduce t,
    eval t,
    ...
end

[leodemoura]

@Kha @jroesch I did not rename run_command to run because @jroesch uses run to name a constructor in the native compiler. In the commit above, I'm using run_cmd instead. What do you think? Should we use run or not?

[leodemoura]

I have already made of the changes discussed above.
Here is what is missing:

1- init_quotient becomes #run quot.init
2- declare_trace id becomes #run trace.declare id
3- add_key_equivalence id1 id2 becomes #run keyed_matching.add_equiv id1 id2

We still have

definition
lemma
axiom

[johoelzl]

Wrt axiom I would prefer to keep axiom and remove constant. What do you think?

[robertylewis]

@johoelzl Is there a particular reason you want to remove constant? I'd be inclined to keep both. We declare many, many meta constants that would be strange to call meta axioms. There's a useful psychological difference between the two, even if there's no difference in implementation. And if we have both def and theorem, it's analogous to have both constant and axiom. (I know def and theorem behave differently.)

I'm also slightly inclined to keep lemma, even if it's used "incorrectly" for small theorems. It doesn't seem likely that you'd want to use it as an identifier elsewhere.

[johoelzl]

@rlewis1988 meta constant makes sense, but constant sounds too innocent for a command which can introduce inconsistencies.