--- Day changed Wed Jun 14 2017 | ||

yhhko | are 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 == false | 14/06 15:45 |
---|---|---|

{AS} | yhhko: how can you assume that | 14/06 16:08 |

{AS} | f x could be false and f y would then be true | 14/06 16:09 |

yhhko | right. 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 yes | 14/06 16:10 |

yhhko | iow, the proof would work out by swapping x and y in your case | 14/06 16:10 |

yhhko | but 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 |

yhhko | yeah, but i'd prefer not to copy a bunch of code | 14/06 16:11 |

yhhko | or perhaps i don't understand you | 14/06 16:12 |

dolio | If 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 |

yhhko | dolio: 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 y | 14/06 16:14 |

{AS} | yhhko: consider using a macro | 14/06 16:15 |

{AS} | One that just takes a function, a list of arguments and then tries them in different orders | 14/06 16:15 |

yhhko | {AS}: you mean a macro as in reflection? | 14/06 16:16 |

{AS} | Yeah | 14/06 16:16 |

comietek | does 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!