Stream: Coq devs & plugin devs

Topic: intuition and auto-star

Karl Palmskog (Mar 26 2022 at 14:43):

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?

Gaëtan Gilbert (Mar 26 2022 at 14:55):

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

Gaëtan Gilbert (Mar 26 2022 at 14:55):

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

Karl Palmskog (Mar 26 2022 at 15:02):

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?

Karl Palmskog (Mar 26 2022 at 15:05):

(for example, in overlays just write out intuition (auto with *). instead of intuition. where you actually need something more than intuition auto)

Gaëtan Gilbert (Mar 26 2022 at 15:06):

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

Karl Palmskog (Mar 26 2022 at 15:06):

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

Karl Palmskog (Mar 26 2022 at 15:08):

for the record, I'm investigating this since we will likely migrate away from intuition/tauto/etc. to itauto in one of our projects

Karl Palmskog (Mar 26 2022 at 15:11):

ah apparently there is a recently discovered reason to not use intuition: https://github.com/coq/coq/issues/15824 (silently assumes axioms)

Pierre-Marie Pédrot (Mar 28 2022 at 06:47):

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

Karl Palmskog (Mar 28 2022 at 14:09):

ah, I wasn't even aware that intuition actually also does (some) first-order reasoning...

Paolo Giarrusso (Mar 28 2022 at 20:43):

Not intuition per se, but the leaf tactic

Karl Palmskog (Mar 28 2022 at 21:04):

@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.

Karl Palmskog (Mar 28 2022 at 21:08):

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

Michael Soegtrop (Mar 29 2022 at 09:16):

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.

Paolo Giarrusso (Mar 29 2022 at 10:50):

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.

Paolo Giarrusso (Mar 29 2022 at 10:53):

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

Karl Palmskog (Mar 29 2022 at 10:54):

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.

Paolo Giarrusso (Mar 29 2022 at 11:01):

intuition idtac.shows the intuition output, and info_auto shows how auto finishes... which fits with what Frédéric Besson claims

Paolo Giarrusso (Mar 29 2022 at 11:03):

both itauto and intuition do "first-order preprocessing" such as intros, but intuition does it also in the middle of the proof

Karl Palmskog (Mar 29 2022 at 11:04):

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

Karl Palmskog (Mar 29 2022 at 11:19):

hmm, Frédéric also mentions one can use itautor for recursive invocations (which would have multiple first-order processings)

Karl Palmskog (Mar 29 2022 at 11:19):

is this perhaps the difference? intuition is recursive by default, which leads to FOL-solver-like behavior on some goals?

Karl Palmskog (Mar 29 2022 at 13:31):

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