Dear Konrad,
thank you for your help and insights!
Yours sincerely,
Jun Jie
2013/4/15 Konrad Slind <[email protected]>
> > g `!n A i j. (A (i) = A (j)) ==> (A (j) = system n A (j))`;
>
> This goal is close to what you want, but you need to restrict the
> scope of quantification in your antecedent. A slightly different version
> gets proved with the same tactic as before:
>
> val lemma1 = Q.prove
> (`!x A. (!i. (A:num->num) i = x) ==> !n j. system n A j = x`,
> RW_TAC arith_ss
> [system_def, replace_smaller_def,combinTheory.APPLY_UPDATE_THM]
> );
>
> As to your question about how to figure out what rewrite rules or lemmas
> to apply,
> and how to find them, that can indeed be hard. The lemmas I've used above
> are
> just the definitions of the "computation" done by system, plus a rewrite
> rule needed
> to apply array updates. When the proof looks harder than your instinct
> tells you it
> should be, then you may have to go back and restate the goal, or even,
> eventually,
> re-adjust your notion of what is really needed to obtain success.
>
> Konrad.
>
>
>
> On Mon, Apr 15, 2013 at 8:52 AM, J. J. W. <[email protected]> wrote:
>
>> Dear Konrad,
>>
>> thank you for your explanation. So I tried something myself: I want to
>> prove for example something really trivial, like that if all elements are
>> the same in the array, after execution everything stays the same, which is
>> pretty straight forward.
>>
>> For example if I have [1,1,1,1,1] after execution, I have [1,1,1,1,1],
>> this is quite trivial.
>>
>> My question now is, how do I start the prove?
>>
>> I was trying it on my own, so I started:
>>
>> g `!n A i j. (A (i) = A (j)) ==> (A (j) = system n A (j))`;
>>
>> If I try this I will have like 10 goals that I need to accomplish, my
>> question now is:
>>
>> How do you "figure out" which rewrite rules I need? I have tried the
>> default rewriting rules that you've been giving me, however I am not
>> getting very far.
>>
>> Going to this page:
>> http://hol.sourceforge.net/kananaskis-8-helpdocs/help/HOLindex.html seems
>> the way to go, but how do I figure out which rewriting rule suits me? As
>> far as I know there is no search function on the page :(.
>>
>> PS: I think this might be easier if we assume that every element in our
>> array is the same, however I have no idea how to express assumptions.
>>
>> Thank you for your help and time.
>>
>> Yours sincerely,
>>
>> Jun Jie
>>
>>
>>
>>
>>
>>
>> 2013/4/15 Konrad Slind <[email protected]>
>>
>>> Hi JJ:
>>>
>>> The definition of replace_smaller is fine, but the rest needs some
>>> tweaking.
>>> My understanding of system_def is the following (I include
>>> replace_smaller too):
>>>
>>> val replace_smaller_def =
>>> Define
>>> `replace_smaller p q (A:num->num) = if A p < A q then (p =+ A q) A
>>> else A`;
>>>
>>> val system_def =
>>> Define
>>> `system n (A:num->num) =
>>> \i. (if i < n
>>> then replace_smaller i (if i=n-1 then 0 else (i+1)) A
>>> else A) i`;
>>>
>>>
>>> With that, you can prove that every array value after "running" system
>>> is not smaller than
>>> before, just by expanding definitions:
>>>
>>> val lemma = Q.prove
>>> (`!n A j. A (j) <= system n A (j)`,
>>> RW_TAC arith_ss
>>> [system_def, replace_smaller_def,combinTheory.APPLY_UPDATE_THM]);
>>>
>>> Konrad.
>>>
>>>
>>>
>>> On Sun, Apr 14, 2013 at 7:23 AM, J. J. W. <[email protected]> wrote:
>>>
>>>> Dear all,
>>>>
>>>> thank you for your help and advice. I've modelled it using the
>>>> functional version:
>>>>
>>>> val replace_smaller_def = Define `replace_smaller p q = \a : int ->
>>>> int. if (a p) < (a q) then (p =+ (a q)) a else a`;
>>>>
>>>> val system_def = Define `system n = {replace_smaller (n-1) 0} UNION
>>>> {replace_smaller i (i+1) | i < n-1}`;
>>>>
>>>> So how do I continue? For example I wish to prove that this program
>>>> does not increase any value of a[i] for any i < n? I need to have access to
>>>> both the state before my program and after my program right? I am not sure
>>>> how to express this condition in HOL.
>>>>
>>>> I think somthing with NOT ?e. A[e] > A'[e], where A'[e] is before the
>>>> execution... but how can I access this?
>>>>
>>>> Thanks!
>>>>
>>>>
>>>> 2013/4/11 Anthony Fox <[email protected]>
>>>>
>>>>> Just to add to Konrad’s e-mail.
>>>>>
>>>>> There is a list “write" operation in listTheory — it is defined as
>>>>> follows:
>>>>>
>>>>> (∀e n. LUPDATE e n [] = []) ∧
>>>>> (∀e x l. LUPDATE e 0 (x::l) = e::l) ∧
>>>>> ∀e n x l. LUPDATE e (SUC n) (x::l) = x::LUPDATE e n l
>>>>>
>>>>> Other representation choices include:
>>>>>
>>>>> - functions of type : ‘a word -> ty
>>>>> - partial functions : ‘a word |-> ty
>>>>>
>>>>> This could make sense if your “int” type is actually a machine word,
>>>>> e.g. ``:word32`` in HOL.
>>>>>
>>>>> Anthony
>>>>>
>>>>> On 11 Apr 2013, at 18:12, Konrad Slind <[email protected]> wrote:
>>>>>
>>>>> > Hi J.J. :
>>>>> >
>>>>> > First you have to choose how arrays are modelled, i.e., which HOL
>>>>> type
>>>>> > is going to be used to represent arrays. Choices:
>>>>> >
>>>>> > - functions of type : num -> ty
>>>>> > - finite functions : num |-> ty
>>>>> > - lists : ty list
>>>>> > - finite products : ty['dim]
>>>>> >
>>>>> > Summary of the read (A[i]) and write (A[i] := e) operations on array
>>>>> A:
>>>>> >
>>>>> > A : num -> ty
>>>>> > read operation: A i
>>>>> > write operation: \j. if (i=j) then e else A j
>>>>> > Note: there is already a definition for update in combinTheory,
>>>>> using an infix
>>>>> >
>>>>> > (i =+ e) A = \j. if (i=j) then e else A(j)
>>>>> >
>>>>> > A : num |-> ty (load finite_mapTheory)
>>>>> > read operation: A ' i
>>>>> > write : A |+ (i,e)
>>>>> >
>>>>> > A : ty list
>>>>> > read operation: EL i list
>>>>> > write operation: not sure an indexed write for lists is defined
>>>>> in HOL. If not, the
>>>>> > following is one version:
>>>>> >
>>>>> > update (h::t) 0 e = e::t
>>>>> > update (h::t) n e = h::update t (n-1) e;
>>>>> >
>>>>> > A : ty['dim] (load fcpTheory)
>>>>> > read operation: A ' i
>>>>> > write operation: (i :+ e) A
>>>>> >
>>>>> > I hope this helps,
>>>>> > Konrad.
>>>>> >
>>>>> >
>>>>> >
>>>>> > On Thu, Apr 11, 2013 at 6:10 AM, J. J. W. <[email protected]>
>>>>> wrote:
>>>>> > Dear all,
>>>>> >
>>>>> > I would like to model the following:
>>>>> >
>>>>> > public replace_smaller(int[] A, int c, int d){
>>>>> > if (A[d] < A[c]){
>>>>> > A[c] = A[q]
>>>>> > }
>>>>> > return A;
>>>>> > }
>>>>> >
>>>>> > and I would like to prove that the resulting array is just like the
>>>>> code.
>>>>> >
>>>>> > So I think I should define the following:
>>>>> >
>>>>> > val replace_smaller_def = Define `replace_smaller a b (\a. if (nth
>>>>> (a, p) < nth (a,q)) then ... else ...`;
>>>>> >
>>>>> > However I have no idea how to continue with this since, I have no
>>>>> idea how to access the array or anything like that.
>>>>> >
>>>>> > Can someone give me some advice?
>>>>> >
>>>>> > Kind regards,
>>>>> >
>>>>> > Jun Jie
>>>>> >
>>>>> >
>>>>> ------------------------------------------------------------------------------
>>>>> > Precog is a next-generation analytics platform capable of advanced
>>>>> > analytics on semi-structured data. The platform includes APIs for
>>>>> building
>>>>> > apps and a phenomenal toolset for data science. Developers can use
>>>>> > our toolset for easy data analysis & visualization. Get a free
>>>>> account!
>>>>> > http://www2.precog.com/precogplatform/slashdotnewsletter
>>>>> > _______________________________________________
>>>>> > hol-info mailing list
>>>>> > [email protected]
>>>>> > https://lists.sourceforge.net/lists/listinfo/hol-info
>>>>> >
>>>>> >
>>>>> >
>>>>> ------------------------------------------------------------------------------
>>>>> > Precog is a next-generation analytics platform capable of advanced
>>>>> > analytics on semi-structured data. The platform includes APIs for
>>>>> building
>>>>> > apps and a phenomenal toolset for data science. Developers can use
>>>>> > our toolset for easy data analysis & visualization. Get a free
>>>>> account!
>>>>> >
>>>>> http://www2.precog.com/precogplatform/slashdotnewsletter_______________________________________________
>>>>> > hol-info mailing list
>>>>> > [email protected]
>>>>> > https://lists.sourceforge.net/lists/listinfo/hol-info
>>>>>
>>>>>
>>>>
>>>
>>
>
------------------------------------------------------------------------------
Precog is a next-generation analytics platform capable of advanced
analytics on semi-structured data. The platform includes APIs for building
apps and a phenomenal toolset for data science. Developers can use
our toolset for easy data analysis & visualization. Get a free account!
http://www2.precog.com/precogplatform/slashdotnewsletter
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
