Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestGears.agda @ 44:5a3c9d087c7c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dead end
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 15 Dec 2019 15:57:07 +0900
parents 8813f26da3b7
children
comparison
equal deleted inserted replaced
42:8813f26da3b7 44:5a3c9d087c7c
8 open import Relation.Binary.PropositionalEquality 8 open import Relation.Binary.PropositionalEquality
9 9
10 open import utilities 10 open import utilities
11 open _/\_ 11 open _/\_
12 12
13 record Env : Set (succ Zero) where 13 record Env (Cxt : Set) : Set (succ Zero) where
14 field 14 field
15 varn : ℕ 15 varn : ℕ
16 vari : ℕ 16 vari : ℕ
17 cx : Set 17 cx : Cxt
18 open Env 18 open Env
19 19
20 whileTest : {l : Level} {t : Set l} (c : Set ) → (c10 : ℕ) → (Code : Env → t) → t 20 whileTest : {l : Level} {t : Set l} {Cxt : Set} (c : Cxt ) → (c10 : ℕ) → (Code : Env Cxt → t) → t
21 whileTest c c10 next = next (record {varn = c10 ; vari = 0 ; cx = c} ) 21 whileTest c c10 next = next (record {varn = c10 ; vari = 0 ; cx = c } )
22 22
23 {-# TERMINATING #-} 23 {-# TERMINATING #-}
24 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t 24 whileLoop : {l : Level} {t : Set l} {Cxt : Set} {c : Cxt } → Env Cxt → (Code : Env Cxt → t) → t
25 whileLoop env next with lt 0 (varn env) 25 whileLoop env next with lt 0 (varn env)
26 whileLoop env next | false = next env 26 whileLoop env next | false = next env
27 whileLoop env next | true = 27 whileLoop env next | true =
28 whileLoop (record env {varn = (varn env) - 1 ; vari = (vari env) + 1}) next 28 whileLoop (record env {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
29 29
30 test1 : (c : Set ) → Env 30 test1 : {Cxt : Set } → (c : Cxt) → Env Cxt
31 test1 c = whileTest c 10 (λ env → whileLoop env (λ env1 → env1 )) 31 test1 c = whileTest c 10 (λ env → whileLoop env (λ env1 → env1 ))
32 32
33 33
34 proof1 : (c : Set ) → whileTest c 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 )) 34 proof1 : {Cxt : Set } (c : Cxt ) → whileTest c 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
35 proof1 c = refl 35 proof1 c = refl
36 36
37 -- ↓PostCondition 37 -- ↓PostCondition
38 whileTest' : {l : Level} {t : Set l} → {c : Set} → {c10 : ℕ } → (Code : (env : Env ) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t 38 whileTest' : {l : Level} {t : Set l} {Cxt : Set} → {c : Cxt} → {c10 : ℕ } → (Code : (env : Env Cxt ) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
39 whileTest' {_} {_} {c} {c10} next = next env proof2 39 whileTest' {_} {_} {Cxt} {c} {c10} next = next env proof2
40 where 40 where
41 env : Env 41 env : Env Cxt
42 env = record {vari = 0 ; varn = c10 ; cx = c } 42 env = record {vari = 0 ; varn = c10 ; cx = c }
43 proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition 43 proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition
44 proof2 = record {pi1 = refl ; pi2 = refl} 44 proof2 = record {pi1 = refl ; pi2 = refl}
45 45
46 open import Data.Empty 46 open import Data.Empty
47 open import Data.Nat.Properties 47 open import Data.Nat.Properties
48 48
49 49
50 {-# TERMINATING #-} -- ↓PreCondition(Invaliant) 50 {-# TERMINATING #-} -- ↓PreCondition(Invaliant)
51 whileLoop' : {l : Level} {t : Set l} → (env : Env ) → {c10 : ℕ } → ((varn env) + (vari env) ≡ c10) → (Code : Env → t) → t 51 whileLoop' : {l : Level} {t : Set l} {Cxt : Set} {c : Cxt } → (env : Env Cxt ) → {c10 : ℕ } → ((varn env) + (vari env) ≡ c10) → (Code : Env Cxt → t) → t
52 whileLoop' env proof next with ( suc zero ≤? (varn env) ) 52 whileLoop' env proof next with ( suc zero ≤? (varn env) )
53 whileLoop' env proof next | no p = next env 53 whileLoop' env proof next | no p = next env
54 whileLoop' env {c10} proof next | yes p = whileLoop' env1 (proof3 p ) next 54 whileLoop' env {c10} proof next | yes p = whileLoop' env1 (proof3 p ) next
55 where 55 where
56 env1 = record env {varn = (varn env) - 1 ; vari = (vari env) + 1} 56 env1 = record env {varn = (varn env) - 1 ; vari = (vari env) + 1}
74 -- ≡⟨ proof ⟩ 74 -- ≡⟨ proof ⟩
75 -- c10 75 -- c10
76 -- ∎ 76 -- ∎
77 77
78 -- Condition to Invaliant 78 -- Condition to Invaliant
79 conversion1 : {l : Level} {t : Set l } → (env : Env ) → {c10 : ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) 79 conversion1 : {l : Level} {t : Set l } {Cxt : Set} {c : Cxt } → (env : Env Cxt ) → {c10 : ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
80 → (Code : (env1 : Env ) → (varn env1 + vari env1 ≡ c10) → t) → t 80 → (Code : (env1 : Env Cxt ) → (varn env1 + vari env1 ≡ c10) → t) → t
81 conversion1 env {c10} p1 next = next env proof4 81 conversion1 env {c10} p1 next = next env proof4
82 where 82 where
83 proof4 : varn env + vari env ≡ c10 83 proof4 : varn env + vari env ≡ c10
84 proof4 = let open ≡-Reasoning in 84 proof4 = let open ≡-Reasoning in
85 begin 85 begin
91 ≡⟨ +-sym {c10} {0} ⟩ 91 ≡⟨ +-sym {c10} {0} ⟩
92 c10 92 c10
93 ∎ 93 ∎
94 94
95 95
96 proofGears : {c10 : ℕ } → Set → Set 96 proofGears : {c10 : ℕ } → { Cxt : Set } → (c : Cxt ) → Set
97 proofGears {c10} c = whileTest' {_} {_} {c} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) 97 proofGears {c10} c = whileTest' {_} {_} {_} {c} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 ))))
98 98
99 data whileTestState (c10 : ℕ ) (env : Env ) : Set where 99 record Context (e : Set ) : Set (succ Zero)
100
101 data whileTestState {Cxt : Set } (c10 : ℕ ) (env : Env Cxt ) : Set where
100 error : whileTestState c10 env 102 error : whileTestState c10 env
101 state1 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → whileTestState c10 env 103 state1 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → whileTestState c10 env
102 state2 : (varn env + vari env ≡ c10) → whileTestState c10 env 104 state2 : (varn env + vari env ≡ c10) → whileTestState c10 env
103 finstate : ((vari env) ≡ c10 ) → whileTestState c10 env 105 finstate : ((vari env) ≡ c10 ) → whileTestState c10 env
104 106
105 -- 107 --
106 -- openended Env c <=> Context 108 -- openended Env Cxt c <=> Context
107 -- 109 --
108 110
109 record Context : Set (succ Zero) where 111 record Context e where
110 field 112 field
111 c10 : ℕ 113 c10 : ℕ
112 whileDG : Env 114 whileDG : Env e
113 whileCond : whileTestState c10 whileDG 115 whileCond : whileTestState c10 whileDG
114 116
115 open Context 117 open Context
116 118
117 open import Relation.Nullary 119 open import Relation.Nullary
119 121
120 -- 122 --
121 -- transparency of condition 123 -- transparency of condition
122 -- 124 --
123 125
124 whileCondP : Env → Set 126 whileCondP : Env {!!} → Set
125 whileCondP env = varn env > 0 127 whileCondP env = varn env > 0
126 128
127 whileDec : (cxt : Context) → Dec (whileCondP (whileDG cxt)) 129 whileDec : (cxt : Context) → Dec (whileCondP (whileDG cxt))
128 whileDec cxt = {!!} 130 whileDec cxt = {!!}
129 131
139 where 141 where
140 proof : (cxt : Context) → (varn (whileDG cxt) - 1) + (vari (whileDG cxt) + 1) ≡ c10 cxt 142 proof : (cxt : Context) → (varn (whileDG cxt) - 1) + (vari (whileDG cxt) + 1) ≡ c10 cxt
141 proof cxt = {!!} 143 proof cxt = {!!}
142 144
143 {-# TERMINATING #-} 145 {-# TERMINATING #-}
144 whileLoopStep : {l : Level} {t : Set l} → Env → (next : (e : Env ) → t) (exit : (e : Env) → t) → t 146 whileLoopStep : {l : Level} {t : Set l} → Env {!!} → (next : (e : Env {!!} ) → t) (exit : (e : Env {!!} ) → t) → t
145 whileLoopStep env next exit with <-cmp 0 (varn env) 147 whileLoopStep env next exit with <-cmp 0 (varn env)
146 whileLoopStep env next exit | tri≈ _ eq _ = exit env 148 whileLoopStep env next exit | tri≈ _ eq _ = exit env
147 whileLoopStep env next exit | tri< gt ¬eq _ = next record env {varn = (varn env) - 1 ; vari = (vari env) + 1} 149 whileLoopStep env next exit | tri< gt ¬eq _ = next record env {varn = (varn env) - 1 ; vari = (vari env) + 1}
148 whileLoopStep env next exit | tri> _ _ c = ⊥-elim (m<n⇒n≢0 {varn env} {0} c refl) 150 whileLoopStep env next exit | tri> _ _ c = ⊥-elim (m<n⇒n≢0 {varn env} {0} c refl)
149 151
150 whileTestProof : {l : Level} {t : Set l} → Context → (Code : (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt) ) → t) → t 152 whileTestProof : {l : Level} {t : Set l} → Context → (Code : (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt) ) → t) → t
151 whileTestProof cxt next = next record cxt { whileDG = out ; whileCond = init } i!=n where 153 whileTestProof cxt next = next record cxt { whileDG = out ; whileCond = init } i!=n where
152 out : Env 154 out : Env {!!}
153 out = whileTest {!!} (c10 cxt) ( λ e → e ) 155 out = whileTest {!!} (c10 cxt) ( λ e → e )
154 init : whileTestState (c10 cxt) out 156 init : whileTestState (c10 cxt) out
155 init = state1 record { pi1 = refl ; pi2 = refl } 157 init = state1 record { pi1 = refl ; pi2 = refl }
156 i!=n : ¬ vari out ≡ varn out 158 i!=n : ¬ vari out ≡ varn out
157 i!=n eq = {!!} 159 i!=n eq = {!!}
160 whileLoopProof : {l : Level} {t : Set l} → (cxt : Context ) → whileCondP (whileDG cxt) 162 whileLoopProof : {l : Level} {t : Set l} → (cxt : Context ) → whileCondP (whileDG cxt)
161 → (continue : (cxt : Context ) → whileCondP (whileDG cxt) → t) (exit : Context → ¬ whileCondP (whileDG cxt) → t) → t 163 → (continue : (cxt : Context ) → whileCondP (whileDG cxt) → t) (exit : Context → ¬ whileCondP (whileDG cxt) → t) → t
162 whileLoopProof cxt i!=n next exit = whileLoopStep (whileDG cxt) 164 whileLoopProof cxt i!=n next exit = whileLoopStep (whileDG cxt)
163 ( λ env → next record cxt { whileDG = env ; whileCond = {!!} } {!!} ) 165 ( λ env → next record cxt { whileDG = env ; whileCond = {!!} } {!!} )
164 ( λ env → exit record cxt { whileDG = env ; whileCond = exitCond env {!!} } {!!} ) where 166 ( λ env → exit record cxt { whileDG = env ; whileCond = exitCond env {!!} } {!!} ) where
165 proof5 : (e : Env ) → varn e + vari e ≡ c10 cxt → 0 ≡ varn e → vari e ≡ c10 cxt 167 proof5 : (e : Env {!!} ) → varn e + vari e ≡ c10 cxt → 0 ≡ varn e → vari e ≡ c10 cxt
166 proof5 record { varn = .0 ; vari = vari } refl refl = refl 168 proof5 record { varn = .0 ; vari = vari } refl refl = refl
167 exitCond : (e : Env ) → 0 ≡ varn e → whileTestState (c10 cxt) e 169 exitCond : (e : Env {!!} ) → 0 ≡ varn e → whileTestState (c10 cxt) e
168 exitCond nenv eq1 with whileCond cxt | inspect whileDG cxt 170 exitCond nenv eq1 with whileCond cxt | inspect whileDG cxt
169 ... | state2 cond | record { eq = eq2 } = finstate ( proof5 nenv {!!} eq1 ) 171 ... | state2 cond | record { eq = eq2 } = finstate ( proof5 nenv {!!} eq1 )
170 ... | _ | _ = error 172 ... | _ | _ = error
171 173
172 whileConvProof : {l : Level} {t : Set l} → (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt)) 174 whileConvProof : {l : Level} {t : Set l} → (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt))
173 → ((cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt)) → t) → t 175 → ((cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt)) → t) → t
174 whileConvProof cxt i!=n next = next record cxt { whileCond = postCond } i!=n where 176 whileConvProof cxt i!=n next = next record cxt { whileCond = postCond } i!=n where
175 proof4 : (e : Env ) → (vari e ≡ 0) /\ (varn e ≡ c10 cxt) → varn e + vari e ≡ c10 cxt 177 proof4 : (e : Env {!!} ) → (vari e ≡ 0) /\ (varn e ≡ c10 cxt) → varn e + vari e ≡ c10 cxt
176 proof4 env p1 = let open ≡-Reasoning in 178 proof4 env p1 = let open ≡-Reasoning in
177 begin 179 begin
178 varn env + vari env 180 varn env + vari env
179 ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩ 181 ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
180 c10 cxt + vari env 182 c10 cxt + vari env