Zulip Chat Archive

Stream: general

Topic: lemma declaration without type ascription?

Junyan Xu (Dec 24 2022 at 05:14):

Is there a way to (and should we) make declarations a and b work? (Lean 3)

theorem a := trivial
don't know how to synthesize placeholder
⊢ Sort ?
lemma b := trivial /- same as above -/
def c := trivial /- works -/
example := trivial /- works -/

Junyan Xu (Dec 24 2022 at 05:32):

The motivation is to extract equivalences between two propositions from a TFAE (docs#list.tfae) statement without writing down the two propositions, see GitHub. Since using docs#list.tfae.out with two numbers isn't very readable, @Eric Wieser thinks we should give names to some of the equivalences, so when they are used in other proofs we can see what's going on. This is somewhat similar to extracting the two directions from an iff statement using alias. I've also tried local attribute [-linter] linter.def_lemma but Lean says "cannot remove attribute [linter]" (why?), and that's definitely not an ideal solution. The viable solutions are the followings, AFAIK:

  • implement a proposal to improve TFAE readability (see also #3532);

  • implement another command like alias to extract from TFAE, or extend the syntax of alias;

  • manually extract lemmas: currently too cumbersome. Need to change the behavior of lemma/theorem declarations to work without type ascription.

Reid Barton (Dec 24 2022 at 07:50):

In Lean 3 the body of a theorem/lemma is not considered when elaborating its type. So, if you don't give a type at all then of course it won't work.

Reid Barton (Dec 24 2022 at 07:51):

This is intentional so that proofs of lemmas can be checked in parallel with the rest of the file (as well as being a generally good thing I think)

Reid Barton (Dec 24 2022 at 07:52):

I would be inclined to suggest not trying to do anything about this TFAE stuff in Lean 3

Junyan Xu (Dec 25 2022 at 01:35):

Thanks; maybe I'll go with [irreducible] def then.

Junyan Xu (Dec 25 2022 at 07:13):

... but that requires disabling the def_lemma linter, otherwise @[irreducible, nolint def_lemma] on every declaration is also pretty cumbersome. Any idea why the linter attribute can't be removed?

Yaël Dillies (Dec 25 2022 at 08:19):

That's just a setting, right? It means the linter attribute doesn't implement removal.

Yaël Dillies (Dec 25 2022 at 08:21):

But I doubt that's what you mean to do anyway. You don't want to locally stop def_lemma being a linter. You want to stop it being run on your declarations during CI. There's a list of linters that are run during CI somewhere, and this list is global. So I'm afraid you can't do what you want.

Reid Barton (Dec 25 2022 at 08:32):

I would generally be inclined to just write out the full lemma statement manually.

David Loeffler (Dec 25 2022 at 09:45):

Reid Barton said:

I would generally be inclined to just write out the full lemma statement manually.

+1 from me. It might take a little while, but probably less time than has already been spent trying to work out how to avoid doing it; and it will result in more readable source code.

Last updated: Aug 03 2023 at 10:10 UTC