When is it acceptable to use tactics outside of theorems?

Stream: general

[Niels Voss]

I'm thinking about adding a section to #general > Documenting lean pitfalls: feedback requested about using tactics outside of theorem. Can someone remind me if it is considered acceptable to:

1. Use tactics to produce terms of arbitrary types, when constraining the list of tactics to "simple" tactics like apply, have, and infer_instance?
2. Use tactics to produce terms of non-definitional subsingletons, such as Decidable, Fintype, and Squash/Trunc?
3. Use tactics to produce noncomputable terms of non-definitional subsingletons?
4. Use tactics to produce terms of type Prop proofs of terms of type Prop, but inside of a def instead of a theorem? These aren't particularly common, but they do exist, like Acc.inv.
5. Use tactics inside a def to construct something that is part data, part proof (e.g. an element of a subtype)?

[suhr]

But why would you prefer using tactics over terms in the first place?

[Kenny Lau]

I personally use refine where I provide all the data, and then use ?_ for any argument that is a proof. For a minimised example:

def Nat.Itself (n : Nat) : Type :=
  { m // m = n }

def me (n : Nat) : n.Itself := by
  refine ⟨n, ?_⟩
  · -- insert very long proof
    rw [← Nat.add_zero n, ← Nat.add_comm]

Other people are probably in better positions than me to answer your questions, but I will try nevertheless (feel free to treat these as just my opinion and wait for another answer):

1. apply, exact, and refine are fine, and other tactics require more caution.
2. it is fine for Decidable and Fintype because terms of those types are never unfolded. In other words, those terms are "irrelevant" (in the technical sense like "proof irrelevance") (edit: see following discussion)
3. whether it's noncomputable or not isn't the issue, the issue is whether those definitions will ever be unfolded and reasoned about.
4. I'm not sure how you can produce a term of type Prop inside a theorem in the first place. But I would argue that one should still keep tactics to a minimum just like defining any other term of any data types.
5. see my example above.

[Eric Wieser]

Kenny Lau said:

2. it is fine for Decidable and Fintype because terms of those types are never unfolded. In other words, those terms are "irrelevant" (in the technical sense like "proof irrelevance")

unfolding these instances is precisely how decide works

[Niels Voss]

suhr said:

But why would you prefer using tactics over terms in the first place?

Well #5 is done all the time in mathlib, but for the other ones, I'm not completely sure. A common pattern in mathlib (maybe this isn't the case anymore) is to use by classical; exact ... when defining something

[Eric Wieser]

Niels Voss said:

4. Use tactics to produce terms of type Prop,

Do you really mean a term ?P : Prop, and not a term ?h : P where P : Prop?

[Kenny Lau]

Eric Wieser said:

Kenny Lau said:

2. it is fine for Decidable and Fintype because terms of those types are never unfolded. In other words, those terms are "irrelevant" (in the technical sense like "proof irrelevance")

unfolding these instances is precisely how decide works

Does decide fail if there are complicated terms using Eq.mpr (aka the triangle)?

[Niels Voss]

Eric Wieser said:

Niels Voss said:

4. Use tactics to produce terms of type Prop,

Do you really mean a term ?P : Prop, and not a term ?h : P where P : Prop?

Oops, you're right, I meant proofs of propositions

[Kenny Lau]

proofs of prositions shouldn't be def, right?

[Kenny Lau]

Niels Voss said:

suhr said:

But why would you prefer using tactics over terms in the first place?

Well #5 is done all the time in mathlib, but for the other ones, I'm not completely sure. A common pattern in mathlib (maybe this isn't the case anymore) is to use by classical; exact ... when defining something

I think I personally have been doing open Classical in for this case

[Eric Wieser]

@Kenny Lau, that's certainly the fear. Either way, "are never unfolded" is definitely wrong in your statement, so I encourage you to replace it with a new one about "Eq.mpr doesn't actually matter" if you can convince yourself this is true.

[Eric Wieser]

Kenny Lau said:

I personally use refine where I provide all the data, and then use ?_ for any argument that is a proof. For a minimised example:

This is certainly safe, though in my opinion it's not great style. Mainly this style is compelling when the use is actually refine ⟨n, ?_, ?_, ?_, ?_, ?_⟩ <;> simp or similar.

[Niels Voss]

Kenny Lau said:

proofs of prositions shouldn't be def, right?

They need to be defs in certain rare situations, because theorem is kind of like opaque and prevents you from unfolding them.

[Niels Voss]

Eric Wieser said:

Kenny Lau said:

I personally use refine where I provide all the data, and then use ?_ for any argument that is a proof. For a minimised example:

This is certainly safe, though in my opinion it's not great style. Mainly this style is compelling when the use is actually refine ⟨n, ?_, ?_, ?_, ?_, ?_⟩ <;> simp or similar.

Is the actual term produced by refine considered part of refine's public interface, or does the public interface only include what subgoals goals it generates?

[Kenny Lau]

Eric Wieser said:

Kenny Lau, that's certainly the fear. Either way, "are never unfolded" is definitely wrong in your statement, so I encourage you to replace it with a new one about "Eq.mpr doesn't actually matter" if you can convince yourself this is true.

I have strucken out \#2

[Eric Wieser]

Niels Voss said:

They need to be defs in certain rare situations, because theorem is kind of like opaque and prevents you from unfolding them.

I wonder with the recent changes to well-founded recursion if this is actually still something that matters.

[Eric Wieser]

Niels Voss said:

3. Use tactics to produce noncomputable terms of non-definitional subsingletons?

This used to be very common as by classical exact term, but an alternate spelling is open scoped classical in term which avoids tactics.

[Robert Maxton]

Personally, my rule of thumb is that you don't want anyone to have to see a 'bare' cast, i.e. ▸ or _root_.cast or an Eq.mp/Eq.mpr, because when you generate such with tactics you are almost always throwing away important type information without which the expanded definition cannot be reduced in the wild.

I'll use tactics primarily to help me manage elaboration order and the like, so that I have to type out fewer explicit type annotations.

Also, anyone checking this thread should be aware of the by? command, which works like by but then gives you a Try this with an attempt at producing a term equivalent to your tactic. Best used with set_option pp.proofs true so that it doesn't throw away proofs necessary to produce your term, and it doesn't do the same elaboration-order-manipulation that the corresponding tactics do so it doesn't always work, but it's a good thing to try before leaving a tactic-created-term in your final result.

[Thomas Zhu]

I think this isn't mentioned yet: it should be acceptable to use specific tactics to defer evaluation (usually for default parameters), such as in by exact decl_name%, by volume_tac.

[Mario Carneiro]

another reason to use tactics in definitions is simply for formatting reasons; I find it easier to lay out an expression with nesting in weird places using a sequence of calls to refine instead of working out how to do the indentation for the term mode "proof". But I would restrict such usage to things like refine, apply, exact and constructor, and avoid rw, simp or any other high power tactics, at least until you have reduced the goal to something in a Prop.

[Mario Carneiro]

I would say that Kenny's example is a case of this. You could certainly write ⟨n, by ...⟩ but the hanging ⟩ is just much more awkward to format if the ... is a long proof

[Yaël Dillies]

Mario's point above is strong. I myself have started to push people towards the following style:

def foo : Bar := by
  refine ⟨data1, data2, ?proof1, ?proof2⟩
  · proof1
  · proof2

[Eric Wieser]

I'd probably prefer .mk n <| by for Kenny's example

[Eric Wieser]

Or where notation, which also solves the trailing } issue

