Pattern matching without K in agda

Question

I was trying to prove K (with without-K) using J to see what goes wrong when we try to do that.

That's all well and good, but in the process of playing around I noticed that agda refuses to match with refl any term (that I tried) of type Id A x x (saying something along the lines of "can't unify x1 ≟ x1").

For example, agda refuses to case split on p in the following example:

data 1 : Type where
 * : 1
test : {l : Level} {A : Type l} -> (x : A) -> (p : x ≡ x) -> 1
test {l} {A} x p = ?

but the following snippet is fine:

data 1 : Type where
 * : 1
test : {l : Level} {A : Type l} -> (x : A) -> (p : x ≡ x) -> 1
test {l} {A} x p = J {A = A} {x = x} (λ y path -> 1) {y = x} p *

Isn't using J here like this essentially the same as case-splitting on p and assuming it to be refl? If yes, then why does agda refuse to split on p in the earlier example?

For reference the type of the J rule being used is this:

J : {A : Set a} {x : A} (B : (y : A) → x ≡ y → Set b)
 {y : A} (p : x ≡ y) → B x refl → B y p

• Dominique Devriese: They're not "essentially the same" because in your use of J, you don't use the type information you learn from the dependent pattern match. A better challenge would be to try to prove test : {l : Level} {A : Set l} -> (x : A) -> (p : x ≡ x) -> p ≡ refl using J. It's obviously easy if you allow pattern matching with K. Note that this challenge requires you to use the fact that p must be reflexivity, something you learn from the pattern match on p.
• Naïm Camille Favier: To put what @DominiqueDevriese said in another way: your use of J could be replaced with an equivalent use of subst, and the version of subst in which x and y are judgementally equal is obviously derivable without K (you just ignore the path x ≡ x and return the identity function P x → P x).
• HPSmash77: @DominiqueDevriese I had tried to do exactly that (knowing that it requires K) before asking this question. The reason I asked this question was to know why we have to reject pattern matching on x=x to make our system such that it doesn't use K. I may be wrong, but what I'm picking up is that J allows us to prove propositions on x=y, but when we pattern match on x=x, we are proving a proposition on x=x using J, which looks something like J (λ y path -> P path) [...], where P : x=x -> Type. But this is a type error as P cannot be applied to path as it is of type x=y, not x=x.
• HPSmash77: Not matching x=x with refl avoids this
• HPSmash77: Is the reasoning in my first comment correct?

Answer 1

Your use of J is roughly equivalent to defining a helper function that pattern matches on a fully general path p : x ≡ y, then calling it with y = x:

test : {l : Level} {A : Type l} -> (x : A) -> (p : x ≡ x) -> 1
test {l} {A} x p = test' {y = x} p where
 test' : {y : A} -> (p : x ≡ y) -> 1
 test' refl = *

• HPSmash77: "Your use of J is roughly equivalent to defining a helper function that pattern matches on a fully general path p : x ≡ y, then calling it with y = x" That it is, what I'm asking is, isn't my use of J essentially the same as case splitting p and assuming it to be refl
• Naïm Camille Favier: Well, no it isn't: it's the same as first generalising your goal to two distinct variables x and y, then pattern matching.

Answer 2

y in x = y must be a free variable as it is quantified in B : (y : A) → x ≡ y → Set b for this reasin it can not be specialize to x when doing an induction. So if you want to prove sth for equality, you must first prove sth for x = y to deduce it for x = x, which is not possible for UIP / axiom K.

• HPSmash77: Can you please expand on this a little more?
• Thomas Lamiaux: Here B : (y : A) → x ≡ y → Set b y is quantified so it can not be a specific value