--- Day changed Mon Jul 31 2017 | ||

dolio | mietek: Well, in the example I gave, the problem is that the hypothetical checker is trying to do normalization in a context that isn't normalizing. | 31/07 01:38 |
---|---|---|

dolio | So, the obvious solution is to not try to do that. | 31/07 01:38 |

dolio | Then you reject more things that should work, but you terminate. And you recover the ability to work by saying exactly what evaluation should happen, instead of having the machine try to figure it out (which is impossible). | 31/07 01:39 |

dolio | Oh, and an example that might be more ordinary with respect to what jonsterling was saying is: just because you can't decide equality for something doesn't mean said equality is ill defined. And you can write down proofs that said things are equal and decide whether the proof is valid. | 31/07 01:50 |

dolio | Only instead of equality, we're trying to 'decide' whether judgments have a derivation, vs. check that a derivation of a judgment is valid. | 31/07 01:50 |

dolio | And the question is how much of the derivation you can omit/automate (for programmer/prover convenience) and still have the decision procedure. | 31/07 01:52 |

mietek | (n : Nat) → n ≟ n ≡ yes refl | 31/07 02:01 |

mietek | whyyy is this not obvious | 31/07 02:01 |

mietek | this is the stupidest lemma ever | 31/07 02:01 |

mietek | stupid : (n : Nat) → n ≟ n ≡ yes refl | 31/07 02:02 |

mietek | stupid n with n ≟ n | 31/07 02:02 |

mietek | stupid n | yes refl = refl | 31/07 02:02 |

mietek | stupid n | no n≢n = contradiction refl n≢n | 31/07 02:02 |

mietek | is this seriously the best we can do here? | 31/07 02:03 |

dolio | Is proving it by induction shorter? | 31/07 02:03 |

comietek | I would really rather wish this was already recognised by Agda as definitionally equal | 31/07 03:04 |

comietek | Agda knows that n = n | 31/07 03:05 |

comietek | definitional equality should be stronger than decidable equality, right? | 31/07 03:06 |

comietek | so we should get n =? n for free, I think | 31/07 03:06 |

comietek | but anyway, at least I can prove this and use this in REWRITE, so it's not half bad | 31/07 03:07 |

glguy | stupid : (n : ℕ) → (n ≟ n) ≡ yes refl | 31/07 03:35 |

glguy | stupid zero = refl | 31/07 03:35 |

glguy | stupid (suc n) rewrite stupid n = refl -- per dolios question | 31/07 03:35 |

glguy | Maybe with some preexisting lemmas that could have been: | 31/07 03:47 |

glguy | always : ∀ {a} {P : Set a} (unique : (p₁ p₂ : P) → p₁ ≡ p₂) (p : P) → (d : Dec P) → d ≡ yes p | 31/07 03:47 |

glguy | unique-refl : ∀ {a} {A : Set a} {x y : A} (p q : x ≡ y) → p ≡ q | 31/07 03:47 |

glguy | stupid n = always unique-refl refl (n ≟ n) | 31/07 03:47 |

mietek | "... is not a legal rewrite rule, since the following variables are not bound by the left hand side: x₁" | 31/07 09:49 |

mietek | what does this mean? x₁ does not appear in the code | 31/07 09:49 |

joel135 | What does {!!} mean? | 31/07 13:33 |

mietek | joel135: it’s a hole marker | 31/07 13:36 |

joel135 | ok | 31/07 13:37 |

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