I've observed that many users, in particular beginners, often use the naked `intuition`

tactic mindlessly (i.e., without a specified leaf tactic). This invocation, as currently defined, will result in `intuition (auto with *)`

, which can have terrible performance with large hint databases. For this reason, Stdpp redefines naked `intuition`

as `intuition auto`

.

Has it ever been discussed to change the official definition of naked `intuition`

? Was there any specific reason against it besides breaking code?

there was https://github.com/coq/coq/pull/11760 for firstorder

see also https://github.com/coq/coq/issues/4949 https://github.com/coq/coq/issues/7725

and https://github.com/coq/coq/pull/8175

thanks, I suspected this had a long history. I remember the firstorder fix, and it seemed reasonable.

@Gaëtan Gilbert I can't deduce from commenter context why https://github.com/coq/coq/pull/8175 wouldn't be a "proper fix". If nearly all Stdpp users can live with it (`intuition auto`

), shouldn't it be *possible*?

(for example, in overlays just write out `intuition (auto with *).`

instead of `intuition.`

where you actually need something more than `intuition auto`

)

I think PMP just didn't have much time to put on it and therefore bailed

ah OK, so it may be a manpower issue in the end.

for the record, I'm investigating this since we will likely migrate away from `intuition`

/`tauto`

/etc. to itauto in one of our projects

ah apparently there is a recently discovered reason to not use `intuition`

: https://github.com/coq/coq/issues/15824 (silently assumes axioms)

the fact it uses axioms is probably because it's using `auto with *`

ah, I wasn't even aware that `intuition`

actually also does (some) first-order reasoning...

Not intuition per se, but the leaf tactic

@Paolo Giarrusso from my understanding of Frédéric Besson's comments here, `intuition`

itself can actually do some first-order stuff. Here is the example we discussed:

```
Goal forall A (s1 s2 s : list A),
(forall x : A, In x s1 \/ In x s2 -> In x s) <->
(forall x : A, In x s1 -> In x s) /\ (forall x : A, In x s2 -> In x s).
Proof.
Fail itauto auto.
intuition auto.
Qed.
```

`itauto`

has a pure SAT core solver and can't instantiate variables to do the discharge, but somehow `intuition`

can

Paolo Giarrusso said:

Not intuition per se, but the leaf tactic

This is not my understanding. The manual says that `tauto`

is equivalent to `intuition fail`

. I read this such that `intuition`

is a first order solver and you can give a tactic to solve whatever goals cannot be solved first order.

I'll believe Frédéric Besson saying that `intros`

is first-order reasoning on faith, but the manual (which might need amending?) clearly states that `tauto`

is a solver for _propositional_ logic (https://coq.inria.fr/refman/proofs/automatic-tactics/logic.html#coq:tacn.tauto):

This tactic implements a decision procedure for intuitionistic propositional calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff [Dyc92]. Note that tauto succeeds on any instance of an intuitionistic tautological proposition.

@Michael Soegtrop but you're right except for `s/first-order/propositional`

.

maybe `intuition`

is doing some first-order preprocessing? I'm trying to move away from it, so I'm not tempted to read the code.

`intuition idtac.`

shows the `intuition`

output, and `info_auto`

shows how `auto`

finishes... which fits with what Frédéric Besson claims

both `itauto`

and `intuition`

do "first-order preprocessing" such as `intros`

, but `intuition`

does it also in the middle of the proof

in my book, that's a strike against `intuition`

predictability

hmm, Frédéric also mentions one can use `itautor`

for recursive invocations (which would have multiple first-order processings)

is this perhaps the difference? `intuition`

is recursive by default, which leads to FOL-solver-like behavior on some goals?

for posterity, I think the following is a good demonstration of the differences between `itauto`

and `intuition`

(assuming `coq-itauto`

is installed):

```
Require Import Cdcl.Itauto.
Require Import List.
Goal forall A (s1 s2 s : list A),
(forall x : A, In x s1 \/ In x s2 -> In x s) <->
(forall x : A, In x s1 -> In x s) /\ (forall x : A, In x s2 -> In x s).
Proof.
Fail itauto info_auto.
split; itauto info_auto.
Restart.
itautor info_auto.
Restart.
intuition idtac.
Restart.
intuition info_auto.
Qed.
```

Last updated: Jul 13 2024 at 02:02 UTC