The Coq mailing list

[See <wongsee AT gmail.com>]

Thank you for your help.  I will look into JMeq_eq and btw I don't really
despise axioms per se as long as they are all consistent :-)

See


Roland Zumkeller-2 wrote:
> 
> 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/
> 
> --------------------------------------------------------
> 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
> 
> 

-- 
View this message in context: 
http://www.nabble.com/Newbie-question-%28Eliminating-some-dependent-types%29-tf3957584.html#a11241800
Sent from the Coq mailing list archive at Nabble.com.