|
2
|
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 )
|
