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 =
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]
Dear Konrad,
thank you for your help and insights!
Yours sincerely,
Jun Jie
2013/4/15 Konrad Slind konrad.sl...@gmail.com
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
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
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
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
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
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 :
