The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

In the following code, valid_bp is a dependent pair whose first element is a non-dependent pair and whose second element is a proof that that (non-dependent) pair has a certain property. I want to write swap, taking such a dependent pair and returning a dependent but in which the given non-dependent pair is swapped. I'm trying to use refine. I match on the structure of the given dependent pair, extracting the non-dependent pair, (x, y), and the proof, pfxy, that it has the given property. The problem I'm having is that in the resulting context, pfxy asserts that the given property pertains to some arbitrarily introduced pair, d, not to the specific pair, x, y; and without the assumption that (x,y) itself satisfies the property, I can't make the proof go through. What am I missing?

Definition swap_basepair (p: valid_bp): valid_bp.

Proof.

refine (

  match p return valid_bp with

  | exist _ (x,y) pfxy => exist _ (y,x) _

  end).