Mercurial > hg > Papers > 2020 > soto-midterm
comparison src/whileLoopPSemSound.agda.replaced @ 1:73127e0ab57c
(none)
| author | soto@cr.ie.u-ryukyu.ac.jp |
|---|---|
| date | Tue, 08 Sep 2020 18:38:08 +0900 |
| parents | |
| children |
comparison
equal
deleted
inserted
replaced
| 0:b919985837a3 | 1:73127e0ab57c |
|---|---|
| 1 loopPPSem : (input output : Envc ) @$\rightarrow$@ output @$\equiv$@ loopPP (varn input) input refl | |
| 2 @$\rightarrow$@ (whileTestStateP s2 input ) @$\rightarrow$@ (whileTestStateP s2 input ) implies (whileTestStateP sf output) | |
| 3 loopPPSem input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p | |
| 4 where | |
| 5 lem : (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc) @$\rightarrow$@ n + suc (vari env) @$\equiv$@ suc (n + vari env) | |
| 6 lem n env = +-suc (n) (vari env) | |
| 7 loopPPSemInduct : (n : @$\mathbb{N}$@) @$\rightarrow$@ (current : Envc) @$\rightarrow$@ (eq : n @$\equiv$@ varn current) @$\rightarrow$@ (loopeq : output @$\equiv$@ loopPP n current eq) | |
| 8 @$\rightarrow$@ (whileTestStateP s2 current ) @$\rightarrow$@ (whileTestStateP s2 current ) implies (whileTestStateP sf output) | |
| 9 loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (@$\lambda$@ x @$\rightarrow$@ refl) | |
| 10 loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) = | |
| 11 whileLoopPSem current refl | |
| 12 (@$\lambda$@ output x @$\rightarrow$@ loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) | |
| 13 (@$\lambda$@ output x @$\rightarrow$@ loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) | |
| 14 | |
| 15 | |
| 16 whileLoopPSemSound : {l : Level} @$\rightarrow$@ (input output : Envc ) | |
| 17 @$\rightarrow$@ (varn input + vari input @$\equiv$@ c10 input) | |
| 18 @$\rightarrow$@ output @$\equiv$@ loopPP (varn input) input refl | |
| 19 @$\rightarrow$@ (varn input + vari input @$\equiv$@ c10 input) implies (vari output @$\equiv$@ c10 output) | |
| 20 whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre |