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

--- Day changed Fri Mar 17 2017
mudrirntz: 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
quchenWhere are all the autoreplacements for »enter symbol« stored? For example, where is \bot defined to yield ⊥?17/03 10:53
quchenIt would be handy to have a long list of possible symbols for reference17/03 10:53
gallaisquchen: `M-x agda-input-show-translations` should do it17/03 10:55
quchengallais: Any chance I can get that out of the Agda executable to STDOUT?17/03 10:55
quchenIt’s strange that I can’t find, say »subseteq«, in the Agda source at all17/03 10:56
gallaisIt's 100% emacs so I don't know17/03 10:56
quchenHmm okay, thanks, I’ll see where that gets me. Good to know something like that exists at all!17/03 10:57
gallaissome of the symbols are inherited17/03 10:57
gallaisthe important file is here: https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el17/03 10:57
gallais(subseteq is in the list produced by `M-x agda-input-show-translations`)17/03 10:58
quchengallais: Inherited?17/03 11:01
quchenFrom what?17/03 11:01
gallaishttps://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el#L15917/03 11:04
gallaisTeX apparently17/03 11:04
quchengallais: Oh. Well that’s pretty fancy then. :-)17/03 11:17
quchenSuppose 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
quchenShould I thus be able to write a theorem »notX : ¬ myTheorem«?17/03 14:12
quchenOr is neither the theorem nor its negation true in this case17/03 14:12
quchenI often find proofs I construct to be »partially impossible«, and I’m wondering what to make of this.17/03 14:15
quchenSome cases work out, others demand proving something absurd.17/03 14:15
quchenThe 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 sense17/03 14:16
comietekquchen: can you expand the first thing you said?17/03 16:08
comietekquchen: two cases, the first is defined, and the second one is...?17/03 16:08
comietekquchen: are you saying the second one is a hole that you know cannot be filled?17/03 16:10
quchencomietek: f true = Unit; f false = ⊥ – something along those lines.17/03 17:03
quchenWait, that went wrong. Let me rephrase.17/03 17:04
quchenf true = Unit, okay, proven.17/03 17:04
quchenThe »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
mietekIt’s not quite a hole, though.17/03 17:05
quchenThis gives me a proof where the »true« case is alright, but the »false« case gives me trouble.17/03 17:05
quchenmietek: Forget the line before the »rephrase« :-)17/03 17:05
mietekuh.17/03 17:06
quchenThat turned out entirely wrong (to my purpose)17/03 17:06
quchens/purpose/intention/17/03 17:06
mietekThen I still don’t understand.17/03 17:06
quchenconsider the »head« function.   head : ∀ {A} -> List A -> a.17/03 17:07
quchenWriting the »x :: xs« case is simple enough.17/03 17:07
quchenWriting the »[]« case is impossible.17/03 17:07
quchenIn conclusion, it is not the case that there is a value »head« of that type.17/03 17:08
quchenSuppose I wanted to put that into a theorem instead. How would I do that?17/03 17:08
mietekOK, so it is like I said in the beginning: you do have a hole that you know cannot be filled.17/03 17:08
mietekNow, you’d like to prove that this hole cannot be filled.17/03 17:08
mietekRight?17/03 17:08
mietekThat would be a meta-theorem about Agda.17/03 17:09
quchenYes, let’s try going that route and see whether we’re talking about the same thing. :-)17/03 17:09
quchenIt certainly sounds interesting.17/03 17:09
mietekIt’s likely that you’d have to formalise Agda in order to state the theorem.17/03 17:09
quchenUUUh okay17/03 17:09
gallaisquchen: you'd prove a weaker result. E.g. "head : ∀ {A} (xs : List A) -> NonEmpty xs -> A"17/03 17:10
quchenThat sounds a bit too tough for me right now hehe.17/03 17:10
mietekOr, perhaps, it would be sufficient to formalise some smaller system in which you can still express your theorem.17/03 17:10
quchengallais: I’d like to prove that »not head« follows from my inability to fill that hole17/03 17:10
gallaiswhere "NonEmpty [] = ⊥; NonEmpty (x :: xs) = Unit" (for instance)17/03 17:10
quchengallais: (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
quchenWhat about a theorem »notHead : \neg (∀ {A} -> List A -> A)?17/03 17:12
lpaste_gallais pasted “NotHead.agda” at http://lpaste.net/35363917/03 17:13
quchengallais: 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
mietekgallais: …17/03 17:14
mietekwow.17/03 17:15
mietekThis amounts to saying "assuming head is total leads to inconsistency", right?17/03 17:15
quchenYes.17/03 17:16
gallaisquchen: it depends17/03 17:16
quchenI find the proof a bit too short for something from this world, but yes. :-)17/03 17:16
mietekgallais: 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
gallaisThe forall is on the left of the arrow. It's a rank 2 type (if that means anything to you)17/03 17:19
quchenIt does.17/03 17:19
mietekquchen: 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
gallaisin other words: the caller gets to pick the type17/03 17:19
mietek[] is a fine list of values of any type, including type ⊥.17/03 17:19
quchenAaaah, the type of the [] is the crux!17/03 17:20
quchenAgda throws me back to the feelings I remember having from learning Haskell the first time :-)17/03 17:20
quchenI 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
quchenI 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
mietekquchen: what do you mean by "isn’t really a quantor/quantifier"?17/03 17:22
quchenmietek: 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
mietekOh, ∀ {A} is just shorthand for {A : Set _}, and it works as long as the level of the set can be inferred17/03 17:23
mietekWell, here, at least17/03 17:24
quchenI don’t think there’s Set in there, otherwise ∀ n -> succ n == succ n wouldn’t work17/03 17:24
mietekYes, I mean in this case17/03 17:24
quchenAh, I see.17/03 17:24
mietekhttp://agda.readthedocs.io/en/v2.5.2/language/function-types.html#notational-conventions17/03 17:25

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