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: May 28 2023 at 13:30 UTC