Mercurial > hg > Members > atton > agda-proofs

comparison sandbox/SetWithConstraint.agda @ 34:d9b394c245c5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Set with constraint
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Mon, 02 Jan 2017 03:17:18 +0000
parents 35ea84d35079
children bf667ec8cba4
comparison
equal deleted inserted replaced
33:35ea84d35079 34:d9b394c245c5
11 11
12 data MySet (A : Set) : Set where 12 data MySet (A : Set) : Set where
13 empty : MySet A 13 empty : MySet A
14 cons : (String × A) -> MySet A -> MySet A 14 cons : (String × A) -> MySet A -> MySet A
15 15
16 elem : {A : Set} -> String -> MySet A -> Bool
17 elem a empty = false
18 elem a (cons (k , v) s) = elem' (a == k) a (k , v) s
19 where
20 elem' : {A : Set} -> Bool -> String -> (String × A) -> MySet A -> Bool
21 elem' false a p s = elem a s
22 elem' true _ _ _ = true
23
24
25 insert' : {A : Set} -> Bool -> (String × A) -> MySet A -> MySet A
26 insert' false p s = cons p s
27 insert' true _ s = s
28
16 insert : {A : Set} -> (String × A) -> MySet A -> MySet A 29 insert : {A : Set} -> (String × A) -> MySet A -> MySet A
17 insert (k , v) empty = cons (k , v) empty 30 insert (k , v) empty = cons (k , v) empty
18 insert (k , v) (cons (sk , sv) s) with (k == sk) 31 insert (k , v) s = insert' (elem k s) (k , v) s
19 ... | true = cons (sk , sv) s 32
20 ... | false = cons (sk , sv) (insert (k , v) s)
21 33
22 length : {A : Set} -> MySet A -> ℕ 34 length : {A : Set} -> MySet A -> ℕ
23 length empty = 0 35 length empty = 0
24 length (cons _ s) = suc (length s) 36 length (cons _ s) = suc (length s)
25
26 elem : {A : Set} -> String -> MySet A -> Bool
27 elem a empty = false
28 elem a (cons (k , v) s) with a == k
29 ... | true = true
30 ... | false = elem a s
31 37
32 head : {A : Set} -> MySet A -> Maybe (String × A) 38 head : {A : Set} -> MySet A -> Maybe (String × A)
33 head empty = nothing 39 head empty = nothing
34 head (cons x _) = just x 40 head (cons x _) = just x
35 41
41 empty-insert-length : (s : MySet ℕ) -> length (insert ("a" , 100) empty) ≡ 1 47 empty-insert-length : (s : MySet ℕ) -> length (insert ("a" , 100) empty) ≡ 1
42 empty-insert-length s = refl 48 empty-insert-length s = refl
43 49
44 open ≡-Reasoning 50 open ≡-Reasoning
45 51
46 expand-non-elem : (k : String) (s : MySet ℕ) -> (nonElem : elem k s ≡ false) -> (just k ≢ (Data.Maybe.map proj₁ (head s)))
47 expand-non-elem k empty nonElem = {!!}
48 expand-non-elem k (cons x s) nonElem = {!!}
49
50
51 insert-length : (k : String) (n : ℕ )(s : MySet ℕ) {nonElem : elem k s ≡ false} -> length (insert (k , n) s) ≡ suc (length s) 52 insert-length : (k : String) (n : ℕ )(s : MySet ℕ) {nonElem : elem k s ≡ false} -> length (insert (k , n) s) ≡ suc (length s)
52 insert-length k n empty = refl 53 insert-length k n empty = refl
53 insert-length k n (cons (ks , vs) s) {nonElem} = begin 54 insert-length k n (cons (ks , vs) s) {nonElem} = begin
54 length (insert (k , n) (cons (ks , vs) s)) 55 length (insert (k , n) (cons (ks , vs) s))
55 ≡⟨ {!!} ⟩ 56 ≡⟨ refl ⟩
57 length (insert' (elem k (cons (ks , vs) s)) (k , n) (cons (ks , vs) s))
58 ≡⟨ cong (\e -> length (insert' e (k , n) (cons (ks , vs) s))) nonElem ⟩
59 length (insert' false (k , n) (cons (ks , vs) s))
60 ≡⟨ refl ⟩
56 suc (suc (length s)) 61 suc (suc (length s))
57 ∎ 62 ∎