diff options
Diffstat (limited to 'assignment8/qs.pvs')
| -rw-r--r-- | assignment8/qs.pvs | 150 |
1 files changed, 150 insertions, 0 deletions
diff --git a/assignment8/qs.pvs b/assignment8/qs.pvs new file mode 100644 index 0000000..086321a --- /dev/null +++ b/assignment8/qs.pvs @@ -0,0 +1,150 @@ +my_list_induction[X:TYPE] : THEORY +BEGIN + less(l1,l2: list[X]) : bool = length(l1) < length(l2) + + less_wf: LEMMA well_founded?(less) % :-) + + list_length_induction :LEMMA % :-) + (FORALL (p:pred[list[X]]): + (FORALL (g:list[X]): + (FORALL (s:list[X]): + less(s,g) IMPLIES p(s)) + IMPLIES p(g)) + IMPLIES (FORALL (l:list[X]): p(l))) + +END my_list_induction + +my_list_props[X:TYPE] : THEORY +BEGIN + occ(x:X,l:list[X]) : RECURSIVE nat = + CASES l + OF null : 0 , + cons(y,l) : IF x=y THEN occ(x,l)+1 ELSE occ(x,l) ENDIF + ENDCASES + MEASURE length(l) + + occ_nth: LEMMA + FORALL(l:list[X]): FORALL(x:X): occ(x,l) > 0 IMPLIES + EXISTS(i:nat): i<length(l) AND nth(l,i) = x + + nth_occ: LEMMA + FORALL(l:list[X]): FORALL(i:nat): i<length(l) IMPLIES occ(nth(l,i),l) > 0 + + perm?( l1,l2 : list[X]) : bool = FORALL(x:X): occ(x,l1) = occ(x,l2) + + perm_null: LEMMA % :-) + FORALL(l:list[X]): perm?(null, l) IMPLIES l = null + + perm_commutative: LEMMA % :-) + FORALL(l1,l2: list[X]):perm?(l1,l2) IMPLIES perm?(l2,l1) + + append_occ: LEMMA % :-) + FORALL( l1,l2:list[X] ): FORALL(x:X): occ(x,append(l1,l2)) = occ(x,l1)+occ(x,l2) + + length_append: LEMMA % :-) + FORALL( l1,l2:list[X] ):length(append(l1,l2)) = length(l1) + length(l2) + + nth_append: LEMMA % :-( to be done + FORALL( l1,l2:list[X] ): FORALL(i:nat): i < length(l1)+length(l2) IMPLIES + nth(append(l1,l2),i) = IF i < length(l1) THEN nth(l1,i) ELSE nth(l2,i-length(l1)) ENDIF + +END my_list_props + + +SPLIT : THEORY +BEGIN + IMPORTING my_list_props + + split (m: nat, l : list[nat]) : RECURSIVE [list[nat], list[nat]] = + CASES l OF + null : (null, null), + cons(h,t) : LET + (l,r) = split (m, t) + IN + IF h < m + THEN (cons(h,l),r) + ELSE (l,cons(h,r)) + ENDIF + ENDCASES + MEASURE (length(l)) + + split_length: LEMMA % :-) + FORALL( m:nat, l:list[nat] ): LET s = split(m,l) IN length(l) = length(s`1) + length(s`2) + + split_occ: LEMMA % :-) + FORALL( n: nat, l:list[nat] ): LET s = split(n, l) IN FORALL(x:nat):occ(x,l) = occ(x,s`1)+occ(x,s`2) + + upb( g:nat, l:list[nat] ): bool = + FORALL(i:nat): i < length(l) IMPLIES nth(l,i) < g + + lwb( s:nat, l:list[nat] ): bool = + FORALL(i:nat): i < length(l) IMPLIES NOT nth(l,i) < s + + split_lwb_upb: LEMMA % :-( to be done + FORALL( m:nat, l:list[nat] ): LET s = split(m,l) IN upb(m,s`1) AND lwb(m,s`2) + +END SPLIT + +QS : THEORY +BEGIN + IMPORTING SPLIT + qs (l : list[nat]) : RECURSIVE list[nat] = + CASES l OF + null : null, + cons(h,t) : LET + (l,r) = split (h, t) + IN + append(qs(l),cons(h,qs(r))) + ENDCASES + MEASURE (length(l)) + +END QS + +SORTED: THEORY +BEGIN + IMPORTING my_list_props[nat] + IMPORTING SPLIT + + sorted?(l:list[nat]) : bool = + FORALL (i,j: nat): i < j AND j < length(l) IMPLIES nth(l,i) <= nth(l,j) + + sorted_append: LEMMA % :-( to be done + FORALL( m:nat, l1,l2:list[nat] ): + sorted?(l1) AND sorted?(l2) and upb(m,l1) AND lwb(m,l2) + IMPLIES sorted?(append(l1,l2)) +END SORTED + +QS_props : THEORY +BEGIN + IMPORTING QS, SORTED + IMPORTING my_list_props[nat], my_list_induction[nat] + + qs_perm: LEMMA % :-( to be done + FORALL(l:list[nat]):perm?(qs(l),l) + + occ_upb: LEMMA % :-) + FORALL( n: nat, l:list[nat] ): upb(n,l) IMPLIES + (FORALL(x:nat):occ(x,l) > 0 IMPLIES x < n) + + occ_lwb: LEMMA % :-) + FORALL( n: nat, l:list[nat] ): lwb(n,l) IMPLIES + (FORALL(x:nat):occ(x,l) > 0 IMPLIES NOT x < n) + + upb_perm: LEMMA % :-) + FORALL(l, lp: list[nat]): perm?(l,lp) IMPLIES + FORALL(n:nat): upb(n,l) IMPLIES upb(n,lp) + + lwb_perm: LEMMA % :-) + FORALL(l, lp: list[nat]): perm?(l,lp) IMPLIES + FORALL(n:nat): lwb(n,l) IMPLIES lwb(n,lp) + + qs_sorted :LEMMA % :-( to be done + FORALL (l:list[nat]): sorted?(qs(l)) + +% tl : VAR list[nat] + +% test : LEMMA +% qs ((:4,3,6,2,5:)) = tl + + +END QS_props |