Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestGears.agda @ 32:bf7c7bd69e35

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
conversion. loop needs cases
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 10 Dec 2019 09:51:12 +0900
parents 600b4e914071
children 7679b9dc4b40
comparison
equal deleted inserted replaced
31:600b4e914071 32:bf7c7bd69e35
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 ))))
98 -- proofGearsMeta {c10} = {!!}
99
100 data whileTestState (c10 : ℕ ) : Set where 97 data whileTestState (c10 : ℕ ) : Set where
101 error : whileTestState c10 98 error : whileTestState c10
102 state1 : (env : Env) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → whileTestState c10 99 state1 : (env : Env) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → whileTestState c10
103 state2 : (env : Env) → (varn env + vari env ≡ c10) → whileTestState c10 100 state2 : (env : Env) → (varn env + vari env ≡ c10) → whileTestState c10
104 finstate : (env : Env) → ((vari env) ≡ c10 ) → whileTestState c10 101 finstate : (env : Env) → ((vari env) ≡ c10 ) → whileTestState c10
105
106 whileLoopProof0 : {c10 : ℕ } → Set
107 whileLoopProof0 {c10 } = Env /\ whileTestState c10 → whileLoop {!!} ( λ env → vari env ≡ c10 )
108 whileTestProof0 : {c10 : ℕ } → Set
109 whileTestProof0 {c10} = Env /\ whileTestState c10 → whileTest c10 (λ env → {!!} )
110
111 proofGearsState : {c10 : ℕ } → whileTestProof0
112 proofGearsState {c10} = {!!} where
113 lemma1 : (env : Env ) → vari env ≡ c10
114 lemma1 = {!!}
115 102
116 record Context : Set where 103 record Context : Set where
117 field 104 field
118 c10 : ℕ 105 c10 : ℕ
119 whileDG : Env 106 whileDG : Env
146 init = state1 out record { pi1 = refl ; pi2 = refl } 133 init = state1 out record { pi1 = refl ; pi2 = refl }
147 134
148 {-# TERMINATING #-} 135 {-# TERMINATING #-}
149 whileLoopProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) (Code : Context -> t) -> t 136 whileLoopProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) (Code : Context -> t) -> t
150 whileLoopProof cxt next exit = whileLoopStep (whileDG cxt) 137 whileLoopProof cxt next exit = whileLoopStep (whileDG cxt)
151 ( λ env → next record cxt { whileDG = env ; whileCond = nextCond env } ) 138 ( λ env → next record cxt { whileDG = env } )
152 ( λ env → exit record cxt { whileDG = env ; whileCond = exitCond env } ) where 139 ( λ env → exit record cxt { whileDG = env ; whileCond = exitCond env } ) where
153 nextCond : Env → whileTestState (c10 cxt)
154 nextCond nenv with whileCond cxt
155 ... | state2 e inv = state2 (whileDG cxt) {!!}
156 ... | _ = error
157 exitCond : Env → whileTestState (c10 cxt) 140 exitCond : Env → whileTestState (c10 cxt)
158 exitCond nenv with whileCond cxt 141 exitCond nenv with whileCond cxt
159 ... | state2 e inv = finstate (whileDG cxt) {!!} 142 ... | state2 e inv = finstate (whileDG cxt) {!!}
160 ... | _ = error 143 ... | _ = error
161 144
162 whileConvProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) -> t 145 whileConvProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) -> t
163 whileConvProof cxt next = next record cxt { whileCond = postCond } where 146 whileConvProof cxt next = next record cxt { whileCond = postCond } where
147 proof4 : (e : Env ) → (vari e ≡ 0) /\ (varn e ≡ c10 cxt) → varn e + vari e ≡ c10 cxt
148 proof4 env p1 = let open ≡-Reasoning in
149 begin
150 varn env + vari env
151 ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
152 c10 cxt + vari env
153 ≡⟨ cong ( λ n → c10 cxt + n ) (pi1 p1 ) ⟩
154 c10 cxt + 0
155 ≡⟨ +-sym {c10 cxt} {0} ⟩
156 c10 cxt
157 ∎
164 postCond : whileTestState (c10 cxt) 158 postCond : whileTestState (c10 cxt)
165 postCond with whileCond cxt 159 postCond with whileCond cxt
166 ... | state1 e inv = state2 (whileDG cxt) {!!} 160 ... | state1 e inv = state2 e (proof4 e inv)
167 ... | _ = error 161 ... | _ = error
168 162
169 {-# TERMINATING #-} 163 {-# TERMINATING #-}
170 loop : {l : Level} {t : Set l} -> Context -> (exit : Context -> t) -> t 164 loop : {l : Level} {t : Set l} -> Context -> (exit : Context -> t) -> t
171 loop cxt exit = whileLoopProof cxt (λ cxt → loop cxt exit ) exit 165 loop cxt exit = whileLoopProof cxt (λ cxt → loop cxt exit ) exit
172 166
173 proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error }) 167 proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error })
174 $ λ cxt → whileConvProof cxt 168 $ λ cxt → whileConvProof cxt
175 $ λ cxt → loop cxt 169 $ λ cxt → loop cxt
176 $ λ cxt → vari (whileDG cxt) ≡ c10 cxt 170 $ λ cxt → vari (whileDG cxt) ≡ c10 cxt
177 proofWhileGear cxt = {!!} 171 proofWhileGear c cxt = {!!}
178 172