Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestGears.agda @ 6:28e80739eed6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix whileTestGears
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 14 Dec 2018 22:06:24 +0900
parents 17e4f3b58148
children e7d6bdb6039d
comparison
equal deleted inserted replaced
5:17e4f3b58148 6:28e80739eed6
6 open import Level renaming ( suc to succ ; zero to Zero ) 6 open import Level renaming ( suc to succ ; zero to Zero )
7 open import Relation.Nullary using (¬_; Dec; yes; no) 7 open import Relation.Nullary using (¬_; Dec; yes; no)
8 open import Relation.Binary.PropositionalEquality 8 open import Relation.Binary.PropositionalEquality
9 9
10 10
11 record Env : Set where 11 record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
12 field 12 field
13 varn : ℕ 13 pi1 : a
14 vari : ℕ 14 pi2 : b
15 open Env 15
16 open _∧_
16 17
17 _-_ : ℕ -> ℕ -> ℕ 18 _-_ : ℕ -> ℕ -> ℕ
18 x - zero = x 19 x - zero = x
19 zero - _ = zero 20 zero - _ = zero
20 (suc x) - (suc y) = x - y 21 (suc x) - (suc y) = x - y
21 22
22 record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where 23 sym1 : { y : ℕ } -> y + zero ≡ y
23 field 24 sym1 {zero} = refl
24 pi1 : a 25 sym1 {suc y} = cong ( λ x → suc x ) ( sym1 {y} )
25 pi2 : b 26
27 +-sym : { x y : ℕ } -> x + y ≡ y + x
28 +-sym {zero} {zero} = refl
29 +-sym {zero} {suc y} = let open ≡-Reasoning in
30 begin
31 zero + suc y
32 ≡⟨⟩
33 suc y
34 ≡⟨ sym sym1 ⟩
35 suc y + zero
36 ∎
37 +-sym {suc x} {zero} = let open ≡-Reasoning in
38 begin
39 suc x + zero
40 ≡⟨ sym1 ⟩
41 suc x
42 ≡⟨⟩
43 zero + suc x
44 ∎
45 +-sym {suc x} {suc y} = cong ( λ z → suc z ) ( let open ≡-Reasoning in
46 begin
47 x + suc y
48 ≡⟨ +-sym {x} {suc y} ⟩
49 suc (y + x)
50 ≡⟨ cong ( λ z → suc z ) (+-sym {y} {x}) ⟩
51 suc (x + y)
52 ≡⟨ sym ( +-sym {y} {suc x}) ⟩
53 y + suc x
54 ∎ )
55
56 minus-plus : { x y : ℕ } -> (suc x - 1) + (y + 1) ≡ suc x + y
57 minus-plus {zero} {y} = +-sym {y} {1}
58 minus-plus {suc x} {y} = cong ( λ z → suc z ) (minus-plus {x} {y})
26 59
27 lt : ℕ -> ℕ -> Bool 60 lt : ℕ -> ℕ -> Bool
28 lt x y with (suc x ) ≤? y 61 lt x y with (suc x ) ≤? y
29 lt x y | yes p = true 62 lt x y | yes p = true
30 lt x y | no ¬p = false 63 lt x y | no ¬p = false
31 64
32 Equal : ℕ -> ℕ -> Bool 65 Equal : ℕ -> ℕ -> Bool
33 Equal x y with x ≟ y 66 Equal x y with x ≟ y
34 Equal x y | yes p = true 67 Equal x y | yes p = true
35 Equal x y | no ¬p = false 68 Equal x y | no ¬p = false
69
70 record Env : Set where
71 field
72 varn : ℕ
73 vari : ℕ
74 open Env
36 75
37 whileTest : {l : Level} {t : Set l} -> (Code : Env -> t) -> t 76 whileTest : {l : Level} {t : Set l} -> (Code : Env -> t) -> t
38 whileTest next = next (record {varn = 10 ; vari = 0} ) 77 whileTest next = next (record {varn = 10 ; vari = 0} )
39 78
40 {-# TERMINATING #-} 79 {-# TERMINATING #-}
48 test1 = whileTest (λ env → whileLoop env (λ env1 → env1 )) 87 test1 = whileTest (λ env → whileLoop env (λ env1 → env1 ))
49 88
50 89
51 proof1 : whileTest (λ env → whileLoop env (λ e → (vari e) ≡ 10 )) 90 proof1 : whileTest (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
52 proof1 = refl 91 proof1 = refl
53
54
55 record EnvWithCond : Set (succ Zero) where
56 field
57 input : Env
58 condition : Set
59 proof : condition
60 open EnvWithCond
61 92
62 93
63 94
64 -- stmt2Cond : {l : Level} → EnvWithCond {l} → 95 -- stmt2Cond : {l : Level} → EnvWithCond {l} →
65 -- stmt2Cond env = (Equal (varn' env) 10) ∧ (Equal (vari' env) 0) 96 -- stmt2Cond env = (Equal (varn' env) 10) ∧ (Equal (vari' env) 0)
78 whileLoop' env proof next | false = next env 109 whileLoop' env proof next | false = next env
79 whileLoop' env proof next | true = whileLoop' env1 proof3 next 110 whileLoop' env proof next | true = whileLoop' env1 proof3 next
80 where 111 where
81 env1 = record {varn = (varn env) - 1 ; vari = (vari env) + 1} 112 env1 = record {varn = (varn env) - 1 ; vari = (vari env) + 1}
82 proof3 : varn env1 + vari env1 ≡ 10 113 proof3 : varn env1 + vari env1 ≡ 10
83 proof3 = {!!} 114 proof3 = let open ≡-Reasoning in
115 begin
116 varn env1 + vari env1
117 ≡⟨⟩
118 (varn env - 1) + (vari env + 1)
119 ≡⟨ {!!} ⟩
120 10
121 ∎
122
84 123
85 conversion1 : {l : Level} {t : Set l } → (env : Env) -> ((vari env) ≡ 0) ∧ ((varn env) ≡ 10) 124 conversion1 : {l : Level} {t : Set l } → (env : Env) -> ((vari env) ≡ 0) ∧ ((varn env) ≡ 10)
86 -> (Code : (env1 : Env) -> (varn env1 + vari env1 ≡ 10) -> t) -> t 125 -> (Code : (env1 : Env) -> (varn env1 + vari env1 ≡ 10) -> t) -> t
87 conversion1 = {!!} 126 conversion1 env p1 next = next env proof4
127 where
128 proof4 : varn env + vari env ≡ 10
129 proof4 = let open ≡-Reasoning in
130 begin
131 varn env + vari env
132 ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
133 10 + vari env
134 ≡⟨ cong ( λ n → 10 + n ) (pi1 p1 ) ⟩
135 10 + 0
136 ≡⟨⟩
137 10
138 ∎
88 139
89 proofGears : whileTest' (λ n → conversion1 n {!!} (λ n1 → whileLoop' n1 {!!} (λ n2 → (vari n2) ≡ 10))) 140
90 proofGears = {!!} 141 proofGears : Set
142 proofGears = whileTest' (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ 10 ))))