Can every theorem that has a proof be completed without DSL tactics?

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.

1 Like

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:

1 Like

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.