Mercurial > hg > Papers > 2020 > ryokka-master
comparison paper/src/whileLoopPSem.agda.replaced @ 19:046b2b20d6c7 default tip
fix
| author | ryokka |
|---|---|
| date | Mon, 09 Mar 2020 11:25:49 +0900 |
| parents | |
| children |
comparison
equal
deleted
inserted
replaced
| 18:df02a304db4b | 19:046b2b20d6c7 |
|---|---|
| 1 whileLoopPSem : {l : Level} {t : Set l} @$\rightarrow$@ (input : Envc ) @$\rightarrow$@ (vari input) + (varn input) @$\equiv$@ (c10 input) | |
| 2 @$\rightarrow$@ (next : (output : Envc ) @$\rightarrow$@ ((vari input) + (varn input) @$\equiv$@ (c10 input) ) implies ((vari output) + (varn output) @$\equiv$@ (c10 output)) @$\rightarrow$@ t) | |
| 3 @$\rightarrow$@ (exit : (output : Envc ) @$\rightarrow$@ ((vari input) + (varn input) @$\equiv$@ (c10 input) ) implies ((vari output @$\equiv$@ c10 output)) @$\rightarrow$@ t) @$\rightarrow$@ t | |
| 4 whileLoopPSem env s next exit with varn env | s | |
| 5 ... | zero | _ = exit env (proof (@$\lambda$@ z @$\rightarrow$@ z)) | |
| 6 ... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } ) (proof @$\lambda$@ x @$\rightarrow$@ +-suc varn (vari env) ) | |
| 7 | |
| 8 | |
| 9 loopPPSem : (input output : Envc ) @$\rightarrow$@ output @$\equiv$@ loopPP (varn input) input refl | |
| 10 @$\rightarrow$@ (vari input) + (varn input) @$\equiv$@ (c10 input) @$\rightarrow$@ ((vari input) + (varn input) @$\equiv$@ (c10 input) ) implies ((vari output @$\equiv$@ c10 output)) | |
| 11 loopPPSem input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p | |
| 12 where | |
| 13 lem : (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc) @$\rightarrow$@ n + suc (vari env) @$\equiv$@ suc (n + vari env) | |
| 14 lem n env = +-suc (n) (vari env) | |
| 15 loopPPSemInduct : (n : @$\mathbb{N}$@) @$\rightarrow$@ (current : Envc) @$\rightarrow$@ (eq : n @$\equiv$@ varn current) @$\rightarrow$@ (loopeq : output @$\equiv$@ loopPP n current eq) | |
| 16 @$\rightarrow$@ ((vari current) + (varn current) @$\equiv$@ (c10 current) ) @$\rightarrow$@ ((vari current) + (varn current) @$\equiv$@ (c10 current) ) implies ((vari output @$\equiv$@ c10 output)) | |
| 17 loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (@$\lambda$@ x @$\rightarrow$@ refl) | |
| 18 loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) = | |
| 19 whileLoopPSem current refl | |
| 20 (@$\lambda$@ output x @$\rightarrow$@ loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) | |
| 21 (@$\lambda$@ output x @$\rightarrow$@ loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) |