The Coq mailing list

[Valentin Robert <valentin.robert.42 AT gmail.com>]

Similarly, the following will also let you remember that pfxy talks about the pair being matched:

refine (

  match p with

  | exist _ p pfxy =>

    match p as _p return p = _p -> _ with

    | (x, y) => fun P => exist _ (y, x) _

    end eq_refl

  end).

- Valentin

On 12 September 2017 at 13:23, Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> wrote:

The elimination of the non dependent pair needs to preserve information about the pfxy, so I don't think you can combine it with the match on the valid_bp.
To preserve information about some hypothesis when matching over a subterm of its type you first abstract the hypothesis, so that the return clause of your match talks about it.
The refine would then be something like

match p with
exist _ xy pf =>
  match xy return valid xy -> valid_bp with
  (x,y) => fun pf' => exist _ (y,x) _
  end pf
end

(where "valid" is whatever the property is called)

Gaëtan Gilbert

On 09/12/2017 10:16 PM, Kevin Sullivan wrote:

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).