coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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:There is a nice hack in the standard library in the trunk, which
> 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.
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
- [Coq-Club] Evaluation with equality proofs, Andrew Rodriguez, 01/24/2014
- Re: [Coq-Club] Evaluation with equality proofs, Pierre-Marie Pédrot, 01/24/2014
- Re: [Coq-Club] Evaluation with equality proofs, Andrew Rodriguez, 01/24/2014
- Re: [Coq-Club] Evaluation with equality proofs, Pierre-Marie Pédrot, 01/24/2014
- Re: [Coq-Club] Evaluation with equality proofs, Daniel Schepler, 01/24/2014
- Re: [Coq-Club] Evaluation with equality proofs, Pierre-Marie Pédrot, 01/24/2014
- Re: [Coq-Club] Evaluation with equality proofs, Andrew Rodriguez, 01/24/2014
- Re: [Coq-Club] Evaluation with equality proofs, Pierre-Marie Pédrot, 01/24/2014
Archive powered by MHonArc 2.6.18.