--- Day changed Sat Feb 25 2017
wedifyi don't know how to write 'toℕ⁺'; http://lpaste.net/35295325/02 02:24
wedifyoh the isDoubleOf exercise turned out to be easy; write a constructor 'doubleOfBase : {a : ℕ} → DoubleOf a (a + a)'25/02 02:52
wedifyhere i was trying to do something with passing in a proof 'div a 2 \== (_ , 0)'25/02 02:53
wedifyer 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/35295425/02 03:38
tomjackwedify: don't touch the green slime ;)25/02 05:00
tomjackI wonder if that really means what I think it means25/02 05:00
tomjackthe blue stuff in the indices in the return types of your constructors -- the '+' in (a + 1) -- is harmful25/02 05:02
tomjackbetter be green, like (1 + a). but agda will render this in blue, even though it's really (suc a) or whatever, which is green25/02 05:02
wedifytomjack: thanks! long time no see. i changed the 'a + 1's to 'suc a' and now i can prove emptiness :)25/02 05:15
wedifyare you willing to help with my 'toℕ⁺'?25/02 05:17
tomjackif you try to split on the argument with C-c C-c, agda gives a somewhat clearer error25/02 05:17
wedifytomjack: 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
wedifyi don't know what to do about it25/02 05:26
tomjackoh, my message was not a response25/02 05:28
tomjackI didn't see your toN25/02 05:28
tomjackI dunno what your definitions are like25/02 05:40
tomjackbut "if n were zero it would've matched the previous clause" -- agda doesn't reason this way25/02 05:40
tomjackmaybe try {-# OPTIONS --exact-split #-} and replace the literal nats with constructors25/02 05:41
tomjackwell, --exact-split will cause an error if you make a mistake like this, but I guess it's not clear25/02 05:44
tomjackthe next case is not (suc n), it's (suc (suc n))25/02 05:44
tomjackuse 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
glguywedify: You'll need a different pattern for the last case25/02 05:47
glguyit's not enough to match   suc n, you need to match suc (suc n)25/02 05:48
glguyIt's only OK to use toN recursively when the input was at least 225/02 05:49
lpaste_wedify pasted “still get a similar error” at http://lpaste.net/35296025/02 06:20
lpaste_wedify revised “still get a similar error”: “still get a similar error” at http://lpaste.net/35296025/02 06:20
glguyYou need : toℕ⁺ (suc (suc n)) = suc⁺ (toℕ⁺ (suc n) {{!!}})25/02 06:28
glguyand you'll need to prove that n >= 0 == true25/02 06:28
glguyBecause of the way that you chose to define _>=_, you'll have to prove that separately25/02 06:28
glguyOr 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
glguyThese == terms aren't good candidates for being implicit parameters25/02 06:32
glguywedify: If you simplify your definition of _>=_, you don't need the extra work in toN+25/02 06:35
glguy_≥_ _ zero = true25/02 06:35
wedifyglguy: ok thanks :) it works now. i would never have figured that out on my own25/02 06:38
wedifyglguy, tomjack: you guys are making this so much easier. it's much appreciated25/02 06:42
lpaste_wedify pasted “did i do it right?” at http://lpaste.net/35296225/02 08:22
wedifynevermind i found an example where it doesn't work25/02 08:27
lpaste_wedify pasted “now i think i have it ” at http://lpaste.net/35296325/02 09:24
wedifyanyways g'night25/02 09:25
wedifyholy it's almost 325/02 09:25
wedifyit doesn't feel like i've been at it for hours :)25/02 09:25
rribeiroHi! Could someone explain to me how to instantiate Algebra.RingSolver to a Semiring, as both defined in standard library?25/02 18:30
glguyYou can't.25/02 18:32
glguyAt at least you can't in general, maybe that was one were it was possible...25/02 18:33
glguyI made a number of solvers in the past for different structures25/02 18:33
glguyhttps://github.com/glguy/my-agda-lib/tree/master/Algebra25/02 18:33
glguyThe 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 work25/02 18:37
glguyDo you perhaps have a commutative semiring?25/02 18:40
rribeiroglguy: Thanks for answering. The point is that my formalization relies on a Semiring.25/02 18:47
glguyOK, then you'll probably need to make a new solver25/02 18:48
rribeiroYeah... that's what I'd like to avoid... :)25/02 18:49
wedifyit's a pity we can't use holes in patterns. it would make proving emptiness easier25/02 23:03
lpaste_wedify pasted “stuck on af” at http://lpaste.net/35298525/02 23:20
wedifyi'm trying to prove that a list contains no duplicates. i'm stuck on 'NotMember 2 (2 \:: [])'25/02 23:21
wedifyit wants '2 \== 2 \r \bot' and i don't know how to show that it's absurd25/02 23:22
lpaste_wedify revised “stuck on af”: “stuck on af” at http://lpaste.net/35298525/02 23:22
mudriwedify: 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
mudriAbsurd 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
mudriAlso, 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
mudriC-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!