|
0
|
1 {-!$\#$! OPTIONS --allow-unsolved-metas !$\#$!-}
|
|
|
2 module utilities where
|
|
|
3
|
|
|
4 open import Function
|
|
|
5 open import Data.Nat
|
|
|
6 open import Data.Product
|
|
|
7 open import Data.Bool hiding ( _≟_ ; _!$\leq$!?_)
|
|
|
8 open import Level renaming ( suc to succ ; zero to Zero )
|
|
|
9 open import Relation.Nullary using (!$\neg$!_; Dec; yes; no)
|
|
|
10 open import Relation.Binary.PropositionalEquality
|
|
|
11
|
|
|
12 Pred : Set !$\rightarrow$! Set!$\_{1}$!
|
|
|
13 Pred X = X !$\rightarrow$! Set
|
|
|
14
|
|
|
15 Imply : Set !$\rightarrow$! Set !$\rightarrow$! Set
|
|
|
16 Imply X Y = X !$\rightarrow$! Y
|
|
|
17
|
|
|
18 Iff : Set !$\rightarrow$! Set !$\rightarrow$! Set
|
|
|
19 Iff X Y = Imply X Y !$\times$! Imply Y X
|
|
|
20
|
|
|
21 record _!$\wedge$!_ {n : Level } (a : Set n) (b : Set n): Set n where
|
|
|
22 field
|
|
|
23 pi1 : a
|
|
|
24 pi2 : b
|
|
|
25
|
|
|
26 open _!$\wedge$!_
|
|
|
27
|
|
|
28 _-_ : !$\mathbb{N}$! !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! !$\mathbb{N}$!
|
|
|
29 x - zero = x
|
|
|
30 zero - _ = zero
|
|
|
31 (suc x) - (suc y) = x - y
|
|
|
32
|
|
|
33 +zero : { y : !$\mathbb{N}$! } !$\rightarrow$! y + zero !$\equiv$! y
|
|
|
34 +zero {zero} = refl
|
|
|
35 +zero {suc y} = cong ( !$\lambda$! x !$\rightarrow$! suc x ) ( +zero {y} )
|
|
|
36
|
|
|
37
|
|
|
38 +-sym : { x y : !$\mathbb{N}$! } !$\rightarrow$! x + y !$\equiv$! y + x
|
|
|
39 +-sym {zero} {zero} = refl
|
|
|
40 +-sym {zero} {suc y} = let open !$\equiv$!-Reasoning in
|
|
|
41 begin
|
|
|
42 zero + suc y
|
|
|
43 !$\equiv$!!$\langle$!!$\rangle$!
|
|
|
44 suc y
|
|
|
45 !$\equiv$!!$\langle$! sym +zero !$\rangle$!
|
|
|
46 suc y + zero
|
|
|
47 !$\blacksquare$!
|
|
|
48 +-sym {suc x} {zero} = let open !$\equiv$!-Reasoning in
|
|
|
49 begin
|
|
|
50 suc x + zero
|
|
|
51 !$\equiv$!!$\langle$! +zero !$\rangle$!
|
|
|
52 suc x
|
|
|
53 !$\equiv$!!$\langle$!!$\rangle$!
|
|
|
54 zero + suc x
|
|
|
55 !$\blacksquare$!
|
|
|
56 +-sym {suc x} {suc y} = cong ( !$\lambda$! z !$\rightarrow$! suc z ) ( let open !$\equiv$!-Reasoning in
|
|
|
57 begin
|
|
|
58 x + suc y
|
|
|
59 !$\equiv$!!$\langle$! +-sym {x} {suc y} !$\rangle$!
|
|
|
60 suc (y + x)
|
|
|
61 !$\equiv$!!$\langle$! cong ( !$\lambda$! z !$\rightarrow$! suc z ) (+-sym {y} {x}) !$\rangle$!
|
|
|
62 suc (x + y)
|
|
|
63 !$\equiv$!!$\langle$! sym ( +-sym {y} {suc x}) !$\rangle$!
|
|
|
64 y + suc x
|
|
|
65 !$\blacksquare$! )
|
|
|
66
|
|
|
67
|
|
|
68 minus-plus : { x y : !$\mathbb{N}$! } !$\rightarrow$! (suc x - 1) + (y + 1) !$\equiv$! suc x + y
|
|
|
69 minus-plus {zero} {y} = +-sym {y} {1}
|
|
|
70 minus-plus {suc x} {y} = cong ( !$\lambda$! z !$\rightarrow$! suc z ) (minus-plus {x} {y})
|
|
|
71
|
|
|
72 +1!$\equiv$!suc : { x : !$\mathbb{N}$! } !$\rightarrow$! x + 1 !$\equiv$! suc x
|
|
|
73 +1!$\equiv$!suc {zero} = refl
|
|
|
74 +1!$\equiv$!suc {suc x} = cong ( !$\lambda$! z !$\rightarrow$! suc z ) ( +1!$\equiv$!suc {x} )
|
|
|
75
|
|
|
76 lt : !$\mathbb{N}$! !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! Bool
|
|
|
77 lt x y with (suc x ) !$\leq$!? y
|
|
|
78 lt x y | yes p = true
|
|
|
79 lt x y | no !$\neg$!p = false
|
|
|
80
|
|
|
81 pred!$\mathbb{N}$! : {n : !$\mathbb{N}$! } !$\rightarrow$! lt 0 n !$\equiv$! true !$\rightarrow$! !$\mathbb{N}$!
|
|
|
82 pred!$\mathbb{N}$! {zero} ()
|
|
|
83 pred!$\mathbb{N}$! {suc n} refl = n
|
|
|
84
|
|
|
85 pred!$\mathbb{N}$!+1=n : {n : !$\mathbb{N}$! } !$\rightarrow$! (less : lt 0 n !$\equiv$! true ) !$\rightarrow$! (pred!$\mathbb{N}$! less) + 1 !$\equiv$! n
|
|
|
86 pred!$\mathbb{N}$!+1=n {zero} ()
|
|
|
87 pred!$\mathbb{N}$!+1=n {suc n} refl = +1!$\equiv$!suc
|
|
|
88
|
|
|
89 suc-pred!$\mathbb{N}$!=n : {n : !$\mathbb{N}$! } !$\rightarrow$! (less : lt 0 n !$\equiv$! true ) !$\rightarrow$! suc (pred!$\mathbb{N}$! less) !$\equiv$! n
|
|
|
90 suc-pred!$\mathbb{N}$!=n {zero} ()
|
|
|
91 suc-pred!$\mathbb{N}$!=n {suc n} refl = refl
|
|
|
92
|
|
|
93 Equal : !$\mathbb{N}$! !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! Bool
|
|
|
94 Equal x y with x ≟ y
|
|
|
95 Equal x y | yes p = true
|
|
|
96 Equal x y | no !$\neg$!p = false
|
|
|
97
|
|
|
98 _!$\Rightarrow$!_ : Bool !$\rightarrow$! Bool !$\rightarrow$! Bool
|
|
|
99 false !$\Rightarrow$! _ = true
|
|
|
100 true !$\Rightarrow$! true = true
|
|
|
101 true !$\Rightarrow$! false = false
|
|
|
102
|
|
|
103 !$\Rightarrow$!t : {x : Bool} !$\rightarrow$! x !$\Rightarrow$! true !$\equiv$! true
|
|
|
104 !$\Rightarrow$!t {x} with x
|
|
|
105 !$\Rightarrow$!t {x} | false = refl
|
|
|
106 !$\Rightarrow$!t {x} | true = refl
|
|
|
107
|
|
|
108 f!$\Rightarrow$! : {x : Bool} !$\rightarrow$! false !$\Rightarrow$! x !$\equiv$! true
|
|
|
109 f!$\Rightarrow$! {x} with x
|
|
|
110 f!$\Rightarrow$! {x} | false = refl
|
|
|
111 f!$\Rightarrow$! {x} | true = refl
|
|
|
112
|
|
|
113 !$\wedge$!-pi1 : { x y : Bool } !$\rightarrow$! x !$\wedge$! y !$\equiv$! true !$\rightarrow$! x !$\equiv$! true
|
|
|
114 !$\wedge$!-pi1 {x} {y} eq with x | y | eq
|
|
|
115 !$\wedge$!-pi1 {x} {y} eq | false | b | ()
|
|
|
116 !$\wedge$!-pi1 {x} {y} eq | true | false | ()
|
|
|
117 !$\wedge$!-pi1 {x} {y} eq | true | true | refl = refl
|
|
|
118
|
|
|
119 !$\wedge$!-pi2 : { x y : Bool } !$\rightarrow$! x !$\wedge$! y !$\equiv$! true !$\rightarrow$! y !$\equiv$! true
|
|
|
120 !$\wedge$!-pi2 {x} {y} eq with x | y | eq
|
|
|
121 !$\wedge$!-pi2 {x} {y} eq | false | b | ()
|
|
|
122 !$\wedge$!-pi2 {x} {y} eq | true | false | ()
|
|
|
123 !$\wedge$!-pi2 {x} {y} eq | true | true | refl = refl
|
|
|
124
|
|
|
125 !$\wedge$!true : { x : Bool } !$\rightarrow$! x !$\wedge$! true !$\equiv$! x
|
|
|
126 !$\wedge$!true {x} with x
|
|
|
127 !$\wedge$!true {x} | false = refl
|
|
|
128 !$\wedge$!true {x} | true = refl
|
|
|
129
|
|
|
130 true!$\wedge$! : { x : Bool } !$\rightarrow$! true !$\wedge$! x !$\equiv$! x
|
|
|
131 true!$\wedge$! {x} with x
|
|
|
132 true!$\wedge$! {x} | false = refl
|
|
|
133 true!$\wedge$! {x} | true = refl
|
|
|
134 bool-case : ( x : Bool ) { p : Set } !$\rightarrow$! ( x !$\equiv$! true !$\rightarrow$! p ) !$\rightarrow$! ( x !$\equiv$! false !$\rightarrow$! p ) !$\rightarrow$! p
|
|
|
135 bool-case x T F with x
|
|
|
136 bool-case x T F | false = F refl
|
|
|
137 bool-case x T F | true = T refl
|
|
|
138
|
|
|
139 impl!$\Rightarrow$! : {x y : Bool} !$\rightarrow$! (x !$\equiv$! true !$\rightarrow$! y !$\equiv$! true ) !$\rightarrow$! x !$\Rightarrow$! y !$\equiv$! true
|
|
|
140 impl!$\Rightarrow$! {x} {y} p = bool-case x (!$\lambda$! x=t !$\rightarrow$! let open !$\equiv$!-Reasoning in
|
|
|
141 begin
|
|
|
142 x !$\Rightarrow$! y
|
|
|
143 !$\equiv$!!$\langle$! cong ( !$\lambda$! z !$\rightarrow$! x !$\Rightarrow$! z ) (p x=t ) !$\rangle$!
|
|
|
144 x !$\Rightarrow$! true
|
|
|
145 !$\equiv$!!$\langle$! !$\Rightarrow$!t !$\rangle$!
|
|
|
146 true
|
|
|
147 !$\blacksquare$!
|
|
|
148 ) ( !$\lambda$! x=f !$\rightarrow$! let open !$\equiv$!-Reasoning in
|
|
|
149 begin
|
|
|
150 x !$\Rightarrow$! y
|
|
|
151 !$\equiv$!!$\langle$! cong ( !$\lambda$! z !$\rightarrow$! z !$\Rightarrow$! y ) x=f !$\rangle$!
|
|
|
152 true
|
|
|
153 !$\blacksquare$!
|
|
|
154 )
|
|
|
155
|
|
|
156 Equal!$\rightarrow$!!$\equiv$! : { x y : !$\mathbb{N}$! } !$\rightarrow$! Equal x y !$\equiv$! true !$\rightarrow$! x !$\equiv$! y
|
|
|
157 Equal!$\rightarrow$!!$\equiv$! {x} {y} eq with x ≟ y
|
|
|
158 Equal!$\rightarrow$!!$\equiv$! {x} {y} refl | yes refl = refl
|
|
|
159 Equal!$\rightarrow$!!$\equiv$! {x} {y} () | no !$\neg$!p
|
|
|
160
|
|
|
161 Equal+1 : { x y : !$\mathbb{N}$! } !$\rightarrow$! Equal x y !$\equiv$! Equal (suc x) (suc y)
|
|
|
162 Equal+1 {x} {y} with x ≟ y
|
|
|
163 Equal+1 {x} {.x} | yes refl = {!!}
|
|
|
164 Equal+1 {x} {y} | no !$\neg$!p = {!!}
|
|
|
165
|
|
|
166 open import Data.Empty
|
|
|
167
|
|
|
168 !$\equiv$!!$\rightarrow$!Equal : { x y : !$\mathbb{N}$! } !$\rightarrow$! x !$\equiv$! y !$\rightarrow$! Equal x y !$\equiv$! true
|
|
|
169 !$\equiv$!!$\rightarrow$!Equal {x} {.x} refl with x ≟ x
|
|
|
170 !$\equiv$!!$\rightarrow$!Equal {x} {.x} refl | yes refl = refl
|
|
|
171 !$\equiv$!!$\rightarrow$!Equal {x} {.x} refl | no !$\neg$!p = !$\bot$!-elim ( !$\neg$!p refl )
|
