--- Day changed Thu Dec 28 2017 | ||

trikl[m] | ReinH: indeed! | 28/12 17:19 |
---|---|---|

trikl[m] | I had a great time doing most of it, but I was stuck in a couple of places for quite some time | 28/12 17:21 |

trikl[m] | About my last question: if I know that `(z ,- []) <[ z ,- xs ]> ys` and `xs ~ ys` I should be able to proof that `xs == ys` and make use of that either as a rewrite or as a view to show the typechecker that `sl` is the only possible constructor for the aforementioned splitting (right?). But I don't know how to go about proving it. | 28/12 18:14 |

trikl[m] | s/proof/prove/ | 28/12 18:15 |

trikl[m] | This is to show that id absorption on the left holds for the transitivity of permutations | 28/12 18:19 |

mietek | trikl[m]: what is `_~_`? | 28/12 19:16 |

trikl[m] | I forgot to define that, sorry. `xs ~ ys` means `ys` is a permutation of `xs`. http://lpaste.net/4907442324037959680 | 28/12 19:25 |

mietek | trikl[m]: what is the theorem you’re trying to prove? | 28/12 19:28 |

trikl[m] | That `{xs ys : List X}(f : xs ~ ys) transP reflP f` where `transP` is transitivity for permutations and `reflP` is the identity permutation | 28/12 19:33 |

trikl[m] | Sorry, that `transP reflP f == f` | 28/12 19:33 |

trikl[m] | Identity absorption on the left | 28/12 19:34 |

mietek | side note: it is useful to write transitivity laws infix | 28/12 19:34 |

trikl[m] | This is because I want to show that lists as objects and permutations as arrows form a category | 28/12 19:34 |

trikl[m] | Noted! This is the way the exercise is set though | 28/12 19:35 |

mietek | https://gist.github.com/mietek/00af5865d819a5ed0b351acb74a57b90 | 28/12 19:35 |

mietek | in the spirit of showing that things form categories | 28/12 19:36 |

pgiarrusso | trikl[m]: whenever I'm curious about your question, I get stuck because I find no context, and I don't know what ....<[...]>... is supposed to be | 28/12 19:41 |

trikl[m] | I believe that was pasted on my previous message: http://lpaste.net/361135 | 28/12 19:42 |

mietek | I believe pgiarrusso is asking about the intended meaning of the datatype | 28/12 19:42 |

pgiarrusso | indeed | 28/12 19:42 |

mietek | I’m reading `ls <[ ms ]> rs` as evidence that `ms` can be decomposed into two parts, `ls` and `rs` | 28/12 19:43 |

mietek | and so, the method by which we can decompose `ms` | 28/12 19:43 |

mietek | some elements of `ms` go into the left part, `ls`; other elements go into the right part, `rs` | 28/12 19:43 |

pgiarrusso | OK, thanks | 28/12 19:43 |

mietek | not sure if this is correct | 28/12 19:44 |

pgiarrusso | and the elements are split preserving order | 28/12 19:44 |

trikl[m] | mietek: Exactly. For example, `sl (sr sz)` means the given list `ms` can be constructed by taking the first element from `ls`, the second from `rs` and then stopping | 28/12 19:44 |

trikl[m] | pgiarrusso: yes | 28/12 19:44 |

pgiarrusso | so this resembles a bit what happens in the merge phase of mergesort (if we drop ordering) | 28/12 19:45 |

pgiarrusso | OK, that answers my question, thanks | 28/12 19:45 |

mietek | `_,-_` is pure evil | 28/12 19:45 |

mietek | notation-wise | 28/12 19:45 |

trikl[m] | The issue I have is with showing that `reflP` can only be constructed with splittings that take the first element from the left and the rest from the right | 28/12 19:46 |

mietek | trikl[m]: I’m getting there; had to rewrite the definitions so that I can read them | 28/12 19:46 |

pgiarrusso | OK, I suspect your earlier question was correct | 28/12 19:46 |

trikl[m] | Thanks for the help people :) | 28/12 19:46 |

pgiarrusso | and that you shouldn't need to know that xs and us are permutations | 28/12 19:47 |

trikl[m] | Then I don't see why Agda doesn't know that `(z ,- []) <[ z ,- xs ]> ys` can only be built with `sl` | 28/12 19:48 |

trikl[m] | And that it implies `xs == ys` | 28/12 19:48 |

trikl[m] | Well, the second I can understand, but not why it doesn't see `sl` is the only possible constructor | 28/12 19:49 |

pgiarrusso | well, the proof might need induction on xs/ys, or be more complicated | 28/12 19:49 |

pgiarrusso | you sound like you're expecting a non-existent sufficiently smart Agda | 28/12 19:50 |

trikl[m] | Hah yeah | 28/12 19:50 |

pgiarrusso | anyway, gotta go, and mietek's working on a solution | 28/12 19:50 |

pgiarrusso | bbl | 28/12 19:50 |

trikl[m] | But what bugs me is that I can't see how to proceed | 28/12 19:50 |

trikl[m] | Thanks pgiarrusso ! | 28/12 19:51 |

mietek | is the definition of the permutation datatype also given in the exercise? | 28/12 19:51 |

trikl[m] | Yes | 28/12 19:51 |

trikl[m] | I would not think of that devil myself, yet | 28/12 19:51 |

trikl[m] | mietek: I'm curious, how did you rewrite the permutation datatype? | 28/12 19:53 |

{AS} | trikl[m]: you can take a look at concepts like bag equality | 28/12 19:57 |

{AS} | for permutations | 28/12 19:57 |

trikl[m] | Cheers | 28/12 19:58 |

{AS} | trikl[m]: http://www.cse.chalmers.se/~nad/publications/danielsson-bag-equivalence.pdf | 28/12 19:58 |

mietek | …although I would be surprised if that was part of solving the exercise… | 28/12 19:58 |

mietek | trikl[m]: how did you define the identity permutation? | 28/12 19:58 |

