Re: [isabelle] Problems with Real addition



On Wed, Jan 20, 2010 at 7:51 PM, Steve W <s.wong.731 at googlemail.com> wrote:
> I'm trying out addition in Real, but have run into some problems. Does
> anyone know why the first example below doesn't work but the second does? Is
> it a problem with the types?

Hi Steve,

This is not a problem with the types. It works exactly the same with
type int or rat as it does with real.

> axioms
> ax : "F(t) = 0"
>
> lemma test: "EX x. F(x) + 1 ~= 0"
> using ax
> by auto

You should realize that you are asking a lot of "auto" here, since
proving this lemma requires it to guess a witness for the existential
quantifier. The "auto" tactic can only guess witnesses in very limited
circumstances.

> axioms
> ax : "F(t) = 0"
>
> lemma test: "EX x. F(x) + 0 = 0"
> using ax
> by auto

Your second example happens to be one of the limited circumstances
where auto *can* solve an existential. Simplification replaces "F(x) +
0" with "F(x)", leaving the subgoal

"EX x. F(x) = 0"

which just happens to match up perfectly with the rule "ax" that you
provided. In general, you should only expect "auto" to solve
existentials if they can be solved in one step by rule exI.

Other tactics besides "auto" are better at solving existentials. For
example, the "metis" tactic can solve your goal:

lemma test: "EX x. F(x) + 1 ~= 0"
using ax
by (metis one_neq_zero add_0_left)

The drawback with metis is that you need to supply all the other
lemmas needed to solve the goal.

In the end, it is often easiest to just provide the witness yourself:

lemma test: "EX x. F(x) + 1 ~= 0"
proof
  show "F(t) + 1 ~= 0"
    using ax by simp
qed

Hope this helps,
- Brian





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.