The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

All of the rules are directed, and thus together define a normalization procedure (which results from repeatedly applying them).  (There is some trickiness with eta for functions, but that is not hard to reason about after the fact.)  It is extremely nontrivial to prove that this normalization procedure is terminating and confluent (that all valid sequences of rule applications result in the same normal form), but these are the two necessary and interesting properties for the standard meta-theoretic presentation, and for computation/evaluation to work.  The proof technique is called logical relations, and the major components of the proof are called progress and preservation.  Once you have that proof in hand, judgmental equality is just the minimal reflexive (syntactic) relation on normal forms, and this is obviously a congurence.

To answer your question about the existence of such a congruence, it is always possible to construct the reflexive transitive symmetric closure of a relation, and if your relation is proof-irrelevant, it'll be minimal almost by definition.

-Jason

On Jan 29, 2014 11:32 PM, "Abhishek Anand" <abhishek.anand.iitg AT gmail.com> wrote:

I've seen the definitional equality of Coq being presented
as a bunch of (mainly computational) rules, e.g. http://adam.chlipala.net/cpdt/html/Equality.html

I've never seen a proof that it is actually a congruence.
Is it just defined as the least congruence containing a bunch
of greek rules? If so, why would such a least relation exist?
(I guess it can be meta-theoretically written as strictly positively inductively defined relation?)

Or, is it completely specified first and then proved to be a congruence? (e.g. in the style of http://www.cs.cornell.edu/Info/Projects/NuPrl/documents/Howe/howeEqualityinLazy_LICS98.ps)

Or something else?

Thanks,
-- Abhishek
http://www.cs.cornell.edu/~aa755/