--- Day changed Sun Feb 19 2017 | ||

subttle | I 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.agda | 19/02 00:24 |
---|---|---|

subttle | Is 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 |

subttle | Man, I just wish my school taught this so I didn't have to ask all these total beginner questions :D | 19/02 00:30 |

subttle | I have one more question if I may be so bold | 19/02 00:51 |

subttle | I have this code | 19/02 00:54 |

subttle | https://gist.github.com/subttle/2653d1dbf536325867541ca12da0e9a3 | 19/02 00:54 |

subttle | And the question is for the bottom comment | 19/02 00:54 |

subttle | what's the best way to go about writing that Injective instance | 19/02 00:55 |

subttle | any advice would be greatly appreciated.. Thanks! | 19/02 00:55 |

subttle | Oh 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 |

subttle | I'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 brevity | 19/02 01:07 |

mudri | subttle: your questions seem reasonable, but I need to sleep. Maybe I can help in the morning. | 19/02 01:09 |

subttle | mudri: no worries!! | 19/02 01:09 |

subttle | Also, if I'm doing something silly, by all means pull no punches, I'd rather know :D | 19/02 01:17 |

serendependy | subttle: I'm working on an lpaste for your first question (re: Eq reasoning). I'm not aware of any material that fully goes into details | 19/02 01:17 |

subttle | serendependy: Thanks!!!!! | 19/02 01:17 |

serendependy | subttle: http://lpaste.net/352696 | 19/02 01:29 |

subttle | serendependy: Excellent! Thank you, let me take a look!! | 19/02 01:30 |

subttle | serendependy: Awesome, thank you very much | 19/02 01:34 |

serendependy | subttle: 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-holes | 19/02 01:35 |

subttle | Nice, I'll check it out :D | 19/02 01:39 |

subttle | Just making sure I have this down... Is something like this alright? | 19/02 02:15 |

subttle | http://lpaste.net/352698 | 19/02 02:16 |

subttle | I'm still not 100% on how to "read" that aloud | 19/02 02:17 |

subttle | I mean I get that it's essentially a verbose version of | 19/02 02:19 |

subttle | n*0≡0 (suc n) rewrite n*0≡0 n = refl | 19/02 02:19 |

subttle | so I could pronounce line 6 as: "by refl.."? and then line 8 as: "by induction on n" ? | 19/02 02:20 |

subttle | sorry for harping on this, having a solid understanding of the fundamentals is very important to me | 19/02 02:20 |

serendependy | subttle: 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 explicitly | 19/02 06:19 |

subttle | serendependy: Awesome thanks again for all your help! | 19/02 06:20 |

serendependy | and 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 normalization | 19/02 06:21 |

serendependy | (i.e. the definition of _*_) | 19/02 06:21 |

subttle | Excellent | 19/02 06:22 |

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