lemma declaration without type ascription?

Stream: general

[Junyan Xu]

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
context:
⊢ Sort ?
-/
lemma b := trivial /- same as above -/
def c := trivial /- works -/
example := trivial /- works -/

[Junyan Xu]

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]

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]

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]

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

[Junyan Xu]

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

[Junyan Xu]

... 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]

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

[Yaël Dillies]

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]

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

[David Loeffler]

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.