From dc939bc8e5e2578b325f748537f4f8591e07be3e Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Wed, 23 Mar 2016 22:48:31 +0100
Subject: Start assignment 8

---
 assignment8/qs.pvs | 150 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 150 insertions(+)
 create mode 100644 assignment8/qs.pvs

(limited to 'assignment8/qs.pvs')

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
-- 
cgit v1.2.3