|
1
|
1 module whileTestProof where
|
|
|
2 --
|
|
|
3 -- Using imply relation to make soundness explicit
|
|
|
4 -- termination is shown by induction on varn
|
|
|
5 --
|
|
|
6
|
|
|
7 data _implies_ (A B : Set ) : Set (succ Zero) where
|
|
|
8 proof : ( A @$\rightarrow$@ B ) @$\rightarrow$@ A implies B
|
|
|
9
|
|
|
10 implies2p : {A B : Set } @$\rightarrow$@ A implies B @$\rightarrow$@ A @$\rightarrow$@ B
|
|
|
11 implies2p (proof x) = x
|
|
|
12
|
|
|
13 whileTestPSem : (c : @$\mathbb{N}$@) @$\rightarrow$@ whileTestP c ( @$\lambda$@ env @$\rightarrow$@ ⊤ implies (whileTestStateP s1 env) )
|
|
|
14 whileTestPSem c = proof ( @$\lambda$@ _ @$\rightarrow$@ record { pi1 = refl ; pi2 = refl } )
|
|
|
15
|
|
|
16 SemGears : (f : {l : Level } {t : Set l } @$\rightarrow$@ (e0 : Envc ) @$\rightarrow$@ ((e : Envc) @$\rightarrow$@ t) @$\rightarrow$@ t ) @$\rightarrow$@ Set (succ Zero)
|
|
|
17 SemGears f = Envc @$\rightarrow$@ Envc @$\rightarrow$@ Set
|
|
|
18
|
|
|
19 GearsUnitSound : (e0 e1 : Envc) {pre : Envc @$\rightarrow$@ Set} {post : Envc @$\rightarrow$@ Set}
|
|
|
20 @$\rightarrow$@ (f : {l : Level } {t : Set l } @$\rightarrow$@ (e0 : Envc ) @$\rightarrow$@ (Envc @$\rightarrow$@ t) @$\rightarrow$@ t )
|
|
|
21 @$\rightarrow$@ (fsem : (e0 : Envc ) @$\rightarrow$@ f e0 ( @$\lambda$@ e1 @$\rightarrow$@ (pre e0) implies (post e1)))
|
|
|
22 @$\rightarrow$@ f e0 (@$\lambda$@ e1 @$\rightarrow$@ pre e0 implies post e1)
|
|
|
23 GearsUnitSound e0 e1 f fsem = fsem e0
|
|
|
24
|
|
|
25 whileTestPSemSound : (c : @$\mathbb{N}$@ ) (output : Envc ) @$\rightarrow$@ output @$\equiv$@ whileTestP c (@$\lambda$@ e @$\rightarrow$@ e) @$\rightarrow$@ ⊤ implies ((vari output @$\equiv$@ 0) @$\wedge$@ (varn output @$\equiv$@ c))
|
|
|
26 whileTestPSemSound c output refl = proof (@$\lambda$@ x @$\rightarrow$@ record { pi1 = refl ; pi2 = refl })
|
|
|
27 -- whileTestPSem c
|
|
|
28
|
|
|
29
|
|
|
30 whileConvPSemSound : {l : Level} @$\rightarrow$@ (input : Envc) @$\rightarrow$@ (whileTestStateP s1 input ) implies (whileTestStateP s2 input)
|
|
|
31 whileConvPSemSound input = proof @$\lambda$@ x @$\rightarrow$@ (conv input x) where
|
|
|
32 conv : (env : Envc ) @$\rightarrow$@ (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env) @$\rightarrow$@ varn env + vari env @$\equiv$@ c10 env
|
|
|
33 conv e record { pi1 = refl ; pi2 = refl } = +zero
|
|
|
34
|
|
|
35 loopPP : (n : @$\mathbb{N}$@) @$\rightarrow$@ (input : Envc ) @$\rightarrow$@ (n @$\equiv$@ varn input) @$\rightarrow$@ Envc
|
|
|
36 loopPP zero input refl = input
|
|
|
37 loopPP (suc n) input refl =
|
|
|
38 loopPP n (record input { varn = pred (varn input) ; vari = suc (vari input)}) refl
|
|
|
39
|
|
|
40 whileLoopPSem : {l : Level} {t : Set l} @$\rightarrow$@ (input : Envc ) @$\rightarrow$@ whileTestStateP s2 input
|
|
|
41 @$\rightarrow$@ (next : (output : Envc ) @$\rightarrow$@ (whileTestStateP s2 input ) implies (whileTestStateP s2 output) @$\rightarrow$@ t)
|
|
|
42 @$\rightarrow$@ (exit : (output : Envc ) @$\rightarrow$@ (whileTestStateP s2 input ) implies (whileTestStateP sf output) @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
43 whileLoopPSem env s next exit with varn env | s
|
|
|
44 ... | zero | _ = exit env (proof (@$\lambda$@ z @$\rightarrow$@ z))
|
|
|
45 ... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } ) (proof @$\lambda$@ x @$\rightarrow$@ +-suc varn (vari env) )
|
|
|
46
|
|
|
47 loopPPSem : (input output : Envc ) @$\rightarrow$@ output @$\equiv$@ loopPP (varn input) input refl
|
|
|
48 @$\rightarrow$@ (whileTestStateP s2 input ) @$\rightarrow$@ (whileTestStateP s2 input ) implies (whileTestStateP sf output)
|
|
|
49 loopPPSem input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p
|
|
|
50 where
|
|
|
51 lem : (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc) @$\rightarrow$@ n + suc (vari env) @$\equiv$@ suc (n + vari env)
|
|
|
52 lem n env = +-suc (n) (vari env)
|
|
|
53 loopPPSemInduct : (n : @$\mathbb{N}$@) @$\rightarrow$@ (current : Envc) @$\rightarrow$@ (eq : n @$\equiv$@ varn current) @$\rightarrow$@ (loopeq : output @$\equiv$@ loopPP n current eq)
|
|
|
54 @$\rightarrow$@ (whileTestStateP s2 current ) @$\rightarrow$@ (whileTestStateP s2 current ) implies (whileTestStateP sf output)
|
|
|
55 loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (@$\lambda$@ x @$\rightarrow$@ refl)
|
|
|
56 loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) =
|
|
|
57 whileLoopPSem current refl
|
|
|
58 (@$\lambda$@ output x @$\rightarrow$@ loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
|
|
|
59 (@$\lambda$@ output x @$\rightarrow$@ loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
|
|
|
60
|
|
|
61 whileLoopPSemSound : {l : Level} @$\rightarrow$@ (input output : Envc )
|
|
|
62 @$\rightarrow$@ whileTestStateP s2 input
|
|
|
63 @$\rightarrow$@ output @$\equiv$@ loopPP (varn input) input refl
|
|
|
64 @$\rightarrow$@ (whileTestStateP s2 input ) implies ( whileTestStateP sf output )
|
|
|
65 whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre
|
