Email Gateway (Aug 19 2022 at 12:02): Email Gateway (Aug 19 2022 at 12:02):From: Michael Vu <michael.vu@rwth-aachen.de>
Hi Andrew,
Thank you for your kind answer, that's what I searched for.
Regarding the first (and more important question) : the relation symbol can be treated as a "<" relation.
Andrew Boyton <Andrew.Boyton@nicta.com.au> schrieb:
Email Gateway (Aug 19 2022 at 12:04):From: Michael Vu <michael.vu@rwth-aachen.de>
Is there nobody with a clue?
Email Gateway (Aug 19 2022 at 12:04):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Dear Michael,
No, we are all clueless. ;)
I presume you refer to the first question you posted some time ago. First of all, the theory snippet you pasted into your email cannot be parsed back by Isabelle (importing "Complex_Complex"). The parser chokes on "⊩". That makes it harder for us to help you.
Second, there is no silver bullet in Isabelle that will prove finite goals. (I'm taking your claim at face value; being unable to parse the formula you sent, I cannot infer the types and check finiteness.) The closest thing to it is Nitpick, but you would have to trust it as an oracle. See e.g. my paper [1] for an instance where we used Nitpick for exhaustive verification.
I presume that a properly set up "blast" or "auto" might be able to finish the job. Sometimes it's just a matter of adding a few intro, elim, or split rules; perhaps one of the experts could help you, once they are given a self-contained example.
Regards,
Jasmin
[1] http://www21.in.tum.de/~blanchet/ppdp2011-cpp-mem.pdf
Email Gateway (Aug 19 2022 at 12:05):From: Michael Vu <michael.vu@rwth-aachen.de>
Dear Jasmin,
Indeed, that was my fault. I work with custom theories where this symbol is treated as "<" (less relation) and I forgot to replace it. Hope you could somehow help me now. My goal is just to make isabelle split all possible cases as they are finite and then solve every case for itself. Thanks!
Regards
Michael
Jasmin Blanchette <jasmin.blanchette@gmail.com> schrieb:
Email Gateway (Aug 19 2022 at 12:05):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Michael,
I fail to see why your problem is finite. The pair of assumptions "forall s. ..." quantify over all states, of which there are infinitely many. I see some "if"s that could perhaps be split into separate cases, but they are under the scope of lambdas that bind again an infinite variable.
Also, some of your variables seem to have overly general types, e.g. "a" has type 'a. Indeed, Nitpick reports a "potentially spurious" counterexample that appears to be genuine.
Regards,
Jasmin
Email Gateway (Aug 19 2022 at 12:05):From: Johannes Hölzl <hoelzl@in.tum.de>
Am Dienstag, den 08.10.2013, 18:14 +0200 schrieb Michael Vu:
Dear isabelle experts,
I am currently working with records and I'm trying to write a small automation tool for generating calculations. But I'm stuck at proving some simple expressions like this one:
record state =
t :: real
c :: reallemma weakly_bounded:
"0 < a ⟹
a < 1 ⟹
0 < b ⟹
b < 1 ⟹
0 < a + b - a * b ⟹
∀s. t s = 0 ∨ t s = 1 ⟹
∀s. c s = 0 ∨ c s = 1 ⟹
λs. (if t s = 0 ∧ c s = 0 then 1 else 0) + (if t s = 0 ∧ c s = 1 then 1 else 0) * a / (a + b - a * b) +
(if t s = 1 ∧ c s = 1 then 1 else 0) * (1 - b) * a /
(a + b -
a * b) ⊩ λs. (if c s ≠ 1 then 1 else 0) * ((if t s = 0 ∧ c s = 0 then 1 else 0) + (if t s = 0 ∧ c s = 1 then 1 else 0) * a / (a + b - a * b) +
(if t s = 1 ∧ c s = 1 then 1 else 0) * (1 - b) * a / (a + b - a * b))"I thought simp would be enough to evaluate this, but it seems not to be the case. So I am looking for a way to make isabelle automatically verify
all possible states (the space is finite due to the conditions). I would appreciate every help.
Is ⊩ point wise less or equal? If yes, you first should
unfold fun_le_def, then the splitter can operate on it. Also I don't
think that the simplifier can deduce that the set of states is finite.
And secondly I've another cosmetic question. Given following subgoals:
- 0 < a ⟹ a < 1 ⟹ 0 < b ⟹ b < 1 ⟹ 0 ≤ a
- 0 < a ⟹ a < 1 ⟹ 0 < b ⟹ b < 1 ⟹ 0 ≤ 1 - b
- 0 < a ⟹ a < 1 ⟹ 0 < b ⟹ b < 1 ⟹ 0 ≤ a
- some complicated subgoal
apply(simp)
apply(simp)
apply(simp)Is there any more elegant way other than to invoke simp 3 times? I also tried "auto" but it gets stuck on subgoal 4.
You can use Isar to proof subgoal 4 first and subgoal 1, 2, 3 by the
qed-command:
proof -
assumes "" then show "" ...
qed simp_all
- Johannes
Email Gateway (Aug 19 2022 at 12:05):From: Michael Vu <michael.vu@rwth-aachen.de>
Hello Johannes,
Yes, "⊩" basically means "≤".
I tried to define a similar lemma:
lemma test_bounded:
"0 < a ⟹ a < 1 ⟹ 0 < b ⟹ b < 1 ⟹ 0 < a + b - a * b ⟹
∀s. ((if t s = 0 ∧ c s = 0 then 1 else 0) + (if t s = 0 ∧ c s = 1 then 1 else 0) * a / (a + b - a * b) +
(if t s = 1 ∧ c s = 1 then 1 else 0) * (1 - b) * a /
(a + b -
a * b)) ≤ ((if c s ≠ 1 then 1 else 0) *
((if t s = 0 ∧ c s = 0 then 1 else 0) + (if t s = 0 ∧ c s = 1 then 1 else 0) * a / (a + b - a * b) +
(if t s = 1 ∧ c s = 1 then 1 else 0) * (1 - b) * a / (a + b - a * b)))"
apply(rule allI)
apply(auto)
In this case the simplifier is able to split all possible cases, it's just the matter that it won't evaluate all expressions afterwards.
So my question is if there's a way how i can deduce this test_bounded lemma from the first one I posted and then make Isabelle evaluate all
cases. Thanks!
Michael
Email Gateway (Aug 19 2022 at 12:05):From: Michael Vu <michael.vu@rwth-aachen.de>
I tried to define a similar lemma:
lemma test_bounded:
"0 < a ⟹ a < 1 ⟹ 0 < b ⟹ b < 1 ⟹ 0 < a + b - a * b ⟹
∀s. ((if t s = 0 ∧ c s = 0 then 1 else 0) + (if t s = 0 ∧ c s = 1 then 1 else 0) * a / (a + b - a * b) +
(if t s = 1 ∧ c s = 1 then 1 else 0) * (1 - b) * a /
(a + b -
a * b)) ≤ ((if c s ≠ 1 then 1 else 0) *
((if t s = 0 ∧ c s = 0 then 1 else 0) + (if t s = 0 ∧ c s = 1 then 1 else 0) * a / (a + b - a * b) +
(if t s = 1 ∧ c s = 1 then 1 else 0) * (1 - b) * a / (a + b - a * b)))"
apply(rule allI)
apply(auto)
In this case the simplifier is able to split all possible cases, it's just the matter that it won't evaluate all expressions afterwards.
So my question is if there's a way how i can deduce this test_bounded lemma from the first one I posted and then make Isabelle evaluate all
cases.
Regarding the variables a and b: That's my fault again, happens when I try to cut a snippet from my code..You can assume that they are defined as ::real.
Michael
Email Gateway (Aug 19 2022 at 12:06):From: Thomas Sewell <thomas.sewell@nicta.com.au>
Hey all.
I had a look at this on the assumption that this was somehow related to
the record package.
Looking at this test lemma, it would seem that
a) it is false in the case where "t s = 1 & c s = 1 & a * 2 = 1 & b * 2 = 1"
b) it seems to have nothing to do with the record package
c) nothing needs to be evaluated, instead, hypotheses need to be proven,
which is hard when they're false.
You can see that the lemma is false via:
apply (rule allI)
apply (case_tac "t s = 1 & c s = 1 & a = 0.5 & b = 0.5")
apply (elim conjE, simp only: )
apply (simp add: field_simps)
(the fact that all these tools are conservative means the original goal
was false also)
I'm not exactly sure what you're looking for.
Good luck,
Thomas.
Email Gateway (Aug 19 2022 at 12:08):From: Michael Vu <michael.vu@rwth-aachen.de>
Hello Thomas, hello all,
you're right, I really failed...Thanks for your counter example. Well the reason behind this is that i work with a custom package of theorems and used the wrong lemma which resulted in an unsolveable goal. So I'm really sorry.
Anyway, I managed to correct this and now Isabelle outputs this subgoal:
0 < (a::real) ⟹
a < 1 ⟹
0 < b ⟹
b < 1 ⟹
0 < a + b - a * b ⟹
∀s. t s = 0 ∨ t s = 1 ⟹
∀s. c s = 0 ∨ c s = 1 ⟹
(THE ba. isLub UNIV
(range (λs. (if t s = 0 ∧ c s = 0 then 1 else 0) + (if t s = 0 ∧ c s = 1 then 1 else 0) * a / (a + b - a * b) +
(if t s = 1 ∧ c s = 1 then 1 else 0) * (1 - b) * a / (a + b - a * b)))
ba)
≤ (THE ba. isLub UNIV
(range (λs. (if c s ≠ 1 then 1 else 0) *
((if t s = 0 ∧ c s = 0 then 1 else 0) + (if t s = 0 ∧ c s = 1 then 1 else 0) * a / (a + b - a * b) +
(if t s = 1 ∧ c s = 1 then 1 else 0) * (1 - b) * a / (a + b - a * b))))
ba)
The remaining functions are all defined in Set.thy/Lubs.thy and now I am stuck on how to prove this. This subgoal just shows that the upper bound of
the first lambda function is less or equal than the upper bound of the second function. Any help would be appreciated. I hope I didn't forget anything this time. Thanks!
Michael
Email Gateway (Aug 19 2022 at 12:08):From: Thomas Sewell <thomas.sewell@nicta.com.au>
Hey Michael.
Sorry about being short with you before. I wasn't actually annoyed by
the previous question, just pointing out that it didn't quite make sense
and there was probably a misunderstanding inherent in it somewhere.
It looks like you're closer to the right track. I note two things you
might want to work on.
My first observation was that you probably want to hide the THE operator
somehow. Using Hilbert choice semantically is fine (as long as you're OK
with it), but the operator also happens to be syntactically difficult to
grapple with.
In short, "THE x. isLub UNIV (range f) x" seems like a verbose
description of the least upper bound of
"range f". I wonder if there's an instantiation/proof anywhere that lets
you show "(THE x. isLub UNIV (range f) x) = Sup (range f)".
I don't have an answer to that myself, I don't really know anything
about reals in Isabelle. Maybe one of the calculus experts can comment?
The other problem is that you're assuming that "t s" is 0 or 1 for every
s. That's never true. So your proof can be finished by:
apply (drule_tac x="some_value (| t := 0.5 |)" in spec)
apply simp
done
That's almost certainly not what you want. I guess you probably just
want to constrain the s's considered in computing the ranges of the
lambda functions, but you would do that by replace range f
with f ` S instead.
Good luck,
Thomas.
Email Gateway (Aug 19 2022 at 12:14):From: Michael Vu <michael.vu@rwth-aachen.de>
Hi Thomas, hi all,
Thank you for your answer. I am using some kind of "framework" so that expression is defined as followed:
definition bound_of :: "('a ⇒ 'b::complete) ⇒ 'b"
where "bound_of P ≡ THE b. isLub UNIV (P ` UNIV) b"
There are also some Lemmas regarding to "bound_of" but none which exactly fits my goal. But that makes it impossible for me to change it nor to fix the second problem because this is just a subgoal of another lemma and I just unfolded the definition. Or could you find any way to improve it?
Any answers would be appreciated :)
Michael
Email Gateway (Aug 19 2022 at 12:15):From: Thomas Sewell <thomas.sewell@nicta.com.au>
Hey Michael.
I've had a think about your bound_of definition and the interesting case
you're using it in.
The only obvious thing I can prove about it is that it has the "obvious"
value if you happen to know what the maximum is:
lemma bound_of_eq_max:
"[| ALL y. f y <= f x |] ==> bound_of f = f x"
apply (simp add: bound_of_def)
apply (rule the_equality)
apply (simp add: isLub_def leastP_def isUb_def setge_def setle_def)
apply (simp add: isLub_def leastP_def isUb_def setge_def setle_def)
apply (auto intro: antisym)
done
(I'm using the ASCII versions of syntax in case of transmission issues,
however maybe Unicode has gotten better than this.)
It's not clear in your case that you'll know what the maximum value is,
however. It might depend on a or b. What simplifies your case is that it
looks like your lambda function is only interested in "t s = 0", "t s =
1" etc. This made me think you could prove it was equal to a composition
of functions:
record state =
t :: real
c :: real
record state =
t :: real
c :: real
lemma ts_01_etc_lemma:
"(%(x :: state). f (t x = 0) (t x = 1) (c x = 0) (c x = 1))
= (%(a, b). f (a = Some False) (a = Some True) (b = Some False) (b
= Some True))
o (%x. ([0 |-> False, 1 |-> True] (t x), [0 |-> False, 1 |->
True] (c x)))"
by (simp add: o_def fun_eq_iff)
lemma fun_01_eq_surj:
"surj (%(x :: state). ([0 |-> False, (1 :: real) |-> True] (t x), [0
|-> False, 1 |-> True] (c x)))"
apply (rule_tac f="%x. (| t = (case x of (Some False, _) => 0 | (Some
True, _) => 1 | (None, _) => 2),
c = (case x of (_, Some False) => 0 | (_,
Some True) => 1 | (_, None) => 2) |)" in surjI)
apply (simp split: sum.split prod.split option.split bool.split)
done
This is useful, because the bound of "g o f" ought to be the bound of g,
assuming f is surjective.
lemma range_compose:
"surj g ==> range (f o g) = range f"
by (metis image_compose)
lemma bound_of_compose:
"surj g ==> bound_of (f o g) = bound_of f"
by (simp add: bound_of_def range_compose)
lemma bound_of_eq_by_compose:
"g = f o h ==> surj h ==> bound_of g = bound_of f"
by (simp add: bound_of_compose)
thm bound_of_eq_by_compose
Finally, computing the bound of the minimal function extracted in this
way ought to be easier since it has a finite domain. I can use
enumeration to expand it:
lemma fold_max_ge:
"(fold max xs y >= (z :: 'a :: linorder)) = (y >= z | (EX x : set xs.
x >= z))"
apply (induct xs arbitrary: y)
apply (auto simp: le_max_iff_disj)
done
lemma fold_max_le:
"(fold max xs y <= (z :: 'a :: linorder)) = (y <= z & (ALL x : set
xs. x <= z))"
by (induct xs arbitrary: y, auto)
lemma bound_of_by_enum_vs:
"UNIV = set vs ==>
bound_of f = fold max (map f vs) (f (hd vs))"
apply (simp add: bound_of_def)
apply (subgoal_tac "hd vs : set vs")
apply (erule ssubst)
apply (rule the_equality[OF _ antisym, rotated])
apply (simp_all add: isLub_def leastP_def isUb_def setge_def
setle_def)
apply clarsimp
apply (drule spec, erule mp)
apply (auto simp: fold_max_le fold_max_ge)
done
lemmas bound_of_by_enum = bound_of_by_enum_vs[OF UNIV_enum]
thm trans[OF bound_of_eq_by_compose[OF ts_01_etc_lemma fun_01_eq_surj]
bound_of_by_enum,
unfolded enum_prod_def enum_sum_def enum_option_def enum_bool_def,
simplified]
It's a bit of a mess, but it looks like we can apply this to your kind
of problem:
lemma "0 < (a::real) ⟹
a < 1 ⟹
0 < b ⟹
b < 1 ⟹
0 < a + b - a * b ⟹
bound_of (λs :: state. (if t s = 0 ∧ c s = 0 then 1 else 0) + (if t
s = 0 ∧ c s = 1 then 1 else 0) * a / (a + b - a * b) +
(if t s = 1 ∧ c s = 1 then 1 else 0) * (1 -
b) * a / (a + b - a * b))
≤ bound_of (λs :: state. (if c s ≠ 1 then 1 else 0) *
((if t s = 0 ∧ c s = 0 then 1 else 0) + (if
t s = 0 ∧ c s = 1 then 1 else 0) * a / (a + b - a * b) +
(if t s = 1 ∧ c s = 1 then 1 else 0) * (1
This approach might be overspecialised, and you might have to use a
bigger intermediate type, but hopefully you can throw away your
records via this kind of reasoning, and maybe get a concrete result via
enumeration.
Hope that helps. Happy hunting,
Thomas.
Email Gateway (Aug 19 2022 at 12:24):From: Andrew Boyton <Andrew.Boyton@nicta.com.au>
To answer the simple question. Instead of
apply(simp)
apply(simp)
apply(simp)
you can go
apply(simp)+
or
apply(simp_all)
Strictly speaking, simp+ and simp_all have different semantics. simp_all works on all subgoals, where as simp+ works on the first subgoal, and if that discharges, it works on the second. Neither does exactly what the calling simp 3 times does, as they both try applying simp to the fourth goal. If you don't want that to happen, you can do the following
apply (simp+)[3]
which will limit simp+ to working on just three subgoals, but I suspect you don't need to.
Hope this helps.
Andrew
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 12:50):From: Michael Vu <michael.vu@rwth-aachen.de>
Hey Thomas,
at first: many many thanks! That was quite a lot of information and very helpful. Sorry for my late answer, I had to take some time to understand the code and to discuss it with my supervisor. The idea is very interesting, I've never worked with enumerations before but it seems to be a good approach here. Anyway, it didn't completely work for me, I had some problems with the lemma "bound_of_by_enum_vs". It does not get proven by reaching the "done" statement:
goal (4 subgoals):
The approach is quite special but can be generalized for finite states, right? At first I thought that all problem classes I'm working with only have a finite number of states, but my supervisor showed me cases with infinite states. This should not work with enumerations should it?
Michael
Email Gateway (Aug 19 2022 at 12:50):From: Thomas Sewell <thomas.sewell@nicta.com.au>
Hey Michael.
OK, two points. Firstly, this enumeration approach will only work for
handling finitely many cases. I brought it up because your function
happened to only care about finitely many valuations of "t x" and "c x".
If it's more general than that, well, you'll need a different approach.
And finding bounds of functions in general requires calculus or similar,
which, of course, may be substantially more challenging. If you end up
having to use Lagrange multipliers then, well, good luck to you.
Secondly, if one of the lemmas I typed didn't prove, it's probably
because I typed it into a different version of Isabelle, but also
possibly because I typed it in a context that contains a different set
of simplification rules to yours.
What I typed seems to work in Isabelle-2013, in a context I built via
"theory Scratch imports Lubs Real begin"
You might have to prove this theorem in the same context, or identify
what's changed and fix it, or come up with a new proof of the same rule,
or give us some more guidance as to how your context is built.
Good luck,
Thomas.
Last updated: Apr 26 2024 at 16:20 UTC