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 metalogical 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 oneline 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 