Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Evaluation with equality proofs

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Evaluation with equality proofs


Chronological Thread 
  • From: Daniel Schepler <dschepler AT gmail.com>
  • To: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
  • Cc: Andrew Rodriguez <amr1 AT andrew.cmu.edu>, Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Evaluation with equality proofs
  • Date: Fri, 24 Jan 2014 12:27:02 -0800

Shouldn't it be easy to do something more generic by recursion on n instead of on v?  Something like:

Definition cast : forall {P : nat -> Type} {n:nat} (x : P n) {m:nat},
  n = m -> P m.
refine (fix cast (P : nat -> Type) (n : nat) (x : P n) (m : nat) (e : n = m)
        {struct n} : P m :=
        match n return (P n -> forall m:nat, n = m -> P m) with
        | 0 => fun x m => match m return (0 = m -> P m) with
                        | 0 => fun _ => x
                        | S m' => _
                        end
        | S n' => fun x m => match m return (S n' = m -> P m) with
                        | 0 => _
                        | S m' => fun _ => cast (fun a => P (S a)) n' x m' _
                        end
        end x m e); clear cast; abstract congruence.
Defined.

Require Import Arith.

Eval compute in (fun P (x : P (3 + 2)) => cast x (plus_comm 3 2)).
-- 
Daniel Schepler


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






Archive powered by MHonArc 2.6.18.

Top of Page