How to get intuition for what kind of goals sniper can prove?

[patrick-nicodemus]

Hello; Where can I learn about what is and is not appropriate for sniper? For example I tried to prove

Theorem abc2 : exists k : Z, k = Z0.
Proof.
  snipe.

but this gave the error

Error:
Anomaly
"Uncaught exception Failure("Verit.tactic: can only deal with equality over bool")."
Please report at http://coq.inria.fr/bugs/.

I would like to know what makes this example hard, is it the existential quantifier or what? I don't understand what it means with "can only deal with equality over bool" because some examples in examples.v deal with decidable equality over other types. for example,

  Theorem app_eq_unit (x y:list A) (a:A) :
      x ++ y = [a] -> x = [] /\ y = [a] \/ x = [a] /\ y = [].

[louiseddp]

Hello ! Thank you for taking interest in Sniper ! To get the intuition of the goals that are provable theoretically with our tool, I suggest that you look at the more recent paper which lists the transformation that are currently available: https://arxiv.org/pdf/2204.02643.pdf. You have the section 4 which presents all the standalone preprocessing transformations and their combination in the snipe tactic. But your question reminds me that it should be indicated precisely in the README.

On the other hand, I think that the error message is misleading and that the problem here is indeed the existential quantifier. My explanation would be the following: snipe is made of two parts : the preprocessing phase with the scope tactic from the Sniper plugin, and the call to the external SMT-solver with the verit tactic from the SMTCoq plugin. But verit has already a preprocessing phase, translating some goals in Prop to goals in bool , thanks to the prop2bool tactic: https://github.com/smtcoq/smtcoq/blob/coq-8.13/src/PropToBool.v#L172. The reason why this is not part of Sniper rather than SMTCoq is for not weakening the verit tactic in more recent versions of SMTCoq. On the other hand, prop2bool does not translate the existentials and thus the "real" verit tactic which deals only with equality over bool fails (in fact it is the primitive tactic verit_bool here: https://github.com/smtcoq/smtcoq/blob/coq-8.13/src/Tactics.v#L82). In the future, we plan to add the trakt transformation, presented in the paper and available here: https://github.com/ecranceMERCE/trakt, which is strictly stronger than prop2bool, to deal with translation between logic in Prop and logic in bool, but unfortunately it will not solve the existential quantifiers problem. It is avalaible in the with-trakt branch of this git. This should be the task of a specific future transformation of scope but for now you have to provide the witness manually.

I hope it helps !

[patrick-nicodemus]

Hi, ok I will read that section of the paper carefully. Thank you! Would it be possible to explain roughly what the problem is with these two goals? Two more examples of things, I am curious why these cannot be proven and what my expectations should be.

Definition abc (n : nat) := True.
Goal abc 0.
  snipe.

or

Goal (match 0 with | 0 => True | _ => False end).
Proof.
  snipe.

So there is no reduction of definitions or pattern matching in snipe? What is the best workaround for this?

[louiseddp]

For the first goal, I would say that you found a bug in the prop2bool tactic, but I don't know if it is planned to be fixed because it will not be used anymore in the future as it should be replaced entirely by Trakt. True should be replaced by true=true.

The second goal it is because elimination of pattern matching is handled in the hypotheses (it transforms the pattern matching into equations) but not in the goal. This transformation is implemented but still not available in the main branch, I planned to merge it in a few weeks. But you still may have a problem because True appears again. For now, I think that destructing the variable manually and using Coq's reduction, then using true=true instead of True is the only workaround