Mercurial > hg > Papers > 2022 > soto-sigos

comparison Paper/src/agda/utilities.agda.replaced @ 0:14a0e409d574

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ADD fast commit
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sun, 24 Apr 2022 23:13:44 +0900
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 0:14a0e409d574
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 )