Mercurial > hg > Papers > 2021 > soto-prosym

comparison Paper/src/agda/hoare-while.agda.replaced @ 2:9176dff8f38a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ADD while loop description
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Fri, 05 Nov 2021 15:19:08 +0900
parents
children 339fb67b4375
comparison
equal deleted inserted replaced
1:3910f4639344 2:9176dff8f38a
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