itauto and intuition · Coq Platform devs & users

As can be seen in this discussion, which references several Coq repo issues, the current state of intuition. being a synonym for intuition auto with *. is not a good thing, and leads for example to dependence on axioms when they aren't needed.

But even if intuition. is redefined as intuition auto. as in Stdpp, there are issues with the tactic(s). For example, intuition auto. is not fully propositional, as one might expect, as is discussed here. Mainly for this reason, I think (something like) the itauto tactic could become a replacement in the long term for intuition.

If no solution to intuition. issues is found soon, how about adding itauto as an alternative in the Platform for 2022.10 or later? While it could be described as experimental, it's part of Coq's CI and I have applied to several large Coq projects (swapping out intuition) with good performance results.

Karl Palmskog (Apr 25 2022 at 12:33):

From Coq Require Import ZArith.ZArith Program.Program.

Lemma foo {A} (n : nat) (a a0 : A)
  (e : Z.succ (Z.of_nat n) = 0%Z) :
  Z.eq_dec (Z.succ (Z.of_nat n)) 0 = left e ->
  Some a = Some a0.
Proof. intuition. Qed.

Print Assumptions foo. (* gives axiom Eqdep.Eq_rect_eq.eq_rect_eq *)

Karl Palmskog (Apr 25 2022 at 12:35):

bottom line: I can open a Platform repo issue about this and ping the necessary people, but a few thumbs up here first would be nice so I know it's worthwhile

Karl Palmskog (Apr 26 2022 at 09:21):

@Michael Soegtrop opinion on this? In my view, itauto essentially fills a niche in between Coq built-in automation and sauto from Hammer (full first order). Currently, to my knowledge, only sauto in the Platform can combine lia and congruence with general reasoning in a good way. But many users may not want to make the jump to that kind of powerful tactic (less predictable).

Karl Palmskog (Apr 26 2022 at 09:22):

itauto gives you predictable SAT + congruence OR lia (there is even congruence AND lia). Even though it may be considered experimental.

Michael Soegtrop (Apr 26 2022 at 09:44):

Since I switched to numerics I don't do that much auto style proof search stuff any more - I mostly use reflective tactics. So I can't really say something founded on recent experience here. But from my past experience I would say that auto with * is in general a bad idea.

I am definitely open to add itauto to the extended level, but I don't think it would be good to add it to full if there might be substantial changes in the future which break usages of it.

Karl Palmskog (Apr 26 2022 at 09:46):

itauto is a reflective tactic, but it can call regular tactics given as arguments.

Stream: Coq Platform devs & users

Topic: itauto and intuition