CODEWITHSUNDEEP
isabelle
MooMooCoding
MooMooCoding

Reputation: 329

Isabelle: proof obligation - proving using counterexamples

For an example lemma like this:

lemma someFuncLemma: "∀ (e::someType) . pre_someFunc 2 e"

which gives the following when using quickcheck:

Auto Quickcheck found a counterexample:
  e = - 1

or when using Nitpick (which isn't really the main point here):

Nitpick found a counterexample:

  Skolem constant:
    e = - 1

How can I then use this counterexample to finish the proof?

As you can see, I'm not very familiar with Isabelle and POs.

Thank you for your help!

Upvotes: 0

Views: 502

Answers (2)

Shou
Shou

Reputation: 2009

I'm assuming you want to prove there exists some e such that pre_someFunc 2 e is false. You would have to change your lemma to use exists instead of forall, and prefix your predicate with not:

lemma "∃e::someType. ¬(pre_someFunc 2 e)"

Then you can provide the counter-example using rule exI[where x=...] which sets the free variable x in exI to something. You can look at the definition of exI and how x is used by clicking it while holding Ctrl in Isabelle JEdit.

A simple example:

lemma "∃n :: nat. ¬ odd n"
apply (rule exI[where x=2])
apply simp
done

Upvotes: 0

Florian Haftmann
Florian Haftmann

Reputation: 131

The presence of a counterexample usually indicates that you won't be able to prove your proposition, except maybe

  • the counterexample is spurious;

  • the underlying logic is inconsistent.

Upvotes: 3

Related Questions