Mercurial > hg > Papers > 2021 > soto-prosym
view Paper/src/agda/hoare-while.agda @ 14:393c839f987b default tip
DONE
author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 08 Jan 2022 12:41:39 +0900 (2022-01-08) |
parents | c59202657321 |
children |
line wrap: on
line source
module hoare-while where open import Data.Nat open import Level renaming ( suc to succ ; zero to Zero ) open import Data.Nat.Properties as NatProp -- <-cmp open import Relation.Binary record Envc : Set (succ Zero) where field c10 : ℕ varn : ℕ vari : ℕ open Envc whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (next : 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 (varn env) ... | zero = exit env ... | suc n = exit (record env { varn = n ; vari = (suc n) }) {-# 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 Data.Empty --open import Relation.Nullary using (¬_; Dec; yes; no) --open import Agda.Builtin.Unit open import utilities open import Relation.Binary.PropositionalEquality open _/\_ data whileTestState : Set where s1 : whileTestState s2 : whileTestState sf : whileTestState 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 ) 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 ∎ 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)) whileTestPSemSound : (c : ℕ ) (output : Envc ) → output ≡ whileTestP c (λ e → e) → ⊤ implies ((vari output ≡ 0) /\ (varn output ≡ c)) whileTestPSemSound c output refl = whileTestPSem c