The Coq mailing list

[roconnor AT theorem.ca]

On Thu, 11 Mar 2010, Robert Helgesson wrote:

> 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.
>
> Many thanks.

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".  For example I 
believe the standard inductive definition of the reflexive, symetric, 
transitive closeure of a relation R to be an equivalence relation where 
"symmetry (symmetry H) <> H".

Inductive EquivClosure (R : A -> A -> Prop) : A -> A -> Prop :=
| base : forall a b, R a b -> EquivClosure R a b
| re : forall a, EquivClosure R a a
| sy : forall a b, EquivClosure R a b -> EquivClosure R b a
| tr : forall a b c, EquivClosure R a b -> EquivClosure R b c -> EquivClosure 
a c.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''