(* ************** SAMPLE SOLUTION TO PRACTICAL 3 *************** *) (* **************** EXERCISE 1 **************** *) signature QUEUE = sig type 'a queue val empty : 'a queue val isempty : 'a queue -> bool val insert : 'a * 'a queue -> 'a queue val front : 'a queue -> 'a val remove : 'a queue -> 'a queue val join : 'a queue * 'a queue -> 'a queue axiom isempty empty == true axiom Forall (a,q) => isempty(insert(a,q)) == false axiom Forall (q1,q2) => isempty(join(q1,q2)) == isempty q1 andalso isempty q2 axiom Forall (a,q) => isempty q implies front(insert(a,q)) == a axiom Forall (a,q) => not(isempty q) implies front(insert(a,q)) == front q axiom Forall (q1,q2) => isempty q1 implies front(join(q1,q2)) == front q2 axiom Forall (q1,q2) => not(isempty q1) implies front(join(q1,q2)) == front q1 axiom Forall (a,q) => isempty q implies remove(insert(a,q)) == empty axiom Forall (a,q) => not(isempty q) implies remove(insert(a,q)) == insert(a,remove q) axiom Forall (q1,q2) => isempty q1 implies remove(join(q1,q2)) == remove q2 axiom Forall (q1,q2) => not(isempty q1) implies remove(join(q1,q2)) == join(remove q1,q2) end Discussion might concern things like whether or not we include axioms like Forall (q1,q2) => isempty q1 implies join(q1,q2) == q2 This is stronger than necessary to ensure "correct" results, and so should preferably be omitted. (* **************** EXERCISE 2 **************** *) This proof contains more detail than required, but the style is what I would expect. First, define a function count' to count the number of occurrences of a given element in a heap: fun count'(x,empty) = 0 | count'(x,node(h,a,h')) = cmp(x,a) + count'(x,h) + count'(x,h') LEMMA 1: Forall (x,a,h) => count'(x,insert(a,h)) = cmp(x,a) + count'(x,h) by structural induction on h. BASE CASE. h=empty count'(x,insert(a,empty)) = {code for insert} count'(x,node(empty,a,empty)) = {code for count'} cmp(x,a) STEP CASE. h=node(h1,b,h2) INDUCTIVE HYPOTHESES: IH1: count'(x,insert(a,h1)) = cmp(x,a) + count'(x,h1) IH2: count'(x,insert(a,h2)) = cmp(x,a) + count'(x,h2) CASE 1. a <= b count'(x,insert(a,node(h1,b,h2))) = {code for insert} count'(x,node(insert(b,h2),a,h1)) = {code for count'} cmp(x,a) + count'(x,insert(b,h2)) + count'(x,h1) = {IH2} cmp(x,a) + cmp(x,b) + count'(x,h2) + count'(x,h1) = {code for count'} cmp(x,a) + count'(x,node(h1,b,h2)) CASE 2. a > b count'(x,insert(a,node(h1,b,h2))) = {code for insert} count'(x,node(insert(a,h2),b,h1)) = {code for count'} cmp(x,b) + count'(x,insert(a,h2)) + count'(x,h1) = {IH2} cmp(x,b) + cmp(x,a) + count'(x,h2) + count'(x,h1) = {code for count'} cmp(x,a) + count'(x,node(h1,b,h2)) ------------------------------------------------------------------------------- LEMMA 2: Forall (x,l) => count(x,l) = count'(x,createheap l) by structural induction on l. BASE CASE. l=nil count(x,nil) = 0 {code for count} count'(x,createheap nil) = {code for createheap} count'(x,empty) = {code for count'} 0 STEP CASE. l=a::l' INDUCTIVE HYPOTHESIS: count(x,l') = count'(x,createheap l') count(x,a::l') = cmp(x,a) + count(x,l') count'(x,createheap (a::l')) = {code for createheap} count'(x,insert(a,createheap l')) {by Lemma 1 with h instantiated to (createheap l')} = cmp(x,a) + count'(x,createheap l') {by IH} = cmp(x,a) + count(x,l') ------------------------------------------------------------------------------- LEMMA 3: Forall (x,l,l') => count(x,merge(l,l')) = count(x,l) + count(x,l') by structural induction on both l, l'. BASE CASE 1. l=nil count(x,merge(nil,l')) = {code for merge} count(x,l') count(x,nil) + count(x,l') = {code for count} count(x,l') BASE CASE 2. l'=nil count(x,merge(l,nil)) = {code for merge} count(x,l) count(x,l) + count(x,nil) = {code for count} count(x,l) STEP CASE. l=a::tl, l'=a'::tl' INDUCTIVE HYPOTHESES: IH1: count(x,merge(a::tl,tl')) = count(x,a::tl) + count(x,tl') IH2: count(x,merge(tl,a'::tl')) = count(x,tl) + count(x,a'::tl') CASE 1. a<=a' count(x,merge(a::tl,a'::tl')) = {code for merge} count(x,a::merge(tl,a'::tl)) = {code for count} cmp(x,a) + count(x,merge(tl,a'::tl)) = {IH2} cmp(x,a) + count(x,tl) + count(x,a'::tl) = {code for count} count(x,a::tl) + count(x,a'::tl) CASE 2. a>a' analogously ------------------------------------------------------------------------------- LEMMA 4: Forall (x,h) => count'(x,h) = count(x,extractheap h) by structural induction on h. BASE CASE. h=empty count'(x,empty) = 0 {code for count'} count(x,extractheap empty) = {code for extractheap} count(x,nil) = 0 {code for count} STEP CASE. h=node(h1,a,h2) INDUCTIVE HYPOTHESES IH1: count'(x,h1) = count(x,extractheap h1) IH2: count'(x,h2) = count(x,extractheap h2) - left side of equality: count'(x,node(h1,a,h2)) = {code for count'} cmp(x,a) + count'(x,h1) + count'(x,h2) = {IH1 and IH2} cmp(x,a) + count(x,extractheap h1) + count(x,extractheap h2) - right side of equality: count(x,extractheap node(h1,a,h2)) = {code for extractheap} count(x,a::merge(extractheap h1,extractheap h2)) = {code for count} cmp(x,a) + count(x,merge(extractheap h1,extractheap h2)) = {Lemma 3} cmp(x,a) + count(x,extractheap h1) + count(x,extractheap h2)) ------------------------------------------------------------------------------- Theorem: Forall l => permutation(l,sort l) Forall l => permutation(l,sort l) <=> {code for sort} Forall l => permutation(l,extractheap (createheap l)) <=> {axiom for permutation} Forall l => (Forall x => count(x,l) = count(x,extractheap (createheap l))) <=> {Lemma 4 with h instantiated to (createheap l)} Forall l => (Forall x => count(x,l) = count'(x,createheap l)) <=> {Lemma 2} Forall l => (Forall x => count(x,l) = count(x,l)) <=> {obvious} true.