Coq question: confusion about [symmetry.]

[Peter LeFanu Lumsdaine]

Here’s a little thing that’s confused me for a while: quite often, I find that [symmetry.] fails to do what I expect, and I’ve never managed to work out why.  It’s trivial to work around, but it would still be nice to know what’s really going on.

For instance, in the following code:

----8<----

Require Import HoTT.

Open Scope equiv_scope.

Open Scope path_scope.

Lemma map_inverse_o_equiv {A B : Type} (e : A <~> B)

  {x y : B} (p : x = y)

: ap e (ap (e ^-1) p)

  = (eisretr e x @ p) @ (eisretr e y)^.

Proof.

  destruct p. simpl.

  path_via (eisretr e x @ (eisretr e x)^).

    symmetry. apply concat_pV.

  apply whiskerR. apply inverse. apply concat_p1. 

Defined.

----8<----

if the [apply inverse] is replaced by [symmetry], it fails with

Error: Impossible to unify "(eisretr e x @ 1) @ 1" with "eisretr e x @ 1".

What is [symmetry] doing that makes it try to unify these terms?  I had understood that [symmetry] simply tried to apply instances of [Symmetric]; but [Print Instances Symmetric] shows no instances other than the expected ones, Equiv and Path, neither of which seems to explain this error.

–p. 

[Michael Shulman]

It's certainly something we've encountered before, hence why the style guide says to use 'apply symmetry' instead. But I don't recall if we ever figured out exactly what is happening.

--
You received this message because you are subscribed to the Google Groups "IAS Univalent Foundations" group.
To unsubscribe from this group and stop receiving emails from it, send an email to univalent-founda...@googlegroups.com.
To post to this group, send email to univalent-...@googlegroups.com.
Visit this group at http://groups.google.com/group/univalent-foundations?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.
 
 

[Matthieu Sozeau]

Hi,

I've investigated this and the problem is that Coq does not know
about the polymorphic equality's symmetry proof so it tries to build
it dynamically on the particular instance at hand. But it does so in
a simple-minded way: (Cut b=a;Intro H;Case H;Constructor 1).
Problem is, if the term on the left appears as a subterm on the right,
this fails (hence the somewhat puzzling behavior). I would recommend
always using [apply symmetry] instead as well.
-- Matthieu