gotcha in constructor tactic

Stream: lean4

[Heather Macbeth]

Currently, if multiple constructors of a type are applicable to a goal, the constructor tactic will apply the first one which works. For example:

example : P ∨ Q := by
  constructor -- uses `Or.inl`, not `Or.inr`

or

import Mathlib.MeasureTheory.MeasurableSpace.Defs

open MeasurableSpace

example (s : Set (Set α)) (U : Set α) : GenerateMeasurable s Uᶜ := by
  constructor -- uses `GenerateMeasurable.basic`, not `GenerateMeasurable.compl`

The first one (with "or") is a big footgun, I have seen many novice users be confused by this.

[Heather Macbeth]

I was going to propose adding an option to make constructor fail when there were multiple applicable constructors. Then I started to dream bigger, since a current theme of the FRO's work is "eliminating papercuts." Maybe the tactic could just be changed to have this behaviour always (not hiding it behind an option)? Does anyone actually use the "pick a random constructor" behaviour of the constructor tactic?

[Adam Topaz]

I think constructor should just fail for inductive types with more than one constructor

[Kyle Miller]

I think it would be reasonable if it threw an error if multiple constructors applied. If people want the "pick a random constructor" behavior, maybe it could be constructor* or something.

[Joachim Breitner]

I sympathize, and if we have evidence for or good reason to believe that this hinders beginners, we should consider this. Do you have a sense how big the impact is, in terms of mathlib breakage? Probably hard to evaluate without just doing it.

[Kyle Miller]

I don't think it should fail for multi-constructor inductive types. There are places, when there are indices, where there's obviously one constructor that would apply, and I don't see why constructor shouldn't work here.

[Heather Macbeth]

Joachim Breitner said:

Do you have a sense how big the impact is, in terms of mathlib breakage?

My guess would be that the "random constructor" feature is used zero times in mathlib ... since people have been trained to use left and right there. But I don't have a sense of whether the "random constructor" feature is used in other (more CS-y) projects.

[Kyle Miller]

It's possible that people order constructors in their inductive types so that it's a "reasonable constructor" rather than a "random constructor"

[Joachim Breitner]

It's not random, it's “first that matches”. I can't think of a good reason to use that behavior besides somewhat shallow convenience, and helping beginners with a good error message is probably worth it.

[Heather Macbeth]

(You're right, my use of the terminology "random" here is more colourful than truthful. I think it's an accurate description of how my students interpret it, though!)

[Heather Macbeth]

I'm not sure how to solicit feedback from people who may be making use of the current behaviour. Is an RFC the next move?

[Joachim Breitner]

I should think so. And someone has to prepare a patch and see what breaks.

[Mario Carneiro]

Also, I would really like to have the version that tries all constructors and backtracks if necessary! There is currently no way to express this directly with tactics right now

[Heather Macbeth]

Quick'n'dirty implementation (cf the current implementation):

import Lean

namespace Lean.Meta

