The Coq mailing list

[Edsko de Vries <edskodevries AT gmail.com>]

Dear all,

I have another question about rewriting, about unsatisfiable
constraints this time. A little bit of context: the lemma I'm
currently working on involves a proof about structural equivalence
[struct] between pi-calculus terms. [struct] is a symmetric and
transitive parametric relation, but is not reflexive because it is
defined only over locally closed terms. I have a proof obligation of
the form

  struct (par P Q) (par (out sub obj Q') (par Q Q''))

and a hypothesis

  IH1 : struct P (par (out sub obj Q') Q'')

I want to rewrite the goal with IH1. This should work since [par] has
been declared as a morphism struct ==> struct ==> struct.
Unfortunately,

  rewrite IH1

give the following error:

?356228 == (Morphisms.MorphismProxy ?356226
              (par (out sub obj Q') (par Q Q'')))
?356227 == (Morphisms.Morphism
              (?356222 ==> ?356226 ==> Basics.flip Basics.impl) struct)
?356226 == (relation proc)
?356225 == (Morphisms.MorphismProxy ?356223 Q)
?356224 == (Morphisms.Morphism (struct ==> ?356223 ==> ?356222) par)
?356223 == (relation proc)
?356222 == (relation proc).

I think the problematic constraint is the constraint

?356225 == (Morphisms.MorphismProxy ?356223 Q)

about the part that remains the same during the rewrite. When I
instantiate ?356223 with Q manually:

  assert (Morphisms.MorphismProxy struct Q) by
    (compute ; auto).

the rewrite goes through. Alternatively, I also have an identity
relation [lc_eq] restricted to locally closed terms (and have proven
that [par] is also a morphism struct ==> lc_eq ==> struct), and when I
replace the above assert by

  assert (Morphisms.MorphismProxy lc_eq Q) by
    (compute ; auto).

the proof goes through too. In both cases, the proof goes through
because there is a hypothesis in the context that Q is locally closed.
Without the assert, however, the rewrite gets stuck. What I *suspect*
happens is that the constraint solver picks 'eq' for the constraint

?356225 == (Morphisms.MorphismProxy ?356223 Q)

which makes the constraint

?356224 == (Morphisms.Morphism (struct ==> ?356223 ==> ?356222) par)

unsolvable (because the proof of that goal will now involve reasoning
about terms that are not locally closed).

Might that suspicion be correct, and if so, what can I do about it?

Thanks,

Edsko