The Coq mailing list

["Roland Zumkeller" <roland.zumkeller AT gmail.com>]

As far as I can see, no. You could use the library JMeq, which
contains a very similar axiom JMeq_eq. If you despise axioms you could
also try to get around using this kind of equality. Sometimes this is
the more rewarding approach...

Best,

Roland

On 21/06/07, See Wong 
<wongsee AT gmail.com>
 wrote:
> Hi
>
> Thanks.  If T wasn't indexed by nat (which is actually my situation) and not
> decidable in general, is there any other properties I can exploit?  Sorry if
> its a trivial question.
>
> Regards
>
> See
>
>
> On 6/22/07, Roland Zumkeller 
> <roland.zumkeller AT gmail.com>
>  wrote:
> > Hi,
> >
> > Using Eqdep_dec is a good idea, but actually the fact that T is
> > indexed by a nat is already sufficient:
> >
> > Require Import Eqdep_dec.
> > Set Implicit Arguments.
> >
> > Variable T : nat -> Type.
> >
> > Inductive T_eq (a : nat) (r1 : T a) : forall b : nat, T b -> Prop :=
> >     T_eq_intro : forall r2 : T a, r1 = r2 -> T_eq r1 r2.
> >
> > Goal forall (a:nat) (r1 r2:T a), T_eq r1 r2 -> r1 = r2.
> > intros.
> > refine(match H in @T_eq _ _ b r2' return forall (e:a=b), eq_rect _ T
> > r1 _ e = r2' with
> > | T_eq_intro a c => _
> > end (refl_equal _)).
> > apply K_dec_type.
> >   decide equality.
> >   assumption.
> > Qed.
> >
> > Best,
> >
> > Roland
> >
> >
> > On 21/06/07, 
> vsiles AT lix.polytechnique.fr
>  
> <vsiles AT lix.polytechnique.fr>
> wrote:
> > > >
> > > > Hi
> > > >
> > > > I've only used Coq for a few months so please forgive my ignorance.
> > > >
> > > > I am trying to do some formalization work in Coq and have ran across a
> > > > problem, the essence of which can be summarized below:
> > > >
> > > > I have a type that's dependent on some other type, say nat for
> example:
> > > > Record T (a:nat) : Type := { some_field : nat }.
> > > >
> > > > I have found that in order to state some theorems I need the following
> > > > equality definition for T:
> > > >
> > > > Inductive T_eq (a:nat) (r1:T a) : forall b:nat, T b -> Prop :=
> > > > | T_eq_intro : forall (r2:T a), r1 = r2 -> T_eq r1 r2.
> > > >
> > > > The intention is that for some r1:T a and r2:T b (where a and b might
> not
> > > > be
> > > > definitionally equal), T_eq r1 r2 iff a = b and r1 = r2.
> > > > The point is that the only way to construct T_eq is to construct with
> (r1
> > > > r2:T a) and a proof of r1 = r2.
> > > >
> > > > Which works fine until I want to make use of T_eq, ie what I want is
> the
> > > > following theorem:
> > > >
> > > > forall (a:nat) (r1 r2:T a), T_eq r1 r2 -> r1 = r2.
> > > >
> > > > So if I have a proof of T_eq r1 r2, I want to get back the proof of
> r1=r2.
> > > > But I can't seem to prove it.  I look at the elimination rule for
> T_eq:
> > > >
> > > > T_eq_ind =
> > > > fun (a : nat) (r1 : T a) (P : forall b : nat, T b -> Prop)
> > > >   (f : forall r2 : T a, r1 = r2 -> P a r2) (b : nat)
> > > >   (t : T b) (t0 : T_eq r1 t) =>
> > > > match t0 in (T_eq _ t1) return (P b0 t1) with
> > > > | T_eq_intro x x0 => f x x0
> > > > end
> > > >
> > > > The return type for the case analysis is (P b0 t1) for some P which,
> as
> > > > far
> > > > as I can see, cannot allow for the return type to be r1=r2, so how do
> I
> > > > get
> > > > back the proof of r1=r2?
> > > >
> > > > Thanks in advance.
> > > >
> > > > See
> > > >
> > > > --
> > > > View this message in context:
> > > >
> http://www.nabble.com/Newbie-question-%28Eliminating-some-dependent-types%29-tf3957584.html#a11229739
> > > > Sent from the Coq mailing list archive at Nabble.com.
> > > >
> > > >
> --------------------------------------------------------
> > > > Bug reports: http://coq.inria.fr/bin/coq-bugs
> > > > Archives: http://pauillac.inria.fr/pipermail/coq-club
> > > >           http://pauillac.inria.fr/bin/wilma/coq-club
> > > > Info:
> http://pauillac.inria.fr/mailman/listinfo/coq-club
> > > >
> > > Hi !
> > > I'm also quite new to coq but I've been playing with the equality on
> > > dependant types lately, so I'll do my best.
> > > The fact is when you have dependant equality, you can't always achieve
> the
> > > transition to the liepniz equality for every dependant types. A well
> known
> > > type family where this holds is when the equality is decidable. Can you
> > > prove on your type that:
> > > forall x y:T, {x=y}+{x<>y} ?
> > >
> > > I invite you to read the Logiv/Eqdep_dec.v file (especially Theorem
> > > eq_dep_eq_dec which I guess is what you're looking for)
> > >
> > > I hope it will help you,
> > >
> > > Regards
> > >
> > > Vincent Siles,
> > > master student (MPRI,Paris)
> > >
> > >
> --------------------------------------------------------
> > > Bug reports: http://coq.inria.fr/bin/coq-bugs
> > > Archives: http://pauillac.inria.fr/pipermail/coq-club
> > >           http://pauillac.inria.fr/bin/wilma/coq-club
> > > Info:
> http://pauillac.inria.fr/mailman/listinfo/coq-club
> > >
> >
> >
> > --
> > http://www.lix.polytechnique.fr/~zumkeller/
> >


--
http://www.lix.polytechnique.fr/~zumkeller/