Mercurial > hg > Members > ryokka > HoareLogic

comparison utilities.agda @ 12:247ce3e67b5f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add utilitites
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 15 Dec 2018 17:24:35 +0900
parents
children 8d546766a9a8
comparison
equal deleted inserted replaced
11:f34066c435cd 12:247ce3e67b5f
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