Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-08-26

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
03:06 JCaesar joined #isabelle
06:19 aindilis` joined #isabelle
07:01 {AS} joined #isabelle
07:01 {AS} Hi, total beginner question. But what corresponds to "intro" from Coq in Isabelle?
07:05 larsrh {AS}: not quite sure what rules "intro" applies, but I think "apply safe" is a close candidate in Isabelle
07:05 larsrh it applies some default introduction rules
07:05 larsrh like conjunction introduction
07:06 {AS} larsrh: Thanks!
07:07 {AS} So maybe I should rephrase my question, if I have "/\ x. P x", how do i get something of P x' where x' is available to apply tactics on
07:10 {AS} Oh, I see, this is already how things work in Isabelle
07:10 ThreeOfEight {AS}: could you clarify that?
07:12 {AS} ThreeOfEight: So in Coq if you have a goal "forall x : Nat. P x" , in order to do induction on x, you have to use "introduction x" which gives you "x : Nat |- P x" (that is moves x to the context) and then you can do "induction x"
07:12 {AS} I was wondering how I moved things to the "context" in isabelle
07:12 ThreeOfEight ⋀ is the meta-logical universal quantifier
07:12 ThreeOfEight it is "transparent" in a way
07:13 ThreeOfEight if you have a goal of the form "⋀ a b c. …", then a, b, and c are locally fixed variables
07:13 {AS} ThreeOfEight: Aha, interesting :)
07:13 {AS} Thanks :)
07:14 ThreeOfEight However, to do induction, you have to do something like "apply (induction a)", which will not work because referencing locally fixed variables is tricky
07:14 ThreeOfEight (depending on where those variables come from, their names might change)
07:14 {AS} ThreeOfEight: Yeah
07:14 ThreeOfEight (so referencing locally fixed variables by name is discouraged)
07:15 ThreeOfEight you can do something like "apply (induct_tac a)", but as I said, that is discouraged
07:15 ThreeOfEight the best way to do something like this is to do a structured Isar proof
07:15 ThreeOfEight but these things are best explained by example, so if you have some snippet of code, I will happily comment on it
07:16 {AS} ThreeOfEight: Sure, I will just paste it
07:17 ThreeOfEight you can use http://downthetypehole.de/paste (which has Isabelle syntax highlighting)
07:18 {AS} ThreeOfEight: Thanks, here it is: http://downthetypehole.de/paste/Aov9eR0g
07:18 {AS} I am stuck on the last proof
07:19 {AS} This is btw one of the sample Isabelle files
07:19 {AS} I just tried adding more methods to it :)
07:20 {AS} So my goal is " ⋀x' xs a seq. conc (reverse xs) (Seq x' Empty) = Seq a seq ⟹ len seq < Suc (Suc (len xs))"
07:20 {AS} so I know that my hypothesis gives me Suc (len xs) = len seq
07:21 {AS} but I don't know how to go from my hypothesis to that
07:28 ThreeOfEight {AS}: you can do this: http://downthetypehole.de/paste/ei8VCLLj
07:28 {AS} ThreeOfEight: Thank you very much!
07:29 ThreeOfEight I think there are probably nicer ways to write down that definition that are more amenable to automation
07:30 ThreeOfEight it takes some experience with the system to write things down in such a way that the automation (especially the simplifier) can handle them easily
07:30 ThreeOfEight (Makarius calls this "proof by correct definition")
07:32 ThreeOfEight {AS}: by the way, are you aware that by your definition, everything is a palindrome?
07:32 {AS} ThreeOfEight: Yes
07:33 {AS} I had the x == y before
07:33 {AS} but I wanted to try a simpler proof before :)
07:33 ThreeOfEight For termination, it should make no differene
07:33 ThreeOfEight *difference
07:34 {AS} Yeah
07:34 {AS} ThreeOfEight: Is there a guide how to write it like this?
07:34 ThreeOfEight In any case, my approach would be to define "isPalindrome xs ⟷  xs = reverse xs"
07:34 ThreeOfEight then you don't have to prove termination
07:35 ThreeOfEight and you can easily prove the recursive characterisation
07:35 {AS} Oh that makes sense
07:35 ThreeOfEight {AS}: What do you mean?
07:35 {AS} I mean, I am unsure how you solved the goals by using fix assume etc. :)
07:35 {AS} and how you were able to pick the right definitions
07:36 {AS} because it seems to me that somehow we only changed the proof state in the "thus" command
07:36 {AS} I was wondering if you got some tips on how to do this
07:39 ThreeOfEight well the "fix" stuff is Isar
07:39 ThreeOfEight there are some tutorials about how to write structured Isar proofs
07:40 ThreeOfEight the relevant step in my proof is to use the equation "reverse (Seq x' xs) = Seq y ys"
07:40 {AS} ThreeOfEight: Thanks, I will take a look at that :)
07:40 ThreeOfEight I essentially said "if they're equal, then their lengths must be equal"
07:40 ThreeOfEight and then everything falls into place easily
07:40 ThreeOfEight automation is not smart enough to figure this out on its own
07:41 {AS} Aha
07:42 {AS} so even if I had len_reverse, it would not apply it to the hypotheses automatically
07:42 {AS} In any case, thanks very much!
08:56 popinman322 joined #isabelle
09:11 silver joined #isabelle
09:25 {AS} So I often find that sledgehammer returns hard to understand proofs. Is the idea more to use sledgehammer to check whether it is provable and then do a manual proof by hand?
09:29 larsrh {AS}: no, many people will happily use complicated sledgehammer proofs
09:29 larsrh But sure, it's no problem to try and reprove it using Isar
09:30 larsrh (it's also very common that auto/force/... solve goals in mysterious ways, but as long as it's solved, you don't care)
09:31 {AS} OK, interesting, thanks. So usually it depedends whether people care about reading their proofs (with Isar) or just want to show that the theorem holds.
09:31 {AS} I see
09:31 larsrh right
09:32 larsrh In an ideal world people would be writing their proofs in a readable way
09:32 larsrh that's what Isar is for!
09:32 larsrh But in the actual world people need to carry on with their task at hand, so there's often a time constraint involved
09:32 larsrh a common workflow is: make it quick & dirty for the paper deadline, make it a little bit more beautiful for AFP submission afterwards
09:33 {AS} Makes sense
09:36 {AS} In a sense I was perhaps wondering if sledgehammer could provide slightly more beautiful proofs automatically (I know, I know, it is a hard research project, but it would be so cool :) ).
09:37 larsrh sledgehammer tries doing that already :-)
09:38 larsrh There is an "Isar proof" option which will give you, well, an Isar proof
09:38 {AS} larsrh: Oh, let me see
09:38 larsrh and it internally tries to compress it so that you don't get lots of tedious details
09:38 larsrh still, it can look strange
09:44 {AS} Ah cool
09:45 {AS} Isabelle really has a lot of cool automation features :)
09:48 ThreeOfEight actually, Sledgehammer's "Isar proofs" are still pretty ugly
09:48 ThreeOfEight and I think sledgehammer only generates Isar proofs when the goal is too difficult for a one-line proof
09:51 {AS} ThreeOfEight: Yeah, I wanted to test it, but I couldn't come up with a "difficult enough" theorem that made sense to see the output :)
10:02 {AS} I mean it should also not be too difficult because then sledgehammer times out :)
11:32 ammbauer http://xkcd.com/1724/
11:41 {AS} Heh
14:19 silver joined #isabelle
15:13 mal`` joined #isabelle
20:47 {AS} joined #isabelle
20:59 kyagrd joined #isabelle
23:19 kyagrd joined #isabelle

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary