September 11, 2013 - Tagged as: en, coq.
While working with constructive systems, at the lowest level you can directly construct proof objects by writing programs. But for realistic scenarios, this is probably too hard to do. Coq and Idris like languages provide an alternative way to construct proof objects: tactics. Tactics provide a way to derive proofs in a way that is somewhat like informal proofs given in spoken languages. But theorems you’re trying to prove is already too complex, and in some parts, very repetitive.
That tactics Coq like theorem provers provide also help you construct proofs with some automation commands. For instance, you can apply same steps several times, until you prove some subgoals. Or you can search for a proof by applying some steps in different combinations.
What doesn’t make sense to me is that in general you cannot really use that automation methods before manually writing long and hard proof by hand and showing that your theorem is really a theorem and it indeed has some repetitive parts.
And at this point you’re probably better off leaving the proof as-is because replacing explicit steps with some magic commands(I’ll come to this point later) only makes the proof harder to read, without any other advantages.
I have similar ideas for auto tactic. What it does is that it searches for a proof by applying different combinations of apply and intros tactics(with some limitations – it only uses apply for hypothesis and hint database which you generate while defining inductive definitions).
Now my problem with auto is that you can only use it when you absolutely sure that your theorem is indeed a theorem – that is, it has a proof. And how can you know that your theorem is correct? The only way to know this is to write a proof for it. Now let’s say auto tactic fails, and when this happens it can’t really say anything. Why did it fail? It may be because your proof is actually too long and it searched for a while but couldn’t find a proof(you can specify search depth as an optional parameter of auto tactic). Or maybe your hint base is not good enough. Or maybe your theorem is not actually a theorem and you cannot prove it.
So both proof search tactics and repetition elimination tactics have this same common problem: you cannot know that they work before writing the proof itself. And automation generally makes the proof unreadable.
Adam Chilpala’s “Certified Programming with Dependent Types” book encourages that automated way of proving. You have that complicated theorem that you don’t even understand what it is saying? No problem, crush tactic(which is not standard, distributed with CPDT book) will prove it for you in one command.
I’m not saying that crush like tactics are necessarily bad and you shouldn’t use it. I’d probably use it in real world when I need a proof that crush can generate and I don’t have time or motivation to do it myself.
And repetition elimination tactics are useful when you have a syntax tree with 15 constructors and you’re proving some theorem that’s relevant with only one of that constructors – 14 subgoals can be easily proved by some clever use of ; operator in Coq.
What I’m saying that is several things:
crush like automation tactics are pure black magic and doesn’t really teach you anthing. As a hobbyist who self-study all this, I prefer learning the principles instead of scripts and magic commands and black boxes.For this reasons I’m trying to use proof automation as little as possible.