spark2014 – problem1

· Uncategorized


We have successfully proved the problem 1 in Coq.

In the proof for the question 1:
(1) we use natural numbers to represent cards;
(2) according to the concept of “precede” defined in the quetion, a(i) precedes a(j) iff i<j and a(i) < a(j), where i and j are indexes of values a(i) and a(j) in the input sequence, so in our proof, we use (Index * nat) to represent the input value and its index in the input sequence;
(3) the induction definitions of “PatienceSolitaire_Rule” and “Insert_Rule” are used to implement the Patience Solitaire algorithm;
(4) the inductive definition of “Precede” in our proof code is an extension of the concept of “precede” defined in the question. Our defined “Precede stack1 stack2″ means that for any element a2(j) in stack2, there exists an element a1(i) in stack1 that i < j and a1(i) < a2(j);
(5) the lemma “Precede_Reserved” is a proof for the invariant of the Patience Solitaire algorithm: it means that for any sequence of stacks “stacks”, if “stacks(i)” Precedes “stacks(i+1)”, then if we insert a new number “a” into the stacks “stacks” according to the Patience Solitaire principle, then this property of the resulting stacks ” stacks’ ” should still hold;
(6) the lemma “lemma1″ is a proof for the proof task 1 in the question 1;
(7) the lemma “lemma2″ is a proof for the proof task 2 in the question 2, it proves that for the resulting stacks “ResultStacks” after the Patience Solitaire gamae, any of its individual stack cannot contain two elements that they precede one another, wihch is proved by showing that the indexes of each individual stack is decreasing;




1 Comment

Comments RSS
  1. SPARK 2014 – vscomp linked to this post.

Leave a Comment