RFC: make constructor tactic fail in ambiguous cases

[hrmacbeth]

Proposal

Currently, if multiple constructors of an inductive type are applicable to a goal, the constructor tactic will apply the first one which works. The proposal is to instead make the constructor tactic fail unless there is exactly one constructor which works. A draft implementation is at #3127.

User Experience: The proposed behaviour makes the tactic slightly less powerful, but more predictable.

The behaviour being disabled is currently used rarely: twice in Std (diff) and twelve times in Mathlib (diff), out of thousands of uses of the constructor tactic. It would be useful to hear if there are other projects (perhaps with a different flavour to the proofs) which use the feature more.

Beneficiaries: I would expect novice/unsophisticated users to be the biggest beneficiaries, and perhaps this is desirable since a current theme of the FRO's work is "eliminating papercuts." A particular example: I frequently see students confused that constructor is a valid tactic to use for Or:

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

(... or reach unprovable goals by simply failing to note the ambiguity).

I'm guessing @robertylewis' students make the same mistake: one of his course repos includes a constructor alias which filters the type of the goal.

The change may also help non-novice users avoid mistakes when they are working with an unfamiliar part of the library.

Maintainability: I imagine this change will not make code maintenance harder, and may possibly make it easier.

Community Feedback

Zulip discussion is here; those that commented seemed open to the change.

@adomani commented that he has encountered this point of confusion in the case of Decidable:

example : Decidable True := by
  constructor -- uses `Decidable.isFalse`, not `Decidable.isTrue`

Impact

Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

[YaelDillies]

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.

[digama0]

(Clarified on Zulip that Yael's example would not be affected by this change in the behavior of constructor.)

[madvorak]

I totally support this change. My students have been confused by the current constructor behavior as well.

[kim-em]

I think this is a good change. There is a small performance penalty from "unnecessarily" checking later constructors, but I think it is reasonable to say that anyone relying on the order of constructors (either to get the right one, or to avoid attempting the unification against other constructors) should be using apply instead of constructor.

The improvement for new users outweighs the slight inconvenience for experts.

If the associated draft PR can gain some tests, I'm happy to merge.

[fpvandoorn]

Another solution to solve this issue: constructor will throw an error when the type is (or reduces to) an inductive type with 0 indices and at least 2 constructors. Otherwise the behavior remains the same as what it is now.

This still takes care of all confusing cases, and has the same outcome for inductive types without indices.

Differences with the suggestion above:

• No need to check other constructors, so this suggestion is a bit more efficient
• For many indexed inductive types at most 1 constructor applies at each time (e.g. vectors as an indexed inductive type), and so the behavior would be the same. However, with indexed inductive types you can have some constructors that sometimes apply, and the last constructor that always apply, and "choose the first constructor that applies" is still a useful tactic to have.

EDIT: Here is an example with a Coq inductive type I wrote for the axioms of Hilbert Calculus. I would be sad if constructor would fail to prove AxiomH (A → A∨A) because two constructors apply.

Inductive AxiomH : PropF -> Prop :=
| HOrI1  : forall A B  , AxiomH (A → A∨B)
| HOrI2  : forall A B  , AxiomH (B → A∨B)
| HAndI  : forall A B  , AxiomH (A → B → A∧B)
| HOrE   : forall A B C, AxiomH (A∨B → (A → C) → (B → C) → C)
| HAndE1 : forall A B  , AxiomH (A∧B → A)
| HAndE2 : forall A B  , AxiomH (A∧B → B)
| HS      : forall A B C, AxiomH ((A → B → C) → (A → B) → A → C)
| HK      : forall A B  , AxiomH (A → B → A)
| HClas  : forall A    , AxiomH (¬(¬A) → A)

[kim-em]

This sounds pretty good! Hopefully we can have some feedback from others who've emoji'd this issue.

We may want to convert this suggestion to an independent RFC if others are happy with it.

[david-christiansen]

It seems to me that this suggestion won't fix the issue at hand, but I may be misunderstanding.

As I see it, the problem with constructor is that non-expert users get an unprovable goal because it succeeds unhelpfully, applying the wrong constructor. This can definitely be a problem with unindexed types - it might pick inl when inr could also have worked - but it also seems to be a problem with indexed types that aren't being used in the way that @fpvandoorn is suggesting.

Sorry for the contrived example, but I could have something like:

inductive Balanced : Tree -> Prop where
  | empty : Balanced .empty
  | same : l.depth = r.depth -> Balanced (.branch l x r)
  | left : l.depth = r.depth + 1 -> Balanced (.branch l x r)
  | right : l.depth + 1 = r.depth -> Balanced (.branch l x r)

This is an indexed type where choosing the first constructor that applies is often the wrong move.

@YaelDillies's suggestion of a slightly longer name for the current behavior seems to take care of @fpvandoorn's use case, but I think that the suggestion of just picking same when confronted with the goal Balanced (branch l x r) is likely to have similar drawbacks.

[madvorak]

I would be sad if constructor would fail to prove AxiomH (A → A∨A) because two constructors apply.

Inductive AxiomH : PropF -> Prop :=
| HOrI1  : forall A B  , AxiomH (A → A∨B)
| HOrI2  : forall A B  , AxiomH (B → A∨B)
| HAndI  : forall A B  , AxiomH (A → B → A∧B)
| HOrE   : forall A B C, AxiomH (A∨B → (A → C) → (B → C) → C)
| HAndE1 : forall A B  , AxiomH (A∧B → A)
| HAndE2 : forall A B  , AxiomH (A∧B → B)
| HS      : forall A B C, AxiomH ((A → B → C) → (A → B) → A → C)
| HK      : forall A B  , AxiomH (A → B → A)
| HClas  : forall A    , AxiomH (¬(¬A) → A)

I personally wouldn't be sad that I cannot use constructor here.

[fpvandoorn]

I agree that my proposal is a trade-off, and there are cases where it might not be desirable. I thought it had maybe a simpler semantics, and I'm confident that the (non-logician) mathematicians will also be happy with it (Mathlib contains few inductive types besides structures and very few indexed inductive types). I am personally happy with either solution, as long as under the RFC-proposed semantics the current behavior remains available under a different name.