1
$\begingroup$

It has been known that if a type $A$ has decidable equality, i.e., $\forall a b: A, a = b \vee a \neq b$, then we can happily say that any two proofs for $a = b$ must be identical. Sometimes, we will need to add this as an axiom for types that do not have decidable equality, but this would make the system inconsistent with univalence.

Given this, I'm seeking methods akin to Streicher's K Axiom, which asserts the uniqueness of identity proofs, but that are compatible with univalence. My interest lies particularly in adjustments or extensions to theorem provers (such as Coq) that enable features like dependent pattern matching in the absence of UIP, without compromising on univalence. Are there techniques or modifications that achieve this balance? Additionally, has there been work done to retrofit existing theorem provers to support these methods "natively"? I'm especially looking for examples or references to literature and implementations that address this challenge.

I know Agda provides us with an option --without-k, but this option makes the type-checking algorithm stricter and makes some case analyses impossible due to the elimination rule restriction over identity types.

Any suggestions or comments would be greatly appreciated!

$\endgroup$
12
  • 2
    $\begingroup$ Agda still has dependent pattern matching. What exactly do you want to recover from K? $\endgroup$
    – Trebor
    Commented Feb 6 at 5:17
  • 1
    $\begingroup$ Can you give an example as to when you "will need to add this as an axiom"? What kind of types do you want to add UIP for? $\endgroup$ Commented Feb 6 at 14:05
  • 1
    $\begingroup$ When you say "makes the algorithm stricter", do you mean you have met a specific spot where it annoys you, or is this just a general worry? If the latter, then I assure you that you don't even feel it unless you are genuinely using something that requires K. $\endgroup$
    – Trebor
    Commented Feb 6 at 16:22
  • 2
    $\begingroup$ Yes, Coq's pattern-matching is completely compatible with univalence, if that is what worries you. And Agda --without-K also is, and it is very expressive (nowadays I think most Agda users use it this way). There might be other reasons why one would want UIP (or, more generally, proof irrelevance), but I don't think that having a "good" pattern-matching is the main reason to do so these days. So I second @Trebor: unless you have a specific good reason, pattern-matching without K is usually quite good. $\endgroup$ Commented Feb 6 at 17:08
  • 1
    $\begingroup$ @AndrejBauer I guess you mean "compatible" rather than "equivalent"? $\endgroup$ Commented Feb 8 at 10:49

3 Answers 3

5
$\begingroup$

The question seems to boil down to the implicit assumption that pattern-matching needs uniqueness of identity proofs to work "well" (I will refrain from calling it "axiom K", because, as you note, UIP can be proven for quite a good class of types, those that HoTT-inclined people call hSets)

There was a time where this was the common conception, seemingly due to Coquand's original paper on the subject¹ relying on UIP under the hood. The important reference here is Eliminating Dependent Pattern-Matching, which reduces Coquand's pattern-matching to more "standard" constructs, including recursors for inductive types (the eliminators you naturally get when modelling inductive types, which are compatible with HoTT), and UIP. You have to remember that at the time HoTT and univalence had not landed, and so the whole understanding of the equality type and its higher structure were much less clear as today! Proving/needing UIP was not necessarily a bad thing, back then.

But then univalence happened, and baking in UIP became an issue rather than an advantage, at least in certain contexts. Fortunately, it can be avoided, as has been shown by Cockx in his PhD thesis. We lose a bit (certain things are not doable by pattern-matching any more), but not too much. And we regain compatibility with univalence. This is more or less what is implemented in Agda's pattern-matching, and as you suggest it had to be retrofitted in the system that before it proved UIP for all types. Coq's pattern-matching is much simpler, and corresponds much more closely to recursors. However, the Equations plugin basically implements Cockx's compilation scheme on top of vanilla pattern-matching. And, as noted by James in his answer, it is even able to use UIP when proven (or assumed axiomatically) to make pattern-matching stronger, similar to Coquand's original proposal.

So all in all, the right way to do pattern-matching these days seems to be by default without K, following Cockx, and is more than enough for most purposes. If you really want, you can throw in UIP when provable or when you want to assume it, but this gives you only relatively marginal improvements.

¹ Thierry Coquand, Pattern Matching with Dependent Types, Types 1992 (apparently there are no "official" stable sources for the paper, but it can easily be found on the internet)

$\endgroup$
3
$\begingroup$

The Equations package for Coq/Rocq provides pattern matching without K, as described by Cockx, Devriese, and Piessens and comparable to Agda --without-K, for all types. It also supports pattern matching with K on sets, as deduced via typeclasses and a deriving mechanism, when the Equations With UIP option is enabled.

Consider the following example. We first load the Equations package and instruct it to look for proven UIP instances. We then define a new type nat. For nat, we can derive NoConfusion (which is necessary for any Equations-based pattern matching on a type) and EqDec, which, as you observed, is enough to justify use of axiom K at type nat. We can observe that Equations makes use of pattern matching with K via a simple proof of K for nat, where really all of the hard work is done by Equations. Finally, we can see that the global axiom K was not used by the fact that Print Assumptions nat_K prints Closed under the global context, and the fact that plain Coq does not prove K for all types.

From Equations Require Import Equations.
Set Equations With UIP.

Inductive nat : Type := O | S (n : nat).
Derive NoConfusion for nat.
Derive EqDec for nat.

Equations nat_K {n : nat} (p : n = n) : p = eq_refl :=
| eq_refl => eq_refl.

Print Assumptions nat_K.
$\endgroup$
2
$\begingroup$

It looks like Meven's answer is what you want, but just to answer the core question as stated:

I'm seeking methods akin to Streicher's K Axiom, which asserts the uniqueness of identity proofs, but that are compatible with univalence

This is not possible in general. The whole premise of univalence is wondering "what if Refl wasn't the only identity proof?" And more specifically, "what if proofs of equality contained computational content?"

For example, with univalence there are two proofs that $Bool = Bool$: reflexivity, and the isomorphism given by $not$. If these two proofs are equal, then transporting along them is equal. But transporting $true$ along $Refl$ gives $true$, and along $not$ gives $false$. So then $true = false$, which is bad.

One option I see is having the default equality be the propositional trunctation of univalent equality. This would let you have all equality proofs of this truncation be equal, but the trick is that then you could only transport in ways that didn't depend on the computational content of the proofs. I don't know what the implication would be for pattern matching, it might give something like Cockx's "without K" system, but maybe with more flexibility in the case that you're producing an hProp as the result of pattern matching?

$\endgroup$
2
  • 1
    $\begingroup$ I think UIP is needed on the indices of the pattern-matching, not its codomain, so producing an hProp is not what helps. $\endgroup$ Commented Feb 8 at 21:36
  • $\begingroup$ @MevenLennon-Bertrand You're right, I think I had it backwards $\endgroup$ Commented Feb 8 at 22:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.