Email Gateway (Aug 18 2022 at 14:34): Email Gateway (Aug 18 2022 at 14:34):From: John Munroe <munddr@googlemail.com>
Hi,
I'm trying to show that two function objects are equal in the following:
theory T1
imports Real
begin
typedecl T
consts
func1 :: "T => real"
func2 :: "T => real"
func3 :: "T => real"
locale loc =
assumes ax1: "func1 p = func2 p / func3 p"
and ax2: "func3 p > 0"
lemma (in loc) lem1: "ALL p. func2 p = func1 p * func3 p"
using ax1 ax2
by (metis divide_le_eq divide_less_eq order_eq_refl order_less_irrefl xt1(11))
lemma (in loc) lem2:
assumes "loc"
shows "func2 = (%s. func1 s * func3 s)"
using lem1
by auto
Does anyone know why having lem1 as a fact is insufficient to complete
the proof?
Any help will be appreciated.
Thanks,
John
Email Gateway (Aug 18 2022 at 14:34):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
John Munroe wrote:
Try rule 'ext', specifically by (auto intro: ext)
by (blast intro: ext) also solves it
Isabelle doesn't apply ext within auto by default, possibly as it can
lead to explosions with recursive functions.
Sincerely,
Rafal Kolanski.
Email Gateway (Aug 18 2022 at 14:35):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi John,
You must tell auto explicitly to use function extensionality. Both
by(auto intro: ext)
and
by(auto simp: expand_fun_eq)
work for your example lemma. expand_fun_eq is more aggressive because it
also works on the assumptions.
Best regards,
Andreas
Email Gateway (Aug 18 2022 at 14:36):From: John Munroe <munddr@googlemail.com>
Thanks for the help. Just curious, what if loc.ax1 is changed to:
"EX p. func1 p ~= func2 p / func3 p"
Can auto/blast intro: ext still be used to show that
"func1 ~= func2 / func3"?
In fact, why isn't ext defined with iff instead, i.e.:
lemma ext: "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) <==> (%x. f(x))=(%x. g(x))"
Thanks again.
John
Email Gateway (Aug 18 2022 at 14:36):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi John,
Thanks for the help. Just curious, what if loc.ax1 is changed to:
"EX p. func1 p ~= func2 p / func3 p"
Can auto/blast intro: ext still be used to show that
"func1 ~= func2 / func3"?
What should func2 / func3 be? There is no division operator for
functions in HOL by default. I guess you mean "%p. func2 p / func3 p".
No, you cannot use ext for that: The inequality is first turned into
equality in the assumptions by the rule notI, which leaves you to show
False. Since ext is typically used as an introduction rule, it cannot be
applied to False. In this case, expand the function equality in the
assumptions with expand_fun_eq: by(auto simp: expand_fun_eq).
In fact, why isn't ext defined with iff instead, i.e.:
lemma ext: "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) <==> (%x. f(x))=(%x. g(x))"
Since "%x. f(x)" is eta-equal to f and similarly for g, the backward
direction of your rule is build into the simplifier, so it is hardly
useful. Your lemma is almost expand_fun_eq[symmetric], except for the
meta-quantifier !! being replaced the HOL quantifier !
If you like, you could also prove this lemma:
lemma "(!!x. f x = g x) == (Trueprop (f = g))"
by(rule equal_intr_rule)(auto intro: ext)
Note that there is no meta-biimplication in Isabelle, so I used
meta-equality instead. Trueprop converts boolean terms to propositions
and is added to most lemmas implicitly. Since meta-quantifiers are mixed
with meta-equality here, it must be explicitly written out.
Andreas
Email Gateway (Aug 18 2022 at 14:36):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi John,
Now, given similar lemmas, it seems several lemmas with a False
consequence can be proven. For example, given:...
lemma (in loc3) lem4:
shows "EX g. func1 g ≠ func 1 g"
using ax21 ax11
by autolemma (in loc3) lem5:
shows "False"
using ax21 ax11
by autoAre lem4 and lem5 essentially the same?
Depends on your understanding of essentially. Syntactically, they are
inherently different. For reasoning, they also behave differently (lem4
cannot be used as an introduction rule for "False", for instance).
However, you can prove everything with either of them, so logically,
they are the same.
Does Isabelle simplify lem4's
goal to False?
Yes, if you tell Isabelle to do so. Try
thm lem4
thm lem4[simplified]
Or even, does it try to simplify every goal to False
first before moving on?
No, Isabelle does no simplification by its own. However, whenever you
apply some method or tactic which invokes the simplifier (like simp,
simp_all, clarsimp, auto, fastsimp, bestsimp, force) then the simplifier
uses its set of rewrite rules to simplify to the goal. Methods and
tactics without simplifier (like rule, clarify, safe, blast, iprover,
best, fast) obviously don't do this.
For more information about the simplifier, read Sec. 3.1 in the Tutorial
on Isabelle/HOL.
Regards,
Andreas
Email Gateway (Aug 18 2022 at 14:36):From: munddr@googlemail.com
Thanks for the input -- that's very useful.
Now, given similar lemmas, it seems several lemmas with a False consequence
can be proven. For example, given:
typedecl T
types S = "T set"
consts
func1 :: "T ⇒ real"
func2 :: "T ⇒ real"
func3 :: "T ⇒ real"
locale loc1 =
assumes ax11: "func1 p = func2 p / func3 p"
and ax12: "func3 p > 0"
locale loc2 =
fixes G :: S
assumes ax21: "EX g : G. func1 g ≠ func2 g / func3 g"
locale loc3 = loc1 + loc2
lemma (in loc3) lem4:
shows "EX g. func1 g ≠ func 1 g"
using ax21 ax11
by auto
lemma (in loc3) lem5:
shows "False"
using ax21 ax11
by auto
Are lem4 and lem5 essentially the same? Does Isabelle simplify lem4's goal
to False? Or even, does it try to simplify every goal to False first before
moving on?
Thanks again
John
Last updated: Apr 23 2024 at 16:19 UTC