Re: [isabelle] Evaluation of record expressions



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):
 1. ⋀b y. hd vs ∈ set vs ⟹ ∀y∈set vs. f y ≤ b ⟹ y ∈ set vs ⟹ f y ≤ fold max (map f vs) (f (hd vs))
 2. ⋀b. hd vs ∈ set vs ⟹ ∀y∈set vs. f y ≤ b ⟹ ∀x. (∀y∈set vs. f y ≤ x) ⟶ b ≤ x ⟹ fold max (map f vs) (f (hd vs)) ≤ b
 3. ⋀y. hd vs ∈ set vs ⟹ y ∈ set vs ⟹ f y ≤ fold max (map f vs) (f (hd vs))
 4. ⋀x. hd vs ∈ set vs ⟹ ∀y∈set vs. f y ≤ x ⟹ fold max (map f vs) (f (hd vs)) ≤ x

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

Am 30-10-13, schrieb Thomas Sewell  <thomas.sewell at 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 - b) * a / (a + b - a * b)))"
>   apply (subst bound_of_eq_by_compose[OF ts_01_etc_lemma fun_01_eq_surj])+
>   apply (simp add: bound_of_by_enum enum_prod_def enum_sum_def enum_option_def enum_bool_def)
>   apply (simp add: max_def)
>   sorry
> 
> 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.
> 
> On 28/10/13 23:04, Michael Vu wrote:
> >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
> >
> >Am 18-10-13, schrieb Thomas Sewell  <thomas.sewell at 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.
> >>
> >>On 18/10/13 12:21, Michael Vu wrote:
> >>>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
> >>>
> >>>Am 15-10-13, schrieb Thomas Sewell  <thomas.sewell at 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.
> >>>>




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