Email Gateway (Aug 22 2022 at 17:05): Email Gateway (Aug 22 2022 at 17:05):From: Shuwei Hu <shuwei.hu@tum.de>
Dear Isabelle list,
I have recently run into an unsolvable subgoal:
"Array.set array (Array.get heap array) heap = heap".
for which Nitpick found a counterexample in a few seconds.
I could not understand the counterexample, however. It requires
an array element type 'a with card = 1, but when I fix the type
to "unit", it is no longer a counterexample.
Does anyone have an idea why (or how) Imperative_HOL is
designed to let this equation fail?
Below is the message from nitpick:
Thanks,
Shuwei
Email Gateway (Aug 22 2022 at 17:05):From: Peter Lammich <lammich@in.tum.de>
Hi Shuwei
The reason is that we cannot prove
to_nat (from_nat n) = n
(b/c n may be outside the range of the encoding)
In Imperative/HOL, the heap is modelled by encoding its content to
natural numbers using precisely to_nat/from_nat.
So if you happen to access an array that has not been allocated, its
encoding might be out of range, and setting it back will replace the
encoding by something else.
Btw: For using Imperative/HOL, you should use the high-level interfaces
to arrays in the heap monad, Array.upd and Array.nth.
Email Gateway (Aug 22 2022 at 17:06):From: Shuwei Hu <shuwei.hu@tum.de>
Hi Peter,
thank you very much for your enlightening respond.
I was proving some kind of triviality of Array.upd of Array.nth, and indeed,
it involves an array whose presence on the heap cannot be assured by the
Heap expression.
The original goal was the identity property of a monad morphism. Applying on
"return v", it boils down to *"x <- Array.nth M i; Array.upd i x M;
return v"*.
I understand that there must be some kind of invariant for an array
implicitly given
by its birth, but I'm afraid that the definition of the morphism have to
stay as it is
without any history of the array, since it might be applied to any monad in
the
middle of a program.
Do you have an idea of what kind of precondition should be given to prove
the
equivalency between the two Heap monads above in bold font?
Thanks!
Shuwei
Email Gateway (Aug 22 2022 at 17:06):From: Peter Lammich <lammich@in.tum.de>
Hi,
the array index must be in range, and the array must have been
allocated. Otherwise, these two programs are intuitively not equal, as
the second would boil down to "undefined behaviour".
Email Gateway (Aug 22 2022 at 17:06):From: Shuwei Hu <shuwei.hu@tum.de>
Yes indeed, but how can one state them formally?
The assumptions below doesn't prevent nitpick from finding a counterexample:
lemma
assumes "i < Array.length h M "
assumes "Array.present h M"
shows "execute (do {x ← Array.nth M i; Array.upd i x M; return v}) h =
execute (return v) h"
And I think that the definition of Array.present suggests that it does not
help
the from_nat / to_nat issue.
Should I invent a new predicate in terms of low level stuffs like from_nat
& to_nat?
Thanks!
Shuwei
Email Gateway (Aug 22 2022 at 17:06):From: Peter Lammich <lammich@in.tum.de>
You could strengthen the ARray.present predicate to also ensure that
the encoding of the array makes sense, e.g.
definition enc_invar :: "Heap.heap ⇒ 'a::heap array ⇒ bool" where
"enc_invar h a ⟷ (addr_of_array a < lim h ∧) (∃xs::'a list.
arrays h TYPEREP('a) (addr_of_array a) = map to_nat xs
)"
lemma "enc_invar h a ⟹ Array.set a (Array.get h a) h = h"
unfolding enc_invar_def Array.set_def Array.get_def
apply auto
by (metis (mono_tags, lifting) comp_def from_nat_to_nat
fun_upd_triv map_eq_conv surjective update_convs(1))
Note that the commented out part can be optinal added, to make
enc_invar stronger than present.
Last updated: May 06 2024 at 12:29 UTC