Members/atton/agda-proofs: sandbox/SetWithConstraint.agda annotate

annotate sandbox/SetWithConstraint.agda @ 77:a2e6f61d5f2b default tip

Add modus-ponens

author	atton <atton@cr.ie.u-ryukyu.ac.jp>
date	Thu, 09 Feb 2017 06:32:03 +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 d9b394c245c5 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 33 diff changeset	16 elem : {A : Set} -> String -> MySet A -> Bool
d9b394c245c5 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 33 diff changeset	17 elem a empty = false
d9b394c245c5 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 33 diff changeset	18 elem a (cons (k , v) s) = elem' (a == k) a (k , v) s
d9b394c245c5 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 33 diff changeset	19 where
d9b394c245c5 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 33 diff changeset	20 elem' : {A : Set} -> Bool -> String -> (String × A) -> MySet A -> Bool
d9b394c245c5 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 33 diff changeset	21 elem' false a p s = elem a s
d9b394c245c5 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 33 diff changeset	22 elem' true _ _ _ = true
d9b394c245c5 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 33 diff changeset	23
d9b394c245c5 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 33 diff changeset	24
d9b394c245c5 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 33 diff changeset	25 insert' : {A : Set} -> Bool -> (String × A) -> MySet A -> MySet A
d9b394c245c5 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 33 diff changeset	26 insert' false p s = cons p s
d9b394c245c5 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 33 diff changeset	27 insert' true _ s = s
d9b394c245c5 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 33 diff changeset	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 d9b394c245c5 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 33 diff changeset	30 insert (k , v) empty = cons (k , v) empty
d9b394c245c5 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 33 diff changeset	31 insert (k , v) s = insert' (elem k s) (k , v) s
d9b394c245c5 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 33 diff changeset	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 d9b394c245c5 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 33 diff changeset	56 ≡⟨ refl ⟩
d9b394c245c5 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 33 diff changeset	57 length (insert' (elem k (cons (ks , vs) s)) (k , n) (cons (ks , vs) s))
d9b394c245c5 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 33 diff changeset	58 ≡⟨ cong (\e -> length (insert' e (k , n) (cons (ks , vs) s))) nonElem ⟩
d9b394c245c5 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 33 diff changeset	59 length (insert' false (k , n) (cons (ks , vs) s))
d9b394c245c5 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 33 diff changeset	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 bf667ec8cba4 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 34 diff changeset	63
bf667ec8cba4 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 34 diff changeset	64 insert-length-exists : (k : String) (n : ℕ )(s : MySet ℕ) {hasKey : elem k s ≡ true} {nonEmpty : s ≢ empty}
bf667ec8cba4 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 34 diff changeset	65 -> length (insert (k , n) s) ≡ (length s)
bf667ec8cba4 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 34 diff changeset	66 insert-length-exists _ _ empty {nonEmpty = n} = ⊥-elim (n refl)
bf667ec8cba4 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 34 diff changeset	67 insert-length-exists k n (cons x s) {hasKey = h} = begin
bf667ec8cba4 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 34 diff changeset	68 length (insert (k , n) (cons x s))
bf667ec8cba4 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 34 diff changeset	69 ≡⟨ refl ⟩
bf667ec8cba4 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 34 diff changeset	70 length (insert' (elem k (cons x s)) (k , n) (cons x s))
bf667ec8cba4 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 34 diff changeset	71 ≡⟨ cong (\e -> length (insert' e (k , n) (cons x s))) h ⟩
bf667ec8cba4 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 34 diff changeset	72 length (insert' true (k , n) (cons x s))
bf667ec8cba4 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 34 diff changeset	73 ≡⟨ refl ⟩
bf667ec8cba4 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 34 diff changeset	74 length (cons x s)
bf667ec8cba4 Set with constraint atton <atton@cr.ie.u-ryukyu.ac.jp> parents: 34 diff changeset	75 ∎

Mercurial > hg > Members > atton > agda-proofs

annotate sandbox/SetWithConstraint.agda @ 77:a2e6f61d5f2b default tip