I’ve been using Coq like 5 years ago, and then decided to use it again recently.
I’m starting to make harder proofs and I have two main problems.
In general I find it really hard to find simple answer to simple questions like how to replace “~ a <> b” with “a = b” (I think I lost 4 hours online and trying other stuffs on this one).
I have similar problem with using “exists!”.
And more recently, I have come to think that my proof was harder than necessary because of the mere formulation of the lemma and the definitions.
So I had :
Definition cover (tiles:list tile) (lat:lattice): Prop :=
(forall tile, In tile tiles → In (to_cell tile) lat) /\ (forall cell, In cell lat → exists! tile, In tile tiles → (to_cell tile) = cell).
Meaning, there is a set of positions (the lattice) and a set of tiles covering it.
There is one and only one tile per position.
I eventually replaced it by :
Definition cover (tiles:list tile) (lat:lattice): Prop :=
(forall tile, In tile tiles → In (to_cell tile) lat) /\ (forall cell, In cell lat → exists! tile, In tile tiles /\ (to_cell tile) = cell).
It’s quite similar, then difference being that instead of P → Q I have P /\ Q.
While I am aware of the difference between the two in general, in this specific instance I have hard time seeing it, but it makes the proof so much worse to use → instead of /.
Uniqueness (exists!) is not preserved if you weaken the property. P /\ Q implies P -> Q (P -> Q is weaker than P /\ Q). So generally there are more things (tile in your example) that satisfy P -> Q than P /\ Q. If there is exactly one thing satisfying P /\ Q, there are probably at least two satisfying P -> Q—unless there is something about the specific P and Q that make P /\ Q equivalent to P -> Q but that’s quite unlikely.
Generally existentials over an implication (exists x, P x -> Q x) are very suspicious (i.e., what you wrote is probably not what you mean), since they can be witnessed by x that does not satisfy P x. That doesn’t tell you much if Q is the actually interesting property.
I actually realised it, at least in my very specific case later?
There are many tiles x such that Q x. But at most one such that P x → Q x. (rather P x /\ Q x in fact).
But for some reasons, there is always exactly one such P x.
The point is that it’s not P x that implies Q x, it’s just that they come together.
I guess, my confusion comes from the curryfication of functions and their types.
If I have a function that takes two object a:A and b:B and gives c:C.
From my understanding, a → b → c, b → a → c and a /\ b → c are “equivalent”.
I can intro a and b (or b and a), or intro (a /\ b) and destruct it, then the context is pretty much the same.
So it seems that somewhere a → b is equivalent to a /\ b.
I was thus wondering, is there a “rule of thumb” for when it is the case and when it is not?
P → Q and P /\ Q in general make very different statements. P → Q means “if P, then Q” while P /\ Q means “P and Q”. It just happens that (P /\ Q) → R and P → (Q → R) are equivalent.
You usually use “forall” with → and “exists” with /\. If you think about what those statements would actually mean, it might make it clearer:
forall x:T, P x -> Q x reads as “For all x, if P x is true, then so is Q x.”
exists x:T, P x /\ Q x reads as “There is some x for which P x is true, and Q x is also true.”
In my teaching, I often encounter students who use “P → Q” when they want to use “P /\ Q”. The thing that they tend to overlook is that a fact of the form “P → Q” is already weaker than a fact of the form “Q” (which guarantees that Q holds no matter what happens to P). Even worse, if (not P) happens to hold, then (P → Q) does not say anything about Q.
I wonder, is there a “prefered” way to write lemmas?
Is A /\ B → C better than A → B → C.
The first is less curry howard but does it mean it’s worse?
Also, I think my confusion was partly due to the fact that my statements are very long (maybe because I write bad Coq). But then I have hard time sometimes telling where the parameters end and where the statement starts.
From the point of view of Coq usability, it is worse. Given the choice, you should always go for A -> B -> C.
Suppose there is a lemma L: A -> B -> C, a hypothesis b: B, and a goal of type C. Then, you can do
apply L with (2 := b).
With the first form A /\ B -> C, instantiating only the second hypothesis would be much more cumbersome.
And if you keep using Coq, you will soon drift toward abusing the Curry-Howard correspondence to write proofs. With the second form, you can write the concise term
refine (L _ b).
while the first form requires the more verbose term