CODEWITHSUNDEEP
coq
Grant Jurgensen
Grant Jurgensen

Reputation: 179

Why is UIP unprovable in Coq? Why does the match construct generalize types?

UIP (and equivalents like axiom K) must be added axiomatically in Coq if it is desired:

uip : ∀ A (x y: A) (p q: x = y), p = q

This is surprising, since it appears obvious from the definition of equality, which only has one constructor. (This of course rests on the interpretation that an inductive definition in Coq captures all elements of its type).

When one tries to prove UIP, one gets stuck on the reflexive subcase:

uip_refl : ∀ A (x: A) (h: x = x), h = eq_refl x

We might hope the following term would be an appropriate proof term:

fun A (x: A) (h: x = x) =>
  match h as h0 in (_ = a) return (h0 = eq_refl x) with
    | eq_refl _ => eq_refl (eq_refl x)
  end

This fails because it is ill-typed. We know that h: x = x, but when we match on the term, we lose the reflexivity information and it is generalized to h0: x = a. As a result, our return type h0 = eq_refl x is ill-typed.

Why is it that the match construct generalizes our type here? Would a non-generalizing alternative be tractable?

Upvotes: 3

Views: 330

Answers (2)

Li-yao Xia
Li-yao Xia

Reputation: 33569

Would a non-generalizing alternative be tractable?

There is precedent for such a match. It is provided in readily available extensions of Coq (in Program; it's also an option in the Equations plugin). Agda also typechecks pattern-matches in a similar manner (if --with-K is enabled, which is the default).

As you've shown, you can define UIP with it, so all the reasons for not adopting UIP carry over to not adopting that match. Conversely that match can be compiled to a term using UIP, as is done by Program and Equations.

I can't really explain why "generalization" makes a difference though. I would bet the answer is in Conor McBride's thesis.

Upvotes: 1

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23622

As hinted in my previous answer, the eliminator for equality in Coq inherits this behavior from intensional type theory, where it was introduced to keep type checking decidable. However, later people realized that it is possible to have an elimination principle for equality that validates axiom K without ruining decidability. This is not implemented in Coq, but it is implemented in Agda:

module Test where

{- Equality type -}

data _≡_ {A : Set} (a : A) : A → Set where
  refl : a ≡ a

{- Proving K by pattern matching -}

K : {A : Set} → (a : A) → (p : a ≡ a) → p ≡ refl
K a refl = refl

(The equation for K is the moral equivalent of the | eq_refl => ... branch in Coq.) I am not entirely sure how Agda checks this definition, but I have the impression that it does not require a generalization step as Coq does.

Upvotes: 1

Related Questions