Mercurial > hg > Members > ryokka > HoareLogic
changeset 47:b07e96029ae3
fixes
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 16 Dec 2019 15:45:39 +0900 |
| parents | 8bf82026e4fe |
| children | cc8de8bdbf7e |
| files | whileTestGears.agda |
| diffstat | 1 files changed, 35 insertions(+), 28 deletions(-) [+] |
line wrap: on
line diff
--- a/whileTestGears.agda Sun Dec 15 22:57:08 2019 +0900 +++ b/whileTestGears.agda Mon Dec 16 15:45:39 2019 +0900 @@ -56,23 +56,22 @@ 1<0 : 1 ≤ zero → ⊥ 1<0 () proof3 : (suc zero ≤ (varn env)) → varn env1 + vari env1 ≡ c10 - proof3 = {!!} - -- proof3 (s≤s lt) with varn env - -- proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p) - -- proof3 (s≤s (z≤n {n'}) ) | suc n = let open ≡-Reasoning in - -- begin - -- n' + (vari env + 1) - -- ≡⟨ cong ( λ z → n' + z ) ( +-sym {vari env} {1} ) ⟩ - -- n' + (1 + vari env ) - -- ≡⟨ sym ( +-assoc (n') 1 (vari env) ) ⟩ - -- (n' + 1) + vari env - -- ≡⟨ cong ( λ z → z + vari env ) +1≡suc ⟩ - -- (suc n' ) + vari env - -- ≡⟨⟩ - -- varn env + vari env - -- ≡⟨ proof ⟩ - -- c10 - -- ∎ + proof3 (s≤s lt) with varn env + proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p) + proof3 (s≤s (z≤n {n'}) ) | suc n = let open ≡-Reasoning in + begin + n' + (vari env + 1) + ≡⟨ cong ( λ z → n' + z ) ( +-sym {vari env} {1} ) ⟩ + n' + (1 + vari env ) + ≡⟨ sym ( +-assoc (n') 1 (vari env) ) ⟩ + (n' + 1) + vari env + ≡⟨ cong ( λ z → z + vari env ) +1≡suc ⟩ + (suc n' ) + vari env + ≡⟨⟩ + varn env + vari env + ≡⟨ proof ⟩ + c10 + ∎ -- Condition to Invariant conversion1 : {l : Level} {t : Set l } → (env : Env ) → {c10 : ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) @@ -134,20 +133,28 @@ whileTestPCall : {c10 : ℕ } → Set whileTestPCall {c10} = whileTestP {_} {_} c10 (λ env → loopP env (λ env → ( pvari env ≡ c10 ))) -wTlemma1 : {l : Level} {t : Set l} → (e : EnvP ) → 0 < pvarn e → cx e ≡ pstate1 {!!} → (exit : EnvP → t) → t -wTlemma1 e lt prev exit = exit record e { cx = pstate2 {!!} } +whileTestPwithProof : {l : Level} {t : Set l} → (c10 : ℕ ) → (next : (e : EnvP ) → cx e ≡ pstate1 {!!} → t) → t +whileTestPwithProof {l} {t} c10 next = next env lemma where + env : EnvP + env = record { pvarn = {!!} ; pvari = {!!} ; c10 = {!!} ; cx = {!!} } + lemma : cx env ≡ pstate1 {!!} + lemma = {!!} -wTlemma2 : {l : Level} {t : Set l} → (e : EnvP ) → 0 ≡ pvarn e → cx e ≡ pstate2 {!!} → (exit : EnvP → t) → t -wTlemma2 e eq prev exit = exit record e { cx = pfinstate {!!} } +loopPwithProof : {l : Level} {t : Set l} → (e : EnvP ) → cx e ≡ pstate2 {!!} → (exit : EnvP → cx e ≡ pstate2 {!!} → t) → t +loopPwithProof env exit = whileLoopP env (λ env → loopPwithProof env {!!} {!!} ) {!!} -whileTestPProof : {c10 : ℕ } → Set -whileTestPProof {c10} = whileTestP {_} {_} c10 - $ λ env → wTlemma1 env {!!} {!!} - $ λ env → loopP env - $ λ env → wTlemma2 env {!!} {!!} - $ λ env → ( pvari env ≡ c10 ) +ConvP : (e : EnvP) → cx e ≡ pstate1 {!!} → cx e ≡ pstate2 {!!} +ConvP = {!!} + +finalProof : {l : Level} {t : Set l} → (e : EnvP ) → cx e ≡ pstate2 {!!} → pvari e ≡ c10 e +finalProof env exit = {!!} + +whileTestPProof : {c : ℕ } → Set +whileTestPProof {c} = whileTestPwithProof c + $ λ env eq → loopPwithProof env (ConvP env eq) + $ λ env eq → pvari env ≡ c10 env whileTestPProofMeta : {c10 : ℕ } → whileTestPProof {c10} -whileTestPProofMeta {c10} = {!!} +whileTestPProofMeta {c10} = ?