The Coq mailing list

[Andrew Rodriguez <amr1 AT andrew.cmu.edu>]

Thanks for the quick response, cast worked great.

Out of curiosity, would it be possible to use UIP to "hide" the opaque proof? My idea, which I haven't been able to implement, would be to use UIP to replace the plus_n_O with eq_refl and then the existing match with eq_refl would go be able to go through. It would avoid the only downside that cast: that it has to recreate the list just to appease the typechecker.

Andrew

On Fri, Jan 24, 2014 at 9:43 AM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

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