Email Gateway (Aug 17 2022 at 13:46): Email Gateway (Aug 17 2022 at 13:46):From: Primrose.Mbanefo@Infineon.com
Hello,
I have a list (a "nat list") with N elements.
I assume that the elements which come before the i-th element are all
less than or equal to i.
I would like to say that if the i+1th element is also less than or equal
to the i-th element,
then if I exchange the elements in the ith and i+1th positions
then all elements upto i+1 are less than or equal to the i+1-th element.
I thought this should look like this:
\<forall> j. (j + 1) < length xs \<and> xs!j < ((xs!(j+1))::nat)
\<longrightarrow> (\<forall>i < j. xs!j < xs!i \<longrightarrow>
(\<forall>k \<le> j+1. xs[j:=xs!(j+1),(j+1) := xs!j]!(j+1) \<le>
xs[j:=xs!(j+1),(j+1):=xs!j]!k))
I thought the best thing to do would be to prove a slightly simpler
version first which states that if all the elements in positions less
than i are less than/equal to the ith element and also that the i+1st
element is less than/equal to the ith element then all the elements upto
i+1 should be less than/equal to the ith element.
I have tried to formulate this in different ways but the formulation I
believe comes close to what I am looking for is:
\<forall> j. (j + 1) < length xs \<and> xs!j < ((xs!(j+1))::nat)
\<longrightarrow> (\<forall>i < j. xs!j < xs!i \<longrightarrow>
(\<forall>k \<le> j+1. xs!j \<le> xs!k) ) )
But I am not capable of proving anything about this statement. I tried
doing the induction on xs or on j (after removing its quantification)
but I didn't go very far.
Trying to reason about the sets involved didn't bring much. Notably, I
am wondering why I couldn't prove the below using an induction on the
list xs.:
\<forall>n j . n < j \<longrightarrow> (\<forall>(i::nat) \<in> set xs.
n < i \<longrightarrow> ( \<forall>k \<in> set xs \<union> {j}. n < k) )
I do not believe I understand what quantification actually is...
Could anyone tell me what is wrong with these formulations and how I can
start reasoning about these?
Thanks in advance!
Regards,
Primrose
Email Gateway (Aug 17 2022 at 13:46):From: Martin Ellis <m.a.ellis@ncl.ac.uk>
On Friday 24 February 2006 15:51, Primrose.Mbanefo@infineon.com wrote:
I assume that the elements which come before the i-th element are all
less than or equal to i.
That's a mouthful. Call it 'P':
constdefs
"P (xs::nat list) == ALL i. i < length xs --> xs!i <= i"
(I'm using the ASCII notation here, see the tutorial appendix for the prettier
representation)
I would like to say that if the i+1th element is also less than or equal
to the i-th element,
then if I exchange the elements in the ith and i+1th positions
then all elements upto i+1 are less than or equal to the i+1-th element.
You can start by defining 'exchange the elements'. Might as well make it for
any two elements, no need to limit ourselves to consecutive elements:
constdefs
"listswap xs i j == xs[i := xs ! j, j := xs ! i]"
The function "preserves the length of xs", in the sense that it's result is
the same length. You don't need this property, but it can tidy up the proof
states you see later if you have these lemmas:
lemma listswap_length:
"!! i j xs. i < length xs & j < length xs -->
length (listswap xs i j) = length xs"
apply(induct_tac i)
by(auto simp add:listswap_def)
lemma listswap_length2:
"[| i< length xs; j < length xs |] ==> length (listswap xs i j) = length xs"
by(simp add: listswap_length)
(Is there an easier way to get the latter?)
I thought this should look like this:
\<forall> j. (j + 1) < length xs \<and> xs!j < ((xs!(j+1))::nat)
\<longrightarrow> (\<forall>i < j. xs!j < xs!i \<longrightarrow>
(\<forall>k \<le> j+1. xs[j:=xs!(j+1),(j+1) := xs!j]!(j+1) \<le>
xs[j:=xs!(j+1),(j+1):=xs!j]!k))
Firstly, the "\<forall>i < j. xs!j < xs!i" doesn't seem to correspond with
anything in your English description.
You seem to be missing either the assumption that P already holds of the list
in the first place, or it holds for some initial number of elements,
depending on what you're trying to prove. If it doesn't already hold, then
your exchange wont fix that property.
Not sure whether you want to assume P true of the whole list, or just up to a
given element. Assuming the former, you could write:
lemma "P xs -->
(ALL j. j < (length xs - 1) -->
xs!(j+1) <= xs!j -->
P (listswap xs j (j+1)) )"
You should see that that much more closely matches your English description
above. ("P xs" is the first paragraph of yours I quoted, etc.)
Using the listswap_length lemma, the last line will expand to:
ALL i < length xs. listswap xs j (j+1) ! i <= i
So there are three cases to consider:
Is that the goal you're trying to prove? If not, and you want P to be a
property only of the first n elements, then redefine it to be a predicate
P (xs::nat list) (n::nat), rather than P (xs::nat list).
Hope that gives you a start.
Martin
Email Gateway (Aug 17 2022 at 13:46):From: nipkow@in.tum.de
Thanks for answering that one, Martin.
(Is there an easier way to get the latter?)
Yes, induction is not needed because the relevant lemma about length and
list-updaate is already known:
lemma listswap_length2:
"[| i< length xs; j < length xs |] ==> length (listswap xs i j) = length xs"
by(simp add: listswap_def)
Tobias
Email Gateway (Aug 17 2022 at 13:46):From: Primrose.Mbanefo@Infineon.com
Thanks a whole lot for the replies!
Firstly, the "\<forall>i < j. xs!j < xs!i" doesn't seem to correspond
with anything in your English description.
I definetly did make a mistake in the english formulation of the
problem.
I am studying your approach now and I believe I can start something
(actually a whole lot) with this.
I am now beginning to think my problem is that I am not used to this
verification snowballing effect where verifying one thing leads to
describing or verifying something smaller or more general.
I will get back once I have been able to do something (or when I am
stuck again :))
Thanks once more.
Primrose
Email Gateway (Aug 17 2022 at 13:46):From: Primrose.Mbanefo@Infineon.com
Hello,
I corrected the specification and simplified it so that P is valid on the entire list (to make the proof simpler for me).
P now looks like:
constdefs
"P (xs::nat list) Y == \<forall>i < length xs. xs!i \<le> Y"
And the lemma I am trying to prove is:
lemma "P xs Y \<longrightarrow> (\<forall> j. j < (length xs - 1) \<longrightarrow> P (listswap xs j (j+1)) Y)"
And I am still using the listswap and listswap_length.
I have tried to prove that lemma in different ways and failed.
The formulation of the proof which reflects my current try looks like:
lemma "P xs Y \<longrightarrow> (\<forall> j. j < (length xs - 1) \<longrightarrow> P (listswap xs j (j+1)) Y)"
proof (simp add: listswap_length P_def)
have "P xs Y \<longrightarrow> (\<forall> j. Suc j < length xs \<longrightarrow>
(\<forall>i. i < length xs \<longrightarrow>
(i \<noteq> j \<and> i \<noteq> (Suc j)
\<longrightarrow> (listswap xs j (Suc j))!i \<le> Y))) "
by (simp add: listswap_def P_def)
also have "P xs Y \<longrightarrow> (\<forall> j. Suc j < length xs \<longrightarrow>
(\<forall>i. i = j \<longrightarrow> (listswap xs j (Suc j))!j \<le> Y))"
by (simp add: listswap_def P_def)
oops
also have "P xs Y \<longrightarrow> (\<forall> j. Suc j < length xs \<longrightarrow>
(\<forall>i. (i = (Suc j)) \<longrightarrow> (listswap xs j (Suc j))!(Suc j) \<le> Y))"
by (simp add: listswap_def P_def)
finally show ?thesis apply ()
qed
With the oops showing where it breaks.
Isn't this a valid way of breaking down this proof?
Thanks for your help!
Regards,
Primrose
P.S: Also how do you convert the X-Symbols to ascii?
Last updated: May 03 2024 at 12:27 UTC