The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Le 30/01/2014 05:31, Abhishek Anand a écrit :

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/

Hi.

The definition is given on http://coq.inria.fr/distrib/current/refman/Reference-Manual006.html#sec171 :

"

Convertibility.

Let us write E[Γ] ⊢ t ▷ u for the contextual closure of the relation t reduces to u in the environment E and context Γ with one of the previous reduction β, ι, δ or ζ.

We say that two terms t₁ and t₂ are βιδζη-convertible, or simply convertible, or equivalent, in the environment E and context Γ iff there exist terms u₁ and u₂ such that E[Γ] ⊢ t₁ ▷ … ▷ u₁ and E[Γ] ⊢ t₂ ▷ … ▷ u₂ and either u₁ and u₂ are identical, or they are convertible up to η-expansion, i.e. u₁ is λ x:T.  u′₁ and u₂ x is recursively convertible to u′₁, or, symmetrically, u₂ is λ x:T.  u′₂ and u₁ x is recursively convertible to u′₂. We then write E[Γ] ⊢ t₁ =_βδιζη t₂."

It is not exactly defined as a least congruence (which always exist since powersets are complete lattices) but it is not too difficult to check that it is indeed a congruence (▷ is the contextual closure of the reduction relations).

Best regards,

Frédéric.