--- Day changed Mon Jan 23 2017 | ||

byorgey | rgrinberg: you mean like \oplus or \otimes ? | 23/01 02:33 |
---|---|---|

byorgey | you can also type \o+ or \ox | 23/01 02:34 |

byorgey | rgrinberg: also, pro tip: if you already have a particular symbol somewhere in a buffer, put the cursor on it and C-u C-x = will show you how to enter it | 23/01 02:35 |

subttle | Hi, my code is causing an internal error in Agda but I'm hesitent to file a bug report because I'm still learning and my code is pretty terrible :D The error is: | 23/01 09:35 |

subttle | An internal error has occurred. Please report this as a bug. Location of the error: src/full/Agda/Auto/CaseSplit.hs:285 | 23/01 09:35 |

subttle | I haven't been able to abstract the bug into a simpler case, so I was hoping someone could look at the code and help me do that so I don't have to publicly post my awful code in the bug report :D | 23/01 09:37 |

Saizan_ | subttle: are you using auto? | 23/01 09:39 |

Saizan_ | *agsy | 23/01 09:39 |

subttle | Saizan_: The bug happens when I try to lookup a solution from within a hole | 23/01 09:40 |

subttle | using Ctrl-C Ctrl-A | 23/01 09:40 |

subttle | here is the code | 23/01 09:45 |

subttle | http://pastebin.com/Ve3q4PhU | 23/01 09:45 |

subttle | the hole is on Line 187 | 23/01 09:46 |

subttle | if that means it is with agsy then would I report the bug somewhere else? | 23/01 09:50 |

Saizan_ | you would still report the bug to agda | 23/01 09:53 |

subttle | Oh and I'm using Agda 2.5.1 for the record | 23/01 09:54 |

subttle | Saizan_: roger | 23/01 09:54 |

Saizan_ | subttle: from the code at src/full/Agda/Auto/CaseSplit.hs the bug is related to metavariables, but it's hard to be more precise than that | 23/01 10:11 |

Saizan_ | subttle: your code is fine enough, maybe you can remove lots of the cases though? | 23/01 10:12 |

subttle | Saizan_: Okay thanks. I was hoping to compact it into fewer cases once I figured out how to finish the proof first. It's taking me a while to figure out though :) | 23/01 10:17 |

Saizan_ | subttle: i meant just for the bug report, to make it smaller, you could delete some of the constructors from the datatypes and also cases in the functions | 23/01 10:19 |

subttle | Saizan_: Ah, I see what you mean, I deleted over a thousand lines to get it this small, I should continue to trim it though :D | 23/01 10:21 |

subttle | Thanks for your help | 23/01 10:21 |

Saizan_ | cheers | 23/01 10:23 |

SuprDewd | Assuming the type of x can be inferred, is there any difference between 1) ∀ x, 2) ∀ (x : T) and 3) (x : T) ? | 23/01 13:23 |

apostolis | Is it possible to prove that A -> \bot , the negation of a proof is equal to any other negation of that proof. | 23/01 13:54 |

apostolis | ? | 23/01 13:54 |

{AS} | apostolis: you need functional extensionality for that I think | 23/01 13:55 |

apostolis | yes, but there must be a way to avoid it. | 23/01 13:55 |

apostolis | I hope. | 23/01 13:56 |

{AS} | apostolis: do you have the function in applied form? | 23/01 13:56 |

{AS} | I think you can prove (x, y : \bot) -> x \== y | 23/01 13:56 |

{AS} | apostolis: Yeah, you cna | 23/01 13:57 |

{AS} | apostolis: Yeah, you can | 23/01 13:57 |

apostolis | ok, but the negation of a proof is used unapplied when we put them in constructors or in types. | 23/01 13:58 |

{AS} | apostolis: why don't you just make them proof irrelevant? | 23/01 13:58 |

apostolis | What do you mean? | 23/01 13:59 |

{AS} | apostolis: like in the constructor | 23/01 13:59 |

{AS} | you can just make the argument proof irrelevant | 23/01 13:59 |

apostolis | I do not know what you mean? Can we do it? | 23/01 14:00 |

{AS} | apostolis: I am unsure what you mean :) | 23/01 14:00 |

apostolis | The last days I was proving that my proofs are unique (any two proofs are equal). | 23/01 14:00 |

{AS} | you can make Foo : .(P -> \bot) -> Bar | 23/01 14:01 |

{AS} | no? | 23/01 14:01 |

apostolis | That is the standard method of putting a negation (\neg) | 23/01 14:02 |

apostolis | It just happenned to have two negations and proofs that rely on any of the two, and I can not values that have one negation with values that have the other. | 23/01 14:05 |

apostolis | Consider a function f : A -> \neg C -> B | 23/01 14:13 |

apostolis | Regardless of the function g : \neg C , function f will produce the same result. | 23/01 14:13 |

apostolis | so one needs to prove that for g1 , g2 f a g1 = f a g2 . | 23/01 14:15 |

apostolis | But we shouldn't have to prove that. Negations should always be considered unique. | 23/01 14:16 |

{AS} | apostolis: you can just postulate uniqueness :) | 23/01 14:18 |

{AS} | or make the argument proof irrelevant | 23/01 14:19 |

apostolis | {AS} First time postulating something. This is it. | 23/01 14:21 |

apostolis | {AS} is there documentation on proof irrelevance. You must be saying something important and me not getting it. | 23/01 14:28 |

{AS} | http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Irrelevance | 23/01 14:28 |

apostolis | {AS} If you use a proof to eliminate a case, it cannot be irrelevant. (with \bot-elim for example) | 23/01 14:51 |

apostolis | Maybe I need to make an issue to disregard \bot-elim from irrelevance checking. | 23/01 14:54 |

{AS} | apostolis: you can make an irrelevant \bot-elim | 23/01 14:54 |

{AS} | apostolis: I tried doing that | 23/01 14:54 |

{AS} | I have a PR for the agda-stdlib | 23/01 14:54 |

apostolis | Oh nice. | 23/01 14:54 |

{AS} | https://github.com/agda/agda-stdlib/pull/116 | 23/01 14:55 |

mpickering | What does (f . _::_ _) mean? | 23/01 15:10 |

mpickering | the answer is (λ E x → θ ( _ ∷ E ) x) | 23/01 15:15 |

mpickering | thanks! | 23/01 15:15 |

apostolis | {AS} If only I knew proof irrelevance yesterday, thanks, now it works. | 23/01 15:42 |

SuprDewd | is it possible to have multiple rewrites in sequence? | 23/01 21:14 |

{AS} | SuprDewd: It is | 23/01 21:27 |

{AS} | use | | 23/01 21:27 |

{AS} | so rewrite a | b | c | 23/01 21:28 |

SuprDewd | {AS}: works great, thanks! | 23/01 21:43 |

{AS} | sure :) | 23/01 21:43 |

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