Mercurial > hg > Papers > 2023 > soto-master

comparison Paper/src/while_loop_verif/verif_loop.agda @ 1:a72446879486

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Init paper
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Thu, 12 Jan 2023 20:28:50 +0900
parents
children
comparison
equal deleted inserted replaced
0:8df537cb6a18 1:a72446879486
1 TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → {Invraiant : Index → Set } → ( reduce : Index → ℕ)
2 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t)
3 → (r : Index) → (p : Invraiant r) → t
4 TerminatingLoopS {_} {t} Index {Invraiant} reduce loop r p with <-cmp 0 (reduce r)
5 ... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) )
6 ... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) where
7 TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t
8 TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1))
9 TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j)
10 ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt
11 ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 )
12 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j )