|
12
|
1 module utilities where
|
|
|
2
|
|
|
3 open import Function
|
|
|
4 open import Data.Nat
|
|
|
5 open import Data.Bool hiding ( _≟_ )
|
|
|
6 open import Level renaming ( suc to succ ; zero to Zero )
|
|
|
7 open import Relation.Nullary using (¬_; Dec; yes; no)
|
|
|
8 open import Relation.Binary.PropositionalEquality
|
|
|
9
|
|
|
10
|
|
|
11 record _/\_ {n : Level } (a : Set n) (b : Set n): Set n where
|
|
|
12 field
|
|
|
13 pi1 : a
|
|
|
14 pi2 : b
|
|
|
15
|
|
|
16 open _/\_
|
|
|
17
|
|
|
18 _-_ : ℕ → ℕ → ℕ
|
|
|
19 x - zero = x
|
|
|
20 zero - _ = zero
|
|
|
21 (suc x) - (suc y) = x - y
|
|
|
22
|
|
|
23 +zero : { y : ℕ } → y + zero ≡ y
|
|
|
24 +zero {zero} = refl
|
|
|
25 +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
|
|
|
26
|
|
|
27
|
|
|
28 +-sym : { x y : ℕ } → x + y ≡ y + x
|
|
|
29 +-sym {zero} {zero} = refl
|
|
|
30 +-sym {zero} {suc y} = let open ≡-Reasoning in
|
|
|
31 begin
|
|
|
32 zero + suc y
|
|
|
33 ≡⟨⟩
|
|
|
34 suc y
|
|
|
35 ≡⟨ sym +zero ⟩
|
|
|
36 suc y + zero
|
|
|
37 ∎
|
|
|
38 +-sym {suc x} {zero} = let open ≡-Reasoning in
|
|
|
39 begin
|
|
|
40 suc x + zero
|
|
|
41 ≡⟨ +zero ⟩
|
|
|
42 suc x
|
|
|
43 ≡⟨⟩
|
|
|
44 zero + suc x
|
|
|
45 ∎
|
|
|
46 +-sym {suc x} {suc y} = cong ( λ z → suc z ) ( let open ≡-Reasoning in
|
|
|
47 begin
|
|
|
48 x + suc y
|
|
|
49 ≡⟨ +-sym {x} {suc y} ⟩
|
|
|
50 suc (y + x)
|
|
|
51 ≡⟨ cong ( λ z → suc z ) (+-sym {y} {x}) ⟩
|
|
|
52 suc (x + y)
|
|
|
53 ≡⟨ sym ( +-sym {y} {suc x}) ⟩
|
|
|
54 y + suc x
|
|
|
55 ∎ )
|
|
|
56
|
|
|
57 minus-plus : { x y : ℕ } → (suc x - 1) + (y + 1) ≡ suc x + y
|
|
|
58 minus-plus {zero} {y} = +-sym {y} {1}
|
|
|
59 minus-plus {suc x} {y} = cong ( λ z → suc z ) (minus-plus {x} {y})
|
|
|
60
|
|
|
61 +1≡suc : { x : ℕ } → x + 1 ≡ suc x
|
|
|
62 +1≡suc {zero} = refl
|
|
|
63 +1≡suc {suc x} = cong ( λ z → suc z ) ( +1≡suc {x} )
|
|
|
64
|
|
|
65 lt : ℕ → ℕ → Bool
|
|
|
66 lt x y with (suc x ) ≤? y
|
|
|
67 lt x y | yes p = true
|
|
|
68 lt x y | no ¬p = false
|
|
|
69
|
|
|
70 predℕ : {n : ℕ } → lt 0 n ≡ true → ℕ
|
|
|
71 predℕ {zero} ()
|
|
|
72 predℕ {suc n} refl = n
|
|
|
73
|
|
|
74 predℕ+1=n : {n : ℕ } → (less : lt 0 n ≡ true ) → (predℕ less) + 1 ≡ n
|
|
|
75 predℕ+1=n {zero} ()
|
|
|
76 predℕ+1=n {suc n} refl = +1≡suc
|
|
|
77
|
|
|
78 suc-predℕ=n : {n : ℕ } → (less : lt 0 n ≡ true ) → suc (predℕ less) ≡ n
|
|
|
79 suc-predℕ=n {zero} ()
|
|
|
80 suc-predℕ=n {suc n} refl = refl
|
|
|
81
|
|
|
82 Equal : ℕ → ℕ → Bool
|
|
|
83 Equal x y with x ≟ y
|
|
|
84 Equal x y | yes p = true
|
|
|
85 Equal x y | no ¬p = false
|
|
|
86
|
|
|
87 _⇒_ : Bool → Bool → Bool
|
|
|
88 false ⇒ _ = true
|
|
|
89 true ⇒ true = true
|
|
|
90 true ⇒ false = false
|
|
|
91
|
|
|
92 ⇒t : {x : Bool} → x ⇒ true ≡ true
|
|
|
93 ⇒t {x} with x
|
|
|
94 ⇒t {x} | false = refl
|
|
|
95 ⇒t {x} | true = refl
|
|
|
96
|
|
|
97 f⇒ : {x : Bool} → false ⇒ x ≡ true
|
|
|
98 f⇒ {x} with x
|
|
|
99 f⇒ {x} | false = refl
|
|
|
100 f⇒ {x} | true = refl
|
|
|
101
|
|
|
102 ∧-pi1 : { x y : Bool } → x ∧ y ≡ true → x ≡ true
|
|
|
103 ∧-pi1 {x} {y} eq with x | y | eq
|
|
|
104 ∧-pi1 {x} {y} eq | false | b | ()
|
|
|
105 ∧-pi1 {x} {y} eq | true | false | ()
|
|
|
106 ∧-pi1 {x} {y} eq | true | true | refl = refl
|
|
|
107
|
|
|
108 ∧-pi2 : { x y : Bool } → x ∧ y ≡ true → y ≡ true
|
|
|
109 ∧-pi2 {x} {y} eq with x | y | eq
|
|
|
110 ∧-pi2 {x} {y} eq | false | b | ()
|
|
|
111 ∧-pi2 {x} {y} eq | true | false | ()
|
|
|
112 ∧-pi2 {x} {y} eq | true | true | refl = refl
|
|
|
113
|
|
|
114 ∧true : { x : Bool } → x ∧ true ≡ x
|
|
|
115 ∧true {x} with x
|
|
|
116 ∧true {x} | false = refl
|
|
|
117 ∧true {x} | true = refl
|
|
|
118
|
|
|
119 true∧ : { x : Bool } → true ∧ x ≡ x
|
|
|
120 true∧ {x} with x
|
|
|
121 true∧ {x} | false = refl
|
|
|
122 true∧ {x} | true = refl
|
|
|
123 bool-case : ( x : Bool ) { p : Set } → ( x ≡ true → p ) → ( x ≡ false → p ) → p
|
|
|
124 bool-case x T F with x
|
|
|
125 bool-case x T F | false = F refl
|
|
|
126 bool-case x T F | true = T refl
|
|
|
127
|
|
|
128 impl⇒ : {x y : Bool} → (x ≡ true → y ≡ true ) → x ⇒ y ≡ true
|
|
|
129 impl⇒ {x} {y} p = bool-case x (λ x=t → let open ≡-Reasoning in
|
|
|
130 begin
|
|
|
131 x ⇒ y
|
|
|
132 ≡⟨ cong ( λ z → x ⇒ z ) (p x=t ) ⟩
|
|
|
133 x ⇒ true
|
|
|
134 ≡⟨ ⇒t ⟩
|
|
|
135 true
|
|
|
136 ∎
|
|
|
137 ) ( λ x=f → let open ≡-Reasoning in
|
|
|
138 begin
|
|
|
139 x ⇒ y
|
|
|
140 ≡⟨ cong ( λ z → z ⇒ y ) x=f ⟩
|
|
|
141 true
|
|
|
142 ∎
|
|
|
143 )
|
|
|
144
|
|
|
145 Equal→≡ : { x y : ℕ } → Equal x y ≡ true → x ≡ y
|
|
|
146 Equal→≡ {x} {y} eq with x ≟ y
|
|
|
147 Equal→≡ {x} {y} refl | yes refl = refl
|
|
|
148 Equal→≡ {x} {y} () | no ¬p
|
|
|
149
|
|
|
150 Equal+1 : { x y : ℕ } → Equal x y ≡ Equal (suc x) (suc y)
|
|
|
151 Equal+1 {x} {y} with x ≟ y
|
|
|
152 Equal+1 {x} {.x} | yes refl = refl
|
|
|
153 Equal+1 {x} {y} | no ¬p = refl
|
|
|
154
|
