> the final version of this exact proof is not human readable any more:
In general, Coq proofs are meant to be read using tools, not as plain text. You start out with the theorem you want to prove, and you apply a rule to it. Then Coq shows two new things to prove. You apply a rule to each of these, and so on.
Without seeing the list of active "proof goals" at each step, there's no way to guess what "apply sym_not_equal" means. But if you step through the proof line-by-line in the editor, then you can examine how each step updates your "proof goals". (I have an old blog post that shows what this looks like: http://www.randomhacks.net/2015/07/19/proving-sorted-lists-c...)
I admit, it can still be pretty arcane. But with the right tools and a bit of experience, it does get a lot easier.
The real head-scratcher are advanced "proof tactics" like "auto", which automatically apply a long lists of possible transformations until they find an answer:
Theorem basic_conj' : forall (A B : Prop),
A -> B -> A /\ B.
Proof. auto. Qed.
This is the Coq version of "the proof is left as a exercise for the computer."
It's pretty cool technology if you like math, well worth some time to puzzle it out. But expect to have to read some tutorials and think about them.
In general, Coq proofs are meant to be read using tools, not as plain text. You start out with the theorem you want to prove, and you apply a rule to it. Then Coq shows two new things to prove. You apply a rule to each of these, and so on.
Without seeing the list of active "proof goals" at each step, there's no way to guess what "apply sym_not_equal" means. But if you step through the proof line-by-line in the editor, then you can examine how each step updates your "proof goals". (I have an old blog post that shows what this looks like: http://www.randomhacks.net/2015/07/19/proving-sorted-lists-c...)
I admit, it can still be pretty arcane. But with the right tools and a bit of experience, it does get a lot easier.
The real head-scratcher are advanced "proof tactics" like "auto", which automatically apply a long lists of possible transformations until they find an answer:
This is the Coq version of "the proof is left as a exercise for the computer."It's pretty cool technology if you like math, well worth some time to puzzle it out. But expect to have to read some tutorials and think about them.