Mercurial > hg > Papers > 2021 > soto-prosym
comparison Paper/src/agda/utilities.agda.replaced @ 2:9176dff8f38a
ADD while loop description
author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 05 Nov 2021 15:19:08 +0900 (2021-11-05) |
parents | |
children | 339fb67b4375 |
comparison
equal
deleted
inserted
replaced
1:3910f4639344 | 2:9176dff8f38a |
---|---|
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 ) |