{AS} | I did not read far enough back :) | 28/12 19:58 |

trikl[m] | Sorry, I didn't actually paste that | 28/12 19:59 |

trikl[m] | http://lpaste.net/7901978872399265792 | 28/12 19:59 |

mietek | trikl[m]: and what is srs? | 28/12 20:00 |

trikl[m] | http://lpaste.net/7723693375488000000 | 28/12 20:00 |

mietek | another side note: a single paste containing all of your working code is preferred | 28/12 20:01 |

trikl[m] | Yes, I'm slowly becoming aware of that | 28/12 20:01 |

trikl[m] | It's just that my original question needed a lot less context than the evolved explanation | 28/12 20:01 |

mietek | that’s what you think :) | 28/12 20:01 |

trikl[m] | Haha | 28/12 20:02 |

trikl[m] | Sorry, I'll be back in 15 minutes tops | 28/12 20:02 |

mietek | no worries | 28/12 20:02 |

trikl[m] | I'm back | 28/12 20:09 |

mietek | trikl[m]: and… how did you show transitivity? | 28/12 20:18 |

mietek | it doesn’t seem easy | 28/12 20:18 |

trikl[m] | It's a little tricky yes | 28/12 20:19 |

trikl[m] | I will put together a paste with all of it | 28/12 20:19 |

trikl[m] | http://lpaste.net/6667239331725312000 | 28/12 20:24 |

trikl[m] | So this is all of it | 28/12 20:24 |

mietek | omg | 28/12 20:24 |

trikl[m] | But it boils down to: `sl` is the only constructor that can build `(l ,- ls) <[ l ,- ms ]> rs`, why is `sr` also present when pattern matching on such a type | 28/12 20:25 |

mietek | you missed: List, +L | 28/12 20:25 |

mietek | `_+L_` that is, then probably Conor’s personal library for `Sg` and `_*_` | 28/12 20:26 |

trikl[m] | Yeah… `_+L_` is list concatenation, `Sg` is the dependent tuple for which `_*_` is a constructor | 28/12 20:27 |

trikl[m] | `Sg` standing for sigma | 28/12 20:27 |

mietek | I can guess that | 28/12 20:27 |

mietek | but I’d rather just load the code | 28/12 20:27 |

mietek | :) | 28/12 20:27 |

trikl[m] | http://lpaste.net/1216983342713405440 | 28/12 20:28 |

trikl[m] | Sorry, `_*_` is the non-dependent tuple | 28/12 20:30 |

mietek | you could’ve said https://github.com/pigworker/CS410-17/tree/master/exercises | 28/12 20:30 |

trikl[m] | I would still need to paste my answers too | 28/12 20:31 |

mietek | yep, but at least then they typecheck | 28/12 20:32 |

mietek | I’m not trying to be annoying; I want to help, but I can’t unless I can see what’s going on :) | 28/12 20:32 |

trikl[m] | I know, and you are right | 28/12 20:33 |

mietek | these are pretty advanced exercises indeed | 28/12 20:34 |

mietek | “Invent other useful operations which transform splittings.” | 28/12 20:35 |

mietek | :) | 28/12 20:35 |

trikl[m] | I like the type of exercise though | 28/12 20:35 |

trikl[m] | Hour hands were hold with the previous two | 28/12 20:36 |

trikl[m] | Sorry, Our* | 28/12 20:36 |

mietek | trikl[m]: so the precise theorem you wanted to show was `goal : {X : Set}{xs ys : List X} -> (f : xs ~ ys) -> transP reflP f == f` ? | 28/12 20:38 |

trikl[m] | Yes | 28/12 20:38 |

trikl[m] | `reflP` could be substituted by `xs ~ xs` too | 28/12 20:38 |

mietek | you mean, an arbitrary proof of `xs ~ xs`? | 28/12 20:39 |

trikl[m] | Yes, by any `g : xs ~ xs` | 28/12 20:39 |

mietek | 18:14 trikl[m]About my last question: if I know that `(z ,- []) <[ z ,- xs ]> ys` and `xs ~ ys` I should be able to proof that `xs == ys` and make use of that either as a rewrite or as a view to show the typechecker that `sl` is the only possible constructor for the aforementioned splitting (right?). But I don't know how to go about proving it. | 28/12 20:42 |

trikl[m] | What about it? | 28/12 20:45 |

mietek | trying to figure out how you got there | 28/12 20:47 |

trikl[m] | Do I actually require a proof of `xs == ys`? | 28/12 20:47 |

mietek | well, what you wrote above could be stated as a `lemma : {X : Set}{xs ys : List X}{z : X} -> (z ,- []) <[ z ,- xs ]> ys -> xs ~ ys -> xs == ys` | 28/12 20:47 |

mietek | have you tried proving it? | 28/12 20:48 |

mietek | and then, you could “show the typechecker” by pattern-matching on the result of applying the lemma | 28/12 20:48 |

trikl[m] | If I pattern match on any `g : xs ~ xs` I get `s ,- p` where `s` is of type `(z ,- []) <[ z ,- xs ]> ys`. If I try to pattern match on `s` I get `sl s` and `sr s`, but I should be able to show that `sr s` is absurd | 28/12 20:48 |

trikl[m] | I tried, briefly, and didn't succeed | 28/12 20:49 |

mietek | sorry — no idea where to attach your previous comment | 28/12 20:49 |

trikl[m] | i was not sure that was the correct path to follow | 28/12 20:49 |

mietek | oh — so you’re talking about proving `goal2 : {X : Set}{xs ys : List X} -> (f : xs ~ ys) (g : xs ~ xs) -> transP g f == f` | 28/12 20:50 |

trikl[m] | > Do I actually require a proof of xs == ys? | 28/12 20:50 |

trikl[m] | It was an explanation to this | 28/12 20:50 |

trikl[m] | Yes | 28/12 20:50 |

trikl[m] | That way I can also pattern match on `g` | 28/12 20:50 |