/--
When the goal `mvarId` type is an inductive datatype,
and exactly one constructor matches the goal,
the `constructor` tactic calls `apply` with that constructor.
-/
def _root_.Lean.MVarId.constructor2 (mvarId : MVarId) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := do
  mvarId.withContext do
    mvarId.checkNotAssigned `constructor
    let target ← mvarId.getType'
    matchConstInduct target.getAppFn
      (fun _ => throwTacticEx `constructor mvarId "target is not an inductive datatype")
      fun ival us => do
        let mut workingCtors := #[]
        for ctor in ival.ctors do
          let s ← saveState
          try
            let _ ← mvarId.apply (Lean.mkConst ctor us) cfg
            workingCtors := workingCtors.push ctor
            s.restore
          catch _ =>
            s.restore
        match workingCtors with
        | #[] => throwTacticEx `constructor mvarId "no applicable constructor found"
        | #[ctor] => return ← mvarId.apply (Lean.mkConst ctor us) cfg
        | _ => throwTacticEx `constructor mvarId "more than one applicable constructor found"

end Lean.Meta

elab "constructor2" : tactic => Lean.Elab.Tactic.liftMetaTactic (fun g => g.constructor2)

example : P ∨ Q := by
  constructor2

/-
tactic 'constructor' failed, more than one applicable constructor found
P Q : Prop
⊢ P ∨ Q
-/

[Mario Carneiro]

This is one of the things that is difficult to implement without support for backtracking in the tactic state, but with some syntactic concessions it could have the form constructor => tacs which tries tacs after applying each constructor and takes the first one that works

[Mario Carneiro]

so that you could write example (hq : Q) : P \/ Q := by constructor => assumption

[Heather Macbeth]

Joachim Breitner said:

And someone has to prepare a patch and see what breaks.

I put this patch on
https://github.com/hrmacbeth/lean4/tree/HM-ambiguous-constructor
I've never written something in Lean core before -- can I lake build locally? Is there a way to run CI on it?

[Mario Carneiro]

lean core doesn't use lake (I know...)

[Mario Carneiro]

you should follow the instructions at https://lean-lang.org/lean4/doc/make/index.html

[Heather Macbeth]

I had some trouble building Lean core locally, is there a way to get the main lean4 repo's CI to run on it? Can I just open a draft PR, or is that a nuisance?

[Mario Carneiro]

yes you can

[Mario Carneiro]

not that I can speak for the team of course

[Henrik Böving]

and if you are just looking for tests you probably want to watch the Nix CI as that is usually the fastest by far

[Heather Macbeth]

The draft PR is lean4#3127, and it passes Lean core's CI without any changes to the codebase. How do I get the automated testing on Mathlib to run? The bot says

Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-12-31' branch does not exist there yet.

[Joachim Breitner]

I responded there, but for other curious souls: The most reliable way to get mathlib CI right away is to make sure your branch branches off nightly-with-mathlib. The error message from the bot isn’t most helpful about this; branching of nightly means you only get mathlib CI once that nightly has had a successful mathlib build.

[Eric Wieser]

Kyle Miller said:

I don't think it should fail for multi-constructor inductive types. There are places, when there are indices, where there's obviously one constructor that would apply, and I don't see why constructor shouldn't work here.

I'm no longer fully convinced by this; just because only one constructor unifies doesn't necessarily mean it's the one you want:

inductive Foo : Nat → Prop
| possible {n} : Foo (n + 1)
| impossible (h : False) {n} : Foo (1 + n)

example {n} : Foo (1 + n) := by
  constructor
  -- unsolvable
  sorry

Perhaps constructor should always error when there is more than one option, but do so with a try this that suggests all the constructors that unify (apply Foo.impossible here). That way, the constructor tactic is always "safe" (in the sense of aesop).

[Yaël Dillies]

However I have some proofs (around docs#Sum.liftRel) which really do use the fact that constructor picks the correct constructor itself.

[Yaël Dillies]

So I would like the current behavior to stay available as constructor!

[Yaël Dillies]

For context, those proofs recombine inductive predicates by breaking everything down in a lot of cases, running constructor to find the one constructor that applies, then assumption to fill everything in. It looks like cases _ <;> constructor <;> assumption.

[Eric Wieser]

I think this is a place where Mario's cases _ <;> any_constructor => assumption syntax would make sense

[Yaël Dillies]

Where is that?

[Mario Carneiro]

Mario Carneiro said:

This is one of the things that is difficult to implement without support for backtracking in the tactic state, but with some syntactic concessions it could have the form constructor => tacs which tries tacs after applying each constructor and takes the first one that works

[Eric Wieser]

Presumably with the extra behavior that if none work, it prints the error message for each one

[Mario Carneiro]

Like Eric says, when you actually try to use this "first matching" feature in a large scale situation it doesn't actually work out most of the time. A recent case that came up for me was the reflected typechecker in lean4lean, which is a low effort macro but I would have preferred to just use repeat constructor

[Eric Wieser]

Ah, I guess the constructor => spelling doesn't work with repeat

[Mario Carneiro]

it kind of does, you can write recursive macros

[Mario Carneiro]

But on the subject of that macro, it is really abhorrently slow, it kind of made me despair for being able to actually write nontrivial tactics using macro_rules

[Kevin Buzzard]

I think one difference between maths and CS here is that in CS it's really normal to have inductive types with more than two constructors and in maths it's much rarer (auxiliary inductive types for defining quotients via a list of rules being the exception but these tend not to be used outside the immediate API building which occurs after their definition)

[Damiano Testa]

Wrt giving the first applicable constructor, I found this confusing, the first time that I saw it:

example : Decidable True := by
  constructor
/-
case h
⊢ ¬True
-/

I think that at least some warning about the fact that another constructor was applicable would be helpful.

[Damiano Testa]

Could constructor apply the unique possible constructor, if available, and give a helpful message otherwise? Then constructor! could apply the first possible constructor and maybe constructor n apply the n-th one?

[Mario Carneiro]

that's what @Heather Macbeth implemented in lean4#3127

[Mario Carneiro]

I don't like constructor n though, the constructor has a name and you should use it if you want it

[Mario Carneiro]

For the most part constructor order doesn't matter but both constructor! and constructor n are order dependent

[Mario Carneiro]

I think we should discourage any proof methods that are constructor order dependent, although one of the more common order dependent proof methods is

induction n
· foo
· rename_i a; bar
· next b => baz

[Eric Wieser]

We should discourage that too, in favor of with |, right?

[Mario Carneiro]

I think? there are certain cases of that we certainly can't deprecate like induction on Nat, but I think it's okay to say that the constructor order of Nat is a stable guarantee

[Mario Carneiro]

@Yaël Dillies said:

As discussed here, I would like the current behavior to stay available under a different syntax, probably constructor!. The reason is that I have proofs involving inductive predicates with six constructors that are of the form by cases h <;> constructor <;> assumption.

Can you elaborate on why the new version would not work for your use case?

[Mario Carneiro]

As long as the six constructors have disjoint applicability, there will be no problem. And if they don't, this proof strategy is already somewhat broken because if the wrong constructor is selected then assumption fails and it doesn't backtrack. You would need the any_constructor => combinator to handle this kind of proof correctly

[Eric Wieser]

I think Yael is referring to why my proposed modification of requiring exactly one constructor would not work for that case

[Eric Wieser]

As long as the six constructors have disjoint applicability,

Does Lean have a mechanism to "know" that constructors are disjoint that would return false on my example above?

[Mario Carneiro]

No, but again I'd like to see the example

[Mario Carneiro]

actually, your example is nonsense anyway, you can't do what you want by applying a constructor

[Mario Carneiro]

I'm very confused, you and Yael seem to be arguing for different cases

[Mario Carneiro]

IMO constructor should only ever do unification, not rewriting or anything else, and it should pick the unique one that unifies if there is one, and people should be discouraged from using constructor when multiple constructors are applicable (but it remains to be seen whether this can be disallowed, be a warning or ignored). That's why I want to see @Yaël Dillies 's example

[Yaël Dillies]

Here it is: https://github.com/YaelDillies/LeanCamCombi/blob/formal_book/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean#L183-L198

[Yaël Dillies]

I'm in the middle of porting, so I can't guarantee you it will compile, but you can see the constructors at least. Indeed, they have disjoint applicability.

[Mario Carneiro]

in your example @Eric Wieser there is exactly one constructor that applies, but you end up in an unsolvable state afterwards. That's okay, you just made a wrong move to apply constructor and you should back up and rw [add_comm] first.

[Eric Wieser]

The argument I am trying to make above is that we should design constructor such that it never makes a goal unprovable. If you want to take a possibly-incorrect step, you should be forced to name it

[Mario Carneiro]

constructor is never going to be a reversible step

[Eric Wieser]

It's always reversible if the type has exactly one constructor, isn't it?

[Mario Carneiro]

not for existentials

[Heather Macbeth]

Just a note that now there is an RFC for this issue, lean4#3129; so people who support the change can upvote it.

I added @Damiano Testa's example there.

[Eric Wieser]

Mario Carneiro said:

not for existentials

I don't agree:

example {a : α} {P : α → Prop} : ∃ a, P a := by
  constructor
  refine Classical.choose_spec ?_
  -- back where we started:
  sorry