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
