--- Day changed Fri Mar 17 2017 | ||

mudri | rntz: IIRC, you can have the function just be id, and inspect still works. | 17/03 01:03 |
---|---|---|

* mudri doesn't understand inspect. | 17/03 01:04 | |

quchen | Where are all the autoreplacements for »enter symbol« stored? For example, where is \bot defined to yield ⊥? | 17/03 10:53 |

quchen | It would be handy to have a long list of possible symbols for reference | 17/03 10:53 |

gallais | quchen: `M-x agda-input-show-translations` should do it | 17/03 10:55 |

quchen | gallais: Any chance I can get that out of the Agda executable to STDOUT? | 17/03 10:55 |

quchen | It’s strange that I can’t find, say »subseteq«, in the Agda source at all | 17/03 10:56 |

gallais | It's 100% emacs so I don't know | 17/03 10:56 |

quchen | Hmm okay, thanks, I’ll see where that gets me. Good to know something like that exists at all! | 17/03 10:57 |

gallais | some of the symbols are inherited | 17/03 10:57 |

gallais | the important file is here: https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el | 17/03 10:57 |

gallais | (subseteq is in the list produced by `M-x agda-input-show-translations`) | 17/03 10:58 |

quchen | gallais: Inherited? | 17/03 11:01 |

quchen | From what? | 17/03 11:01 |

gallais | https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el#L159 | 17/03 11:04 |

gallais | TeX apparently | 17/03 11:04 |

quchen | gallais: Oh. Well that’s pretty fancy then. :-) | 17/03 11:17 |

quchen | Suppose I have a function with two cases, one of which is true (has a value on the RHS of the =), and one does provably not. This shows that »for some inputs, the theorem is wrong, for some inputs, the theorem is right«. This means that the theorem as a whole is not right, at least to my intuition. | 17/03 14:11 |

quchen | Should I thus be able to write a theorem »notX : ¬ myTheorem«? | 17/03 14:12 |

quchen | Or is neither the theorem nor its negation true in this case | 17/03 14:12 |

quchen | I often find proofs I construct to be »partially impossible«, and I’m wondering what to make of this. | 17/03 14:15 |

quchen | Some cases work out, others demand proving something absurd. | 17/03 14:15 |

quchen | The theorem ought to be wrong, since it claims that »for all X, something works«; but I can neither use the absurdity to prove everything (since I have valid cases), nor the valid cases to prove the theorem (since I have unprovable ones). | 17/03 14:16 |

quchen | … if that makes any sense | 17/03 14:16 |

comietek | quchen: can you expand the first thing you said? | 17/03 16:08 |

comietek | quchen: two cases, the first is defined, and the second one is...? | 17/03 16:08 |

comietek | quchen: are you saying the second one is a hole that you know cannot be filled? | 17/03 16:10 |

quchen | comietek: f true = Unit; f false = ⊥ – something along those lines. | 17/03 17:03 |

quchen | Wait, that went wrong. Let me rephrase. | 17/03 17:04 |

quchen | f true = Unit, okay, proven. | 17/03 17:04 |

quchen | The »false« case gives me a hole that is obviously un-fillable, like »x ∈ []«. | 17/03 17:04 |

mietek | ⊥ is uninhabited, yes. | 17/03 17:05 |

mietek | It’s not quite a hole, though. | 17/03 17:05 |

quchen | This gives me a proof where the »true« case is alright, but the »false« case gives me trouble. | 17/03 17:05 |

quchen | mietek: Forget the line before the »rephrase« :-) | 17/03 17:05 |

mietek | uh. | 17/03 17:06 |

quchen | That turned out entirely wrong (to my purpose) | 17/03 17:06 |

quchen | s/purpose/intention/ | 17/03 17:06 |

mietek | Then I still don’t understand. | 17/03 17:06 |

quchen | consider the »head« function. head : ∀ {A} -> List A -> a. | 17/03 17:07 |

quchen | Writing the »x :: xs« case is simple enough. | 17/03 17:07 |

quchen | Writing the »[]« case is impossible. | 17/03 17:07 |

quchen | In conclusion, it is not the case that there is a value »head« of that type. | 17/03 17:08 |

quchen | Suppose I wanted to put that into a theorem instead. How would I do that? | 17/03 17:08 |

mietek | OK, so it is like I said in the beginning: you do have a hole that you know cannot be filled. | 17/03 17:08 |

mietek | Now, you’d like to prove that this hole cannot be filled. | 17/03 17:08 |

