Mercurial > hg > Members > ryokka > HoareLogic
changeset 90:fb2e12dca19a
Terminating done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 31 Oct 2021 22:31:19 +0900 |
| parents | c2bc4ee841af |
| children | bbbdc8ce8d04 |
| files | whileTestGears1.agda |
| diffstat | 1 files changed, 7 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/whileTestGears1.agda Sun Oct 31 22:15:12 2021 +0900 +++ b/whileTestGears1.agda Sun Oct 31 22:31:19 2021 +0900 @@ -138,22 +138,22 @@ nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥ lemma3 refl () -lemma5 : {i j : ℕ} → i ≤ zero → j < i → ⊥ -lemma5 z≤n () +lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥ +lemma5 (s≤s z≤n) () TerminatingLoop : {l : Level} {t : Set l} {c10 : ℕ } → (i : ℕ) → (env : Env) → i ≡ varn env → varn env + vari env ≡ c10 → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t TerminatingLoop {_} {t} {c10} i env refl p exit with <-cmp 0 i ... | tri≈ ¬a b ¬c = whileLoopSeg {_} {t} {c10} env p (λ e1 eq lt → ⊥-elim (lemma3 b lt) ) exit -... | tri< a ¬b ¬c = whileLoopSeg {_} {t} {c10} env p (λ e1 p1 lt1 → TerminatingLoop1 i env e1 (<⇒≤ lt1) p1 lt1 ) exit where -- varn e1 ≤ varn env - TerminatingLoop1 : (j : ℕ) → (env e1 : Env) → varn e1 ≤ j → varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t +... | tri< a ¬b ¬c = whileLoopSeg {_} {t} {c10} env p (λ e1 p1 lt1 → TerminatingLoop1 i env e1 (≤-step lt1) p1 lt1 ) exit where -- varn e1 < suc (varn env) + TerminatingLoop1 : (j : ℕ) → (env e1 : Env) → varn e1 < suc j → varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t TerminatingLoop1 zero env e1 n≤j eq lt = whileLoopSeg {_} {t} {c10} e1 eq (λ e2 eq lt1 → ⊥-elim (lemma5 n≤j lt1)) exit TerminatingLoop1 (suc j) env e1 n≤j eq lt with <-cmp (varn e1) (suc j) - ... | tri< (s≤s a) ¬b ¬c = TerminatingLoop1 j env e1 a eq lt + ... | tri< a ¬b ¬c = TerminatingLoop1 j env e1 a eq lt ... | tri≈ ¬a refl ¬c = whileLoopSeg {_} {t} {c10} e1 eq lemma4 exit where lemma4 : (e2 : Env) → varn e2 + vari e2 ≡ c10 → varn e2 < varn e1 → t - lemma4 e2 eq lt1 = TerminatingLoop1 j e1 e2 {!!} eq lt1 -- varn e2 ≤ j - ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n≤j c ) + lemma4 e2 eq lt1 = TerminatingLoop1 j e1 e2 lt1 eq lt1 + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j )