Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestGears.agda @ 53:03235251b3a7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
discrete state
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 20 Dec 2019 15:57:17 +0900
parents 0bde332e1215
children 3adf50622101
comparison
equal deleted inserted replaced
52:0bde332e1215 53:03235251b3a7
103 -- 103 --
104 104
105 open import Relation.Nullary 105 open import Relation.Nullary
106 open import Relation.Binary 106 open import Relation.Binary
107 107
108 whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t 108 record Envc : Set (succ Zero) where
109 whileTestP c10 next = next (record {varn = c10 ; vari = 0 } ) 109 field
110 c10 : ℕ
111 varn : ℕ
112 vari : ℕ
113 open Envc
110 114
111 whileLoopP : {l : Level} {t : Set l} → Env → (next : Env → t) → (exit : Env → t) → t 115 whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Envc → t) → t
116 whileTestP c10 next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } )
117
118 whileLoopP : {l : Level} {t : Set l} → Envc → (next : Envc → t) → (exit : Envc → t) → t
112 whileLoopP env next exit with <-cmp 0 (varn env) 119 whileLoopP env next exit with <-cmp 0 (varn env)
113 whileLoopP env next exit | tri≈ ¬a b ¬c = exit env 120 whileLoopP env next exit | tri≈ ¬a b ¬c = exit env
114 whileLoopP env next exit | tri< a ¬b ¬c = 121 whileLoopP env next exit | tri< a ¬b ¬c =
115 next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) 122 next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 })
116 123
117 {-# TERMINATING #-} 124 {-# TERMINATING #-}
118 loopP : {l : Level} {t : Set l} → Env → (exit : Env → t) → t 125 loopP : {l : Level} {t : Set l} → Envc → (exit : Envc → t) → t
119 loopP env exit = whileLoopP env (λ env → loopP env exit ) exit 126 loopP env exit = whileLoopP env (λ env → loopP env exit ) exit
120 127
121 whileTestPCall : {c10 : ℕ } → Set 128 whileTestPCall : (c10 : ℕ ) → Envc
122 whileTestPCall {c10} = whileTestP {_} {_} c10 (λ env → loopP env (λ env → ( vari env ≡ c10 ))) 129 whileTestPCall c10 = whileTestP {_} {_} c10 (λ env → loopP env (λ env → env))
123 130
124 data whileTestStateP (c10 i n : ℕ ) : Set where 131 data whileTestState : Set where
125 pstate1 : (i ≡ 0) /\ (n ≡ c10) → whileTestStateP c10 i n -- n ≡ c10 132 s1 : whileTestState
126 pstate2 : (0 ≤ n) → (n ≤ c10) → (n + i ≡ c10) → whileTestStateP c10 i n -- 0 < n < c10 133 s2 : whileTestState
127 pfinstate : (n ≡ 0 ) → (i ≡ c10 ) → whileTestStateP c10 i n -- n ≡ 0 134 sf : whileTestState
128 135
129 record EnvP : Set (succ Zero) where 136 whileTestStateP : whileTestState → Envc → Set
130 field 137 whileTestStateP s1 env = (vari env ≡ 0) /\ (varn env ≡ c10 env)
131 env : Env 138 whileTestStateP s2 env = (varn env + vari env ≡ c10 env)
132 c10 : ℕ 139 whileTestStateP sf env = (vari env ≡ c10 env)
133 cx : whileTestStateP c10 (vari env) (varn env)
134 140
135 open EnvP 141 whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) → ((env : Envc ) → whileTestStateP s1 env → t) → t
142 whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
143 env : Envc
144 env = whileTestP c10 ( λ env → env )
136 145
137 s1 : (c10 : ℕ) → EnvP 146 whileLoopPwP : {l : Level} {t : Set l} → Envc
138 s1 c10 = record {env = record {vari = 0 ; varn = c10} ; c10 = c10 ; cx = pstate1 (record {pi1 = refl ; pi2 = refl})} 147 → (next : (env : Envc ) → whileTestStateP s2 env → t)
148 → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
149 whileLoopPwP env next exit with <-cmp 0 (varn env)
150 whileLoopPwP env next exit | tri≈ ¬a b ¬c = exit env {!!}
151 whileLoopPwP env next exit | tri< a ¬b ¬c =
152 next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) {!!}
139 153
140 s2 : (e : EnvP) → varn (env e) > 0 → varn (env e) < c10 e → EnvP 154 {-# TERMINATING #-}
141 s2 e n>0 n<c10 with <-cmp 0 (varn (env e)) 155 loopPwP : {l : Level} {t : Set l} → Envc → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
142 s2 e n>0 n<c10 | tri< a ¬b ¬c = 156 loopPwP env exit = whileLoopPwP env (λ env s → loopPwP env exit ) exit
143 record e { env = record { varn = varn (env e) - 1 ; vari = vari (env e) + 1 } ; cx = pstate2 {!!} {!!} {!!} } where
144 s2-1 : 0 ≤ (varn (env e) - 1)
145 s2-1 = {!!}
146 s2 e n>0 n<c10 | tri≈ ¬a b ¬c = record { env = record { varn = varn (env e) - 1 ; vari = vari (env e) + 1 } ; c10 = c10 e ; cx = pfinstate {!!} {!!} }
147 157
148 s3 : (e : EnvP) → varn (env e) ≡ 0 → vari (env e) ≡ c10 e 158 whileTestPCallwP : (c10 : ℕ ) → Set
149 s3 record { env = record { varn = .0 ; vari = vari₁ } ; c10 = c11 ; cx = cx₁ } refl = {!!} 159 whileTestPCallwP c10 = whileTestPwP {_} {_} c10 (λ env → loopPwP env (λ env x x1 → vari env ≡ c10 ))
150
151 s1ors2 : (e : EnvP) → EnvP
152 s1ors2 e = {!!}
153
154 proofs : (c : ℕ) → (λ e → vari (env e) ≡ c10 e ) (s2 {!!} {!!} {!!})
155 proofs c = {!!} -- s3 (s2 ({!!}) {!!} {!!}) {!!}
156
157 s3' : (e : EnvP) → varn (env e) ≡ 0 → (ℕ → EnvP → vari (env e) ≡ c10 e) → vari (env e) ≡ c10 e
158 s3' record { env = record { varn = .0 ; vari = vari₁ } ; c10 = c11 ; cx = cx₁ } refl proof = {!!}
159 160
160 161
161 162
162 whileTestPwithProof : {l : Level} {t : Set l} → (c10 : ℕ ) → (next : (e : EnvP ) → t) → t
163 whileTestPwithProof {l} {t} c10 next = next record { env = env1 ; c10 = c10 ; cx = cx1 } where
164 env1 : Env
165 env1 = whileTestP c10 ( λ e → e )
166 cx1 : whileTestStateP c10 (vari env1) (varn env1)
167 cx1 = pstate1 record { pi1 = refl ; pi2 = refl }
168
169 {-# TERMINATING #-}
170 loopPwithProof : {l : Level} {t : Set l} → (e : EnvP ) → (exit : (e : EnvP ) → t ) → t
171 loopPwithProof e exit with <-cmp 0 (varn (env e)) | whileLoopP (env e) (λ e1 → pstate2 {!!} {!!} {!!} ) ( λ env → pfinstate {!!} {!!} )
172 loopPwithProof e exit | tri≈ ¬a b ¬c | tt = loopPwithProof {!!} {!!}
173 loopPwithProof e exit | tri< a ¬b ¬c | tt = exit {!!}
174
175 ConvP : (e : EnvP) → EnvP
176 ConvP = {!!}
177
178 whileTestPProof : {c : ℕ } → Set
179 whileTestPProof {c} = whileTestPwithProof c
180 $ λ e → loopPwithProof e (λ e eq → vari (env e) ≡ c10 e ) (ConvP e )
181
182 whileTestPProofMeta : {c10 : ℕ } → whileTestPProof {c10}
183 whileTestPProofMeta {c10} = {!!}
184 163
185 164
165
166
167