mietek | I suppose you can, but what does that give you? :) | 28/12 20:50 |

mietek | I’d rather ask, have you considered the other direction? | 28/12 20:51 |

mietek | `goal3 : {X : Set}{xs ys : List X} -> (f : xs ~ ys) -> transP f reflP == f`? | 28/12 20:51 |

trikl[m] | No, not yet | 28/12 20:52 |

mietek | one could be easier than the other | 28/12 20:52 |

mietek | (I don’t know in this specific case) | 28/12 20:52 |

trikl[m] | I should be able to proof both without making use of the fact that permutations are symmetric though | 28/12 20:53 |

trikl[m] | So I can't use one to prove the other | 28/12 20:53 |

trikl[m] | But yeah, I should explore that road too | 28/12 20:53 |

mietek | in general, I would expect that if proving transitivity is this hairy, proving properties of transitivity will be at least the same amount of hairy | 28/12 20:54 |

mietek | I’m sorry I can’t be of more help | 28/12 20:55 |

trikl[m] | That's ok. But what bugs me is the pattern matching against `(z ,- []) <[ z ,- xs ]> ys` and getting both constructors `sl` and `sr` | 28/12 20:57 |

mietek | if you could paste the exact code where you’re getting it… | 28/12 20:57 |

trikl[m] | I don't understand why that happens | 28/12 20:57 |

trikl[m] | http://lpaste.net/6542860987253391360 | 28/12 20:59 |

mietek | I don’t understand how this code maps to what you just said | 28/12 21:01 |

trikl[m] | http://lpaste.net/668484850436538368 | 28/12 21:02 |

trikl[m] | That's why I said the last case is absurd | 28/12 21:02 |

trikl[m] | Or impossible | 28/12 21:02 |

trikl[m] | I guess I should send Conor an email with these questions | 28/12 21:04 |

mietek | you may get a better chance at a response to a tweet | 28/12 21:05 |

trikl[m] | I don't want to use Twitter though | 28/12 21:05 |

trikl[m] | It's centralised and proprietary | 28/12 21:05 |

trikl[m] | And they don't even offer RSS feeds, which is just plain mean | 28/12 21:06 |

mietek | it’s irrelevant to the problem of getting a response | 28/12 21:06 |

trikl[m] | I don't think of my principles as irrelevant :) | 28/12 21:06 |

mietek | I regret offering advice already :) | 28/12 21:07 |

trikl[m] | I'd rather send an email that doesn't get any response | 28/12 21:07 |

trikl[m] | Haha | 28/12 21:07 |

trikl[m] | The advice was good | 28/12 21:07 |

trikl[m] | I just can't use it | 28/12 21:07 |

mietek | I’m wondering why you think the `sr` case is absurd | 28/12 21:09 |

trikl[m] | To construct something of type `xs ~ xs` you can only prepend things to the start of both lists | 28/12 21:10 |

trikl[m] | So the splitting you give indicating where on the right hand side of the permutation the element is should always say it's on the far left, the first element | 28/12 21:10 |

mietek | that’s not quite what the constructors of `_~_` say | 28/12 21:10 |

mietek | first, `[] ~ []` holds | 28/12 21:11 |

trikl[m] | Wait, what I said is irrelevant | 28/12 21:11 |

mietek | oh, also, why are you talking about `xs ~ xs` | 28/12 21:11 |

mietek | you’re not pattern-matching on `g` | 28/12 21:11 |

trikl[m] | What matters is the constructors of `_<[_]>_` | 28/12 21:11 |

trikl[m] | Yes, sorry, got carried away by other ideas in my head | 28/12 21:11 |

mietek | ok | 28/12 21:12 |

trikl[m] | How can `sr` build something of type `(z ,- []) <[ z ,- xs ]> xs`? | 28/12 21:12 |

trikl[m] | Is it not only `sl` that can do that? | 28/12 21:12 |

mietek | http://lpaste.net/6220784520757510144 | 28/12 21:13 |

mietek | I’ve identified two absurd possibilities | 28/12 21:14 |

mietek | but not one that would rule out using `sr` | 28/12 21:14 |

mietek | I don’t feel like I understand the datatypes involved, though | 28/12 21:14 |

trikl[m] | I think you are confusing things | 28/12 21:14 |

trikl[m] | I'm talking about disproving `sr` but in the case of `g` | 28/12 21:14 |

trikl[m] | I'm pattern mathing against something of type `xs ~ xs` (`reflP`) | 28/12 21:15 |

mietek | oh. you are. | 28/12 21:15 |

mietek | I don’t see why, though | 28/12 21:15 |

mietek | the theorem should also hold for reflP | 28/12 21:16 |

trikl[m] | Yes, because `reflP` is of type `xs ~ xs` | 28/12 21:16 |

trikl[m] | http://lpaste.net/6542860987253391360 | 28/12 21:16 |

trikl[m] | I pattern match against `g : xs ~ xs` to be able to proof that | 28/12 21:16 |

mietek | yes, so this tells me that we should be able to prove it for the special case of `reflP` | 28/12 21:16 |

trikl[m] | Yes, we should | 28/12 21:17 |

trikl[m] | I just ignore how | 28/12 21:17 |

mietek | my intuition is telling me to start with that | 28/12 21:17 |

trikl[m] | There is nothing in `xs ~ xs` that isn't represented by `reflP`, so as far as I understand both proofs should be interchangeable | 28/12 21:18 |

trikl[m] | I will give that another go | 28/12 21:18 |

trikl[m] | But I remember the frustration :D | 28/12 21:18 |

mietek | I expect that if indeed `xs ~ xs` is uniquely inhabited, this would be provable | 28/12 21:19 |

mietek | examples of other uniqueness properties: https://mietek.github.io/coquand/html/Section3.html#uniq∋ | 28/12 21:19 |

trikl[m] | Do those work by showing that for any element in the type, that element is equal to the unique element? | 28/12 21:21 |

mietek | `uniqP : {X : Set}{xs : List X} -> (p q : xs ~ xs) -> p == q` | 28/12 21:22 |

trikl[m] | Oh right | 28/12 21:22 |

mietek | for any two elements in the type, they are structurally identical | 28/12 21:23 |

trikl[m] | I'm just wondering what `{p : xs ~ xs} -> p == reflP` would mean compared to that | 28/12 21:23 |

trikl[m] | As in: are they equal in strength? | 28/12 21:24 |

mietek | on the meta-level, both this question and the one about transitivity with `xs ~ xs` and with `reflP` are similar | 28/12 21:24 |

pgiarrusso | semi-sleepy, but I’m back for a bit | 28/12 21:25 |

mietek | trikl[m]: how do you measure strength? | 28/12 21:25 |

pgiarrusso | let me point out that, IMHO, you shouldn’t be talking about permutations... | 28/12 21:25 |

pgiarrusso | I think at least | 28/12 21:26 |

mietek | pgiarrusso: before you say anything, https://github.com/pigworker/CS410-17/blob/master/exercises/Ex3.agda#L108 | 28/12 21:26 |

trikl[m] | > trikl[m]: how do you measure strength? | 28/12 21:26 |

mietek | trikl[m]: ultimately, what we’re doing here is manipulating trees according to rules | 28/12 21:26 |

trikl[m] | If a proof p is able to proof everything that a proof q is able and more, I would say that intuitively p is stronger | 28/12 21:26 |

mietek | trikl[m]: if the rules we’ve got allow us to obtain the same resulting tree by more than one route, great | 28/12 21:27 |

mietek | trikl[m]: some routes are quicker than others | 28/12 21:27 |

pgiarrusso | trikl[m]: “p is stronger than q” is language for “p implies q” | 28/12 21:28 |

pgiarrusso | mietek: uh | 28/12 21:28 |

trikl[m] | > let me point out that, IMHO, you shouldn’t be talking about permutations... | 28/12 21:28 |

trikl[m] | I think so too. It's either solving the issue about the pattern matching against `sl srs` splittings or completing the theorem without pattern matching against them | 28/12 21:28 |

trikl[m] | > trikl[m]: “p is stronger than q” is language for “p implies q” | 28/12 21:29 |

trikl[m] | Oh yes! | 28/12 21:29 |

mietek | trikl[m]: in that case, clearly `{p : xs ~ xs} -> p == reflP` follows from `uniqP` | 28/12 21:29 |

trikl[m] | Yes | 28/12 21:29 |

mietek | trikl[m]: it’s not obvious to me if the converse is true, but perhaps it also is | 28/12 21:29 |

trikl[m] | But I wonder if it goes the other way too | 28/12 21:30 |

mietek | trikl[m]: it could be fun to prove that | 28/12 21:30 |

trikl[m] | On my way! | 28/12 21:30 |

mietek | but getting back to your original question, I really think it’s a matter of understanding the datatypes involved | 28/12 21:30 |

mietek | because Agda will only see absurdities if things are set up properly | 28/12 21:30 |

pgiarrusso | trikl[m]: again, many things are absurd but aren’t recognized as “immediately absurd” by Agda — and only immediately absurd things are rejected during pattern matching | 28/12 21:31 |

mietek | I don’t even see the absurdity you were trying to point out | 28/12 21:31 |

trikl[m] | The issue is then that I don't know how to show Agda that you can't make something of type `(z ,- []) <[ z ,- xs ]> ys` with an `sr` constructor | 28/12 21:32 |

mietek | are you sure you can’t? | 28/12 21:32 |

trikl[m] | No, because if I were I would know how to proof I can't | 28/12 21:32 |

trikl[m] | But I guess I don't know how to proof you can't do things, in Agda | 28/12 21:33 |

pgiarrusso | trikl[m]: for instance, it’s been proved there’s no solution to x^n + y^n = z^n with n > 2, but Agda won’t easily know that :-) | 28/12 21:33 |

pgiarrusso | trikl[m]: have you seen how to define negation? | 28/12 21:33 |

pgiarrusso | and how to prove negation? | 28/12 21:33 |

trikl[m] | pgiarrusso: But in this case it's the splitting constructors that have this types | 28/12 21:33 |

trikl[m] | In general, yes, but not in Agda | 28/12 21:34 |

pgiarrusso | OK, that seems relevant | 28/12 21:35 |

pgiarrusso | but before that, I’d like to look more closely at this result | 28/12 21:35 |

trikl[m] | Also, sorry for the multiple mistakes involving the noun proof and the verb to prove | 28/12 21:36 |

pgiarrusso | thanks but, at least I understood you anyway :-) | 28/12 21:37 |

pgiarrusso | *no comma | 28/12 21:37 |

trikl[m] | So how do you use negation to tell Agda not to go down a particular path? | 28/12 21:48 |

pgiarrusso | trikl[m], I stand corrected: you *can* instantiate type (z ,- []) <[ z,- xs ]> ys for particular values | 28/12 21:49 |

trikl[m] | In a way similar to how you use views? | 28/12 21:49 |

pgiarrusso | sorry, you can instantiate it with sr | 28/12 21:49 |

pgiarrusso | and when you first figured you can, you were right | 28/12 21:49 |

pgiarrusso | in particular, looking for such a solution by solving the equalities that arise | 28/12 21:49 |

pgiarrusso | and with a touch of fantasy | 28/12 21:49 |

trikl[m] | Haha | 28/12 21:49 |

trikl[m] | So I have to use both the infamous splitting and `xs ~ ys`? | 28/12 21:50 |

pgiarrusso | you can for instance instantiate (z ,- []) <[ z ,- z ,- xs’ ]> z ,- xs’ | 28/12 21:50 |

trikl[m] | (To show that `sl` is the way?) | 28/12 21:50 |

pgiarrusso | but sl isn’t the only way | 28/12 21:50 |

