https://stackoverflow.com/questions/20997548
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
RussianYou can let the auto tools give you a big head start. It will take me much more work to tell you the multiple ways to get feedback from the auto tools than it took me to prove the theorem.
datatype bc_t = B | C
lemma "∀ x::bc_t . (x = B ⟶ x ~= C)"
try0
using[[simp_trace]]
using [[simp_trace_depth_limit=100]]
apply(simp)
done
lemma "∀ x::bc_t . (x = B ⟶ x ~= C)"
sledgehammer
by (metis bc_t.distinct(1))
I used try0 because I had unchecked Auto Methods in "Plugin Options / Isabelle / General". Many times in the options I have all the auto tools boxes checked other than Sledgehammer.
You can use sledgehammer as I show there or you can use it in the Sledgehammer panel of the PIDE. With simp_trace, when you put your cursor on the line with apply(simp), you can learn how the simp method proved it, which will be based on substitution rules.
Update 140108_1305
The auto tools are important for helping us work fast, but it's also important to sometimes understand the basic logic of the proof. This is where simp_trace and other attributes of the simp method can be useful. Read tutorial.pdf, prog-prove.pdf and isar-ref.pdf for some details and lessons on using simp.
Three such attributes for controlling the simp method are add, del, and only.
In your example, I want to use the simp_trace, along with only, to make it explicit what rules are being used, to maybe help me understand the logic.
The metis proof by Sledgehammer makes it appear that simp may only be using a few rules. I look at the simp trace and let simp only use rules that I can cut and paste from the control panel. I count 4 named rules, and this is not going to actually turn out to be something that's worth doing, though I had to find that out.
[Update 140101_0745: Trying not to over analyze the situation, I ended up using del because my grand scheme of using only wasn't working out. With simp only in the place of simp del below, the apply method fails with an error, which means it can't simplify the goal with only those four rules. This will not be the case with auto simp only instead of simp only. The auto method isn't limited in the way simp is, and it may do many things it won't tell you about, such as calling blast.]
lemma "∀ x::bc_t . (x = B ⟶ x ~= C)"
using[[simp_trace]]
using [[simp_trace_depth_limit=100]]
apply(simp del:
bc_t.distinct(1)
simp_thms(8)
simp_thms(17)
simp_thms(35)
)
oops
Well, now when I look at the newest simp trace, there are bunch more simp rules. The simplifier has more than 1 stone to kill the bird, so I give up.
One thing to remember is that you can use simp with methods like auto and fastforce, like apply(auto simp add: stufferThm). With auto in particular, if the simp rules are not enough to prove a theorem, it may resort to using blast, which won't show up in the simp trace. This is important to know when using only, so you're not under the impressions that the simp rules are all that's needed for a proof that's found by auto.
Here I make some comments about your comment below.
If simp stays purple very long, it's having to do a massive number of simplifications, or it's in a non-terminating loop, as Eberl mentions. Either is bad. I don't consider a 40 second simp proof a good proof.
Basically, it's very easy to get simp in a loop, or any of the other methods that call simp, especially if you're defining your own simp rules. The simp method is easy when it works. When it doesn't, you may have to work for your logic.
Use try0, and when no proof is found, it will give you a list of automatic proof methods to experiment with, like force, fastforce, auto, etc. If simp is looping with auto, you might try it with fastforce. Experimenting counts for a lot.
One other important thing to remember is to unfold definitions that aren't simp rules. Sledgehammer can sometimes find definitions, but sometimes the most simple of theorems can't be proved because a definition hasn't been unfolded.
[Update 140109_0750: Making generalizations is always risky. Unfolding a definition will many times prevent Sledgehammer from finding a proof. Sledgehammer works well by matching up high-level theorems, so a hopelessly expanded formula will many times doom it to failure. Even a hugely expanded formula can cause other auto methods to not be able to find a proof. However, for things of a computational nature based on equations, expanding definitions can allow simp to completely reduce a huge, complicated expression. You have to know when to hold them, and when to unfold them. The great thing is it's easy to try lots of things reasonably fast.]
definition stuffTrue :: "bool" where
"stuffTrue = True"
theorem "stuffTrue"
apply(unfold stuffTrue_def)
by(simp)
It's not the question that's trivial. Simple things aren't necessarily easy to prove. What's trivial is the typing that's required once you learn how to use the auto tools.
