|
1
|
1 {-# TERMINATING #-}
|
|
3
|
2 whileLoop!$\prime$! : {l : Level} {t : Set l} !$\rightarrow$! (env : Env) !$\rightarrow$! {c10 : !$\mathbb{N}$! } !$\rightarrow$! ((varn env) + (vari env) !$\equiv$! c10)
|
|
1
|
3 !$\rightarrow$! (Code : (e1 : Env )!$\rightarrow$! vari e1 !$\equiv$! c10 !$\rightarrow$! t) !$\rightarrow$! t
|
|
3
|
4 whileLoop!$\prime$! env proof next with ( suc zero !$\leq$!? (varn env) )
|
|
|
5 whileLoop!$\prime$! env {c10} proof next | no p = next env ( begin
|
|
1
|
6 vari env !$\equiv$!!$\langle$! refl !$\rangle$!
|
|
|
7 0 + vari env !$\equiv$!!$\langle$! cong (!$\lambda$! k !$\rightarrow$! k + vari env) (sym (lemma1 p )) !$\rangle$!
|
|
|
8 varn env + vari env !$\equiv$!!$\langle$! proof !$\rangle$!
|
|
|
9 c10 !$\blacksquare$! ) where open !$\equiv$!-Reasoning
|
|
3
|
10 whileLoop!$\prime$! env {c10} proof next | yes p = whileLoop!$\prime$! env1 (proof3 p ) next where
|
|
1
|
11 env1 = record {varn = (varn env) - 1 ; vari = (vari env) + 1}
|
|
|
12 1<0 : 1 !$\leq$! zero !$\rightarrow$! !$\bot$!
|
|
|
13 1<0 ()
|
|
|
14 proof3 : (suc zero !$\leq$! (varn env)) !$\rightarrow$! varn env1 + vari env1 !$\equiv$! c10
|
|
|
15 proof3 (s!$\leq$!s lt) with varn env
|
|
|
16 proof3 (s!$\leq$!s z!$\leq$!n) | zero = !$\bot$!-elim (1<0 p)
|
|
3
|
17 proof3 (s!$\leq$!s (z!$\leq$!n {n!$\prime$!}) ) | suc n = let open !$\equiv$!-Reasoning in begin
|
|
|
18 n!$\prime$! + (vari env + 1) !$\equiv$!!$\langle$! cong ( !$\lambda$! z !$\rightarrow$! n!$\prime$! + z ) ( +-sym {vari env} {1} ) !$\rangle$!
|
|
|
19 n!$\prime$! + (1 + vari env ) !$\equiv$!!$\langle$! sym ( +-assoc (n!$\prime$!) 1 (vari env) ) !$\rangle$!
|
|
|
20 (n!$\prime$! + 1) + vari env !$\equiv$!!$\langle$! cong ( !$\lambda$! z !$\rightarrow$! z + vari env ) +1!$\equiv$!suc !$\rangle$!
|
|
|
21 (suc n!$\prime$! ) + vari env !$\equiv$!!$\langle$!!$\rangle$!
|
|
1
|
22 varn env + vari env !$\equiv$!!$\langle$! proof !$\rangle$!
|
|
|
23 c10
|
|
|
24 !$\blacksquare$! |
