--- Day changed Mon Jul 31 2017
doliomietek: 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
dolioSo, the obvious solution is to not try to do that.31/07 01:38
dolioThen 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
dolioOh, 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
dolioOnly 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
dolioAnd 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 refl31/07 02:01
mietekwhyyy is this not obvious31/07 02:01
mietekthis is the stupidest lemma ever31/07 02:01
mietekstupid : (n : Nat) → n ≟ n ≡ yes refl31/07 02:02
mietekstupid n with n ≟ n31/07 02:02
mietekstupid n | yes refl = refl31/07 02:02
mietekstupid n | no n≢n   = contradiction refl n≢n31/07 02:02
mietekis this seriously the best we can do here?31/07 02:03
dolioIs proving it by induction shorter?31/07 02:03
comietekI would really rather wish this was already recognised by Agda as definitionally equal31/07 03:04
comietekAgda knows that n = n31/07 03:05
comietekdefinitional equality should be stronger than decidable equality, right?31/07 03:06
comietekso we should get n =? n for free, I think31/07 03:06
comietekbut anyway, at least I can prove this and use this in REWRITE, so it's not half bad31/07 03:07
glguystupid : (n : ℕ) → (n ≟ n) ≡ yes refl31/07 03:35
glguystupid zero = refl31/07 03:35
glguystupid (suc n) rewrite stupid n = refl -- per dolios question31/07 03:35
glguyMaybe with some preexisting lemmas that could have been:31/07 03:47
glguyalways : ∀ {a} {P : Set a} (unique : (p₁ p₂ : P) → p₁ ≡ p₂) (p : P) → (d : Dec P) → d ≡ yes p31/07 03:47
glguyunique-refl : ∀ {a} {A : Set a} {x y : A} (p q : x ≡ y) → p ≡ q31/07 03:47
glguystupid 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
mietekwhat does this mean?   x₁ does not appear in the code31/07 09:49
joel135What does {!!} mean?31/07 13:33
mietekjoel135: it’s a hole marker31/07 13:36
joel135ok31/07 13:37

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