Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestGears.agda @ 30:dd66b94bf365

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
loop causes agda inifinite loop
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 10 Dec 2019 08:57:11 +0900
parents 816b44e5e674
children 600b4e914071
comparison
equal deleted inserted replaced
29:816b44e5e674 30:dd66b94bf365
92 92
93 93
94 proofGears : {c10 : ℕ } → Set 94 proofGears : {c10 : ℕ } → Set
95 proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) 95 proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 ))))
96 96
97 proofGearsMeta : {c10 : ℕ } → whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) 97 -- proofGearsMeta : {c10 : ℕ } → whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 ))))
98 proofGearsMeta {c10} = {!!} 98 -- proofGearsMeta {c10} = {!!}
99 99
100 data whileTestState : Set where 100 data whileTestState (c10 : ℕ ) : Set where
101 101 error : whileTestState c10
102 state1 : whileTestState 102 state1 : (env : Env) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → whileTestState c10
103 state2 : whileTestState 103 state2 : (env : Env) → (varn env + vari env ≡ c10) → whileTestState c10
104 finstate : whileTestState 104 finstate : (env : Env) → ((vari env) ≡ c10 ) → whileTestState c10
105 105
106 record whileTestCondition (c10 : ℕ) (t : whileTestState) : Set where 106 whileLoopProof0 : {c10 : ℕ } → Set
107 coinductive 107 whileLoopProof0 {c10 } = Env /\ whileTestState c10 → whileLoop {!!} ( λ env → vari env ≡ c10 )
108 field 108 whileTestProof0 : {c10 : ℕ } → Set
109 fincase : (env : Env) → (t ≡ finstate) → (vari env ≡ c10) 109 whileTestProof0 {c10} = Env /\ whileTestState c10 → whileTest c10 (λ env → {!!} )
110 case1 : (env : Env) → (t ≡ state1) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → whileTestCondition c10 state2
111 case2 : (env : Env) → (t ≡ state2) → (varn env + vari env ≡ c10) → whileTestCondition c10 state2
112 110
113 open whileTestCondition 111 proofGearsState : {c10 : ℕ } → whileTestProof0
112 proofGearsState {c10} = {!!} where
113 lemma1 : (env : Env ) → vari env ≡ c10
114 lemma1 = {!!}
114 115
115 test2 : (c10 : ℕ) → whileTestCondition c10 state1 → whileTestCondition c10 state2 116 record Context : Set where
116 test2 c10 cond1 = whileTest 10 (λ env → whileLoop env (λ env1 → {!!})) 117 field
117 where 118 c10 : ℕ
118 whileLoopCond : (e env1 : Env) → varn env1 + vari env1 ≡ c10 → varn e + vari e ≡ c10 → whileTestCondition c10 state2 119 whileDG : Env
119 whileLoopCond = {!!} 120 whileCond : whileTestState c10
120 proof3 : (env env1 : Env) → whileTestCondition c10 finstate
121 fincase (proof3 env env1) = {!!}
122 case1 (proof3 env env1 ) e ()
123 case2 (proof3 env env1 ) e ()
124 121
125 -- conversion1 e {c10} (case2 (case1 cond1 ? ? ?)) {!!} 122 open Context
123
124 whileTestContext : {l : Level} {t : Set l} -> Context → (Code : Context -> t) -> t
125 whileTestContext cxt next = next (record cxt { whileDG = record (whileDG cxt) {varn = c10 cxt ; vari = 0}} )
126
127 {-# TERMINATING #-}
128 whileLoopContext : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) -> t
129 whileLoopContext cxt next with lt 0 (varn (whileDG cxt) )
130 whileLoopContext cxt next | false = next cxt
131 whileLoopContext cxt next | true =
132 whileLoopContext (record cxt { whileDG = record {varn = (varn (whileDG cxt)) - 1 ; vari = (vari (whileDG cxt)) + 1} } ) next
133
134 {-# TERMINATING #-}
135 whileLoopStep : {l : Level} {t : Set l} -> Env -> (Code : Env -> t) (Code : Env -> t) -> t
136 whileLoopStep env next exit with lt 0 (varn env)
137 whileLoopStep env next exit | false = exit env
138 whileLoopStep env next exit | true =
139 next (record {varn = (varn env) - 1 ; vari = (vari env) + 1})
140
141 whileTestProof : {l : Level} {t : Set l} -> Context → (Code : Context -> t) -> t
142 whileTestProof cxt next = next record cxt { whileDG = out ; whileCond = init } where
143 out : Env
144 out = whileTest (c10 cxt) ( λ e → e )
145 init : whileTestState (c10 cxt)
146 init = state1 out record { pi1 = refl ; pi2 = refl }
147
148 {-# TERMINATING #-}
149 whileLoopProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) (Code : Context -> t) -> t
150 whileLoopProof cxt next exit = next record cxt { whileDG = out ; whileCond = postCond } where
151 out : Env
152 out = whileLoopStep (whileDG cxt) ( λ e → e ) {!!}
153 postCond : whileTestState (c10 cxt)
154 postCond with whileCond cxt
155 ... | state2 e inv = state2 out {!!} where
156 proof3 : {!!}
157 proof3 = {!!}
158 ... | _ = error
159
160 whileConvProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) -> t
161 whileConvProof cxt next = next record cxt { whileCond = postCond } where
162 postCond : whileTestState (c10 cxt)
163 postCond with whileCond cxt
164 ... | state1 e inv = state2 (whileDG cxt) {!!}
165 ... | _ = error
166
167 whileFinConvProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) -> t
168 whileFinConvProof cxt next = next record cxt { whileCond = postCond } where
169 postCond : whileTestState (c10 cxt)
170 postCond with whileCond cxt
171 ... | state2 e inv = finstate (whileDG cxt) {!!}
172 ... | _ = error
173
174 {-# TERMINATING #-}
175 loop : {l : Level} {t : Set l} -> Context -> (exit : Context -> t) -> t
176 loop cxt exit = whileLoopProof cxt (λ cxt → loop cxt exit) exit
177
178 proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error })
179 $ λ cxt → whileConvProof cxt
180 $ λ cxt → loop cxt
181 $ λ cxt → whileFinConvProof cxt
182 $ λ cxt → vari (whileDG cxt) ≡ c10 cxt
183 proofWhileGear cxt = refl
184