The Coq mailing list

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

Dear all,

I had sent a question about rewriting and non-existential variables to
coq-club but it doesn't seem to have appeared; no matter, I solved the
problem, but I thought the solution might be worth sharing. The proof
(an example lemma in a locally nameless formalization of the
pi-calculus) looked like

Example reds_ex1 : forall P Q (c d x : atom), lc P -> lc Q ->
  d `notin` fn (inpx c x P) ->
  reds (par (inpx c x P) (new d (out c d Q))) (new d (par ([x ~> d] P) Q)).
Proof.
  intros.
  rewrite (struct_extrude_new _ _).
  rewrite (red_commx _ _).
Qed.

That doesn't work, however. The proof went through, but after the last
auto Coq complains about non-instantiated existential variables,
corresponding to the proofs at the underscores (which, by the way, can
be solved by auto). I couldn't figure out a way to make rewrite try
and find the proofs, but actually it's very simple:

Proof.
  intros.
  rewrite struct_extrude_new ; auto.
  rewrite red_commx ; auto.
Qed.

Doh. Still, somebody else might have the same problem some day so I
thought I'd share (and perhaps the behaviour of rewrite in the first
proof wasn't entirely what one would expect?)

By the way, the use of support subrelations in setoids makes these
proofs really pretty!

Edsko