Mercurial > hg > Members > ryokka > HoareLogic
changeset 93:a7263ecf8671
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 01 Nov 2021 09:59:43 +0900 |
| parents | 9c91d23c2836 |
| children | c3b08293a72e |
| files | whileTestGears.agda whileTestGears1.agda whileTestPrim.agda whileTestPrimProof.agda |
| diffstat | 4 files changed, 121 insertions(+), 419 deletions(-) [+] |
line wrap: on
line diff
--- a/whileTestGears.agda Mon Nov 01 08:34:07 2021 +0900 +++ b/whileTestGears.agda Mon Nov 01 09:59:43 2021 +0900 @@ -1,298 +1,188 @@ module whileTestGears where open import Function -open import Data.Nat -open import Data.Bool hiding ( _≟_ ; _≤?_ ; _≤_ ; _<_) -open import Data.Product +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) open import Relation.Binary.PropositionalEquality -open import Agda.Builtin.Unit open import utilities open _/\_ --- original codeGear (with non terminatinng ) - -record Env : Set (succ Zero) where +record Env : Set where field varn : ℕ vari : ℕ open Env -whileTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t -whileTest c10 next = next (record {varn = c10 ; vari = 0 } ) +whileTestS : { m : Level} → (c10 : ℕ) → (Code : Env → Set m) → Set m +whileTestS c10 next = next (record {varn = c10 ; vari = 0} ) + +whileTestS1 : (c10 : ℕ) → whileTestS c10 (λ e → ((varn e ≡ c10) /\ (vari e ≡ 0 )) ) +whileTestS1 c10 = record { pi1 = refl ; pi2 = refl } + + +whileTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t +whileTest c10 next = next (record {varn = c10 ; vari = 0} ) {-# TERMINATING #-} whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t whileLoop env next with lt 0 (varn env) whileLoop env next | false = next env whileLoop env next | true = - whileLoop (record env {varn = (varn env) - 1 ; vari = (vari env) + 1}) next + whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next test1 : Env test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 )) + proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 )) proof1 = refl --- codeGear with pre-condtion and post-condition --- -- ↓PostCondition -whileTest' : {l : Level} {t : Set l} → {c10 : ℕ } → (Code : (env : Env ) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t -whileTest' {_} {_} {c10} next = next env proof2 +whileTest' : {l : Level} {t : Set l} → {c10 : ℕ } → (Code : (env : Env) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t +whileTest' {_} {_} {c10} next = next env proof2 where env : Env - env = record {vari = 0 ; varn = c10 } + env = record {vari = 0 ; varn = c10} proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition proof2 = record {pi1 = refl ; pi2 = refl} open import Data.Empty open import Data.Nat.Properties +lemma1 : {i : ℕ} → ¬ 1 ≤ i → i ≡ 0 +lemma1 {zero} not = refl +lemma1 {suc i} not = ⊥-elim ( not (s≤s z≤n) ) {-# TERMINATING #-} -- ↓PreCondition(Invaliant) -whileLoop' : {l : Level} {t : Set l} → (env : Env ) → {c10 : ℕ } → ((varn env) + (vari env) ≡ c10) → (Code : Env → t) → t +whileLoop' : {l : Level} {t : Set l} → (env : Env) → {c10 : ℕ } → ((varn env) + (vari env) ≡ c10) + → (Code : (e1 : Env )→ vari e1 ≡ c10 → t) → t whileLoop' env proof next with ( suc zero ≤? (varn env) ) -whileLoop' env proof next | no p = next env -whileLoop' env {c10} proof next | yes p = whileLoop' env1 (proof3 p ) next - where - env1 = record env {varn = (varn env) - 1 ; vari = (vari env) + 1} +whileLoop' env {c10} proof next | no p = next env ( begin + vari env ≡⟨ refl ⟩ + 0 + vari env ≡⟨ cong (λ k → k + vari env) (sym (lemma1 p )) ⟩ + varn env + vari env ≡⟨ proof ⟩ + c10 ∎ ) where open ≡-Reasoning +whileLoop' env {c10} proof next | yes p = whileLoop' env1 (proof3 p ) next where + env1 = record {varn = (varn env) - 1 ; vari = (vari env) + 1} 1<0 : 1 ≤ zero → ⊥ 1<0 () 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) - 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 ⟩ + 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) - → (Code : (env1 : Env ) → (varn env1 + vari env1 ≡ c10) → t) → t -conversion1 env {c10} p1 next = next env proof4 - where +-- Condition to Invaliant +conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 : ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) + → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t +conversion1 env {c10} p1 next = next env proof4 where proof4 : varn env + vari env ≡ c10 - proof4 = let open ≡-Reasoning in - begin - varn env + vari env - ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩ - c10 + vari env - ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩ - c10 + 0 - ≡⟨ +-sym {c10} {0} ⟩ + proof4 = let open ≡-Reasoning in begin + varn env + vari env ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩ + c10 + vari env ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩ + c10 + 0 ≡⟨ +-sym {c10} {0} ⟩ c10 ∎ --- all proofs are connected -proofGears : {c10 : ℕ } → Set -proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) - --- but we cannot prove the soundness of the last condition --- --- proofGearsMeta : {c10 : ℕ } → proofGears {c10} --- proofGearsMeta {c10} = {!!} -- net yet done +open import Data.Unit hiding ( _≟_ ; _≤?_ ; _≤_) --- --- codeGear with loop step and closed environment --- - -open import Relation.Binary +whileTestSpec1 : (c10 : ℕ) → (e1 : Env ) → vari e1 ≡ c10 → ⊤ +whileTestSpec1 _ _ x = tt -record Envc : Set (succ Zero) where - field - c10 : ℕ - varn : ℕ - vari : ℕ -open Envc +proofGears : {c10 : ℕ } → ⊤ +proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 p3 → whileTestSpec1 c10 n2 p3 ))) -whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Envc → t) → t -whileTestP c10 next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } ) - -whileLoopP : {l : Level} {t : Set l} → Envc → (next : Envc → t) → (exit : Envc → t) → t -whileLoopP env next exit with <-cmp 0 (varn env) -whileLoopP env next exit | tri≈ ¬a b ¬c = exit env -whileLoopP env next exit | tri< a ¬b ¬c = - next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) +-- ↓PreCondition(Invaliant) +whileLoopSeg : {l : Level} {t : Set l} → {c10 : ℕ } → (env : Env) → ((varn env) + (vari env) ≡ c10) + → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t) + → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t +whileLoopSeg env proof next exit with ( suc zero ≤? (varn env) ) +whileLoopSeg {_} {_} {c10} env proof next exit | no p = exit env ( begin + vari env ≡⟨ refl ⟩ + 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 (varn env) p) where + env1 = record {varn = (varn env) - 1 ; vari = (vari env) + 1} + 1<0 : 1 ≤ zero → ⊥ + 1<0 () + 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) + 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 + ∎ --- equivalent of whileLoopP but it looks like an induction on varn -whileLoopP' : {l : Level} {t : Set l} → Envc → (next : Envc → t) → (exit : Envc → t) → t -whileLoopP' env@record { c10 = c10 ; varn = zero ; vari = vari } _ exit = exit env -whileLoopP' record { c10 = c10 ; varn = suc varn1 ; vari = vari } next _ = next (record {c10 = c10 ; varn = varn1 ; vari = suc vari }) - --- normal loop without termination -{-# TERMINATING #-} -loopP : {l : Level} {t : Set l} → Envc → (exit : Envc → t) → t -loopP env exit = whileLoopP env (λ env → loopP env exit ) exit - -whileTestPCall : (c10 : ℕ ) → Envc -whileTestPCall c10 = whileTestP {_} {_} c10 (λ env → loopP env (λ env → env)) +open import Relation.Binary.Definitions --- --- codeGears with states of condition --- -data whileTestState : Set where - s1 : whileTestState - s2 : whileTestState - sf : whileTestState +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 < 1 → j < i → ⊥ +lemma5 (s≤s z≤n) () -whileTestStateP : whileTestState → Envc → Set -whileTestStateP s1 env = (vari env ≡ 0) /\ (varn env ≡ c10 env) -whileTestStateP s2 env = (varn env + vari env ≡ c10 env) -whileTestStateP sf env = (vari env ≡ c10 env) - -whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) → ((env : Envc ) → whileTestStateP s1 env → t) → t -whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where - env : Envc - env = whileTestP c10 ( λ env → env ) +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 (≤-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< 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 lt1 eq lt1 + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) -whileLoopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env - → (next : (env : Envc ) → whileTestStateP s2 env → t) - → (exit : (env : Envc ) → whileTestStateP sf env → t) → t -whileLoopPwP env s next exit with <-cmp 0 (varn env) -whileLoopPwP env s next exit | tri≈ ¬a b ¬c = exit env (lem (sym b) s) - where - lem : (varn env ≡ 0) → (varn env + vari env ≡ c10 env) → vari env ≡ c10 env - lem refl refl = refl -whileLoopPwP env s next exit | tri< a ¬b ¬c = next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) (proof5 a) - where - 1<0 : 1 ≤ zero → ⊥ - 1<0 () - proof5 : (suc zero ≤ (varn env)) → (varn env - 1) + (vari env + 1) ≡ c10 env - proof5 (s≤s lt) with varn env - proof5 (s≤s z≤n) | zero = ⊥-elim (1<0 a) - proof5 (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 - ≡⟨ s ⟩ - c10 env - ∎ +proofGearsTerm : {c10 : ℕ } → ⊤ +proofGearsTerm {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → TerminatingLoop (varn n1) n1 refl p2 (λ n2 p3 → whileTestSpec1 c10 n2 p3 ))) +TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → (Invraiant : Index → Set ) → (ExitCond : Index → Set) → ( reduce : Index → ℕ) + → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → (exit : (re : Index) → ExitCond re → t) → t) + → (r : Index) → (p : Invraiant r) → (exit : (re : Index) → ExitCond re → t) → t +TerminatingLoopS {_} {t} Index Invraiant ExitCond reduce loop r p exit with <-cmp 0 (reduce r) +... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) exit +... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) exit where + TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t + TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) exit + TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) + ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt + ... | tri≈ ¬a b ¬c = loop r1 p1 lemma4 exit where + lemma4 : (r2 : Index) → Invraiant r2 → reduce r2 < reduce r1 → t + lemma4 r2 p2 lt1 = TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) -whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env - → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env → t) - → (exit : (env : Envc ) → whileTestStateP sf env → t) → t -whileLoopPwP' zero env refl refl next exit = exit env refl -whileLoopPwP' (suc n) env refl refl next exit = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env)) +proofGearsTermS : {c10 : ℕ } → ⊤ +proofGearsTermS {c10} = whileTest' {_} {_} {c10} (λ n p → conversion1 n p (λ n1 p1 → + TerminatingLoopS Env (λ env → varn env + vari env ≡ c10) (λ e1 → vari e1 ≡ c10) (λ env → varn env) + (λ n2 p2 loop exit → whileLoopSeg {_} {_} {c10} n2 p2 loop exit) n1 p1 (λ ne pe → whileTestSpec1 c10 ne pe))) -{-# TERMINATING #-} -loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t -loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit -loopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t -loopPwP' zero env refl refl exit = exit env refl -loopPwP' (suc n) env refl refl exit = whileLoopPwP' (suc n) env refl refl (λ env x y → loopPwP' n env x y exit) exit - - -loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) → (seq : whileTestStateP s2 env) → loopPwP' n env (sym eq) seq λ env₁ x → (vari env₁ ≡ c10 env₁) -loopHelper zero env eq refl rewrite eq = refl -loopHelper (suc n) env eq refl rewrite eq = loopHelper n (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) refl (+-suc n (vari env)) - - --- all codtions are correctly connected and required condtion is proved in the continuation --- use required condition as t in (env → t) → t --- -whileTestPCallwP : (c : ℕ ) → Set -whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c10 env ) ) where - conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env - conv e record { pi1 = refl ; pi2 = refl } = +zero - -whileTestPCallwP' : (c : ℕ ) → Set -whileTestPCallwP' c = whileTestPwP {_} {_} c (λ env s → loopPwP' (varn env) env refl (conv env s) ( λ env s → vari env ≡ c10 env ) ) where - conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env - conv e record { pi1 = refl ; pi2 = refl } = +zero - -helperCallwP : (c : ℕ) → whileTestPCallwP' c -helperCallwP c = whileTestPwP {_} {_} c (λ env s → loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero) - --- --- Using imply relation to make soundness explicit --- termination is shown by induction on varn --- - -data _implies_ (A B : Set ) : Set (succ Zero) where - proof : ( A → B ) → A implies B - -implies2p : {A B : Set } → A implies B → A → B -implies2p (proof x) = x - -bwhileTestPSem : (c : ℕ) → whileTestP c ( λ env → ⊤ implies (whileTestStateP s1 env) ) -whileTestPSem c = proof ( λ _ → record { pi1 = refl ; pi2 = refl } ) - -SemGears : (f : {l : Level } {t : Set l } → (e0 : Envc ) → ((e : Envc) → t) → t ) → Set (succ Zero) -SemGears f = Envc → Envc → Set - -GearsUnitSound : (e0 e1 : Envc) {pre : Envc → Set} {post : Envc → Set} - → (f : {l : Level } {t : Set l } → (e0 : Envc ) → (Envc → t) → t ) - → (fsem : (e0 : Envc ) → f e0 ( λ e1 → (pre e0) implies (post e1))) - → f e0 (λ e1 → pre e0 implies post e1) -GearsUnitSound e0 e1 f fsem = fsem e0 - -whileTestPSemSound : (c : ℕ ) (output : Envc ) → output ≡ whileTestP c (λ e → e) → ⊤ implies ((vari output ≡ 0) /\ (varn output ≡ c)) -whileTestPSemSound c output refl = whileTestPSem c -whileConvPSemSound : {l : Level} → (input : Envc) → (whileTestStateP s1 input ) implies (whileTestStateP s2 input) -whileConvPSemSound input = proof λ x → (conv input x) where - conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env - conv e record { pi1 = refl ; pi2 = refl } = +zero -loopPP : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc -loopPP zero input refl = input -loopPP (suc n) input refl = - loopPP n (record input { varn = pred (varn input) ; vari = suc (vari input)}) refl - -whileLoopPSem : {l : Level} {t : Set l} → (input : Envc ) → whileTestStateP s2 input - → (next : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output) → t) - → (exit : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) → t) → t -whileLoopPSem env s next exit with varn env | s -... | zero | _ = exit env (proof (λ z → z)) -... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } ) (proof λ x → +-suc varn (vari env) ) - -loopPPSem : (input output : Envc ) → output ≡ loopPP (varn input) input refl - → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) -loopPPSem input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p - where - lem : (n : ℕ) → (env : Envc) → n + suc (vari env) ≡ suc (n + vari env) - lem n env = +-suc (n) (vari env) - loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) → (loopeq : output ≡ loopPP n current eq) - → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output) - loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl) - loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) = - whileLoopPSem current refl - (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) - (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) - -whileLoopPSemSound : {l : Level} → (input output : Envc ) - → whileTestStateP s2 input - → output ≡ loopPP (varn input) input refl - → (whileTestStateP s2 input ) implies ( whileTestStateP sf output ) -whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre - - --- whileTestSound : {l : Level} (c : ℕ) → (output : Envc) → ⊤ → whileTestStateP sf output --- whileTestSound {l} c record { c10 = c10 ; varn = varn ; vari = vari } top = --- implies2p (whileLoopPSemSound {l} (record { c10 = c ; varn = c ; vari = zero }) (record { c10 = c10 ; varn = c ; vari = vari}) (+zero) {!!}) --- (implies2p (whileConvPSemSound {l} (record { c10 = c ; varn = c ; vari = zero })) (implies2p (whileTestPSemSound c (whileTestP c (λ e → e)) refl) top))
--- a/whileTestGears1.agda Mon Nov 01 08:34:07 2021 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,188 +0,0 @@ -module whileTestGears1 where - -open import Function -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) -open import Relation.Binary.PropositionalEquality - -open import utilities -open _/\_ - -record Env : Set where - field - varn : ℕ - vari : ℕ -open Env - -whileTestS : { m : Level} → (c10 : ℕ) → (Code : Env → Set m) → Set m -whileTestS c10 next = next (record {varn = c10 ; vari = 0} ) - -whileTestS1 : (c10 : ℕ) → whileTestS c10 (λ e → ((varn e ≡ c10) /\ (vari e ≡ 0 )) ) -whileTestS1 c10 = record { pi1 = refl ; pi2 = refl } - - -whileTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t -whileTest c10 next = next (record {varn = c10 ; vari = 0} ) - -{-# TERMINATING #-} -whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t -whileLoop env next with lt 0 (varn env) -whileLoop env next | false = next env -whileLoop env next | true = - whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next - -test1 : Env -test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 )) - - -proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 )) -proof1 = refl - --- ↓PostCondition -whileTest' : {l : Level} {t : Set l} → {c10 : ℕ } → (Code : (env : Env) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t -whileTest' {_} {_} {c10} next = next env proof2 - where - env : Env - env = record {vari = 0 ; varn = c10} - proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition - proof2 = record {pi1 = refl ; pi2 = refl} - -open import Data.Empty -open import Data.Nat.Properties - -lemma1 : {i : ℕ} → ¬ 1 ≤ i → i ≡ 0 -lemma1 {zero} not = refl -lemma1 {suc i} not = ⊥-elim ( not (s≤s z≤n) ) - -{-# TERMINATING #-} -- ↓PreCondition(Invaliant) -whileLoop' : {l : Level} {t : Set l} → (env : Env) → {c10 : ℕ } → ((varn env) + (vari env) ≡ c10) - → (Code : (e1 : Env )→ vari e1 ≡ c10 → t) → t -whileLoop' env proof next with ( suc zero ≤? (varn env) ) -whileLoop' env {c10} proof next | no p = next env ( begin - vari env ≡⟨ refl ⟩ - 0 + vari env ≡⟨ cong (λ k → k + vari env) (sym (lemma1 p )) ⟩ - varn env + vari env ≡⟨ proof ⟩ - c10 ∎ ) where open ≡-Reasoning -whileLoop' env {c10} proof next | yes p = whileLoop' env1 (proof3 p ) next where - env1 = record {varn = (varn env) - 1 ; vari = (vari env) + 1} - 1<0 : 1 ≤ zero → ⊥ - 1<0 () - 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) - 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 Invaliant -conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 : ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) - → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t -conversion1 env {c10} p1 next = next env proof4 where - proof4 : varn env + vari env ≡ c10 - proof4 = let open ≡-Reasoning in begin - varn env + vari env ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩ - c10 + vari env ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩ - c10 + 0 ≡⟨ +-sym {c10} {0} ⟩ - c10 - ∎ - -open import Data.Unit hiding ( _≟_ ; _≤?_ ; _≤_) - -whileTestSpec1 : (c10 : ℕ) → (e1 : Env ) → vari e1 ≡ c10 → ⊤ -whileTestSpec1 _ _ x = tt - -proofGears : {c10 : ℕ } → ⊤ -proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 p3 → whileTestSpec1 c10 n2 p3 ))) - --- ↓PreCondition(Invaliant) -whileLoopSeg : {l : Level} {t : Set l} → {c10 : ℕ } → (env : Env) → ((varn env) + (vari env) ≡ c10) - → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t) - → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t -whileLoopSeg env proof next exit with ( suc zero ≤? (varn env) ) -whileLoopSeg {_} {_} {c10} env proof next exit | no p = exit env ( begin - vari env ≡⟨ refl ⟩ - 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 (varn env) p) where - env1 = record {varn = (varn env) - 1 ; vari = (vari env) + 1} - 1<0 : 1 ≤ zero → ⊥ - 1<0 () - 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) - 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 - ∎ - -open import Relation.Binary.Definitions - -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 < 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 (≤-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< 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 lt1 eq lt1 - ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) - -proofGearsTerm : {c10 : ℕ } → ⊤ -proofGearsTerm {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → TerminatingLoop (varn n1) n1 refl p2 (λ n2 p3 → whileTestSpec1 c10 n2 p3 ))) - -TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → (Invraiant : Index → Set ) → (ExitCond : Index → Set) → ( reduce : Index → ℕ) - → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → (exit : (re : Index) → ExitCond re → t) → t) - → (i : ℕ) → (r : Index) → reduce r ≡ i → (p : Invraiant r) → (exit : (re : Index) → ExitCond re → t) → t -TerminatingLoopS {_} {t} Index Invraiant ExitCond reduce loop i r refl p exit with <-cmp 0 i -... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) exit -... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 i r r1 (≤-step lt1) p1 lt1 ) exit where - TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t - TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) exit - TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) - ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt - ... | tri≈ ¬a b ¬c = loop r1 p1 lemma4 exit where - lemma4 : (r2 : Index) → Invraiant r2 → reduce r2 < reduce r1 → t - lemma4 r2 p2 lt1 = TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 - ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) - -proofGearsTermS : {c10 : ℕ } → ⊤ -proofGearsTermS {c10} = whileTest' {_} {_} {c10} (λ n p → conversion1 n p (λ n1 p1 → - TerminatingLoopS Env (λ env → varn env + vari env ≡ c10) (λ e1 → vari e1 ≡ c10) (λ env → varn env) - (λ n2 p2 loop exit → whileLoopSeg {_} {_} {c10} n2 p2 loop exit) (varn n1) n1 refl p1 (λ ne pe → whileTestSpec1 c10 ne pe))) - - - - - - - -
--- a/whileTestPrim.agda Mon Nov 01 08:34:07 2021 +0900 +++ b/whileTestPrim.agda Mon Nov 01 09:59:43 2021 +0900 @@ -1,7 +1,7 @@ module whileTestPrim 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)
--- a/whileTestPrimProof.agda Mon Nov 01 08:34:07 2021 +0900 +++ b/whileTestPrimProof.agda Mon Nov 01 09:59:43 2021 +0900 @@ -1,7 +1,7 @@ module whileTestPrimProof 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)