Mercurial > hg > Members > ryokka > HoareLogic
diff whileTestGears1.agda @ 89:c2bc4ee841af
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 31 Oct 2021 22:15:12 +0900 |
parents | accd3d99cc86 |
children | fb2e12dca19a |
line wrap: on
line diff
--- a/whileTestGears1.agda Sun Oct 31 16:25:46 2021 +0900 +++ b/whileTestGears1.agda Sun Oct 31 22:15:12 2021 +0900 @@ -1,7 +1,7 @@ module whileTestGears1 where open import Function -open import Data.Nat +open import Data.Nat renaming ( _∸_ to _-_) open import Data.Bool hiding ( _≟_ ; _≤?_ ; _≤_ ; _<_ ) open import Level renaming ( suc to succ ; zero to Zero ) open import Relation.Nullary using (¬_; Dec; yes; no) @@ -111,12 +111,15 @@ 0 + vari env ≡⟨ cong (λ k → k + vari env) (sym (lemma1 p )) ⟩ varn env + vari env ≡⟨ proof ⟩ c10 ∎ ) where open ≡-Reasoning -whileLoopSeg {_} {_} {c10} env proof next exit | yes p = next env1 (proof3 p ) proof4 where +whileLoopSeg {_} {_} {c10} env proof next exit | yes p = next env1 (proof3 p ) (proof4 (varn env) p) where env1 = record {varn = (varn env) - 1 ; vari = (vari env) + 1} 1<0 : 1 ≤ zero → ⊥ 1<0 () - proof4 : varn env1 < varn env - proof4 = {!!} + proof4 : (i : ℕ) → 1 ≤ i → i - 1 < i + proof4 zero () + proof4 (suc i) lt = begin + suc (suc i - 1 ) ≤⟨ ≤-refl ⟩ + suc i ∎ where open ≤-Reasoning proof3 : (suc zero ≤ (varn env)) → varn env1 + vari env1 ≡ c10 proof3 (s≤s lt) with varn env proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p) @@ -133,22 +136,24 @@ nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥ 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 () 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 e1 b lt) ) exit where - lemma3 : (e1 : Env) → 0 ≡ varn env → varn e1 < varn env → ⊥ - lemma3 e refl () -... | tri< a ¬b ¬c = whileLoopSeg {_} {t} {c10} env p (TerminatingLoop1 i) exit where - TerminatingLoop1 : (j : ℕ) → (e1 : Env) → varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t - TerminatingLoop1 zero e1 eq lt = whileLoopSeg {_} {t} {c10} env p {!!} exit - TerminatingLoop1 (suc j) e1 eq lt with <-cmp j (varn e1) - ... | tri< (s≤s a) ¬b ¬c = TerminatingLoop1 j e1 {!!} {!!} - ... | tri≈ ¬a b ¬c = whileLoopSeg {_} {t} {c10} e1 {!!} lemma4 exit where +... | 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 + 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 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 lt = TerminatingLoop1 j {!!} {!!} {!!} - ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> lt {!!} ) + lemma4 e2 eq lt1 = TerminatingLoop1 j e1 e2 {!!} eq lt1 -- varn e2 ≤ j + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n≤j c )