# IRC log for #isabelle, 2012-04-18

All times shown according to UTC.

Time Nick Message
21:47 Kaki joined #isabelle
21:48 Kaki hello
21:48 Kaki Hello
21:48 Kaki I have a question about the Isabelle/Hol prover.
21:49 tomprince Kaki: If you have a question, you should just ask it (although this channel tends to be very quiet)
21:57 Kaki joined #isabelle
21:59 Kaki I have a bad internet connection so I'm answering late, sry
21:59 Kaki I want to prove a simple thing in the system: http://pastebin.com/jMbey9DW
22:01 Kaki It seems to be a fairly simple step, but "by (simp)" is not accepted by the system
22:05 int-e are the 'n' the same?
22:10 int-e I think you should really provide a small theory to experiment with if you want help. Pasting the goal does not provide complete information (color is lost) and is impossible to experiment with.
22:12 Kaki Ok, ill prepare a small theory file.
22:23 Kaki joined #isabelle
22:24 int-e The  linarith  method may work. (it can prove  (n + 1) * (n + 1) + n * (n + 1) * (2 * n + 1) div 6 = (6 * (n + 1) * (n + 1) + n * (n + 1) * (2 * n + 1)) div 6  directly for me)
22:30 Kaki joined #isabelle
22:30 Kaki linarith worked for me too. Thats nice, thank you. But I'd like to know why my way didn't work. I'd appreciate your help. http://pastebin.com/tzcKxssE
22:36 Kaki "(6*(n + 1)*(n + 1) + n*(n + 1)*(2 * n + 1)) div 6 =((n + 1)*(6*(n + 1) + n*(2*n + 1))) div 6" is not working even with "by (linarith)"
22:47 int-e Oh I see. 6*((n + 1)*(n + 1)) and 6*(n+1)*(n+1) are not obviously the same.
22:50 int-e so... unfolding nat_mult_assoc by simp  also finishes that step.