/home/laney/.irssi/irclogs/Freenode/#agda.log-20170615

--- Day changed Wed Jun 14 2017
yhhkoare there any common idioms for doing proofs that involve "without loss of generality"? my particular use case is an assumption that with f : X -> Bool,  and x,y : X,  and assuming f x \= f y,  we may assume wlog that f x == true and f y == false14/06 15:45
{AS}yhhko: how can you assume that14/06 16:08
{AS}f x could be false and f y would then be true14/06 16:09
yhhkoright. but the claim being made is symmetric (in a vague sense) in x and y.14/06 16:09
{AS}But in general you can make these proofs yes14/06 16:10
yhhkoiow, the proof would work out by swapping x and y in your case14/06 16:10
yhhkobut what's an elegant way to say "in that case, swap x and y" in agda?14/06 16:10
{AS}I mean you can write it using an either, no?14/06 16:11
yhhkoyeah, but i'd prefer not to copy a bunch of code14/06 16:11
yhhkoor perhaps i don't understand you14/06 16:12
dolioIf you write a proof that assumes that f x = true and f y = false, then you can write a proof that tests whether f x = true and f y = false or the opposite, and calls your first proof with x and y swapped.14/06 16:12
yhhkodolio: okay. that's roughly what i'm doing so far, except i'm finding it quite tiresome to do this testing as there's actually not just an x, but really an x1, x2, x3, x4, and ditto for y14/06 16:14
{AS}yhhko: consider using a macro14/06 16:15
{AS}One that just takes a function, a list of arguments and then tries them in different orders14/06 16:15
yhhko{AS}: you mean a macro as in reflection?14/06 16:16
{AS}Yeah14/06 16:16
comietekdoes a higher order function not work here?14/06 18:59

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