--- Day changed Sat Feb 25 2017 | ||

wedify | i don't know how to write 'toℕ⁺'; http://lpaste.net/352953 | 25/02 02:24 |
---|---|---|

wedify | oh the isDoubleOf exercise turned out to be easy; write a constructor 'doubleOfBase : {a : ℕ} → DoubleOf a (a + a)' | 25/02 02:52 |

wedify | here i was trying to do something with passing in a proof 'div a 2 \== (_ , 0)' | 25/02 02:53 |

wedify | er wait i mean 'div a b \== (2 , 0)' | 25/02 02:55 |

lpaste_ | wedify pasted “why can't i prove emptiness?” at http://lpaste.net/352954 | 25/02 03:38 |

tomjack | wedify: don't touch the green slime ;) | 25/02 05:00 |

tomjack | I wonder if that really means what I think it means | 25/02 05:00 |

tomjack | the blue stuff in the indices in the return types of your constructors -- the '+' in (a + 1) -- is harmful | 25/02 05:02 |

tomjack | better be green, like (1 + a). but agda will render this in blue, even though it's really (suc a) or whatever, which is green | 25/02 05:02 |

wedify | tomjack: thanks! long time no see. i changed the 'a + 1's to 'suc a' and now i can prove emptiness :) | 25/02 05:15 |

wedify | are you willing to help with my 'toℕ⁺'? | 25/02 05:17 |

tomjack | if you try to split on the argument with C-c C-c, agda gives a somewhat clearer error | 25/02 05:17 |

wedify | tomjack: it tells me it is stuck on a unification problem. i don't find the message any clearer than before. i think i get what the problem is though. i have 'n >= 0 == true' but need 'n >= 1 == true' | 25/02 05:26 |

wedify | i don't know what to do about it | 25/02 05:26 |

tomjack | oh, my message was not a response | 25/02 05:28 |

tomjack | I didn't see your toN | 25/02 05:28 |

tomjack | I dunno what your definitions are like | 25/02 05:40 |

tomjack | but "if n were zero it would've matched the previous clause" -- agda doesn't reason this way | 25/02 05:40 |

tomjack | maybe try {-# OPTIONS --exact-split #-} and replace the literal nats with constructors | 25/02 05:41 |

tomjack | well, --exact-split will cause an error if you make a mistake like this, but I guess it's not clear | 25/02 05:44 |

tomjack | the next case is not (suc n), it's (suc (suc n)) | 25/02 05:44 |

tomjack | use C-c C-c more :P. if you let agda do it for you it won't get screwed up (as often?) | 25/02 05:46 |

glguy | wedify: You'll need a different pattern for the last case | 25/02 05:47 |

glguy | it's not enough to match suc n, you need to match suc (suc n) | 25/02 05:48 |

glguy | It's only OK to use toN recursively when the input was at least 2 | 25/02 05:49 |

lpaste_ | wedify pasted “still get a similar error” at http://lpaste.net/352960 | 25/02 06:20 |

lpaste_ | wedify revised “still get a similar error”: “still get a similar error” at http://lpaste.net/352960 | 25/02 06:20 |

glguy | You need : toℕ⁺ (suc (suc n)) = suc⁺ (toℕ⁺ (suc n) {{!!}}) | 25/02 06:28 |

glguy | and you'll need to prove that n >= 0 == true | 25/02 06:28 |

glguy | Because of the way that you chose to define _>=_, you'll have to prove that separately | 25/02 06:28 |

glguy | Or if you want to do it inline you can expand out another case and you'll have: toℕ⁺ (suc (suc (suc n))) = suc⁺ (toℕ⁺ (suc (suc n)) {refl}) | 25/02 06:31 |

glguy | These == terms aren't good candidates for being implicit parameters | 25/02 06:32 |

glguy | wedify: If you simplify your definition of _>=_, you don't need the extra work in toN+ | 25/02 06:35 |

glguy | _≥_ _ zero = true | 25/02 06:35 |

wedify | glguy: ok thanks :) it works now. i would never have figured that out on my own | 25/02 06:38 |

wedify | glguy, tomjack: you guys are making this so much easier. it's much appreciated | 25/02 06:42 |

lpaste_ | wedify pasted “did i do it right?” at http://lpaste.net/352962 | 25/02 08:22 |

wedify | nevermind i found an example where it doesn't work | 25/02 08:27 |

lpaste_ | wedify pasted “now i think i have it ” at http://lpaste.net/352963 | 25/02 09:24 |

wedify | anyways g'night | 25/02 09:25 |

wedify | holy it's almost 3 | 25/02 09:25 |

wedify | it doesn't feel like i've been at it for hours :) | 25/02 09:25 |

rribeiro | Hi! Could someone explain to me how to instantiate Algebra.RingSolver to a Semiring, as both defined in standard library? | 25/02 18:30 |

glguy | You can't. | 25/02 18:32 |

glguy | At at least you can't in general, maybe that was one were it was possible... | 25/02 18:33 |

glguy | I made a number of solvers in the past for different structures | 25/02 18:33 |

glguy | https://github.com/glguy/my-agda-lib/tree/master/Algebra | 25/02 18:33 |

glguy | The ring solver will rely on the type having all the operations of a ring to normalize the inputs. If you don't have ring then that process won't work | 25/02 18:37 |

glguy | Do you perhaps have a commutative semiring? | 25/02 18:40 |

rribeiro | glguy: Thanks for answering. The point is that my formalization relies on a Semiring. | 25/02 18:47 |

glguy | OK, then you'll probably need to make a new solver | 25/02 18:48 |

rribeiro | Yeah... that's what I'd like to avoid... :) | 25/02 18:49 |

wedify | it's a pity we can't use holes in patterns. it would make proving emptiness easier | 25/02 23:03 |

lpaste_ | wedify pasted “stuck on af” at http://lpaste.net/352985 | 25/02 23:20 |

wedify | i'm trying to prove that a list contains no duplicates. i'm stuck on 'NotMember 2 (2 \:: [])' | 25/02 23:21 |

wedify | it wants '2 \== 2 \r \bot' and i don't know how to show that it's absurd | 25/02 23:22 |

lpaste_ | wedify revised “stuck on af”: “stuck on af” at http://lpaste.net/352985 | 25/02 23:22 |

mudri | wedify: the way to get around that is to keep up the supposition that you have f : 2 ≡ 2 → ⊥, and from it prove your desired ⊥. | 25/02 23:38 |

mudri | Absurd patterns only really work on sum-of-products data types, not functions. With functions, you usually have to apply them a bit more. | 25/02 23:40 |

mudri | Also, fresh variables in patterns are as good a holes. You always have a hole on the right-hand side, and refining your pattern variable means case splitting using C-c C-c. | 25/02 23:43 |

mudri | C-c C-c will also make absurd patterns for you. | 25/02 23:44 |

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