Inequality reasoning in Isabelle

Question

I have the following simple proof:

lemma
    fixes a b n :: nat
    assumes a: "a > n" "b > n"
    shows "a*b > n*n"
proof -
    from assms show "a*b > n*n" by(simp_all add: field_simps)  ERROR
qed

In the proof state, Isabelle says:

Successful attempt to solve goal by exported rule: n * n < a * b

But then:

Failed to apply initial proof method⌂: using this: n < a n < b goal (1 subgoal): 1. n * n < a * b

What is the problem?. Actually im interested in the actual single steps to do the proff, so i tought isabelle could show me the way.

Manuel Eberl Manuel Eberl · Accepted Answer · 2016-11-16T07:08:57

field_simps is good for rearranging terms, but not so good for this kind of reasoning. When you want to prove something like this, you typically need a good rule for it; in this case something about (strict) inequalities and multiplication.

If you have something that looks trivial but you don't know how to prove it exactly and/or you don't know what the relevant facts are called in Isabelle, sledgehammer is often helpful:

from assms show "a*b > n*n"
  sledgehammer

  > Sledgehammering... 
  > Proof found... 
  > "cvc4": Try this:
  >   by (metis (no_types, lifting) dual_order.strict_trans gr_implies_not_zero 
  >         linorder_neqE_nat mult.commute nat_0_less_mult_iff 
  >         nat_mult_less_cancel1) (796 ms)

The problem with proofs found by sledgehammer is that, as you can see, they are frequently lengthy, slow, and not very illuminating. On the maintenance side of things, they are also somewhat fragile w.r.t. changes in the background theory. Still, it's a good place to start and you can often read relevant facts for your proof from the sledgehammer proofs (e.g. nat_mult_less_cancel1 here).

Another way to find relevant facts is the find_theorems command or, equivalently, the Query panel in the Isabelle/jEdit IDE. If you do

find_theorems "_ * _ > _ * _"

or, equivalently, enter _ * _ > _ * _ into the Query panel, you get a lot of output to read through, but some relevant facts hide at the end of that output, e.g. mult_strict_mono':

thm mult_strict_mono'
> ?a < ?b ⟹ ?c < ?d ⟹ 0 ≤ ?a ⟹ 0 ≤ ?c ⟹ ?a * ?c < ?b * ?d

Your proof then looks like this:

from assms show "a*b > n*n"
  by (rule mult_strict_mono') simp_all

The simp_all just discharges the remaining proof obligations n ≥ 0.

Oh and by the way: The fact that you get a Successful attempt to solve goal but then an error message is a consequence of the non-linear nature of interactive Isabelle: When you write a by, the proof attempt is forked to the background and the processing of the proof document afterwards proceeds as if the proof had succeeded. This is in order to allow for parallelisation and to allow users to continue working on documents even if some proofs are broken.

The Successful attempt message comes from the part of Isabelle that is invoked after a show, and that part sees a successful (but still pending) proof of a*b > n*n. However, you then immediately get an error message from the by (simp_all …) saying that the proof method failed. In batch processing mode, failures such as this are more drastic (and more obvious).

Inequality reasoning in Isabelle

1 Answers