--- Day changed Mon Apr 24 2017
mietek!ops24/04 00:23
mietek$ops24/04 00:23
SrPxWhy is "not A" defined as ∀ (C : *) . (A => C)? Something is not true if it implies everything? What24/04 04:22
SrPxYou can't construct a term of that type24/04 04:23
SrPxThat makes no sense24/04 04:23
doguiYou can if A is false :-)24/04 04:26
mietekSrPx: where are you getting this definition from?24/04 04:27
mietekit may be useful to look at https://agda.github.io/agda-stdlib/Relation.Nullary.html and https://agda.github.io/agda-stdlib/Data.Empty.html24/04 04:28
SrPxmietek: I was reading the wikipedia Wiki on type theory24/04 04:28
SrPxthe wikipedia entry*24/04 04:28
mietekintuitionistically, "not A" is short hand for "A implies empty type"24/04 04:29
SrPxgen't get through the syntax, what is `Set t`, and what is `∀ {l}`? 24/04 04:30
mietekand the empty type is eliminated with the principle of explosion24/04 04:30
SrPxcan't24/04 04:30
mietekI suppose what you’re reading collapses the two together24/04 04:30
mietekyou do know you’re asking in #agda, right?24/04 04:31
mietekhttp://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf24/04 04:32
SrPxmietek: well you're right, where else could I ask though24/04 04:32
mietek##typetheory24/04 04:32
SrPxfair enough24/04 04:32
SrPxthanks for the paper though, I can't really use agda for being too vim-dependent ): I'll ask there24/04 04:33
mietekit’s possible to use agda only from the command-line24/04 04:33
mietekI did that for a while, but I wouldn’t really recommend it24/04 04:33
SrPxI guess I see what that meant though, seems like this is parametric on the universes (?)24/04 04:33
mietekyes, but that’s really irrelevant to the question24/04 04:33
mietek"l" is a universe level24/04 04:33
SrPxok makes total snse24/04 04:35
Guest51433Hi all, I am currently working through the 'Dependently typed programming in Agda' paper and struggling with exercise 2.2: proving 'lem-tab-! : forall {A n} (xs : Vec A n) -> tabulate (_!_ xs) == xs', could you give me a hint there?24/04 19:19
mietekGuest51433: I suggest using a more memorable nickname24/04 19:25
mietekGuest51433: have you tried pattern-matching on the implicit {xs} argument?  you may need to write {xs = xs} to pattern-match past the first two implicits24/04 19:26
mietekoh wait, it’s not an implicit; damn my eyes24/04 19:27
mietekGuest51433: have you tried pattern-matching on xs?24/04 19:27
Guest51433Yes, the [] part is easy24/04 19:27
mietekGuest51433: do you know the concept of proof by induction?24/04 19:28
mietekGuest51433: in the other pars, you should make use of the induction hypotheses, by calling lem-tab-! again with a smaller argument24/04 19:29
mietekpart*24/04 19:29
Guest51433mietek: I am just working through the tutorial and I managed to complete the other exercises. The problem is I don't know how to reduce the rest, see: https://pastebin.com/tLWyBk7v24/04 19:29
mietekGuest51433: well, the goal is to provide a proof of some equality, _==_24/04 19:30
mietekGuest51433: look at the building blocks that are available to you. what can you use to build an object of type Something == Something?24/04 19:31
mietekGuest51433: I don’t remember the details of the Iowa library that this book is using, but there should be something that allows you to show a congruence 24/04 19:31
Guest51433there is the definition 'data _==_ {A : Set} (x : A) : A -> Set where refl : x == x24/04 19:31
mietekyes, you already used that one for []24/04 19:32
mietekit’s likely you need something else24/04 19:32
mieteknote both Somethings in the goal look similar 24/04 19:32
mietekboth have (x ::_) applied24/04 19:32
mietekif we apply (x ::_) to ThingA, and ThingB, then we’ll get an equality as long as ThingA and ThingB are equal24/04 19:33
mietekthis is the notion you want to express now24/04 19:33
Guest51433mietek: Ah, I see, let me try it out, i'll be right back24/04 19:33
Guest51433mietek: Mmh, apparently I still don't get it. Here is what I tried so far: https://pastebin.com/FBpZ3AUw24/04 19:52
Guest51433I think the solution on top should work, but refl is still kind of black magic for me..24/04 19:53
Guest51433Because there *is* a proof that xs == ys in scope?24/04 19:54
Guest51433mietek: Oh, god, I have to pattern match on refl to make sure, it exists.. Thank you, now it compiles!24/04 19:59

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