Skip to main content
Stack Overflow
  1. About
  3. For Teams

You are not logged in. Your edit will be placed in a queue until it is peer reviewed.

We welcome edits that make the post easier to understand and more valuable for readers. Because community members review edits, please try to make the post substantially better than how you found it, for example, by fixing grammar or adding additional resources and hyperlinks.

Required fields*

Pattern matching without K in agda

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

Answer*

Draft saved
Draft discarded
Cancel
2
  • "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 Commented Oct 24, 2025 at 8:58
  • Well, no it isn't: it's the same as first generalising your goal to two distinct variables x and y, then pattern matching. Commented Oct 24, 2025 at 10:14

AltStyle によって変換されたページ (->オリジナル) /