Assume that the statement we want to prove has a proof.
Can we find it with only the “standard” Coq tactics?
i.e. is programming a custom tactic ever necessary? (not sufficient is not what I care, if it has a proof this in theory could be a silly tactic that encodes the proof of the statement which is not interested)
Motivation: I recently learned that one can implement their own tactics…!
Yes, (in theory) every theorem that has a proof can be proved with just the exact tactic. You just have to give it the proof term (which might be huge).
Even if this answer is purely theoretical, yes, in practice you can decide to rely only on standard tactics to do all your proofs. The point of writing custom tactics is to be more efficient, not to prove more things.
Awesome. Thanks for the feedback.
Now let’s try to make it slightly more practical. I am aware the next question in general might be extremely hard to know, but I am curious to learn and get what people’s intuitions are and why.
Which one is probably easier? Tactic creation via programming (or program synthesis for automation) or term creation by human guessing (or term synthesis via automation)?
Writing explicit terms is highly unpractical, while tactics provide a higher-level interface, even for primitive tactics. It would be a nightmare to write the proof terms corresponding to rewrite or congruence for instance. Furthermore, writing your own DSL usually makes proofs much easier to write, understand and maintain.
There are actually some medium-sized projects where the author has used the equivalent of exact for every proof, for example:
Why is it unpractical to write out proof terms? Isn’t that necessary for example when writing out Loop Invariants (LP)?
Try it for yourself, by writing a proof that true <> false. Now imagine that this is an inductive type with a lot of constructors that you modify regularly.
Are you talking about a specific Coq library? In Gallina, there are no loops, only recursive functions, and much less “invariants”, since it features dependent types.
Hi Theo,
To expand on this discussion. I was curious if we can “reduce” Coq to only a set of inference rules (like in FOL or other systems I’ve seen in logic classes). If that were the case then the exact tactic would never be used. I am aware that is not the way Coq users would do it but I am curious if that is possible (e.g. it could be useful for automated proof searching).
Perhaps a way to summarize my question could be what is the difference between CoC and Natural Deductions? (I am more used to Isabelle to give context)
I’m not sure what you mean exactly but many of Coq tactics were initially thought to mimic some inference rules of natural deduction and this is still the way Coq is taught in my university (natural deduction inference rules and Coq tactics are taught at the same time). The assumption tactic can then indeed be used instead of exact to conclude such proofs.
To expand on this discussion. I was curious if we can “reduce” Coq to only a set of inference rules (like in FOL or other systems I’ve seen in logic classes).
Yes; the rules are described in the “core” chapter of the reference manual: https://coq.inria.fr/distrib/current/refman/language/core/index.html
In particular, see https://coq.inria.fr/distrib/current/refman/language/cic.html and https://coq.inria.fr/distrib/current/refman/language/core/inductive.html .