coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gyesik Lee <gslee AT ropas.snu.ac.kr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] eq_rect, proof-irrelevance, JMeq and rewriting
- Date: Mon, 10 May 2010 10:52:21 +0900
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:content-type; b=OYIAyDF25GHZFjMZVBnF5MYWZ1eGyy20vmW+0evIPJD5MUeZbwZHExCKY4ML12v0rv FfdFHALV9aDmQOSotKNricGjVUq9YNBoCTX8JkVy+W+L4czOO/MHF/Xem/3JerTkaei+ uPN0rcG2I2J4Nms18VeADiv9wyPNqMgMiBakM=
Dear Andreas, Yves and Chung-Kil,
many thanks for the explanation.
Your answers gave me a brief overview of the current state of the art.
Cheers,
Gyesik
PS. Concerning 3. question, I almost expected Chung-Kil's answer. I
will try Heq.
2010/5/10 Chung Kil Hur
<Chung-Kil.Hur AT pps.jussieu.fr>:
> Hi Gyesik,
>
>>
>> 1) For a term construction, assume you have used eq_rect with a proof
>> H as in the following
>>
>> eq_rect x P t x H
>>
>> But if H is not syntactically equal to refl_equal, then simpl tactic
>> won't convert the term above to t.
>> Is proof-irrelevance necessary to get the reduction?
>>
>
> You don't need the general proof irrelevance.
> You just need a much weaker assumption, the uniqueness of identity
> proof~(UIP),
> or equivalently Streicher's Axiom K, to derive H = refl_equal.
> Actually, in Agda, this axiom is internalized (ie, H is convertible to
> refl_equal) and
> I heard that it is going to be internalized in a later version of Coq as
> well.
>
>>
>> 3) Assume the goal is to show
>>
>> JMeq t s
>>
>> and you know t = t'. Is there any tactic which functions like rewrite
>> for the usual equality?
>> You could work with JMeq_ind, and there are some explanations in
>> CoqArt, Section 8.2.7, how to deal with it.
>> But I am wondering if some tactics have been developed in the meantime.
>>
>
> If your question is about rewriting tactics for JMeq, I developed something
> similar.
> The library Heq supports rewriting of heterogeneous equality.
> You can find it in the following address.
> http://www.pps.jussieu.fr/~gil/Heq
> But, you should use equality on dependent pairs instead of JMeq, which is
> usually not a big deal.
>
> Cheers,
> Chung-Kil Hur
>
- [Coq-Club] eq_rect, proof-irrelevance, JMeq and rewriting, Gyesik Lee
- Re: [Coq-Club] eq_rect, proof-irrelevance, JMeq and rewriting, Andreas Abel
- Re: [Coq-Club] eq_rect, proof-irrelevance, JMeq and rewriting, Yves Bertot
- Re: [Coq-Club] eq_rect, proof-irrelevance, JMeq and rewriting,
Chung Kil Hur
- Re: [Coq-Club] eq_rect, proof-irrelevance, JMeq and rewriting, Gyesik Lee
Archive powered by MhonArc 2.6.16.