Hi, I’m trying to proof the following th.
forall A B, ((((A → B) → A) → A) → B) → B.
As reference I’m looking at this:
Theorem forward_small : (forall A B : Prop, A → (A->B) → B).
Proof.
intros A.
intros B.
intros proof_of_A.
intros A_implies_B.
pose (proof_of_B := A_implies_B proof_of_A).
exact proof_of_B.
Qed.
The main problem I think that is about the statement that I want to prove, since I didn’t fully understand what I’m supposed to proof… The other problem is that I’m a noob in coq . I tried learning from nahas_tutorial, but I can’t quite get together all the things. Can you give me some hints about the statement that I want to prove?
If your goal is to learn using Coq, I’d recommend working through https://softwarefoundations.cis.upenn.edu/.
That theorem is not easy to prove by hand, but it’s also IMHO not a great exercise — Coq has tactics (tauto, eauto) that can find the proof easily, but using them doesn’t teach you anything. And otherwise it’s not a great exercise to start with.
However, if you have strong reasons to want to prove this theorem and understand it directly, ask again and maybe somebody can give you a hint.
Understanding the problem is my main goal, so If someone could explain what the theorem is about I would be very glad.
I’ll start looking at the resource that you linked to me, thank you.
But (IMHO) that theorem is not about anything, so it’d be really hard to explain and the explanation would be confusing. Maybe somebody generated a random proposition that is provable in Coq. If they didn’t and this means something, it’s a waste of time to reverse-engineer that without some explanation.
More productively: Do you understand the statement and proof of forward_small? And the meaning of universal quantification (forall) and implication (->)? That book should help with that, and feel free to ask when you get stuck.
I got a proof of that goal (by “cheating”) and I don’t really understand it, so I’m not sure it’s about anything, and writing this specific nonsense is not a usual part of working in Coq. However, I understand how to deal with universal quantification and implication, and how to write and read proofs involving them, so I can deal with it.
If this exercise is useful, it’s just to practice rule manipulation on a pointless example — just as if I asked to find m, n and o such that a * s * d * a * d * a * s * a * s * d * a * s * d * s * a * d * a * a * s = a^m * s ^ n * d ^ o. What does it mean? Nothing.
what do you mean by “cheating”?
Also how do you prove somethings that you don’t understand?(I’m probably asking this because, I’m new to the language and I’m thinking more in a mathematical way)
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.
Proof.
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. *)
Restart.
info_auto. (* Use auto, and show the proof in a more familiar format. *)
Show Proof. (* same proof as above *)
Restart.
(* A manual proof, extracted from what [auto] does. *)
intros A B HimplImpliesB.
apply HimplImpliesB. intros HaImpliesBImpliesA.
apply HaImpliesBImpliesA. intros HA.
apply HimplImpliesB. intros _.
exact HA.
Qed.
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 (foo implies bar), then you can try the apply H tactic to turn your goal from bar into foo — this is called a backward proof step, in which you work on the conclusion bar, and show that, since foo implies bar, to prove the goal bar it’s sufficient to prove the goal foo. Here, whatever foo and 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.
Now I understand better, what do you mean, thank you for the answer. I’ll slowly start to learn coq. (really slowly since I’m not a mathematician xD)
1 Like
FWIW: just learned (on zulip) this was part of a challenge. That explains why somebody would make the problem so mean :-). My criticism of the teacher doesn’t apply.
Btw, the theorem doesn’t look that random to me. The inner premise ((A -> B) -> A) -> A is an instance of Peirce’s law which is an equivalent of excluded middle and hence not provable in Coq. However, adding the two outer implications to B can be seen like a generalised double negation that turns the claim into a provable theorem.
So @ofeynqed, although this might not help you directly with the proof, I guess the intended take-home of this exercise could be to hint that some logical principles you might expect to hold (like Peirce’s law and excluded middle) are not provable in Coq’s constructive type theory and that one recipe is to weaken the statements with double negations so they become provable. If this doesn’t make much sense to you now I’m sure it will once you have done more proofs in Coq and learned more about its underlying logic.
In case you want another example, you can just try and prove excluded middle forall X, X \/ ~ X itself and see why this fails. Then prove forall X, ~ ~ (X \/ ~ X) instead.
3 Likes