--- Day changed Sun Feb 19 2017
subttleI have an awkward confession to make, I'm still not sure how to use equational reasoning from stdlib... This example doesn't help me because without comments, I don't follow https://github.com/agda/agda-stdlib/blob/e3893da0ebca8f80ca2919426529b544503d2010/src/Relation/Binary/EqReasoning.agda19/02 00:24
subttleIs there any short explaination somewhere? I've looked and it's hard to find one that gives at least a small comment at each step.. I'm not sure how to chain it all together. Would anyone be so kind as to enlighten me, please?19/02 00:24
subttleMan, I just wish my school taught this so I didn't have to ask all these total beginner questions :D19/02 00:30
subttleI have one more question if I may be so bold19/02 00:51
subttleI have this code19/02 00:54
subttlehttps://gist.github.com/subttle/2653d1dbf536325867541ca12da0e9a319/02 00:54
subttleAnd the question is for the bottom comment19/02 00:54
subttlewhat's the best way to go about writing that Injective instance19/02 00:55
subttleany advice would be greatly appreciated.. Thanks!19/02 00:55
subttleOh and to add to that real quick... I also have more relations... ne, le, etc... Is there a good way to prove generically that the relations hold for the Nats inside... I'm thinking maybe I'm supposed to use "Related" or something along those lines?19/02 01:01
subttleI'm thinking for my second question maybe I use some sort of Partial Order Reasoning? I have lots of proofs for _<r_ I just left them out for brevity19/02 01:07
mudrisubttle: your questions seem reasonable, but I need to sleep. Maybe I can help in the morning.19/02 01:09
subttlemudri: no worries!!19/02 01:09
subttleAlso, if I'm doing something silly, by all means pull no punches, I'd rather know :D19/02 01:17
serendependysubttle: I'm working on an lpaste for your first question (re: Eq reasoning). I'm not aware of any material that fully goes into details19/02 01:17
subttleserendependy: Thanks!!!!!19/02 01:17
serendependysubttle: http://lpaste.net/35269619/02 01:29
subttleserendependy: Excellent! Thank you, let me take a look!!19/02 01:30
subttleserendependy: Awesome, thank you very much19/02 01:34
serendependysubttle: There's also this library that makes writing the equations a little easier. Haven't tried it myself but looks neat: https://github.com/bch29/agda-holes19/02 01:35
subttleNice, I'll check it out :D19/02 01:39
subttleJust making sure I have this down... Is something like this alright?19/02 02:15
subttlehttp://lpaste.net/35269819/02 02:16
subttleI'm still not 100% on how to "read" that aloud19/02 02:17
subttleI mean I get that it's essentially a verbose version of19/02 02:19
subttlen*0≡0 (suc n) rewrite n*0≡0 n = refl19/02 02:19
subttleso I could pronounce line 6 as: "by refl.."? and then line 8 as: "by induction on n" ?19/02 02:20
subttlesorry for harping on this, having a solid understanding of the fundamentals is very important to me19/02 02:20
serendependysubttle: Yes basically a bit more verbose, though I believe if you wanted to reason about n*0=0 then using rewrite can make that a bit trickier. Generally, if the equality you want to show is not trivial, it's nicer to lay out the steps for any reader explicitly19/02 06:19
subttleserendependy: Awesome thanks again for all your help!19/02 06:20
serendependyand I would read it out loud as "0 + n * 0 = 0 by congruence of 0 +_ and induction". The refl part is completely superfluous - you get suc n * 0 = 0 + n * 0 by normalization19/02 06:21
serendependy(i.e. the definition of _*_)19/02 06:21
subttleExcellent19/02 06:22

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