Dear Coq users,

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 /.

Thank you very much for you explanations.