mietek | Right? | 17/03 17:08 |

mietek | That would be a meta-theorem about Agda. | 17/03 17:09 |

quchen | Yes, let’s try going that route and see whether we’re talking about the same thing. :-) | 17/03 17:09 |

quchen | It certainly sounds interesting. | 17/03 17:09 |

mietek | It’s likely that you’d have to formalise Agda in order to state the theorem. | 17/03 17:09 |

quchen | UUUh okay | 17/03 17:09 |

gallais | quchen: you'd prove a weaker result. E.g. "head : ∀ {A} (xs : List A) -> NonEmpty xs -> A" | 17/03 17:10 |

quchen | That sounds a bit too tough for me right now hehe. | 17/03 17:10 |

mietek | Or, perhaps, it would be sufficient to formalise some smaller system in which you can still express your theorem. | 17/03 17:10 |

quchen | gallais: I’d like to prove that »not head« follows from my inability to fill that hole | 17/03 17:10 |

gallais | where "NonEmpty [] = ⊥; NonEmpty (x :: xs) = Unit" (for instance) | 17/03 17:10 |

quchen | gallais: (Aside: wow, encoding properties into types like that is nice. I tried doing it in a much more complicated way, such as adding a proof that for some ys, ys = x::ys. | 17/03 17:11 |

quchen | ) | 17/03 17:11 |

quchen | What about a theorem »notHead : \neg (∀ {A} -> List A -> A)? | 17/03 17:12 |

lpaste_ | gallais pasted “NotHead.agda” at http://lpaste.net/353639 | 17/03 17:13 |

quchen | gallais: Oh. Well that was easy. :-) But now consider the more general case: I have any number of case splits, one of which has an unfillable hole. I assume (due to the lack of LEM), this does not imply that I can write a »notX« proof? | 17/03 17:14 |

mietek | gallais: … | 17/03 17:14 |

mietek | wow. | 17/03 17:15 |

mietek | This amounts to saying "assuming head is total leads to inconsistency", right? | 17/03 17:15 |

quchen | Yes. | 17/03 17:16 |

gallais | quchen: it depends | 17/03 17:16 |

quchen | I find the proof a bit too short for something from this world, but yes. :-) | 17/03 17:16 |

mietek | gallais: thank you. I need to apply this somewhere… | 17/03 17:17 |

quchen | (Why does ⊥ work here? Why does not not complain about that it expected ⊥’? Do all uninhabited things unify automatically?) | 17/03 17:17 |

gallais | The forall is on the left of the arrow. It's a rank 2 type (if that means anything to you) | 17/03 17:19 |

quchen | It does. | 17/03 17:19 |

mietek | quchen: the assumption in notHead is that we have a machine which, given a list of values of type A, produces a value of type A. | 17/03 17:19 |

gallais | in other words: the caller gets to pick the type | 17/03 17:19 |

mietek | [] is a fine list of values of any type, including type ⊥. | 17/03 17:19 |

quchen | Aaaah, the type of the [] is the crux! | 17/03 17:20 |

quchen | Agda throws me back to the feelings I remember having from learning Haskell the first time :-) | 17/03 17:20 |

quchen | I don’t really understand how higher-rank types work in Agda, but that’s because I’m not very familiar with its type system, all types being passed as arguments and such. | 17/03 17:21 |

quchen | I mean the ∀ isn’t really a quantor in Agda, it’s a »find the type yourself« directive, and if you pair that with implicit parameters you get something that looks like rank-N types. | 17/03 17:22 |

mietek | quchen: what do you mean by "isn’t really a quantor/quantifier"? | 17/03 17:22 |

quchen | mietek: Well, ∀ just says that the following variables without types should have their types inferred, no? | 17/03 17:23 |

quchen | ∀ x {y} ⇒ (x : _) -> {y : _} | 17/03 17:23 |

mietek | Oh, ∀ {A} is just shorthand for {A : Set _}, and it works as long as the level of the set can be inferred | 17/03 17:23 |

mietek | Well, here, at least | 17/03 17:24 |

quchen | I don’t think there’s Set in there, otherwise ∀ n -> succ n == succ n wouldn’t work | 17/03 17:24 |

mietek | Yes, I mean in this case | 17/03 17:24 |

quchen | Ah, I see. | 17/03 17:24 |

mietek | http://agda.readthedocs.io/en/v2.5.2/language/function-types.html#notational-conventions | 17/03 17:25 |

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