Mercurial > hg > Members > ryokka > HoareLogic
annotate utilities.agda @ 60:ad83c2d5e869
agda2 can't stop case
| author | ryokka |
|---|---|
| date | Sat, 21 Dec 2019 18:28:46 +0900 |
| parents | a39a82820742 |
| children | 52d957db0222 |
| rev | line source |
|---|---|
| 27 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
| 12 | 2 module utilities where |
| 3 | |
| 4 open import Function | |
| 5 open import Data.Nat | |
| 21 | 6 open import Data.Product |
| 27 | 7 open import Data.Bool hiding ( _≟_ ; _≤?_) |
| 12 | 8 open import Level renaming ( suc to succ ; zero to Zero ) |
| 9 open import Relation.Nullary using (¬_; Dec; yes; no) | |
| 10 open import Relation.Binary.PropositionalEquality | |
| 11 | |
| 21 | 12 Pred : Set -> Set₁ |
| 13 Pred X = X -> Set | |
| 14 | |
| 15 Imply : Set -> Set -> Set | |
| 16 Imply X Y = X -> Y | |
| 17 | |
| 18 Iff : Set -> Set -> Set | |
| 19 Iff X Y = Imply X Y × Imply Y X | |
| 12 | 20 |
| 21 record _/\_ {n : Level } (a : Set n) (b : Set n): Set n where | |
| 22 field | |
| 23 pi1 : a | |
| 24 pi2 : b | |
| 25 | |
| 26 open _/\_ | |
| 27 | |
| 28 _-_ : ℕ → ℕ → ℕ | |
| 29 x - zero = x | |
| 30 zero - _ = zero | |
| 31 (suc x) - (suc y) = x - y | |
| 32 | |
| 33 +zero : { y : ℕ } → y + zero ≡ y | |
| 34 +zero {zero} = refl | |
| 35 +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} ) | |
| 36 | |
| 37 | |
| 38 +-sym : { x y : ℕ } → x + y ≡ y + x | |
| 39 +-sym {zero} {zero} = refl | |
| 40 +-sym {zero} {suc y} = let open ≡-Reasoning in | |
| 41 begin | |
| 42 zero + suc y | |
| 43 ≡⟨⟩ | |
| 44 suc y | |
| 45 ≡⟨ sym +zero ⟩ | |
| 46 suc y + zero | |
| 47 ∎ | |
| 48 +-sym {suc x} {zero} = let open ≡-Reasoning in | |
| 49 begin | |
| 50 suc x + zero | |
| 51 ≡⟨ +zero ⟩ | |
| 52 suc x | |
| 53 ≡⟨⟩ | |
| 54 zero + suc x | |
| 55 ∎ | |
| 56 +-sym {suc x} {suc y} = cong ( λ z → suc z ) ( let open ≡-Reasoning in | |
| 57 begin | |
| 58 x + suc y | |
| 59 ≡⟨ +-sym {x} {suc y} ⟩ | |
| 60 suc (y + x) | |
| 61 ≡⟨ cong ( λ z → suc z ) (+-sym {y} {x}) ⟩ | |
| 62 suc (x + y) | |
| 63 ≡⟨ sym ( +-sym {y} {suc x}) ⟩ | |
| 64 y + suc x | |
| 65 ∎ ) | |
| 66 | |
| 67 minus-plus : { x y : ℕ } → (suc x - 1) + (y + 1) ≡ suc x + y | |
| 68 minus-plus {zero} {y} = +-sym {y} {1} | |
| 69 minus-plus {suc x} {y} = cong ( λ z → suc z ) (minus-plus {x} {y}) | |
| 70 | |
| 71 +1≡suc : { x : ℕ } → x + 1 ≡ suc x | |
| 72 +1≡suc {zero} = refl | |
| 73 +1≡suc {suc x} = cong ( λ z → suc z ) ( +1≡suc {x} ) | |
| 74 | |
| 75 lt : ℕ → ℕ → Bool | |
| 76 lt x y with (suc x ) ≤? y | |
| 77 lt x y | yes p = true | |
| 78 lt x y | no ¬p = false | |
| 79 | |
| 80 predℕ : {n : ℕ } → lt 0 n ≡ true → ℕ | |
| 81 predℕ {zero} () | |
| 82 predℕ {suc n} refl = n | |
| 83 | |
| 84 predℕ+1=n : {n : ℕ } → (less : lt 0 n ≡ true ) → (predℕ less) + 1 ≡ n | |
| 85 predℕ+1=n {zero} () | |
| 86 predℕ+1=n {suc n} refl = +1≡suc | |
| 87 | |
| 88 suc-predℕ=n : {n : ℕ } → (less : lt 0 n ≡ true ) → suc (predℕ less) ≡ n | |
| 89 suc-predℕ=n {zero} () | |
| 90 suc-predℕ=n {suc n} refl = refl | |
| 91 | |
| 92 Equal : ℕ → ℕ → Bool | |
| 93 Equal x y with x ≟ y | |
| 94 Equal x y | yes p = true | |
| 95 Equal x y | no ¬p = false | |
| 96 | |
| 97 _⇒_ : Bool → Bool → Bool | |
| 98 false ⇒ _ = true | |
| 99 true ⇒ true = true | |
| 100 true ⇒ false = false | |
| 101 | |
| 102 ⇒t : {x : Bool} → x ⇒ true ≡ true | |
| 103 ⇒t {x} with x | |
| 104 ⇒t {x} | false = refl | |
| 105 ⇒t {x} | true = refl | |
| 106 | |
| 107 f⇒ : {x : Bool} → false ⇒ x ≡ true | |
| 108 f⇒ {x} with x | |
| 109 f⇒ {x} | false = refl | |
| 110 f⇒ {x} | true = refl | |
| 111 | |
| 112 ∧-pi1 : { x y : Bool } → x ∧ y ≡ true → x ≡ true | |
| 113 ∧-pi1 {x} {y} eq with x | y | eq | |
| 114 ∧-pi1 {x} {y} eq | false | b | () | |
| 115 ∧-pi1 {x} {y} eq | true | false | () | |
| 116 ∧-pi1 {x} {y} eq | true | true | refl = refl | |
| 117 | |
| 118 ∧-pi2 : { x y : Bool } → x ∧ y ≡ true → y ≡ true | |
| 119 ∧-pi2 {x} {y} eq with x | y | eq | |
| 120 ∧-pi2 {x} {y} eq | false | b | () | |
| 121 ∧-pi2 {x} {y} eq | true | false | () | |
| 122 ∧-pi2 {x} {y} eq | true | true | refl = refl | |
| 123 | |
| 124 ∧true : { x : Bool } → x ∧ true ≡ x | |
| 125 ∧true {x} with x | |
| 126 ∧true {x} | false = refl | |
| 127 ∧true {x} | true = refl | |
| 128 | |
| 129 true∧ : { x : Bool } → true ∧ x ≡ x | |
| 130 true∧ {x} with x | |
| 131 true∧ {x} | false = refl | |
| 132 true∧ {x} | true = refl | |
| 133 bool-case : ( x : Bool ) { p : Set } → ( x ≡ true → p ) → ( x ≡ false → p ) → p | |
| 134 bool-case x T F with x | |
| 135 bool-case x T F | false = F refl | |
| 136 bool-case x T F | true = T refl | |
| 137 | |
| 138 impl⇒ : {x y : Bool} → (x ≡ true → y ≡ true ) → x ⇒ y ≡ true | |
| 139 impl⇒ {x} {y} p = bool-case x (λ x=t → let open ≡-Reasoning in | |
| 140 begin | |
| 141 x ⇒ y | |
| 142 ≡⟨ cong ( λ z → x ⇒ z ) (p x=t ) ⟩ | |
| 143 x ⇒ true | |
| 144 ≡⟨ ⇒t ⟩ | |
| 145 true | |
| 146 ∎ | |
| 147 ) ( λ x=f → let open ≡-Reasoning in | |
| 148 begin | |
| 149 x ⇒ y | |
| 150 ≡⟨ cong ( λ z → z ⇒ y ) x=f ⟩ | |
| 151 true | |
| 152 ∎ | |
| 153 ) | |
| 154 | |
| 155 Equal→≡ : { x y : ℕ } → Equal x y ≡ true → x ≡ y | |
| 156 Equal→≡ {x} {y} eq with x ≟ y | |
| 157 Equal→≡ {x} {y} refl | yes refl = refl | |
| 158 Equal→≡ {x} {y} () | no ¬p | |
| 159 | |
| 160 Equal+1 : { x y : ℕ } → Equal x y ≡ Equal (suc x) (suc y) | |
| 161 Equal+1 {x} {y} with x ≟ y | |
| 27 | 162 Equal+1 {x} {.x} | yes refl = {!!} |
| 163 Equal+1 {x} {y} | no ¬p = {!!} | |
| 12 | 164 |
|
15
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
165 open import Data.Empty |
|
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
166 |
|
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
167 ≡→Equal : { x y : ℕ } → x ≡ y → Equal x y ≡ true |
|
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
168 ≡→Equal {x} {.x} refl with x ≟ x |
|
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
169 ≡→Equal {x} {.x} refl | yes refl = refl |
|
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
170 ≡→Equal {x} {.x} refl | no ¬p = ⊥-elim ( ¬p refl ) |