The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

Hi Gyesik,

On May 8, 2010, at 10:19 AM, Gyesik Lee wrote:
> I have encountered 3 three cases which I could handle with some
> reflection, but I think it would be interesting, not just for me, to
> know how you would solve them.
>
> Here are the three.
>
> 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?

I am considering an extension of type theory where this term would  
reduce, because

  H : x = x

is eta-expanded to refl_equal.

@InProceedings{abel:nbe09,
  author =       {Andreas Abel},
  title = 	 {Extensional Normalization in the Logical Framework with  
Proof Irrelevant Equality},
  booktitle = {Workshop on Normalization by Evaluation, affiliated to  
LiCS 2009, Los Angeles, 15 August 2009},
  year =         2009,
  editor =       {Olivier Danvy}
}

There is a prototypical implementation, MiniAgda:

  http://www2.tcs.ifi.lmu.de/~abel/miniagda/

> 2) It's about eq's polymorphism.
>
> Coq complained once that [nat = nat] is different from [nat = nat].
> Then using Set Printing All, I found out Coq was right because
>
> @eq Set nat nat and @eq Type nat nat are syntactically different.
>
> However how should I understand this apart from that syntactic  
> inequality?

This is a bit harder.  A priori, it is natural to assume these two  
types are different, in the same way as vect Set n and vect Type n are  
different.  The only reason why these type could be equal because they  
are both singleton sets, namely { refl_equal }.  But then, one would  
need a type theory that unifies all singletons, which smells very  
extensional.

Cheers,
Andreas

> 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.
>
> Thanks for any comments in advance.
>
> Gyesik

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/