The Coq mailing list

[Robert Helgesson <robert AT rycee.net>]

> >But I haven't been able to figure out how to prove something like
> >
> >Lemma sym_sym_equiv : forall (A : Type) (S : Setoid A) (x y : A)
> >   (H : x == y), symmetry (symmetry H) = H.
> >
> >Is it at all possible to prove this general case and if so, how?
> >If it's not possible then I would appreciate a short description
> >why.
> 
> I don't think that this will be provable in general because in
> general the proof of "x == y" may not be unique.  In particular the
> proof may contain trace information making "symmetry (symmetry H) <>
> H".
> [snip example]

Thank you for the explanation and example, it makes the situation more
clear to me.  After sending the mail, however, I happened to think of
the notion of proof irrelevance and found the corresponding module.

So, showing the sym_sym_equiv lemma becomes trivial once the axiom of
proof_irrelevance is added.  But perhaps it's a bad idea to introduce
this axiom without careful consideration?  My specific situation now
is that I'm continuing learning Coq by developing some category theory
and have reached the point where I would like to show

  Theorem dual_dual_category :
          forall (ob : Type) (hom : ob -> ob -> Type)
          (C : Category ob hom), JMeq (dualCat (dualCat C)) C.

which is rather straight-forward until I hit precisely the problem in
my previous message, i.e., I have to show something like

  setoid_sym (setoid_sym (assoc f g h)) = assoc f g h

applying proof irrelevance does indeed do away with this equality and
subsequently makes the whole theorem pass.  Seeing the "proof
completed" fills me with giddy joy but I'm worried that introducing
the axiom in this situation is bad.  Am I worrying unnecessarily?

/Robert