|
2
|
1 module hoare-while where
|
|
|
2
|
|
|
3 open import Data.Nat
|
|
|
4 open import Level renaming ( suc to succ ; zero to Zero )
|
|
|
5 open import Data.Nat.Properties as NatProp -- <-cmp
|
|
|
6 open import Relation.Binary
|
|
|
7
|
|
|
8 record Envc : Set (succ Zero) where
|
|
|
9 field
|
|
|
10 c10 : @$\mathbb{N}$@
|
|
|
11 varn : @$\mathbb{N}$@
|
|
|
12 vari : @$\mathbb{N}$@
|
|
|
13 open Envc
|
|
|
14
|
|
|
15 whileTestP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (next : Envc @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
16 whileTestP c10 next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } )
|
|
|
17
|
|
|
18 whileLoopP : {l : Level} {t : Set l} @$\rightarrow$@ Envc @$\rightarrow$@ (next : Envc @$\rightarrow$@ t) @$\rightarrow$@ (exit : Envc @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
19 whileLoopP env next exit with (varn env)
|
|
|
20 ... | zero = exit env
|
|
|
21 ... | suc n = exit (record env { varn = n ; vari = (suc n) })
|
|
|
22
|
|
|
23
|
|
|
24 {-@$\#$@ TERMINATING @$\#$@-}
|
|
|
25 loopP : {l : Level} {t : Set l} @$\rightarrow$@ Envc @$\rightarrow$@ (exit : Envc @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
26 loopP env exit = whileLoopP env (@$\lambda$@ env @$\rightarrow$@ loopP env exit ) exit
|
|
|
27
|
|
|
28 whileTestPCall : (c10 : @$\mathbb{N}$@ ) @$\rightarrow$@ Envc
|
|
|
29 whileTestPCall c10 = whileTestP {_} {_} c10 (@$\lambda$@ env @$\rightarrow$@ loopP env (@$\lambda$@ env @$\rightarrow$@ env))
|
|
|
30
|
|
|
31 ---
|
|
|
32 open import Data.Empty
|
|
|
33 --open import Relation.Nullary using (@$\neg$@_; Dec; yes; no)
|
|
|
34
|
|
|
35 --open import Agda.Builtin.Unit
|
|
|
36 open import utilities
|
|
|
37
|
|
|
38 open import Relation.Binary.PropositionalEquality
|
|
|
39
|
|
|
40 open _@$\wedge$@_
|
|
|
41
|
|
|
42 data whileTestState : Set where
|
|
|
43 s1 : whileTestState
|
|
|
44 s2 : whileTestState
|
|
|
45 sf : whileTestState
|
|
|
46
|
|
|
47 whileTestStateP : whileTestState @$\rightarrow$@ Envc @$\rightarrow$@ Set
|
|
|
48 whileTestStateP s1 env = (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env)
|
|
|
49 whileTestStateP s2 env = (varn env + vari env @$\equiv$@ c10 env)
|
|
|
50 whileTestStateP sf env = (vari env @$\equiv$@ c10 env)
|
|
|
51
|
|
|
52 whileTestPwP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ ((env : Envc ) @$\rightarrow$@ whileTestStateP s1 env @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
53 whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
|
|
|
54 env : Envc
|
|
|
55 env = whileTestP c10 ( @$\lambda$@ env @$\rightarrow$@ env )
|
|
|
56
|
|
|
57 whileLoopPwP : {l : Level} {t : Set l} @$\rightarrow$@ (env : Envc ) @$\rightarrow$@ whileTestStateP s2 env
|
|
|
58 @$\rightarrow$@ (next : (env : Envc ) @$\rightarrow$@ whileTestStateP s2 env @$\rightarrow$@ t)
|
|
|
59 @$\rightarrow$@ (exit : (env : Envc ) @$\rightarrow$@ whileTestStateP sf env @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
60 whileLoopPwP env s next exit with <-cmp 0 (varn env)
|
|
|
61 whileLoopPwP env s next exit | tri≈ @$\neg$@a b @$\neg$@c = exit env (lem (sym b) s)
|
|
|
62 where
|
|
|
63 lem : (varn env @$\equiv$@ 0) @$\rightarrow$@ (varn env + vari env @$\equiv$@ c10 env) @$\rightarrow$@ vari env @$\equiv$@ c10 env
|
|
|
64 lem refl refl = refl
|
|
|
65 whileLoopPwP env s next exit | tri< a @$\neg$@b @$\neg$@c = next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) (proof5 a)
|
|
|
66 where
|
|
|
67 1<0 : 1 @$\leq$@ zero @$\rightarrow$@ @$\bot$@
|
|
|
68 1<0 ()
|
|
|
69 proof5 : (suc zero @$\leq$@ (varn env)) @$\rightarrow$@ ((varn env ) - 1) + (vari env + 1) @$\equiv$@ c10 env
|
|
|
70 proof5 (s@$\leq$@s lt) with varn env
|
|
|
71 proof5 (s@$\leq$@s z@$\leq$@n) | zero = @$\bot$@-elim (1<0 a)
|
|
|
72 proof5 (s@$\leq$@s (z@$\leq$@n {n'}) ) | suc n = let open @$\equiv$@-Reasoning in
|
|
|
73 begin
|
|
|
74 n' + (vari env + 1)
|
|
|
75 @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ n' + z ) ( +-sym {vari env} {1} ) @$\rangle$@
|
|
|
76 n' + (1 + vari env )
|
|
|
77 @$\equiv$@@$\langle$@ sym ( +-assoc (n') 1 (vari env) ) @$\rangle$@
|
|
|
78 (n' + 1) + vari env
|
|
|
79 @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ z + vari env ) +1@$\equiv$@suc @$\rangle$@
|
|
|
80 (suc n' ) + vari env
|
|
|
81 @$\equiv$@@$\langle$@@$\rangle$@
|
|
|
82 varn env + vari env
|
|
|
83 @$\equiv$@@$\langle$@ s @$\rangle$@
|
|
|
84 c10 env
|
|
|
85 @$\blacksquare$@
|
|
|
86
|
|
|
87
|
|
|
88 whileLoopPwP' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc ) @$\rightarrow$@ (n @$\equiv$@ varn env) @$\rightarrow$@ whileTestStateP s2 env
|
|
|
89 @$\rightarrow$@ (next : (env : Envc ) @$\rightarrow$@ (pred n @$\equiv$@ varn env) @$\rightarrow$@ whileTestStateP s2 env @$\rightarrow$@ t)
|
|
|
90 @$\rightarrow$@ (exit : (env : Envc ) @$\rightarrow$@ whileTestStateP sf env @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
91 whileLoopPwP' zero env refl refl next exit = exit env refl
|
|
|
92 whileLoopPwP' (suc n) env refl refl next exit = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env))
|
|
|
93
|
|
|
94
|
|
|
95
|
|
|
96 whileTestPSemSound : (c : @$\mathbb{N}$@ ) (output : Envc ) @$\rightarrow$@ output @$\equiv$@ whileTestP c (@$\lambda$@ e @$\rightarrow$@ e) @$\rightarrow$@ @$\top$@ implies ((vari output @$\equiv$@ 0) @$\wedge$@ (varn output @$\equiv$@ c))
|
|
|
97 whileTestPSemSound c output refl = whileTestPSem c
|
|
|
98
|