[Yaël Dillies]

Sorry, I meant to give an example with a non-standard constructor:

def foo : Bar := by
  refine .nonStandardMk data1 data2 ?proof1 ?proof2
  · proof1
  · proof2

[Yaël Dillies]

... the point being that where notation only applies to the standard constructor

[Matthew Ballard]

I thought Eric meant

def Nat.Itself (n : Nat) : Type :=
  { m // m = n }

def me (n : Nat) : n.Itself :=
  ⟨n, prf⟩
where prf := by -- insert very long proof
       rw [← Nat.add_zero n, ← Nat.add_comm]

[Kenny Lau]

wait, u can do that?

[Weiyi Wang]

This is where I need a list of "lean syntax you probably don't know yet"

[Eric Wieser]

I did not mean that, but I should have

[Eric Wieser]

Though I think that makes prf a def not a theorem, which flags the linter?

[Jz Pan]

Matthew Ballard said:

I thought Eric meant

def Nat.Itself (n : Nat) : Type :=
  { m // m = n }

def me (n : Nat) : n.Itself :=
  ⟨n, prf⟩
where prf := by -- insert very long proof
       rw [← Nat.add_zero n, ← Nat.add_comm]

I think this will introduce a me.prf in the global context, which is not good I think.

[Kyle Miller]

I've thought that named arguments were a reasonable compromise.

def foo : Bar :=
  .nonStandardMk data1 data2
    (commociative := by
      tac1
      tac2)
    (ramitated := by
      tac1
      tac2)

It's not as sleek as where for structures, but to me it seems more structured than using refine.

[Matthew Ballard]

Eric Wieser said:

Though I think that makes prf a def not a theorem, which flags the linter?

whatsnew reports theorem me.prf

[Matthew Ballard]

Jz Pan said:

I think this will introduce a me.prf in the global context, which is not good I think.

Actually this might help avoid unfolding the proofs.

[suhr]

Kenny Lau said:

wait, u can do that?

Yes, but where has limitations compared to refine.

[Niels Voss]

Given all the discussion above, is there a consensus on whether:

1. The terms generated by exact, refine, construct, intro, let, and apply is to be considered part of the tactic's public interface?
2. The terms generated by advanced tactics like rw, simp, and aesop are considered part of the tactic's public interface?

It seems to me that the answer to 1. is yes and 2. is no, but where do we draw the line between "simple" and "complex" tactics?

[Robin Arnez]

I think it's just that some tactics are "term" tactics:

• exact and refine literally produce exactly what you give it with maybe some subgoals (emulating
• apply is basically function application
• constructor is also function application or, well, structure instance notation
• intro is basically lambda abstraction
• let and have are, well, let and have
• by_cases is if-then-else
• match is a match expression
• induction is recursor application
• infer_instance is inferInstance
• sorry is sorry

Other tactics are more trying to do something specific to goal (e.g. solve it or rewrite something) instead of being tied to a term and should therefore be avoided for definitions.

[Kyle Miller]

I worry about saying that any tactic has any guarantee about what terms they produce.

For example, intro also has a feature to do pattern matching. It's currently implemented with a match term, but is that in the interface? What if intro gains rfl patterns? Then that means intro can effectively wrap terms in rewrites, which is one of the main goals of avoiding rw and simp.

The induction tactic does make use of the recursor, but maybe one day it will have some capacity for dependent elimination like cases, which people periodically ask for? That introduces rewrites. Furthermore, using induction means your definition won't have equation lemmas for each induction case.

The by_cases is if-then-else, but it's free to pull in Classical. Even the if _ then _ else _ tactic will do this.

That all said, it's hard to imagine that exact/refine/apply will ever do anything except use the term you provide it. (I've been kicking around an idea to make apply t be something like refine apply% t, so that it's even more nothing out of the ordinary.)

I'm focusing on rewrites here because those are what tend to make tactic-defined definitions fail to have good definitional equality properties.