Timeline for Pattern matching without K in agda
Current License: CC BY-SA 4.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 5, 2025 at 20:28 | comment | added | HPSmash77 | That is kinda what I said. also by proposition on x=y I mean a property on x=y (basically a function P : x=y -> Type). Not sure why i called them propositions back then | |
| Oct 31, 2025 at 10:17 | comment | added | Dominique Devriese | Sounds about right, you seem to be saying that you cannot obtain the effect of K using J, which is correct. | |
| Oct 24, 2025 at 12:53 | comment | added | HPSmash77 | Is the reasoning in my first comment correct? | |
| Oct 24, 2025 at 12:51 | comment | added | HPSmash77 | Not matching x=x with refl avoids this | |
| Oct 24, 2025 at 12:50 | comment | added | 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. | |
| Oct 24, 2025 at 12:39 | comment | added | 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).
|
|
| Oct 24, 2025 at 12:35 | vote | accept | HPSmash77 | ||
| Oct 24, 2025 at 12:54 | |||||
| Oct 24, 2025 at 12:31 | comment | added | 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.
|
|
| Oct 24, 2025 at 8:41 | answer | added | Naïm Camille Favier | timeline score: 1 | |
| Oct 24, 2025 at 8:40 | answer | added | Thomas Lamiaux | timeline score: 0 | |
| Oct 24, 2025 at 8:38 | history | edited | marc_s | CC BY-SA 4.0 |
deleted 1 character in body; edited title
|
| Oct 24, 2025 at 8:30 | history | edited | HPSmash77 |
edited tags
|
|
| S Oct 24, 2025 at 7:53 | review | Triage | |||
| Oct 24, 2025 at 10:40 | |||||
| S Oct 24, 2025 at 7:53 | history | asked | HPSmash77 | CC BY-SA 4.0 |