--- 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 time28/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 permutations28/12 18:19
mietektrikl[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/490744232403795968028/12 19:25
mietektrikl[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 left28/12 19:34
mietekside note: it is useful to write transitivity laws infix28/12 19:34
trikl[m]This is because I want to show that lists as objects and permutations as arrows form a category28/12 19:34
trikl[m]Noted! This is the way the exercise is set though28/12 19:35
mietekhttps://gist.github.com/mietek/00af5865d819a5ed0b351acb74a57b9028/12 19:35
mietekin the spirit of showing that things form categories28/12 19:36
pgiarrussotrikl[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 be28/12 19:41
trikl[m]I believe that was pasted on my previous message: http://lpaste.net/36113528/12 19:42
mietekI believe pgiarrusso is asking about the intended meaning of the datatype28/12 19:42
pgiarrussoindeed28/12 19:42
mietekI’m reading `ls <[ ms ]> rs` as evidence that `ms` can be decomposed into two parts, `ls` and `rs`28/12 19:43
mietekand so, the method by which we can decompose `ms`28/12 19:43
mieteksome elements of `ms` go into the left part, `ls`; other elements go into the right part, `rs`28/12 19:43
pgiarrussoOK, thanks28/12 19:43
mieteknot sure if this is correct28/12 19:44
pgiarrussoand the elements are split preserving order28/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 stopping28/12 19:44
trikl[m]pgiarrusso: yes28/12 19:44
pgiarrussoso this resembles a bit what happens in the merge phase of mergesort (if we drop ordering)28/12 19:45
pgiarrussoOK, that answers my question, thanks28/12 19:45
mietek`_,-_` is pure evil28/12 19:45
mieteknotation-wise28/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 right28/12 19:46
mietektrikl[m]: I’m getting there; had to rewrite the definitions so that I can read them28/12 19:46
pgiarrussoOK, I suspect your earlier question was correct28/12 19:46
trikl[m]Thanks for the help people :)28/12 19:46
pgiarrussoand that you shouldn't need to know that xs and us are permutations28/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 constructor28/12 19:49
pgiarrussowell, the proof might need induction on xs/ys, or be more complicated28/12 19:49
pgiarrussoyou sound like you're expecting a non-existent sufficiently smart Agda28/12 19:50
trikl[m]Hah yeah28/12 19:50
pgiarrussoanyway, gotta go, and mietek's working on a solution28/12 19:50
pgiarrussobbl28/12 19:50
trikl[m]But what bugs me is that I can't see how to proceed28/12 19:50
trikl[m]Thanks pgiarrusso !28/12 19:51
mietekis the definition of the permutation datatype also given in the exercise?28/12 19:51
trikl[m]Yes28/12 19:51
trikl[m]I would not think of that devil myself, yet28/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 equality28/12 19:57
{AS}for permutations28/12 19:57
trikl[m]Cheers28/12 19:58
{AS}trikl[m]: http://www.cse.chalmers.se/~nad/publications/danielsson-bag-equivalence.pdf28/12 19:58
mietek…although I would be surprised if that was part of solving the exercise…28/12 19:58
mietektrikl[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 that28/12 19:59
trikl[m]http://lpaste.net/790197887239926579228/12 19:59
mietektrikl[m]: and what is srs?28/12 20:00
trikl[m]http://lpaste.net/772369337548800000028/12 20:00
mietekanother side note: a single paste containing all of your working code is preferred28/12 20:01
trikl[m]Yes, I'm slowly becoming aware of that28/12 20:01
trikl[m]It's just that my original question needed a lot less context than the evolved explanation28/12 20:01
mietekthat’s what you think :)28/12 20:01
trikl[m]Haha28/12 20:02
trikl[m]Sorry, I'll be back in 15 minutes tops28/12 20:02
mietekno worries28/12 20:02
trikl[m]I'm back28/12 20:09
mietektrikl[m]: and… how did you show transitivity? 28/12 20:18
mietekit doesn’t seem easy28/12 20:18
trikl[m]It's a little tricky yes28/12 20:19
trikl[m]I will put together a paste with all of it28/12 20:19
trikl[m]http://lpaste.net/666723933172531200028/12 20:24
trikl[m]So this is all of it28/12 20:24
mietekomg28/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 type28/12 20:25
mietekyou missed: List, +L28/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 constructor28/12 20:27
trikl[m]`Sg` standing for sigma28/12 20:27
mietekI can guess that28/12 20:27
mietekbut I’d rather just load the code28/12 20:27
mietek:)28/12 20:27
trikl[m]http://lpaste.net/121698334271340544028/12 20:28
trikl[m]Sorry, `_*_` is the non-dependent tuple28/12 20:30
mietekyou could’ve said https://github.com/pigworker/CS410-17/tree/master/exercises28/12 20:30
trikl[m]I would still need to paste my answers too28/12 20:31
mietekyep, but at least then they typecheck28/12 20:32
mietekI’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 right28/12 20:33
mietekthese are pretty advanced exercises indeed28/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 though28/12 20:35
trikl[m]Hour hands were hold with the previous two28/12 20:36
trikl[m]Sorry, Our*28/12 20:36
mietektrikl[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]Yes28/12 20:38
trikl[m]`reflP` could be substituted by `xs ~ xs` too28/12 20:38
mietekyou mean, an arbitrary proof of `xs ~ xs`?28/12 20:39
trikl[m]Yes, by any `g : xs ~ xs`28/12 20:39
mietek18: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
mietektrying to figure out how you got there28/12 20:47
trikl[m]Do I actually require a proof of `xs == ys`?28/12 20:47
mietekwell, 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
mietekhave you tried proving it?28/12 20:48
mietekand then, you could “show the typechecker” by pattern-matching on the result of applying the lemma28/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 absurd28/12 20:48
trikl[m]I tried, briefly, and didn't succeed28/12 20:49
mieteksorry — no idea where to attach your previous comment28/12 20:49
trikl[m]i was not sure that was the correct path to follow28/12 20:49
mietekoh — 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 this28/12 20:50
trikl[m]Yes28/12 20:50
trikl[m]That way I can also pattern match on `g`28/12 20:50
mietekI suppose you can, but what does that give you? :)28/12 20:50
mietekI’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 yet28/12 20:52
mietekone could be easier than the other28/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 though28/12 20:53
trikl[m]So I can't use one to prove the other28/12 20:53
trikl[m]But yeah, I should explore that road too28/12 20:53
mietekin general, I would expect that if proving transitivity is this hairy, proving properties of transitivity will be at least the same amount of hairy28/12 20:54
mietekI’m sorry I can’t be of more help28/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
mietekif you could paste the exact code where you’re getting it…28/12 20:57
trikl[m]I don't understand why that happens28/12 20:57
trikl[m]http://lpaste.net/654286098725339136028/12 20:59
mietekI don’t understand how this code maps to what you just said28/12 21:01
trikl[m]http://lpaste.net/66848485043653836828/12 21:02
trikl[m]That's why I said the last case is absurd28/12 21:02
trikl[m]Or impossible28/12 21:02
trikl[m]I guess I should send Conor an email with these questions28/12 21:04
mietekyou may get a better chance at a response to a tweet28/12 21:05
trikl[m]I don't want to use Twitter though28/12 21:05
trikl[m]It's centralised and proprietary28/12 21:05
trikl[m]And they don't even offer RSS feeds, which is just plain mean28/12 21:06
mietekit’s irrelevant to the problem of getting a response28/12 21:06
trikl[m]I don't think of my principles as irrelevant :)28/12 21:06
mietekI regret offering advice already :)28/12 21:07
trikl[m]I'd rather send an email that doesn't get any response28/12 21:07
trikl[m]Haha28/12 21:07
trikl[m]The advice was good28/12 21:07
trikl[m]I just can't use it28/12 21:07
mietekI’m wondering why you think the `sr` case is absurd28/12 21:09
trikl[m]To construct something of type `xs ~ xs` you can only prepend things to the start of both lists28/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 element28/12 21:10
mietekthat’s not quite what the constructors of `_~_` say28/12 21:10
mietekfirst, `[] ~ []` holds28/12 21:11
trikl[m]Wait, what I said is irrelevant28/12 21:11
mietekoh, also, why are you talking about `xs ~ xs`28/12 21:11
mietekyou’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 head28/12 21:11
mietekok28/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
mietekhttp://lpaste.net/622078452075751014428/12 21:13
mietekI’ve identified two absurd possibilities28/12 21:14
mietekbut not one that would rule out using `sr`28/12 21:14
mietekI don’t feel like I understand the datatypes involved, though28/12 21:14
trikl[m]I think you are confusing things28/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
mietekoh. you are.28/12 21:15
mietekI don’t see why, though28/12 21:15
mietekthe theorem should also hold for reflP28/12 21:16
trikl[m]Yes, because `reflP` is of type `xs ~ xs`28/12 21:16
trikl[m]http://lpaste.net/654286098725339136028/12 21:16
trikl[m]I pattern match against `g : xs ~ xs` to be able to proof that28/12 21:16
mietekyes, 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 should28/12 21:17
trikl[m]I just ignore how28/12 21:17
mietekmy intuition is telling me to start with that28/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 go28/12 21:18
trikl[m]But I remember the frustration :D28/12 21:18
mietekI expect that if indeed `xs ~ xs` is uniquely inhabited, this would be provable28/12 21:19
mietekexamples 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 right28/12 21:22
mietekfor any two elements in the type, they are structurally identical28/12 21:23
trikl[m]I'm just wondering what `{p : xs ~ xs} -> p == reflP` would mean compared to that28/12 21:23
trikl[m]As in: are they equal in strength?28/12 21:24
mietekon the meta-level, both this question and the one about transitivity with `xs ~ xs` and with `reflP` are similar28/12 21:24
pgiarrussosemi-sleepy, but I’m back for a bit28/12 21:25
mietektrikl[m]: how do you measure strength?28/12 21:25
pgiarrussolet me point out that, IMHO, you shouldn’t be talking about permutations...28/12 21:25
pgiarrussoI think at least28/12 21:26
mietekpgiarrusso: before you say anything, https://github.com/pigworker/CS410-17/blob/master/exercises/Ex3.agda#L10828/12 21:26
trikl[m] > trikl[m]: how do you measure strength?28/12 21:26
mietektrikl[m]: ultimately, what we’re doing here is manipulating trees according to rules28/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 stronger28/12 21:26
mietektrikl[m]: if the rules we’ve got allow us to obtain the same resulting tree by more than one route, great28/12 21:27
mietektrikl[m]: some routes are quicker than others28/12 21:27
pgiarrussotrikl[m]: “p is stronger than q” is language for “p implies q”28/12 21:28
pgiarrussomietek: uh28/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
mietektrikl[m]: in that case, clearly `{p : xs ~ xs} -> p == reflP` follows from `uniqP`28/12 21:29
trikl[m]Yes28/12 21:29
mietektrikl[m]: it’s not obvious to me if the converse is true, but perhaps it also is28/12 21:29
trikl[m]But I wonder if it goes the other way too28/12 21:30
mietektrikl[m]: it could be fun to prove that28/12 21:30
trikl[m]On my way!28/12 21:30
mietekbut getting back to your original question, I really think it’s a matter of understanding the datatypes involved28/12 21:30
mietekbecause Agda will only see absurdities if things are set up properly28/12 21:30
pgiarrussotrikl[m]: again, many things are absurd but aren’t recognized as “immediately absurd” by Agda — and only immediately absurd things are rejected during pattern matching28/12 21:31
mietekI don’t even see the absurdity you were trying to point out28/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` constructor28/12 21:32
mietekare you sure you can’t?28/12 21:32
trikl[m]No, because if I were I would know how to proof I can't28/12 21:32
trikl[m]But I guess I don't know how to proof you can't do things, in Agda28/12 21:33
pgiarrussotrikl[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
pgiarrussotrikl[m]: have you seen how to define negation?28/12 21:33
pgiarrussoand how to prove negation?28/12 21:33
trikl[m]pgiarrusso: But in this case it's the splitting constructors that have this types28/12 21:33
trikl[m]In general, yes, but not in Agda28/12 21:34
pgiarrussoOK, that seems relevant28/12 21:35
pgiarrussobut before that, I’d like to look more closely at this result28/12 21:35
trikl[m]Also, sorry for the multiple mistakes involving the noun proof and the verb to prove28/12 21:36
pgiarrussothanks but, at least I understood you anyway :-)28/12 21:37
pgiarrusso*no comma28/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
pgiarrussotrikl[m], I stand corrected: you *can* instantiate type (z ,- []) <[ z,- xs ]> ys for particular values28/12 21:49
trikl[m]In a way similar to how you use views?28/12 21:49
pgiarrussosorry, you can instantiate it with sr28/12 21:49
pgiarrussoand when you first figured you can, you were right28/12 21:49
pgiarrussoin particular, looking for such a solution by solving the equalities that arise28/12 21:49
pgiarrussoand with a touch of fantasy28/12 21:49
trikl[m]Haha28/12 21:49
trikl[m]So I have to use both the infamous splitting and `xs ~ ys`?28/12 21:50
pgiarrussoyou 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
pgiarrussobut sl isn’t the only way28/12 21:50
pgiarrussoin the instance I gave you, you *can* start with sr28/12 21:51
trikl[m]Oh28/12 21:51
pgiarrussothen use sl28/12 21:51
trikl[m]Now I see28/12 21:51
trikl[m]All my past days were a lie28/12 21:51
trikl[m]Or a half discovered truth28/12 21:51
pgiarrussoyour other question on negation is still good, it’s just not the one you need next28/12 21:51
pgiarrussolet’s press on the half-discovered truth28/12 21:52
pgiarrussofirst, do you buy what I wrote?28/12 21:52
trikl[m]It's already in my pocket!28/12 21:52
pgiarrussoLOL28/12 21:52
trikl[m]Sorry, we are students of Conor McBride after all28/12 21:53
trikl[m]Plus, we live in Glasgow28/12 21:53
pgiarrussoto 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 z28/12 21:53
pgiarrussomietek: ^^28/12 21:53
trikl[m]Yes28/12 21:53
pgiarrussotrikl[m]: so can I assume you learned about unification and how pattern matching uses unification?28/12 21:54
pgiarrussoI haven’t seen the course and I don’t know if you’ve seen this with those words28/12 21:54
trikl[m]Only intuitively28/12 21:54
pgiarrussowell, that’s good enough28/12 21:54
trikl[m]We didn't go into what exactly Agda does28/12 21:55
pgiarrussoI never studied it formally either28/12 21:55
pgiarrussoConor co-wrote a paper on it, but it’s tough28/12 21:55
pgiarrussobut when you pattern match, Agda solves equations between the “arguments of the constructors” and “the datatype you match on”28/12 21:55
mietekpgiarrusso: 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 tough28/12 21:55
trikl[m]God, I'm not the only one who thinks so28/12 21:55
pgiarrussomietek: yes28/12 21:56
pgiarrussomietek: I said otherwise before and I retract28/12 21:56
mietekok, good28/12 21:56
pgiarrussoand 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't28/12 21:57
trikl[m]Now I know that we can28/12 21:57
mietekmy 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
mietekif in fact it is showable28/12 21:57
mietek(it’s not clear to me that it is)28/12 21:57
trikl[m]It is showable28/12 21:58
trikl[m]But it doesn't imply that `sl` is the constructor used for that splitting28/12 21:58
pgiarrussomietek: I’m not sure, but even in my example, it seems that it would hold28/12 21:58
mietektrikl[m]: if it is showable, then it provides an additional piece of information to Agda28/12 21:58
pgiarrussoOTOH, I still feel that `xs ~ ys` should be redundant28/12 21:58
mietekwell, 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
pgiarrussoand... my last comment’s wrong: if you invert sr ....: (z ,- []) <[ z ,- xs ]> (z ,- ys’)28/12 22:03
pgiarrussoyou only get a proof that `(z ,- []) <[ xs ]> ys’`28/12 22:03
pgiarrussothat is, you get `xs` by inserting `z` into `ys’` *somewhere* — start, middle or end28/12 22:04
trikl[m]`z` into `xs`*?28/12 22:04
trikl[m]Otherwise I don't understand why "inverting" sr means28/12 22:05
pgiarrussono28/12 22:05
pgiarrussowell, I wanted to just read `(z ,- []) <[ xs ]> ys’`28/12 22:05
pgiarrussowhich says that `xs` is a merge of the other two lists28/12 22:06
trikl[m]yes28/12 22:06
pgiarrussothat is, if you inserted `z` somewhere into `ys’`, you’d get `xs`28/12 22:06
pgiarrussoby “invert” I’m talking about an inversion lemma28/12 22:06
pgiarrussoactually, a trivial one here28/12 22:07
pgiarrussosaid more simply: if you have a value constructed by `sr` with that type28/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 this28/12 22:07
pgiarrussoit must get as argument a proof of `_ <[ _ ]> _` of a certain type28/12 22:07
pgiarrussoand in particular, the “certain type” is `(z ,- []) <[ xs ]> ys’`28/12 22:08
pgiarrussotrikl[m]: OK?28/12 22:09
trikl[m]Yes28/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 arguments28/12 22:10
pgiarrussowhich is pretty close to (dependent) pattern matching28/12 22:10
pgiarrussostill not sure how to do the exercise, but I suspect we’re (almost) out of questions?28/12 22:11
pgiarrussoregarding negation:28/12 22:11
pgiarrussoin 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 is28/12 22:11
trikl[m]And how do you prove it?28/12 22:12
pgiarrussofirst, how do we use it, OK?28/12 22:12
trikl[m]Fair enough :)28/12 22:12
pgiarrussoso, if you have `P -> False`, and some pattern matching gives you `P`28/12 22:12
pgiarrussomaybe, say we know that `n + 1 == n -> False`28/12 22:13
pgiarrussoand we get `n + 1 == n` in some pattern matching28/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
pgiarrussoyes28/12 22:14
trikl[m]Ok28/12 22:14
pgiarrussoso you get a proof of False, pattern match on it, and you’re done28/12 22:14
trikl[m]Yes28/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 arguments28/12 22:15
trikl[m]I mean, the arguments that come before28/12 22:15
pgiarrussothat makes sense, but I haven’t taken courses with Conor :-)28/12 22:16
pgiarrussoI only know of “views” in Haskell, which are superficially different28/12 22:16
mietekmakes sense especially when you consider the “inspect idiom”28/12 22:16
pgiarrussoprobably 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 too28/12 22:17
pgiarrussowell, I said that paper is tough, I haven’t said I gave it an honest try28/12 22:17
mietekFYI https://agda.github.io/agda-stdlib/Relation.Binary.PropositionalEquality.html#302628/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
pgiarrussomietek: the term makes some sense to me, but the inspect pattern doesn’t happen to help my intuition :-) YMMV though!28/12 22:18
pgiarrussoanyway28/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 Chapman28/12 22:18
mietekthe inspect idiom helps us retain the view that we *had*, before we ruined it by pattern-matching on it28/12 22:18
mietekthis could be argued to be a case of Agda being stupid28/12 22:19
mietekbut it’s just trees and rules and there’s no rule for that ;)28/12 22:19
pgiarrussotrikl[m]: about proving False: I suppose you either use other proofs of negated facts, or do enough reasoning you get an absurd pattern matches28/12 22:19
pgiarrusso*absurd pattern28/12 22:19
trikl[m]Oh ok, so no magic :(28/12 22:20
pgiarrussotrikl[m]: for instance, to show that `n + 1 == n -> False`, I suspect you’ll need induction on `n`28/12 22:20
trikl[m]Yeah28/12 22:20
trikl[m]Ok!28/12 22:20
pgiarrussobecause I chose it deviously, so that `n + 1` is a normal form28/12 22:20
trikl[m]Well, thanks both pgiarrusso  and mietek  for challenging my assumptions :D28/12 22:20
pgiarrussothe only thing is, some things are false but it can be arbitrarily hard to prove that28/12 22:21
pgiarrussoI mean, earlier I hinted at Fermat’s last theorem28/12 22:21
trikl[m]Yeah28/12 22:21
pgiarrussoproving 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
pgiarrussotrikl[m]: yes and no28/12 22:22
pgiarrusso“yes”, as in you just exhibit a witness and prove it satisfies the property28/12 22:22
pgiarrusso“no”, because that also works in classical logic28/12 22:22
pgiarrussoalso no, because the proof might still take centuries :-)28/12 22:22
pgiarrussohowever, *using* an existence proof in constructive logic is easier28/12 22:22
pgiarrussobecause it *must* contain a witness28/12 22:23
trikl[m]Oh I see28/12 22:23
pgiarrussowhich you can just project out of the sigma28/12 22:23
trikl[m]In classical logic a proof of existence doesn't need a witness28/12 22:23
pgiarrussoyep28/12 22:23
trikl[m]Such madness28/12 22:23
mietekindeed28/12 22:24
pgiarrussowell, classical axiom of choice is not so unreasonable28/12 22:24
pgiarrussouncomputable, sure, not unreasonable28/12 22:24
trikl[m]It's also not as strong28/12 22:25
trikl[m](As a witness)28/12 22:25
mietekpgiarrusso: are you saying that human reasoning is hypercomputable? :>28/12 22:25
pgiarrussoand 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
pgiarrussomietek: no no28/12 22:25
pgiarrussoI’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 IRC28/12 22:26
pgiarrussoor sth. like that28/12 22:26
mietekjust making a joke on “uncomputable, sure, not unreasonable” 28/12 22:26
pgiarrussoclassical logic just lets you omit the `not not`28/12 22:26
pgiarrussomietek: ah OK28/12 22:26
pgiarrussosorry, time to sleep28/12 22:26
pgiarrussotrikl[m]: happy this helped28/12 22:26
trikl[m]For me too, goodnight!28/12 22:27
mieteko/28/12 22:27
pgiarrussogood night! 😴28/12 22:27
* infinisil peeks from around the corner and thinks about asking his question now28/12 22:27
mietekinfinisil: I’m still here28/12 22:28
infinisil:D28/12 22:28
infinisilIs there a library for handling sets?28/12 22:28
infinisilI'm actually coming from Idris and am hoping to find them implemented in agda already, because i don't know how to do it28/12 22:29
mietekwhich Idris library are you using?28/12 22:29
* mietek pokes {AS}28/12 22:29
infinisilnone, I'm trying to write the Set type myself28/12 22:29
mietekah, sorry, misunderstood28/12 22:30
infinisilI haven't found any library28/12 22:30
mietekwell, what are you trying to achieve?28/12 22:30
mietekyou’re effectively asking for a constructive formalisation of set theory28/12 22:30
mietekthis is such an annoyingly foundational thing that the next question becomes, *which* set theory28/12 22:30
infinisilHeh28/12 22:30
Eduard_MunteanuI guess classical sets are annoying to handle without some notion of subtyping.28/12 22:32
infinisilI'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 them28/12 22:32
infinisilEduard_Munteanu: How would you do it with subtyping?28/12 22:33
mietekinfinisil: and then we’re one step away from https://i.imgur.com/o3IlETL.jpg28/12 22:33
Eduard_MunteanuI'm not sure if you're talking about sets or things like Data.Set from Haskell.28/12 22:33
infinisilmietek: Haha28/12 22:34
Eduard_Munteanuinfinisil, I'm just saying classical mathematics makes heavy use of subtyping, e.g. representing subsets28/12 22:34
Eduard_Munteanumietek, cool, where do you find memes like that?28/12 22:35
infinisilEduard_Munteanu: I see28/12 22:35
mietekEduard_Munteanu: hard to say; I had this one saved28/12 22:36
infinisilHmm alright I guess I'm not ready then to "implement" such a Set type28/12 22:37
mietekinfinisil: if you are actually interested in constructive set theory28/12 22:37
mietekhttps://www.dropbox.com/s/exj8js7vyizef1n/Aczel1977.pdf28/12 22:37
mietekhttps://www.dropbox.com/s/09zoysy07xii7ck/Aczel1982.pdf28/12 22:37
mietekhere’s my aborted attempt at formalising that; https://gist.github.com/mietek/4b7b83068f3d7b59e0410b444b4b4ae528/12 22:37
mietek(ignore the HoTT in the module name; no idea why it’s there)28/12 22:38
mietekand if this kind of thing seems like fun, join us in ##dependent28/12 22:38
mietekI think I got stuck somewhere around set intersection28/12 22:38
infinisilmietek: Oh sweet28/12 22:38
infinisilthanks a lot28/12 22:39
infinisilmietek: You german I assume?28/12 22:39
mietekno :)28/12 22:39
mietekhttp://www.cs.nott.ac.uk/~psztxa/g53cfr/l20.html/l20.html28/12 22:39
mietekyou may also find this interesting28/12 22:39
infinisilHuh, because "Menge" means set in german28/12 22:39
mietekyes, I know28/12 22:40
mietekannoyingly, Agda already occupies “Set” 28/12 22:40
mietekin this exercise, Thorsten shows how we can pretend that Agda’s “Set” is the native set-theoretic set28/12 22:41
mietekand enjoy the resulting paradox28/12 22:41
infinisilHmm, I guess it's time for me to learn Agda then28/12 22:42
mietekhttp://www.cs.nott.ac.uk/~psztxa/g53cfr/ — that’s Thorsten’s course28/12 22:42
mietekhttps://github.com/pigworker/CS410-17 — and Conor’s28/12 22:42
infinisilmietek: Thanks, have taken note of those :D28/12 22:43
pgiarrussoinfinisil: 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
infinisilpgiarrusso: Oh interesting28/12 22:43
pgiarrussoif you can live with `O(n)` search maybe it’s even reasonable28/12 22:44
pgiarrussobut 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
infinisilHmm, I guess more like the latter28/12 22:44
Eduard_Munteanuinfinisil, there's the AVL if you need a Map-like structure.28/12 22:45
pgiarrussoand `Set t` is close (equal) to `Map t Bool` or `Map t Unit`, so you’re set :-)28/12 22:46
pgiarrussobut warning: if you want an Idris-like language with more usable libraries, I’m sure Agda will also frustrate you eventually28/12 22:46
mietekimmediately*28/12 22:47
Eduard_Munteanuhttps://github.com/agda/agda-stdlib/blob/master/src/Data/AVL/Sets.agda28/12 22:47
pgiarrussowell, this time there was an actual answer in Agda’s standard library28/12 22:47
mietekwell…28/12 22:48
mietekI’ll just innocently ask if you’ve managed to actually use the AVLs28/12 22:48
pgiarrussobut I do agree overall :-)28/12 22:48
Eduard_MunteanuI haven't tried in a long time.28/12 22:48
infinisilNice28/12 22:48
pgiarrussomietek: I’m not trying to actually program in Agda28/12 22:48
infinisilThat all seems rather promising, but I'll have to learn Agda because I don't really get the syntax heh28/12 22:49
pgiarrussoI take it they’re not easy to use?28/12 22:49
pgiarrussoBTW, for *programming* in Agda I hear https://github.com/UlfNorell/agda-prelude might be preferable28/12 22:49
mietekI only remember failing 28/12 22:49
mietekI think I tried to use them instead of lists for contexts28/12 22:49
infinisilThe main reason I'd learn agda for is to get better at proving stuff and putting those to use in Idris :P28/12 22:49
infinisilMaybe I should also check out Coq for the same reason28/12 22:50
pgiarrussomietek: using that interface to prove things looks reasonably easy28/12 22:50
pgiarrussono clue on doing *proofs* on those28/12 22:50
pgiarrussowell actually...28/12 22:50
pgiarrussohttps://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp is relevant28/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
pgiarrussonot28/12 22:53
pgiarrussonot haskell :-)28/12 22:53
pgiarrussomietek: do AVL trees satisfy that requirement? I suspect not28/12 22:53
infinisil> 1:2:[]28/12 22:53
mietekpgiarrusso: no idea28/12 22:53
lambdabot [1,2]28/12 22:53
infinisilthat very much seems like haskell28/12 22:54
mietekpgiarrusso: I wonder how portable that library is28/12 22:54
pgiarrussobut as soon as you do proofs on data structures, you quickly want that property28/12 22:54
pgiarrussobecause, well, otherwise you end up needing to bother with setoids28/12 22:54
pgiarrussothis came up when formalizing a paper, so we just postulated bags satisfying the correct properties28/12 22:55
mietekha.28/12 22:55
mietekoh right28/12 22:55
mietekbut did you look at Danielsson’s work?28/12 22:55
pgiarrussomy PLDI’14 paper28/12 22:55
mietekhttp://www.cse.chalmers.se/~nad/publications/danielsson-bag-equivalence.pdf28/12 22:55
pgiarrussowell, getting that right wasn’t our main goal28/12 22:56
mietekright28/12 22:56
mietekI mean, aside from AVLs, in Agda we should have his bags28/12 22:56
mietekwhich I forgot about28/12 22:56
mietekhttps://agda.github.io/agda-stdlib/Data.List.Any.BagAndSetEquality.html28/12 22:57
mietekthey’re … in there somewhere28/12 22:57
pgiarrussoOK, NAD’s paper seems to define the setoid you’d want for bags28/12 22:57
mietekwhich brings me again to the “immediate frustration” bit28/12 22:57
pgiarrussobut I suspect switching to setoids would have forced us to modify quite a bit of our code28/12 22:58
pgiarrussowhich was around 5000 LoC of Agda28/12 22:58
pgiarrussohowever, 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
infinisilWhat do you think is the most challenging part of formalizing and proving correctness of bigger programs?28/12 23:03
infinisilBecause 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 that28/12 23:04
infinisilasking in ##dependent instead28/12 23:04

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