Mercurial > hg > Papers > 2020 > soto-midterm
diff src/gears-while.agda.replaced @ 1:73127e0ab57c
(none)
author | soto@cr.ie.u-ryukyu.ac.jp |
---|---|
date | Tue, 08 Sep 2020 18:38:08 +0900 |
parents | |
children |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/gears-while.agda.replaced Tue Sep 08 18:38:08 2020 +0900 @@ -0,0 +1,51 @@ +whileTest : {l : Level} {t : Set l} @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ (Code : (env : Env) @$\rightarrow$@ + ((vari env) @$\equiv$@ 0) @$\wedge$@ ((varn env) @$\equiv$@ c10) @$\rightarrow$@ t) @$\rightarrow$@ t +whileTest {_} {_} {c10} next = next env proof2 + where + env : Env + env = record {vari = 0 ; varn = c10} + proof2 : ((vari env) @$\equiv$@ 0) @$\wedge$@ ((varn env) @$\equiv$@ c10) + proof2 = record {pi1 = refl ; pi2 = refl} + +conversion1 : {l : Level} {t : Set l } @$\rightarrow$@ (env : Env) @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ ((vari env) @$\equiv$@ 0) @$\wedge$@ ((varn env) @$\equiv$@ c10) + @$\rightarrow$@ (Code : (env1 : Env) @$\rightarrow$@ (varn env1 + vari env1 @$\equiv$@ c10) @$\rightarrow$@ t) @$\rightarrow$@ t +conversion1 env {c10} p1 next = next env proof4 + where + proof4 : varn env + vari env @$\equiv$@ c10 + proof4 = let open @$\equiv$@-Reasoning in + begin + varn env + vari env + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ n @$\rightarrow$@ n + vari env ) (pi2 p1 ) @$\rangle$@ + c10 + vari env + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ n @$\rightarrow$@ c10 + n ) (pi1 p1 ) @$\rangle$@ + c10 + 0 + @$\equiv$@@$\langle$@ +-sym {c10} {0} @$\rangle$@ + c10 + @$\blacksquare$@ + +{-@$\#$@ TERMINATING @$\#$@-} +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 +whileLoop env proof next with ( suc zero @$\leq$@? (varn env) ) +whileLoop env proof next | no p = next env +whileLoop env {c10} proof next | yes p = whileLoop env1 (proof3 p ) next + where + env1 = record {varn = (varn env) - 1 ; vari = (vari env) + 1} + 1<0 : 1 @$\leq$@ zero @$\rightarrow$@ @$\bot$@ + 1<0 () + proof3 : (suc zero @$\leq$@ (varn env)) @$\rightarrow$@ varn env1 + vari env1 @$\equiv$@ c10 + proof3 (s@$\leq$@s lt) with varn env + proof3 (s@$\leq$@s z@$\leq$@n) | zero = @$\bot$@-elim (1<0 p) + proof3 (s@$\leq$@s (z@$\leq$@n {n'}) ) | suc n = let open @$\equiv$@-Reasoning in + begin + n' + (vari env + 1) + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ n' + z ) ( +-sym {vari env} {1} ) @$\rangle$@ + n' + (1 + vari env ) + @$\equiv$@@$\langle$@ sym ( +-assoc (n') 1 (vari env) ) @$\rangle$@ + (n' + 1) + vari env + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ z + vari env ) +1@$\equiv$@suc @$\rangle$@ + (suc n' ) + vari env + @$\equiv$@@$\langle$@@$\rangle$@ + varn env + vari env + @$\equiv$@@$\langle$@ proof @$\rangle$@ + c10 + @$\blacksquare$@