Mercurial > hg > Papers > 2020 > ryokka-master

comparison paper/src/gears-while.agda.replaced @ 13:e8655e0264b8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix paper, slide
author ryokka
date Tue, 11 Feb 2020 02:31:26 +0900
parents b5fffa8ae875
children
comparison
equal deleted inserted replaced
12:bf3288c36d7e 13:e8655e0264b8
1 whileTest : {l : Level} {t : Set l} @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ (Code : (env : Env) @$\rightarrow$@ 1 whileTest : {l : Level} {t : Set l} @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ (Code : (env : Env) @$\rightarrow$@
2 ((vari env) @$\equiv$@ 0) /\ ((varn env) @$\equiv$@ c10) @$\rightarrow$@ t) @$\rightarrow$@ t 2 ((vari env) @$\equiv$@ 0) @$\wedge$@ ((varn env) @$\equiv$@ c10) @$\rightarrow$@ t) @$\rightarrow$@ t
3 whileTest {_} {_} {c10} next = next env proof2 3 whileTest {_} {_} {c10} next = next env proof2
4 where 4 where
5 env : Env 5 env : Env
6 env = record {vari = 0 ; varn = c10} 6 env = record {vari = 0 ; varn = c10}
7 proof2 : ((vari env) @$\equiv$@ 0) /\ ((varn env) @$\equiv$@ c10) 7 proof2 : ((vari env) @$\equiv$@ 0) @$\wedge$@ ((varn env) @$\equiv$@ c10)
8 proof2 = record {pi1 = refl ; pi2 = refl} 8 proof2 = record {pi1 = refl ; pi2 = refl}
9 9
10 conversion1 : {l : Level} {t : Set l } @$\rightarrow$@ (env : Env) @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ ((vari env) @$\equiv$@ 0) /\ ((varn env) @$\equiv$@ c10) 10 conversion1 : {l : Level} {t : Set l } @$\rightarrow$@ (env : Env) @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ ((vari env) @$\equiv$@ 0) @$\wedge$@ ((varn env) @$\equiv$@ c10)
11 @$\rightarrow$@ (Code : (env1 : Env) @$\rightarrow$@ (varn env1 + vari env1 @$\equiv$@ c10) @$\rightarrow$@ t) @$\rightarrow$@ t 11 @$\rightarrow$@ (Code : (env1 : Env) @$\rightarrow$@ (varn env1 + vari env1 @$\equiv$@ c10) @$\rightarrow$@ t) @$\rightarrow$@ t
12 conversion1 env {c10} p1 next = next env proof4 12 conversion1 env {c10} p1 next = next env proof4
13 where 13 where
14 proof4 : varn env + vari env @$\equiv$@ c10 14 proof4 : varn env + vari env @$\equiv$@ c10
15 proof4 = let open @$\equiv$@-Reasoning in 15 proof4 = let open @$\equiv$@-Reasoning in
21 c10 + 0 21 c10 + 0
22 @$\equiv$@@$\langle$@ +-sym {c10} {0} @$\rangle$@ 22 @$\equiv$@@$\langle$@ +-sym {c10} {0} @$\rangle$@
23 c10 23 c10
24 @$\blacksquare$@ 24 @$\blacksquare$@
25 25
26 {-# TERMINATING #-} 26 {-@$\#$@ TERMINATING @$\#$@-}
27 whileLoop : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env) @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ ((varn env) + (vari env) @$\equiv$@ c10) @$\rightarrow$@ (Code : Env @$\rightarrow$@ t) @$\rightarrow$@ t 27 whileLoop : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env) @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ ((varn env) + (vari env) @$\equiv$@ c10) @$\rightarrow$@ (Code : Env @$\rightarrow$@ t) @$\rightarrow$@ t
28 whileLoop env proof next with ( suc zero @$\leq$@? (varn env) ) 28 whileLoop env proof next with ( suc zero @$\leq$@? (varn env) )
29 whileLoop env proof next | no p = next env 29 whileLoop env proof next | no p = next env
30 whileLoop env {c10} proof next | yes p = whileLoop env1 (proof3 p ) next 30 whileLoop env {c10} proof next | yes p = whileLoop env1 (proof3 p ) next
31 where 31 where