I agree that sensible theorem statements can be understood, and I don’t know why you picked one that you can’t, but since you’re still curious, here’s a longer answer.
- High-school students do proofs without understanding all the time. They can solve my stupid exercise (on
a * s * d ...) by algebraic computation, without understanding what the question is about. They just apply some mechanical process that you could teach computers — in fact, that is implemented in Computer Algebra Systems, IIUC. You can check the steps
- This problem can be solved by a different mechanical process (in fact, two), a bit similarly to exercises in formal logic — which can be studied by mathematicians working on (constructive) proof theory, and which are implemented in Coq. Then you can look into the solution they produce — that’s the cheating part. Most proofs cannot be produced mechanically, but this one can — moreover, since this statement only uses implication (it is a statement in propositional logic), we know that if it is provable in Coq, it can be proved by such a process — the
tauto tactic. I added a proof script below, with some comments, but I don’t expect this to fully make sense until you work for a while through Software Foundations.
Lemma yourThm : forall A B, ((((A -> B) -> A) -> A) -> B) -> B.
tauto. (* Solve the goal automatically *)
Show Proof. (* Show the proof from [tauto] as a proof term, which you might
not be familiar with *)
Restart. (* Start over, even if we are basically done and could write [Qed.] here.*)
auto. (* Solve the goal automatically with a completely different procedure. *)
Show Proof. (* Show the proof from [auto] as a proof term, which you might not be familiar with. *)
info_auto. (* Use auto, and show the proof in a more familiar format. *)
Show Proof. (* same proof as above *)
(* A manual proof, extracted from what [auto] does. *)
intros A B HimplImpliesB.
apply HimplImpliesB. intros HaImpliesBImpliesA.
apply HaImpliesBImpliesA. intros HA.
apply HimplImpliesB. intros _.
After you understand enough about Coq, you can follow the proof. I can even tell you the basic idea — if you need to prove
bar, and you know that hypothesis
H tells you that
foo -> bar (
bar), then you can try the
apply H tactic to turn your goal from
foo — this is called a backward proof step, in which you work on the conclusion
bar, and show that, since
bar, to prove the goal
bar it’s sufficient to prove the goal
foo. Here, whatever
bar is, the
apply H proof step is certainly a plausible thing to try; usually you need more original steps, but here you don’t.