> 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
