StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

POIsabelle: Sledgehammer finds a proof but it fails
text
Body
copied!<p>Often times I have the problem that <code>sledgehammer</code> finds a proof, but when I insert it, it doesn't terminate. I guess <code>sledgehammer</code> is one of the most important parts of Isabelle, but then it gets annoying if a proof fails.</p> <p>In the <a href="http://isabelle.in.tum.de/doc/sledgehammer.pdf" rel="nofollow">Sledgehammer tutorial</a>, there is a small chapter on "Why does Metis fail to reconstruct the proof?".</p> <p>It lists:</p> <ol> <li>Try the <code>isar_proofs</code> option to obtain a step-by-step Isar proof where each step is justiﬁed by <code>metis</code>. Since the steps are fairly small, <code>metis</code> is more likely to be able to replay them.</li> <li>Try the <code>smt</code> proof method instead of <code>metis</code>. It is usually stronger, but you need to either have Z3 available to replay the proofs, trust the SMT solver, or use certificates.</li> <li>Try the <code>blast</code> or <code>auto</code> proof methods, passing the necessary facts via <code>unfolding</code>, <code>using</code>, <code>intro:</code>, <code>elim:</code>, <code>dest:</code>, or <code>simp:</code>, as appropriate.</li> </ol> <p>The problem is that the first option makes the proof more verbose and also it involves manual intervention. The second option rarely works.</p> <p>So what about the third option. Are there any easy to follow heuristics that I can apply?</p> <p>What's the difference between <code>unfolding</code> and <code>using</code>? Also are there any best practices on how to use <code>intro:</code>, <code>elim:</code>, and <code>dest:</code> from a failed <code>metis</code> proof?</p> <p><strong>Partial EXAMPLE</strong></p> <pre><code>proof- have "(det (?lm)) = (det (transpose ?lm))" by (smt det_transpose) then have "(det (?lm)) = [...][not shown]" unfolding det_transpose transpose_mat_factor_col by auto then show ?thesis [...][not shown] qed </code></pre> <p>I would like to get rid of the first line of the proof, as the line seems trivial. If I remove the first line, <code>sledgehammer</code> will still find a proof, but this found proof fails (doesn't terminate).</p>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload