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 )