The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 24/01/2014 18:28, Andrew Rodriguez wrote:
> The main question is how to define my helper lemmas so they don't try to
> match on a proof object. I also suspect that maybe my definition of
> vrev' is making things more complicated than they need to be. If there
> were a way to use an equality of types in the typechecking of vrev', I
> wouldn't have to apply the function that matches on the proof object --
> but I don't know if that's possible.

There is a nice hack in the standard library in the trunk, which
bypasses that sort of issues. It uses equality proofs on integers in a
purely negative way, that is, only to prove absurdity, which is
precisely something that won't occur, so the reduction don't get stuck.

Here is the code:

 Definition cast: forall {A m} (v: t A m) {n}, m = n -> t A n.
 Proof.
 refine (fix cast {A m} (v: t A m) {struct v} :=
  match v in t _ m' return forall n, m' = n -> t A n with
  |[] => fun n => match n with
    | 0 => fun _ => []
    | S _ => fun H => False_rect _ _
  end
  |h :: w => fun n => match n with
    | 0 => fun H => False_rect _ _
    | S n' => fun H => h :: (cast w n' (f_equal pred H))
  end
 end); discriminate.
 Defined.

(Dunno if it works in v8.4, but you can adapt it anyway.)

You can prove that cast preserves equality on reflexivity proofs, which
should be easy, and use it whenever you need to do some integer casts.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature