Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

replaced depricated ==. with === #2

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

replaced depricated ==. with === #2

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Binary file removed vfa/.DS_Store
View file
Open in desktop
Binary file not shown.
118 changes: 58 additions & 60 deletions vfa2/BST.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -114,26 +114,26 @@ t_apply_empty x v1 = (lookup x (Bind x v1 Empty Empty) ) *** QED
{-@ t_update_eq :: (Eq k, Ord k, Eq v) => t: (BST k v) -> x:k -> v1 :v -> { lookup x (insert x v1 t) = (Just v1) } @-}
t_update_eq :: (Eq k, Ord k, Eq v) => (BST k v) -> k -> v -> Proof
t_update_eq Empty x v1 = lookup x (insert x v1 Empty)
==. lookup x (Bind x v1 Empty Empty)
==. (Just v1)
=== lookup x (Bind x v1 Empty Empty)
=== (Just v1)
*** QED

t_update_eq (Bind k v l r) x v1
| k == x = lookup x (insert x v1 (Bind k v l r))
==. lookup x (Bind x v1 l r)
==. Just v1
=== lookup x (Bind x v1 l r)
=== Just v1
*** QED

| k < x = lookup x (insert x v1 (Bind k v l r))
==. lookup x ( Bind k v l (insert x v1 r))
==. lookup x (insert x v1 r)
==. (Just v1) ? t_update_eq r x v1
=== lookup x ( Bind k v l (insert x v1 r))
=== lookup x (insert x v1 r) ? t_update_eq r x v1
=== (Just v1)
*** QED

| k > x = lookup x (insert x v1 (Bind k v l r))
==. lookup x ( Bind k v (insert x v1 l) r)
==. lookup x (insert x v1 l)
==. (Just v1) ? t_update_eq l x v1
=== lookup x ( Bind k v (insert x v1 l) r)
=== lookup x (insert x v1 l) ? t_update_eq l x v1
=== (Just v1)
*** QED


Expand All @@ -143,54 +143,54 @@ t_update_eq (Bind k v l r) x v1
t_update_neq :: (Eq k, Ord k, Eq v) => k -> k -> v -> (BST k v) -> Proof
t_update_neq k1 k2 v2 Empty
| k1 < k2 = lookup k1 (insert k2 v2 Empty)
==. lookup k1 (Bind k2 v2 Empty Empty)
==. lookup k1 Empty
=== lookup k1 (Bind k2 v2 Empty Empty)
=== lookup k1 Empty
*** QED

| otherwise = lookup k1 (insert k2 v2 Empty)
==. lookup k1 (Bind k2 v2 Empty Empty)
==. lookup k1 Empty
=== lookup k1 (Bind k2 v2 Empty Empty)
=== lookup k1 Empty
*** QED

t_update_neq k1 k2 v2 (Bind k v l r)
| k1 < k, k < k2 = lookup k1 (insert k2 v2 (Bind k v l r))
==. lookup k1 (Bind k v l (insert k2 v2 r))
==. lookup k1 (Bind k v l r)
=== lookup k1 (Bind k v l (insert k2 v2 r))
=== lookup k1 (Bind k v l r)
*** QED

| k == k2 = lookup k1 (insert k2 v2 (Bind k v l r))
==. lookup k1 (Bind k v2 l r)
==. lookup k1 (Bind k v l r)
=== lookup k1 (Bind k v2 l r)
=== lookup k1 (Bind k v l r)
*** QED

| k1 == k, k < k2 = lookup k1 (insert k2 v2 (Bind k v l r))
==. lookup k1 (Bind k v l (insert k2 v2 r))
==. lookup k1 (Bind k v l r)
=== lookup k1 (Bind k v l (insert k2 v2 r))
=== lookup k1 (Bind k v l r)
*** QED

| k2 < k, k == k1 = lookup k1 (insert k2 v2 (Bind k v l r))
==. lookup k1 (Bind k v (insert k2 v2 l) r)
==. lookup k1 (Bind k v l r)
=== lookup k1 (Bind k v (insert k2 v2 l) r)
=== lookup k1 (Bind k v l r)
*** QED

| k2 < k, k < k1 = lookup k1 (insert k2 v2 (Bind k v l r))
==. lookup k1 (Bind k v (insert k2 v2 l) r)
==. lookup k1 r
==. lookup k1 (Bind k v l r)
=== lookup k1 (Bind k v (insert k2 v2 l) r)
=== lookup k1 r
=== lookup k1 (Bind k v l r)
*** QED

| k1 < k, k2 < k = lookup k1 (insert k2 v2 (Bind k v l r))
==. lookup k1 (Bind k v (insert k2 v2 l) r)
==. lookup k1 (insert k2 v2 l) ? t_update_neq k1 k2 v2 l
==. lookup k1 l
==. lookup k1 (Bind k v l r)
=== lookup k1 (Bind k v (insert k2 v2 l) r) ? t_update_neq k1 k2 v2 l
=== lookup k1 (insert k2 v2 l)
=== lookup k1 l
=== lookup k1 (Bind k v l r)
*** QED

| k < k1, k < k2 = lookup k1 (insert k2 v2 (Bind k v l r))
==. lookup k1 (Bind k v l (insert k2 v2 r))
==. lookup k1 (insert k2 v2 r) ? t_update_neq k1 k2 v2 r
==. lookup k1 r
==. lookup k1 (Bind k v l r)
=== lookup k1 (Bind k v l (insert k2 v2 r)) ? t_update_neq k1 k2 v2 r
=== lookup k1 (insert k2 v2 r)
=== lookup k1 r
=== lookup k1 (Bind k v l r)
*** QED


Expand All @@ -199,31 +199,31 @@ t_update_neq k1 k2 v2 (Bind k v l r)
thm_same_tree :: (Eq k, Ord k, Eq v) => (BST k v) -> v -> v -> k -> Proof

thm_same_tree Empty v1 v2 x = (insert x v2 (insert x v1 Empty))
==. (insert x v2 (Bind x v1 Empty Empty))
==. (Bind x v2 Empty Empty)
==. (insert x v2 Empty)
=== (insert x v2 (Bind x v1 Empty Empty))
=== (Bind x v2 Empty Empty)
=== (insert x v2 Empty)
*** QED

thm_same_tree (Bind x1 v l r) v1 v2 x

| x == x1 = (insert x v2 (insert x v1 (Bind x v l r)))
==. (insert x v2 (Bind x v1 l r))
==. (Bind x v2 l r)
==. (insert x v2 (Bind x1 v l r))
=== (insert x v2 (Bind x v1 l r))
=== (Bind x v2 l r)
=== (insert x v2 (Bind x1 v l r))
*** QED

| x < x1 = (insert x v2 (insert x v1 (Bind x1 v l r)))
==. (insert x v2 (Bind x1 v (insert x v1 l) r))
==. (Bind x1 v (insert x v2 (insert x v1 l)) r)
==. (Bind x1 v (insert x v2 l) r) ? thm_same_tree l v1 v2 x
==. (insert x v2 (Bind x1 v l r))
=== (insert x v2 (Bind x1 v (insert x v1 l) r))
=== (Bind x1 v (insert x v2 (insert x v1 l)) r) ? thm_same_tree l v1 v2 x
=== (Bind x1 v (insert x v2 l) r)
=== (insert x v2 (Bind x1 v l r))
*** QED

| x > x1 = (insert x v2 (insert x v1 (Bind x1 v l r)))
==. (insert x v2 (Bind x1 v l (insert x v1 r)))
==. (Bind x1 v l (insert x v2 (insert x v1 r)))
==. (Bind x1 v l (insert x v2 r)) ? thm_same_tree r v1 v2 x
==. (insert x v2 (Bind x1 v l r))
=== (insert x v2 (Bind x1 v l (insert x v1 r)))
=== (Bind x1 v l (insert x v2 (insert x v1 r))) ? thm_same_tree r v1 v2 x
=== (Bind x1 v l (insert x v2 r))
=== (insert x v2 (Bind x1 v l r))
*** QED


Expand All @@ -248,34 +248,32 @@ t_update_same t x y = (t_update_same_aux t x)*** QED
:: (Eq k, Ord k, Eq v)
=> t:BST k v
-> x: {k | isJust (lookup x t) }
-> {(insert x (fromJust (lookup x t)) t) == t} @-}
-> {(insert x (fromJust (lookup x t)) t) = t} @-}
t_update_same_aux
:: (Eq k, Ord k, Eq v)
=> BST k v -> k -> Proof
t_update_same_aux (Bind k v l r) x
| x == k
= insert x (fromJust (lookup x (Bind x v l r))) (Bind x v l r)
==. insert x (fromJust (Just v)) (Bind x v l r)
==. insert x v (Bind x v l r)
==. Bind x v l r
=== insert x (fromJust (Just v)) (Bind x v l r)
=== insert x v (Bind x v l r)
=== Bind x v l r
*** QED
| x < k
= insert x (fromJust (lookup x (Bind k v l r))) (Bind k v l r)
==. insert x (fromJust (lookup x l)) (Bind k v l r)
==. Bind k v (insert x (fromJust (lookup x l)) l) r
? t_update_same_aux l x
==. Bind k v l r
=== insert x (fromJust (lookup x l)) (Bind k v l r)
=== Bind k v (insert x (fromJust (lookup x l)) l) r
? t_update_same_aux l x
*** QED
| x > k
= insert x (fromJust (lookup x (Bind k v l r))) (Bind k v l r)
==. insert x (fromJust (lookup x r)) (Bind k v l r)
==. Bind k v l (insert x (fromJust (lookup x r)) r)
? t_update_same_aux r x
==. Bind k v l r
=== insert x (fromJust (lookup x r)) (Bind k v l r)
=== Bind k v l (insert x (fromJust (lookup x r)) r)
? t_update_same_aux r x
*** QED
t_update_same_aux Empty x
= isJust (lookup x Empty)
==. isJust Nothing
=== isJust Nothing
*** QED


Expand Down
8 changes: 1 addition & 7 deletions vfa2/InsertionSort.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ module ISort where
import qualified Language.Haskell.Liquid.Bag as B
import Language.Haskell.Liquid.ProofCombinators
import Permutations
import Lists


{-@ infix : @-}
Expand Down Expand Up @@ -40,9 +41,6 @@ thmSortPerm [] = trivial
thmSortPerm (x:xs) = [ thmSortPerm xs, thmInsertPerm x (sort xs) ] *** QED





{-@ reflect sorted1 @-}
sorted1 :: (Ord a) => a -> [a] -> Bool
sorted1 x [] = True
Expand All @@ -55,9 +53,6 @@ sorted [] = True
sorted (h:t) = sorted1 h t





{-@ thmInsertSorted :: x:a -> ys:{[a] | sorted ys} -> { sorted (insert2 x ys) } @-}
thmInsertSorted :: (Ord a) => a -> [a] -> Proof
thmInsertSorted x [] = trivial
Expand All @@ -70,7 +65,6 @@ thmInsertSorted x (h:(y:t))
| x > h && x > y = thmInsertSorted x (y:t)



{-@ thmSortSorted :: xs: [a] -> { sorted (sort xs) } @-}
thmSortSorted :: (Ord a) => [a] -> Proof
thmSortSorted [] = trivial
Expand Down
23 changes: 12 additions & 11 deletions vfa2/Lists.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,12 @@

module Lists where
import Language.Haskell.Liquid.ProofCombinators
import Prelude hiding (length, (++), reverse, pred, (^))
import Prelude hiding ((++), reverse, pred, (^))


{-@ infix ++ @-}
{-@ reflect ++ @-}
{-@ (++) :: forall <p :: a -> Bool>. [a<p>] -> [a<p>] -> [a<p>] @-} -- used for binomial queues
(++) :: [a] -> [a] -> [a]
[] ++ ys = ys
(x:xs) ++ ys = x:(xs ++ ys)
Expand All @@ -31,14 +32,14 @@ app_assoc4 [] ys zs ws = appendAssoc ys zs ws
app_assoc4 (x:xs) ys zs ws = app_assoc4 xs ys zs ws


{-@ measure length @-}
{-@ length :: [a] -> Nat @-}
length :: [a] -> Int
length [] = 0
length (x:xs) = 1 + length xs
{-@ measure len @-}
{-@ len :: [a] -> Nat @-}
len :: [a] -> Int
len [] = 0
len (x:xs) = 1 + len xs


{-@ app_length :: xs:_ -> ys:_ -> { length (xs ++ ys) == length xs + length ys } @-}
{-@ app_length :: xs:_ -> ys:_ -> { len (xs ++ ys) == len xs + len ys } @-}
app_length :: [a] -> [a] -> Proof
app_length [] ys = trivial
app_length (x:xs) ys = app_length xs ys
Expand All @@ -48,7 +49,6 @@ app_length (x:xs) ys = app_length xs ys
reverse :: [a] -> [a]
reverse [] = []
reverse (x:xs) = reverse xs ++ [x]
reverse (x:xs) = reverse xs ++ [x]


{-@ lemma_rev_app :: xs:_ -> ys:_ -> {reverse (xs ++ ys) = reverse (ys) ++ reverse (xs)} @-}
Expand All @@ -63,7 +63,7 @@ theorem_rev_rev [] = trivial
theorem_rev_rev (x:xs)=[lemma_rev_app (reverse xs) ([x]), theorem_rev_rev xs] *** QED


{-@ rev_length :: xs:_ ->{ length (reverse xs) == length xs } @-}
{-@ rev_length :: xs:_ ->{ len (reverse xs) == len xs } @-}
rev_length :: [a] -> Proof
rev_length [] = trivial
rev_length (x:xs)=[ app_length (reverse xs) [x], rev_length xs, app_length [x] xs ] *** QED
Expand All @@ -88,7 +88,7 @@ pred n
| n == 0 = 0
| otherwise = n-1


{-@ reflect lHd @-}
{-@ lHd :: (Ord a) => {v: [a] | len v > 0} -> a @-}
lHd :: (Ord a) => [a] -> a
lHd (x:_) =x
Expand All @@ -100,7 +100,7 @@ lTl [] = []
lTl (_:xs) = xs


{-@ tl_length_pred :: xs:_ -> { pred (length xs) == length (lTl xs) } @-}
{-@ tl_length_pred :: xs:_ -> { pred (len xs) == len (lTl xs) } @-}
tl_length_pred :: [a] -> Proof
tl_length_pred [] = trivial
tl_length_pred (x:xs) = tl_length_pred xs
Expand All @@ -118,3 +118,4 @@ beq_list (x:xs) (y:ys) = if (x==y) then (beq_list xs ys) else False
beq_natlist_refl :: [Int] -> Proof
beq_natlist_refl [] = trivial
beq_natlist_refl (x:xs) = beq_natlist_refl xs

9 changes: 4 additions & 5 deletions vfa2/PRIQUEUE.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -177,11 +177,10 @@ thm_perm1 :: (Eq a, Ord a) => [a] -> Proof
thm_perm1 []
= ()
thm_perm1 (x:xs)
= permutation xs []
==. bag xs == bag []
==. B.put x (bag xs) == B.empty
? B.thm_emp x (bag xs)
==. False
= (permutation xs []
, bag xs == bag []
,B.put x (bag xs) == B.empty
, B.thm_emp x (bag xs) )
*** QED


Expand Down
Loading