Mercurial > hg > Members > atton > agda-proofs
annotate sandbox/SetWithConstraint.agda @ 50:ccb34e3f1514
Rename named-product to subtype
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 10 Jan 2017 01:40:55 +0000 |
parents | bf667ec8cba4 |
children |
rev | line source |
---|---|
32
5af5f1a930bc
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 module SetWithConstraint where |
5af5f1a930bc
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 |
33
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
3 open import Data.Nat |
32
5af5f1a930bc
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 open import Data.Bool |
5af5f1a930bc
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 open import Data.Product |
33
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
6 open import Data.String |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
7 open import Relation.Binary.PropositionalEquality |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
8 open import Data.Empty |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
9 open import Data.Maybe |
32
5af5f1a930bc
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 |
33
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
11 |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
12 data MySet (A : Set) : Set where |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
13 empty : MySet A |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
14 cons : (String × A) -> MySet A -> MySet A |
32
5af5f1a930bc
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 |
34 | 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 | |
33
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
29 insert : {A : Set} -> (String × A) -> MySet A -> MySet A |
34 | 30 insert (k , v) empty = cons (k , v) empty |
31 insert (k , v) s = insert' (elem k s) (k , v) s | |
32 | |
33
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
33 |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
34 length : {A : Set} -> MySet A -> ℕ |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
35 length empty = 0 |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
36 length (cons _ s) = suc (length s) |
32
5af5f1a930bc
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 |
33
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
38 head : {A : Set} -> MySet A -> Maybe (String × A) |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
39 head empty = nothing |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
40 head (cons x _) = just x |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
41 |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
42 |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
43 |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
44 empty-length : {A : Set} -> (length {A} empty) ≡ 0 |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
45 empty-length = refl |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
46 |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
47 empty-insert-length : (s : MySet ℕ) -> length (insert ("a" , 100) empty) ≡ 1 |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
48 empty-insert-length s = refl |
32
5af5f1a930bc
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 |
5af5f1a930bc
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 open ≡-Reasoning |
5af5f1a930bc
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 |
33
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
52 insert-length : (k : String) (n : ℕ )(s : MySet ℕ) {nonElem : elem k s ≡ false} -> length (insert (k , n) s) ≡ suc (length s) |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
53 insert-length k n empty = refl |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
54 insert-length k n (cons (ks , vs) s) {nonElem} = begin |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
55 length (insert (k , n) (cons (ks , vs) s)) |
34 | 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 ⟩ | |
33
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
61 suc (suc (length s)) |
35ea84d35079
Trying Set with constraint...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
62 ∎ |
35 | 63 |
64 insert-length-exists : (k : String) (n : ℕ )(s : MySet ℕ) {hasKey : elem k s ≡ true} {nonEmpty : s ≢ empty} | |
65 -> length (insert (k , n) s) ≡ (length s) | |
66 insert-length-exists _ _ empty {nonEmpty = n} = ⊥-elim (n refl) | |
67 insert-length-exists k n (cons x s) {hasKey = h} = begin | |
68 length (insert (k , n) (cons x s)) | |
69 ≡⟨ refl ⟩ | |
70 length (insert' (elem k (cons x s)) (k , n) (cons x s)) | |
71 ≡⟨ cong (\e -> length (insert' e (k , n) (cons x s))) h ⟩ | |
72 length (insert' true (k , n) (cons x s)) | |
73 ≡⟨ refl ⟩ | |
74 length (cons x s) | |
75 ∎ |