-
Notifications
You must be signed in to change notification settings - Fork 0
/
Sets.agda
68 lines (56 loc) · 4.69 KB
/
Sets.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
module Sets where
open import Basics
open import Fin
open import Vect
_∈_ : {A : Set} {n : nat} (a : A) (as : vect A n) -> Set
_∈_ {A} {n} a as = fin n * (λ i -> (as ! i) == a)
inCons : {A : Set} {n : nat} {a a' : A} {as : vect A n} -> a ∈ as -> a ∈ (a' :: as)
inCons (i , mem) = FS i , mem
data isSet {A : Set} : {n : nat} -> vect A n -> Set where
EmptySet : isSet []
Insert : {n : nat} {as : vect A n} (a : A) -> isSet as -> not (a ∈ as) -> isSet (a :: as)
in? : {A : Set} {n : nat} -> equality A -> (a : A) (as : vect A n) -> decide (a ∈ as)
in? {A} {Zero} eq a [] = No (λ { (() , y) })
in? {A} {Suc n} eq a (a' :: as) with eq a a'
in? {A} {Suc n} eq a (.a :: as) | Yes Refl = Yes (FZ , Refl)
in? {A} {Suc n} eq a (a' :: as) | No neq with in? eq a as
in? {A} {Suc n} eq a (a' :: as) | No neq | Yes mem = Yes (inCons mem)
in? {A} {Suc n} eq a (a' :: as) | No neq | No nmem' = No (inLemma a a' as neq nmem')
where
inLemma : (a a' : A) (as : vect A n) -> not (a == a') -> not (fin n * (λ i → (as ! i) == a)) -> not (fin (Suc n) * (λ i -> ((a' :: as) ! i) == a))
inLemma a .a as neq nmem (FZ , Refl) = neq Refl
inLemma a a' as neq nmem (FS i , mem) = nmem (i , mem)
remove : {A : Set} {n : nat} (a : A) (as : vect A (Suc n)) -> a ∈ as -> vect A n
remove {A} {n} a (.a :: as) (FZ , Refl) = as
remove {A} {Zero} a (a' :: as) (FS () , mem)
remove {A} {Suc n} a (a' :: as) (FS i , mem) = a' :: remove a as (i , mem)
removeRetainsOthers : {A : Set} {n : nat} (a a' : A) (as : vect A (Suc n)) (mem : a ∈ as) -> not (a == a') -> a' ∈ as -> a' ∈ remove a as mem
removeRetainsOthers {A} {n} a .a (.a :: as) (FZ , Refl) neq (FZ , Refl) with neq Refl
removeRetainsOthers {A} {n} a .a (.a :: as) (FZ , Refl) neq (FZ , Refl) | ()
removeRetainsOthers {A} {n} a a' (.a :: as) (FZ , Refl) neq (FS i' , mem') = i' , mem'
removeRetainsOthers {A} {Zero} a a' (a2 :: as) (FS () , mem) neq (i' , mem')
removeRetainsOthers {A} {Suc n} a a' (.a' :: as) (FS i , mem) neq (FZ , Refl) = FZ , Refl
removeRetainsOthers {A} {Suc n} a a' (a2 :: as) (FS i , mem) neq (FS i' , mem') = inCons (removeRetainsOthers a a' as (i , mem) neq (i' , mem'))
removeRetainsOthers' : {A : Set} {n : nat} (a a' : A) (as : vect A (Suc n)) (mem : a ∈ as) -> not (a == a') -> not (a' ∈ remove a as mem) -> not (a' ∈ as)
removeRetainsOthers' {A} {n} a .a (.a :: as) (FZ , Refl) neq nmem (FZ , Refl) = neq Refl
removeRetainsOthers' {A} {n} a a' (.a :: as) (FZ , Refl) neq nmem (FS i' , mem') = nmem (i' , mem')
removeRetainsOthers' {A} {Zero} a a' (a2 :: as) (FS () , mem) neq nmem (i' , mem')
removeRetainsOthers' {A} {Suc n} a a' (.a' :: as) (FS i , mem) neq nmem (FZ , Refl) = nmem (FZ , Refl)
removeRetainsOthers' {A} {Suc n} a a' (a2 :: as) (FS i , mem) neq nmem (FS i' , mem') = removeRetainsOthers' a a' as (i , mem) neq (λ x -> nmem (inCons x)) (i' , mem')
removeDoesNotAdd : {A : Set} {n : nat} (a a' : A) (as : vect A (Suc n)) (mem : a ∈ as) -> a' ∈ remove a as mem -> a' ∈ as
removeDoesNotAdd a a' (.a :: as) (FZ , Refl) mem' = inCons mem'
removeDoesNotAdd a a' (.a' :: as) (FS i , mem) (FZ , Refl) = FZ , Refl
removeDoesNotAdd a a' (a2 :: as) (FS i , mem) (FS i' , mem') = inCons (removeDoesNotAdd a a' as (i , mem) (i' , mem'))
removeDoesNotAdd' : {A : Set} {n : nat} (a a' : A) (as : vect A (Suc n)) (mem : a ∈ as) -> not (a' ∈ as) -> not (a' ∈ remove a as mem)
removeDoesNotAdd' a a' (.a :: as) (FZ , Refl) nmem mem' = nmem (inCons mem')
removeDoesNotAdd' a a' (.a' :: as) (FS i , mem) nmem (FZ , Refl) = nmem (FZ , Refl)
removeDoesNotAdd' a a' (a2 :: as) (FS i , mem) nmem (FS i' , mem') = removeDoesNotAdd' a a' as (i , mem) (λ mem2 -> nmem (inCons mem2)) (i' , mem')
removeSet : {A : Set} {n : nat} (a : A) (as : vect A (Suc n)) (mem : a ∈ as) -> isSet as -> isSet (remove a as mem)
removeSet {A} {n} a (.a :: as) (FZ , Refl) (Insert .a is nmem) = is
removeSet {A} {Zero} a (a' :: as) (FS () , mem) (Insert .a' is nmem)
removeSet {A} {Suc n} a (a' :: as) (FS i , mem) (Insert .a' is nmem) = Insert a' (removeSet a as (i , mem) is) (removeDoesNotAdd' a a' as (i , mem) nmem)
removeRemoves : {A : Set} {n : nat} (a : A) (as : vect A (Suc n)) (mem : a ∈ as) -> isSet as -> not (a ∈ remove a as mem)
removeRemoves {A} {n} a (.a :: as) (FZ , Refl) (Insert .a is nmem) mem' = nmem mem'
removeRemoves {A} {Zero} a (a' :: as) (FS () , mem) (Insert .a' is nmem) (i' , mem')
removeRemoves {A} {Suc n} a (.a :: as) (FS i , mem) (Insert .a is nmem) (FZ , Refl) = nmem (i , mem)
removeRemoves {A} {Suc n} a (a' :: as) (FS i , mem) (Insert .a' is nmem) (FS i' , mem') = removeRemoves a as (i , mem) is (i' , mem')