Mercurial > hg > Papers > 2022 > soto-sigos
comparison Paper/src/while_loop_verif/verif_loop.agda.replaced @ 0:14a0e409d574
ADD fast commit
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 24 Apr 2022 23:13:44 +0900 |
| parents | |
| children |
comparison
equal
deleted
inserted
replaced
| -1:000000000000 | 0:14a0e409d574 |
|---|---|
| 1 TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) !$\rightarrow$! {Invraiant : Index !$\rightarrow$! Set } !$\rightarrow$! ( reduce : Index !$\rightarrow$! !$\mathbb{N}$!) | |
| 2 !$\rightarrow$! (loop : (r : Index) !$\rightarrow$! Invraiant r !$\rightarrow$! (next : (r1 : Index) !$\rightarrow$! Invraiant r1 !$\rightarrow$! reduce r1 < reduce r !$\rightarrow$! t ) !$\rightarrow$! t) | |
| 3 !$\rightarrow$! (r : Index) !$\rightarrow$! (p : Invraiant r) !$\rightarrow$! t | |
| 4 TerminatingLoopS {_} {t} Index {Invraiant} reduce loop r p with <-cmp 0 (reduce r) | |
| 5 ... | tri!$\approx$! !$\neg$!a b !$\neg$!c = loop r p (!$\lambda$! r1 p1 lt !$\rightarrow$! !$\bot$!-elim (lemma3 b lt) ) | |
| 6 ... | tri< a !$\neg$!b !$\neg$!c = loop r p (!$\lambda$! r1 p1 lt1 !$\rightarrow$! TerminatingLoop1 (reduce r) r r1 (!$\leq$!-step lt1) p1 lt1 ) where | |
| 7 TerminatingLoop1 : (j : !$\mathbb{N}$!) !$\rightarrow$! (r r1 : Index) !$\rightarrow$! reduce r1 < suc j !$\rightarrow$! Invraiant r1 !$\rightarrow$! reduce r1 < reduce r !$\rightarrow$! t | |
| 8 TerminatingLoop1 zero r r1 n!$\leq$!j p1 lt = loop r1 p1 (!$\lambda$! r2 p1 lt1 !$\rightarrow$! !$\bot$!-elim (lemma5 n!$\leq$!j lt1)) | |
| 9 TerminatingLoop1 (suc j) r r1 n!$\leq$!j p1 lt with <-cmp (reduce r1) (suc j) | |
| 10 ... | tri< a !$\neg$!b !$\neg$!c = TerminatingLoop1 j r r1 a p1 lt | |
| 11 ... | tri!$\approx$! !$\neg$!a b !$\neg$!c = loop r1 p1 (!$\lambda$! r2 p2 lt1 !$\rightarrow$! TerminatingLoop1 j r1 r2 (subst (!$\lambda$! k !$\rightarrow$! reduce r2 < k ) b lt1 ) p2 lt1 ) | |
| 12 ... | tri> !$\neg$!a !$\neg$!b c = !$\bot$!-elim ( nat-!$\leq$!> c n!$\leq$!j ) |