pgiarrusso | in the instance I gave you, you *can* start with sr | 28/12 21:51 |

trikl[m] | Oh | 28/12 21:51 |

pgiarrusso | then use sl | 28/12 21:51 |

trikl[m] | Now I see | 28/12 21:51 |

trikl[m] | All my past days were a lie | 28/12 21:51 |

trikl[m] | Or a half discovered truth | 28/12 21:51 |

pgiarrusso | your other question on negation is still good, it’s just not the one you need next | 28/12 21:51 |

pgiarrusso | let’s press on the half-discovered truth | 28/12 21:52 |

pgiarrusso | first, do you buy what I wrote? | 28/12 21:52 |

trikl[m] | It's already in my pocket! | 28/12 21:52 |

pgiarrusso | LOL | 28/12 21:52 |

trikl[m] | Sorry, we are students of Conor McBride after all | 28/12 21:53 |

trikl[m] | Plus, we live in Glasgow | 28/12 21:53 |

pgiarrusso | to explain this in words: if the merging of two lists is z ,- xs, the first list is z ,- [], and the second is ys, maybe we *did* merge them by picking the start of ys, because it also starts with z | 28/12 21:53 |

pgiarrusso | mietek: ^^ | 28/12 21:53 |

trikl[m] | Yes | 28/12 21:53 |

pgiarrusso | trikl[m]: so can I assume you learned about unification and how pattern matching uses unification? | 28/12 21:54 |

pgiarrusso | I haven’t seen the course and I don’t know if you’ve seen this with those words | 28/12 21:54 |

trikl[m] | Only intuitively | 28/12 21:54 |

pgiarrusso | well, that’s good enough | 28/12 21:54 |

trikl[m] | We didn't go into what exactly Agda does | 28/12 21:55 |

pgiarrusso | I never studied it formally either | 28/12 21:55 |

pgiarrusso | Conor co-wrote a paper on it, but it’s tough | 28/12 21:55 |

pgiarrusso | but when you pattern match, Agda solves equations between the “arguments of the constructors” and “the datatype you match on” | 28/12 21:55 |

mietek | pgiarrusso: you’re answering “I don't know how to show Agda that you can't make something of type `(z ,- []) <[ z ,- xs ]> ys` with an `sr` constructor” by saying that in fact, we _can_, yes? | 28/12 21:55 |

trikl[m] | > Conor co-wrote a paper on it, but it’s tough | 28/12 21:55 |

trikl[m] | God, I'm not the only one who thinks so | 28/12 21:55 |

pgiarrusso | mietek: yes | 28/12 21:56 |

pgiarrusso | mietek: I said otherwise before and I retract | 28/12 21:56 |

mietek | ok, good | 28/12 21:56 |

pgiarrusso | and I spelled out how to do it (also in words) | 28/12 21:56 |

trikl[m] | Initially I said we couldn't, then that we could, and then again that we couldn't | 28/12 21:57 |

trikl[m] | Now I know that we can | 28/12 21:57 |

mietek | my earlier suggestion was to try showing `lemma : {X : Set}{xs ys : List X}{z : X} -> (z ,- []) <[ z ,- xs ]> ys -> xs ~ ys -> xs == ys` | 28/12 21:57 |

mietek | if in fact it is showable | 28/12 21:57 |

mietek | (it’s not clear to me that it is) | 28/12 21:57 |

trikl[m] | It is showable | 28/12 21:58 |

trikl[m] | But it doesn't imply that `sl` is the constructor used for that splitting | 28/12 21:58 |

pgiarrusso | mietek: I’m not sure, but even in my example, it seems that it would hold | 28/12 21:58 |

mietek | trikl[m]: if it is showable, then it provides an additional piece of information to Agda | 28/12 21:58 |

pgiarrusso | OTOH, I still feel that `xs ~ ys` should be redundant | 28/12 21:58 |

mietek | well, maybe it is! | 28/12 21:59 |

trikl[m] | Even if `xs == ys`, the splitting can be constructed by `sr`, as pgiarrusso showed | 28/12 21:59 |

pgiarrusso | and... my last comment’s wrong: if you invert sr ....: (z ,- []) <[ z ,- xs ]> (z ,- ys’) | 28/12 22:03 |

pgiarrusso | you only get a proof that `(z ,- []) <[ xs ]> ys’` | 28/12 22:03 |

pgiarrusso | that is, you get `xs` by inserting `z` into `ys’` *somewhere* — start, middle or end | 28/12 22:04 |

trikl[m] | `z` into `xs`*? | 28/12 22:04 |

trikl[m] | Otherwise I don't understand why "inverting" sr means | 28/12 22:05 |

pgiarrusso | no | 28/12 22:05 |

pgiarrusso | well, I wanted to just read `(z ,- []) <[ xs ]> ys’` | 28/12 22:05 |

pgiarrusso | which says that `xs` is a merge of the other two lists | 28/12 22:06 |

trikl[m] | yes | 28/12 22:06 |

pgiarrusso | that is, if you inserted `z` somewhere into `ys’`, you’d get `xs` | 28/12 22:06 |

pgiarrusso | by “invert” I’m talking about an inversion lemma | 28/12 22:06 |

pgiarrusso | actually, a trivial one here | 28/12 22:07 |

pgiarrusso | said more simply: if you have a value constructed by `sr` with that type | 28/12 22:07 |

trikl[m] | > that is, if you inserted \`z\` somewhere into \`ys’\`, you’d get \`xs\` | 28/12 22:07 |

trikl[m] | I understand this | 28/12 22:07 |

pgiarrusso | it must get as argument a proof of `_ <[ _ ]> _` of a certain type | 28/12 22:07 |

pgiarrusso | and in particular, the “certain type” is `(z ,- []) <[ xs ]> ys’` | 28/12 22:08 |

pgiarrusso | trikl[m]: OK? | 28/12 22:09 |

trikl[m] | Yes | 28/12 22:09 |

pgiarrusso | “inversion” here just meant a specific thing: if I have a proof of some P, by looking at possible constructors for proofs of `P`’s, I can deduce some of those constructors were used and they got certain arguments | 28/12 22:10 |

pgiarrusso | which is pretty close to (dependent) pattern matching | 28/12 22:10 |

pgiarrusso | still not sure how to do the exercise, but I suspect we’re (almost) out of questions? | 28/12 22:11 |

pgiarrusso | regarding negation: | 28/12 22:11 |

pgiarrusso | in Agda you encode not P as “P -> False” | 28/12 22:11 |

trikl[m] | At least now I know that I'm more stupid than Agda is | 28/12 22:11 |

trikl[m] | And how do you prove it? | 28/12 22:12 |

pgiarrusso | first, how do we use it, OK? | 28/12 22:12 |

trikl[m] | Fair enough :) | 28/12 22:12 |

pgiarrusso | so, if you have `P -> False`, and some pattern matching gives you `P` | 28/12 22:12 |

pgiarrusso | maybe, say we know that `n + 1 == n -> False` | 28/12 22:13 |

pgiarrusso | and we get `n + 1 == n` in some pattern matching | 28/12 22:13 |

pgiarrusso | (not sure this helps) | 28/12 22:13 |

trikl[m] | we can use `P -> False` as a view? | 28/12 22:13 |

trikl[m] | I mean, in a with clause? | 28/12 22:14 |

pgiarrusso | yes | 28/12 22:14 |

trikl[m] | Ok | 28/12 22:14 |

pgiarrusso | so you get a proof of False, pattern match on it, and you’re done | 28/12 22:14 |

trikl[m] | Yes | 28/12 22:15 |

pgiarrusso | (didn’t know `with` clauses were called views, can’t be surprised) | 28/12 22:15 |

trikl[m] | I think you call views stuff you use in with clauses that teach you something about the previous arguments | 28/12 22:15 |

trikl[m] | I mean, the arguments that come before | 28/12 22:15 |

pgiarrusso | that makes sense, but I haven’t taken courses with Conor :-) | 28/12 22:16 |

pgiarrusso | I only know of “views” in Haskell, which are superficially different | 28/12 22:16 |

mietek | makes sense especially when you consider the “inspect idiom” | 28/12 22:16 |

pgiarrusso | probably it’s terminology from “the view from the left” | 28/12 22:17 |

trikl[m] | I think it's a fairly common idiom in papers too | 28/12 22:17 |

pgiarrusso | well, I said that paper is tough, I haven’t said I gave it an honest try | 28/12 22:17 |

mietek | FYI https://agda.github.io/agda-stdlib/Relation.Binary.PropositionalEquality.html#3026 | 28/12 22:17 |

mietek | “Inspect can be used when you want to pattern match on the result r of some expression e, and you also need to "remember" that r ≡ e.” | 28/12 22:17 |

pgiarrusso | mietek: the term makes some sense to me, but the inspect pattern doesn’t happen to help my intuition :-) YMMV though! | 28/12 22:18 |

pgiarrusso | anyway | 28/12 22:18 |

trikl[m] | It's also mentioned in The Power of Pi and Dependently Typed Programming in Agda by Ulf Norell and James Chapman | 28/12 22:18 |

mietek | the inspect idiom helps us retain the view that we *had*, before we ruined it by pattern-matching on it | 28/12 22:18 |

mietek | this could be argued to be a case of Agda being stupid | 28/12 22:19 |

mietek | but it’s just trees and rules and there’s no rule for that ;) | 28/12 22:19 |

pgiarrusso | trikl[m]: about proving False: I suppose you either use other proofs of negated facts, or do enough reasoning you get an absurd pattern matches | 28/12 22:19 |

pgiarrusso | *absurd pattern | 28/12 22:19 |

trikl[m] | Oh ok, so no magic :( | 28/12 22:20 |

pgiarrusso | trikl[m]: for instance, to show that `n + 1 == n -> False`, I suspect you’ll need induction on `n` | 28/12 22:20 |

trikl[m] | Yeah | 28/12 22:20 |

trikl[m] | Ok! | 28/12 22:20 |

pgiarrusso | because I chose it deviously, so that `n + 1` is a normal form | 28/12 22:20 |

trikl[m] | Well, thanks both pgiarrusso and mietek for challenging my assumptions :D | 28/12 22:20 |

pgiarrusso | the only thing is, some things are false but it can be arbitrarily hard to prove that | 28/12 22:21 |

pgiarrusso | I mean, earlier I hinted at Fermat’s last theorem | 28/12 22:21 |

trikl[m] | Yeah | 28/12 22:21 |

pgiarrusso | proving that a solution to that equation can’t exist took a couple centuries :-) | 28/12 22:21 |

trikl[m] | Aren't proofs of existence far easier? At least in a constructive logic? | 28/12 22:21 |

pgiarrusso | trikl[m]: yes and no | 28/12 22:22 |

pgiarrusso | “yes”, as in you just exhibit a witness and prove it satisfies the property | 28/12 22:22 |

pgiarrusso | “no”, because that also works in classical logic | 28/12 22:22 |

pgiarrusso | also no, because the proof might still take centuries :-) | 28/12 22:22 |

pgiarrusso | however, *using* an existence proof in constructive logic is easier | 28/12 22:22 |

pgiarrusso | because it *must* contain a witness | 28/12 22:23 |

trikl[m] | Oh I see | 28/12 22:23 |

pgiarrusso | which you can just project out of the sigma | 28/12 22:23 |

trikl[m] | In classical logic a proof of existence doesn't need a witness | 28/12 22:23 |

pgiarrusso | yep | 28/12 22:23 |

trikl[m] | Such madness | 28/12 22:23 |

mietek | indeed | 28/12 22:24 |

pgiarrusso | well, classical axiom of choice is not so unreasonable | 28/12 22:24 |

pgiarrusso | uncomputable, sure, not unreasonable | 28/12 22:24 |

trikl[m] | It's also not as strong | 28/12 22:25 |

trikl[m] | (As a witness) | 28/12 22:25 |

mietek | pgiarrusso: are you saying that human reasoning is hypercomputable? :> | 28/12 22:25 |

pgiarrusso | and all classical logic can be encoded in constructive logic (with the double-negation translation) | 28/12 22:25 |

mietek | ##dependent time! | 28/12 22:25 |

pgiarrusso | mietek: no no | 28/12 22:25 |

pgiarrusso | I’m just saying that sometimes you’re happy with not (not (exists x such that P x)) | 28/12 22:26 |

trikl[m] | I think I never had so much fun out of a couple of hours on IRC | 28/12 22:26 |

pgiarrusso | or sth. like that | 28/12 22:26 |

mietek | just making a joke on “uncomputable, sure, not unreasonable” | 28/12 22:26 |

pgiarrusso | classical logic just lets you omit the `not not` | 28/12 22:26 |

pgiarrusso | mietek: ah OK | 28/12 22:26 |

pgiarrusso | sorry, time to sleep | 28/12 22:26 |

pgiarrusso | trikl[m]: happy this helped | 28/12 22:26 |

trikl[m] | For me too, goodnight! | 28/12 22:27 |

mietek | o/ | 28/12 22:27 |

pgiarrusso | good night! 😴 | 28/12 22:27 |

* infinisil peeks from around the corner and thinks about asking his question now | 28/12 22:27 | |

mietek | infinisil: I’m still here | 28/12 22:28 |

infinisil | :D | 28/12 22:28 |

infinisil | Is there a library for handling sets? | 28/12 22:28 |

infinisil | I'm actually coming from Idris and am hoping to find them implemented in agda already, because i don't know how to do it | 28/12 22:29 |

mietek | which Idris library are you using? | 28/12 22:29 |

* mietek pokes {AS} | 28/12 22:29 | |

infinisil | none, I'm trying to write the Set type myself | 28/12 22:29 |

mietek | ah, sorry, misunderstood | 28/12 22:30 |

infinisil | I haven't found any library | 28/12 22:30 |

mietek | well, what are you trying to achieve? | 28/12 22:30 |

mietek | you’re effectively asking for a constructive formalisation of set theory | 28/12 22:30 |

mietek | this is such an annoyingly foundational thing that the next question becomes, *which* set theory | 28/12 22:30 |

infinisil | Heh | 28/12 22:30 |

Eduard_Munteanu | I guess classical sets are annoying to handle without some notion of subtyping. | 28/12 22:32 |

infinisil | I'm actually not sure myself. I thought about just creating a Set interface that provides functions for inserting, removing, checking elements with type signatures that make sense and allow for reasoning about them | 28/12 22:32 |

infinisil | Eduard_Munteanu: How would you do it with subtyping? | 28/12 22:33 |

mietek | infinisil: and then we’re one step away from https://i.imgur.com/o3IlETL.jpg | 28/12 22:33 |

Eduard_Munteanu | I'm not sure if you're talking about sets or things like Data.Set from Haskell. | 28/12 22:33 |

infinisil | mietek: Haha | 28/12 22:34 |

Eduard_Munteanu | infinisil, I'm just saying classical mathematics makes heavy use of subtyping, e.g. representing subsets | 28/12 22:34 |

Eduard_Munteanu | mietek, cool, where do you find memes like that? | 28/12 22:35 |

infinisil | Eduard_Munteanu: I see | 28/12 22:35 |

mietek | Eduard_Munteanu: hard to say; I had this one saved | 28/12 22:36 |

infinisil | Hmm alright I guess I'm not ready then to "implement" such a Set type | 28/12 22:37 |

mietek | infinisil: if you are actually interested in constructive set theory | 28/12 22:37 |

mietek | https://www.dropbox.com/s/exj8js7vyizef1n/Aczel1977.pdf | 28/12 22:37 |

mietek | https://www.dropbox.com/s/09zoysy07xii7ck/Aczel1982.pdf | 28/12 22:37 |

mietek | here’s my aborted attempt at formalising that; https://gist.github.com/mietek/4b7b83068f3d7b59e0410b444b4b4ae5 | 28/12 22:37 |

mietek | (ignore the HoTT in the module name; no idea why it’s there) | 28/12 22:38 |

mietek | and if this kind of thing seems like fun, join us in ##dependent | 28/12 22:38 |

mietek | I think I got stuck somewhere around set intersection | 28/12 22:38 |

infinisil | mietek: Oh sweet | 28/12 22:38 |

infinisil | thanks a lot | 28/12 22:39 |

infinisil | mietek: You german I assume? | 28/12 22:39 |

mietek | no :) | 28/12 22:39 |

mietek | http://www.cs.nott.ac.uk/~psztxa/g53cfr/l20.html/l20.html | 28/12 22:39 |

mietek | you may also find this interesting | 28/12 22:39 |

infinisil | Huh, because "Menge" means set in german | 28/12 22:39 |

mietek | yes, I know | 28/12 22:40 |

mietek | annoyingly, Agda already occupies “Set” | 28/12 22:40 |

mietek | in this exercise, Thorsten shows how we can pretend that Agda’s “Set” is the native set-theoretic set | 28/12 22:41 |

mietek | and enjoy the resulting paradox | 28/12 22:41 |

infinisil | Hmm, I guess it's time for me to learn Agda then | 28/12 22:42 |

mietek | http://www.cs.nott.ac.uk/~psztxa/g53cfr/ — that’s Thorsten’s course | 28/12 22:42 |

mietek | https://github.com/pigworker/CS410-17 — and Conor’s | 28/12 22:42 |

infinisil | mietek: Thanks, have taken note of those :D | 28/12 22:43 |

pgiarrusso | infinisil: if you were talking about `Data.Set`-like things, you might get away with implementing `Set t` as `T -> Bool` | 28/12 22:43 |

pgiarrusso | ;-) | 28/12 22:43 |

infinisil | pgiarrusso: Oh interesting | 28/12 22:43 |

pgiarrusso | if you can live with `O(n)` search maybe it’s even reasonable | 28/12 22:44 |

pgiarrusso | but I’m still not sure how you’d answer > 11:33 PM <Eduard_Munteanu> I'm not sure if you're talking about sets or things like Data.Set from Haskell. | 28/12 22:44 |

infinisil | Hmm, I guess more like the latter | 28/12 22:44 |

Eduard_Munteanu | infinisil, there's the AVL if you need a Map-like structure. | 28/12 22:45 |

pgiarrusso | and `Set t` is close (equal) to `Map t Bool` or `Map t Unit`, so you’re set :-) | 28/12 22:46 |

pgiarrusso | but warning: if you want an Idris-like language with more usable libraries, I’m sure Agda will also frustrate you eventually | 28/12 22:46 |

mietek | immediately* | 28/12 22:47 |

Eduard_Munteanu | https://github.com/agda/agda-stdlib/blob/master/src/Data/AVL/Sets.agda | 28/12 22:47 |

pgiarrusso | well, this time there was an actual answer in Agda’s standard library | 28/12 22:47 |

mietek | well… | 28/12 22:48 |

mietek | I’ll just innocently ask if you’ve managed to actually use the AVLs | 28/12 22:48 |

pgiarrusso | but I do agree overall :-) | 28/12 22:48 |

Eduard_Munteanu | I haven't tried in a long time. | 28/12 22:48 |

infinisil | Nice | 28/12 22:48 |

pgiarrusso | mietek: I’m not trying to actually program in Agda | 28/12 22:48 |

infinisil | That all seems rather promising, but I'll have to learn Agda because I don't really get the syntax heh | 28/12 22:49 |

pgiarrusso | I take it they’re not easy to use? | 28/12 22:49 |

pgiarrusso | BTW, for *programming* in Agda I hear https://github.com/UlfNorell/agda-prelude might be preferable | 28/12 22:49 |

mietek | I only remember failing | 28/12 22:49 |

mietek | I think I tried to use them instead of lists for contexts | 28/12 22:49 |

infinisil | The main reason I'd learn agda for is to get better at proving stuff and putting those to use in Idris :P | 28/12 22:49 |

infinisil | Maybe I should also check out Coq for the same reason | 28/12 22:50 |

pgiarrusso | mietek: using that interface to prove things looks reasonably easy | 28/12 22:50 |

pgiarrusso | no clue on doing *proofs* on those | 28/12 22:50 |

pgiarrusso | well actually... | 28/12 22:50 |

pgiarrusso | https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp is relevant | 28/12 22:51 |

pgiarrusso | > Most data structures are represented in canonical ways so that Leibniz equality can be used as much as possible (for example, for maps we have m1 = m2 iff ∀ i, m1 !! i = m2 !! i). On top of that, the library provides setoid instances for most types and operations. | 28/12 22:52 |

lambdabot | <hint>:1:6: error: parse error on input ‘data’ | 28/12 22:52 |

infinisil | > putStrLn "Is this Haskell?" | 28/12 22:53 |

lambdabot | <IO ()> | 28/12 22:53 |

pgiarrusso | not | 28/12 22:53 |

pgiarrusso | not haskell :-) | 28/12 22:53 |

pgiarrusso | mietek: do AVL trees satisfy that requirement? I suspect not | 28/12 22:53 |

infinisil | > 1:2:[] | 28/12 22:53 |

mietek | pgiarrusso: no idea | 28/12 22:53 |

lambdabot | [1,2] | 28/12 22:53 |

infinisil | that very much seems like haskell | 28/12 22:54 |

mietek | pgiarrusso: I wonder how portable that library is | 28/12 22:54 |

pgiarrusso | but as soon as you do proofs on data structures, you quickly want that property | 28/12 22:54 |

pgiarrusso | because, well, otherwise you end up needing to bother with setoids | 28/12 22:54 |

pgiarrusso | this came up when formalizing a paper, so we just postulated bags satisfying the correct properties | 28/12 22:55 |

mietek | ha. | 28/12 22:55 |

mietek | oh right | 28/12 22:55 |

mietek | but did you look at Danielsson’s work? | 28/12 22:55 |

pgiarrusso | my PLDI’14 paper | 28/12 22:55 |

mietek | http://www.cse.chalmers.se/~nad/publications/danielsson-bag-equivalence.pdf | 28/12 22:55 |

pgiarrusso | well, getting that right wasn’t our main goal | 28/12 22:56 |

mietek | right | 28/12 22:56 |

mietek | I mean, aside from AVLs, in Agda we should have his bags | 28/12 22:56 |

mietek | which I forgot about | 28/12 22:56 |

mietek | https://agda.github.io/agda-stdlib/Data.List.Any.BagAndSetEquality.html | 28/12 22:57 |

mietek | they’re … in there somewhere | 28/12 22:57 |

pgiarrusso | OK, NAD’s paper seems to define the setoid you’d want for bags | 28/12 22:57 |

mietek | which brings me again to the “immediate frustration” bit | 28/12 22:57 |

pgiarrusso | but I suspect switching to setoids would have forced us to modify quite a bit of our code | 28/12 22:58 |

pgiarrusso | which was around 5000 LoC of Agda | 28/12 22:58 |

pgiarrusso | however, having real bags in our paper wouldn’t have mattered one bit, so it’s good we didn’t waste time :-) | 28/12 22:59 |

infinisil | What do you think is the most challenging part of formalizing and proving correctness of bigger programs? | 28/12 23:03 |

infinisil | Because it seems that basic data structures are already really challenging. But I have a feeling that this could be the most important part since everything can be built upon that | 28/12 23:04 |

infinisil | asking in ##dependent instead | 28/12 23:04 |

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!