# HG changeset patch # User soto@cr.ie.u-ryukyu.ac.jp # Date 1602579702 -32400 # Node ID f5705a66e9ea4b971705238c0cec4072b5e6102c diff -r 000000000000 -r f5705a66e9ea .DS_Store Binary file .DS_Store has changed diff -r 000000000000 -r f5705a66e9ea Hoare.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Hoare.agda Tue Oct 13 18:01:42 2020 +0900 @@ -0,0 +1,76 @@ +module Hoare + (PrimComm : Set) + (Cond : Set) + (Axiom : Cond -> PrimComm -> Cond -> Set) + (Tautology : Cond -> Cond -> Set) + (_and_ : Cond -> Cond -> Cond) + (neg : Cond -> Cond ) + where + +-- Hoare Logicでのコマンドを表しているらしい +data Comm : Set where + Skip : Comm　-- 何もしない。 + Abort : Comm -- 中断 + PComm : PrimComm → Comm -- PrimCommを受けてコマンドを返す + Seq : Comm → Comm → Comm -- コマンドの実行結果をさらに次のコマンドの引数として渡す + If : Cond → Comm → Comm → Comm -- Condにより実行するコマンドを分岐する + While : Cond → Comm → Comm -- Condとコマンドを受け取り、Condがtrueである間コマンドを繰り返し実行するコマンド + +{- + prPre pr prPost + ------------- ------------------ ---------------- + bPre => bPre' {bPre'} c {bPost'} bPost' => bPost +Weakening : ---------------------------------------------------- + {bPre} c {bPost} + +Assign: ---------------------------- + {bPost[v<-e]} v:=e {bPost} + + pr1 pr2 + ----------------- ------------------ + {bPre} cm1 {bMid} {bMid} cm2 {bPost} +Seq: --------------------------------------- + {bPre} cm1 ; cm2 {bPost} + + pr1 pr2 + ----------------------- --------------------------- + {bPre /\ c} cm1 {bPost} {bPre /\ neg c} cm2 {bPost} +If: ------------------------------------------------------ + {bPre} If c then cm1 else cm2 fi {bPost} + + pr + ------------------- + {inv /\ c} cm {inv} +While: --------------------------------------- + {inv} while c do cm od {inv /\ neg c} +-} + + +data HTProof : Cond -> Comm -> Cond -> Set where + PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} -> + (pr : Axiom bPre pcm bPost) -> + HTProof bPre (PComm pcm) bPost + SkipRule : (b : Cond) -> HTProof b Skip b + AbortRule : (bPre : Cond) -> (bPost : Cond) -> + HTProof bPre Abort bPost + WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} -> + {bPost' : Cond} -> {bPost : Cond} -> + Tautology bPre bPre' -> + HTProof bPre' cm bPost' -> + Tautology bPost' bPost -> + HTProof bPre cm bPost + SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} -> + {cm2 : Comm} -> {bPost : Cond} -> + HTProof bPre cm1 bMid -> + HTProof bMid cm2 bPost -> + HTProof bPre (Seq cm1 cm2) bPost + IfRule : {cmThen : Comm} -> {cmElse : Comm} -> + {bPre : Cond} -> {bPost : Cond} -> + {b : Cond} -> + HTProof (bPre and b) cmThen bPost -> + HTProof (bPre and neg b) cmElse bPost -> + HTProof bPre (If b cmThen cmElse) bPost + WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} -> + HTProof (bInv and b) cm bInv -> + HTProof bInv (While b cm) (bInv and neg b) + diff -r 000000000000 -r f5705a66e9ea HoareSoundness.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/HoareSoundness.agda Tue Oct 13 18:01:42 2020 +0900 @@ -0,0 +1,210 @@ +{-# OPTIONS --universe-polymorphism #-} + +open import Level +open import Data.Nat +open import Data.Product +open import Data.Bool +open import Data.Empty +open import Data.Sum +open import Relation.Binary +open import Relation.Nullary +open import Relation.Binary.Core +open import Relation.Binary.PropositionalEquality +open import RelOp +open import utilities + +module HoareSoundness + (Cond : Set) + (PrimComm : Set) + (neg : Cond -> Cond) + (_/\_ : Cond -> Cond -> Cond) + (Tautology : Cond -> Cond -> Set) + (State : Set) + (SemCond : Cond -> State -> Set) + (tautValid : (b1 b2 : Cond) -> Tautology b1 b2 -> + (s : State) -> SemCond b1 s -> SemCond b2 s) + (respNeg : (b : Cond) -> (s : State) -> + Iff (SemCond (neg b) s) (¬ SemCond b s)) + (respAnd : (b1 b2 : Cond) -> (s : State) -> + Iff (SemCond (b1 /\ b2) s) + ((SemCond b1 s) × (SemCond b2 s))) + (PrimSemComm : ∀ {l} -> PrimComm -> Rel State l) + (Axiom : Cond -> PrimComm -> Cond -> Set) + (axiomValid : ∀ {l} -> (bPre : Cond) -> (pcm : PrimComm) -> (bPost : Cond) -> + (ax : Axiom bPre pcm bPost) -> (s1 s2 : State) -> + SemCond bPre s1 -> PrimSemComm {l} pcm s1 s2 -> SemCond bPost s2) where + +open import Hoare PrimComm Cond Axiom Tautology _/\_ neg + +open import RelOp +module RelOpState = RelOp State + +NotP : {S : Set} -> Pred S -> Pred S +NotP X s = ¬ X s + +_\/_ : Cond -> Cond -> Cond +b1 \/ b2 = neg (neg b1 /\ neg b2) + +when : {X Y Z : Set} -> (X -> Z) -> (Y -> Z) -> + X ⊎ Y -> Z +when f g (inj₁ x) = f x +when f g (inj₂ y) = g y + +{- +SemComm' : Comm -> Rel State (Level.zero) +SemComm' Skip = {!!} +SemComm' Abort = {!!} +SemComm' (PComm pc) = {!!} +SemComm' (Seq c1 c2) = {!!} +SemComm' (If b c1 c2) = {!!} +SemComm' (While b c) = {!!} +-} + +-- semantics of commands +SemComm : Comm -> Rel State (Level.zero) +SemComm Skip = RelOpState.deltaGlob +SemComm Abort = RelOpState.emptyRel +SemComm (PComm pc) = PrimSemComm pc +SemComm (Seq c1 c2) = RelOpState.comp (SemComm c1) (SemComm c2) +SemComm (If b c1 c2) + = RelOpState.union + (RelOpState.comp (RelOpState.delta (SemCond b)) + (SemComm c1)) + (RelOpState.comp (RelOpState.delta (NotP (SemCond b))) + (SemComm c2)) +SemComm (While b c) + = RelOpState.unionInf + (λ (n : ℕ) -> + RelOpState.comp (RelOpState.repeat + n + (RelOpState.comp + (RelOpState.delta (SemCond b)) + (SemComm c))) + (RelOpState.delta (NotP (SemCond b)))) + +-- 入力として入ってくるのは((s1 : State) -> (s2 : State) -> SemCond bPre s1 -> SemComm cm s1 s2)の部分 +-- +Satisfies : Cond -> Comm -> Cond -> Set +Satisfies bPre cm bPost + = (s1 : State) -> (s2 : State) -> + SemCond bPre s1 -> SemComm cm s1 s2 -> SemCond bPost s2 + +Soundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} -> + HTProof bPre cm bPost -> Satisfies bPre cm bPost +Soundness (PrimRule {bPre} {cm} {bPost} pr) s1 s2 q1 q2 + = axiomValid bPre cm bPost pr s1 s2 q1 q2 + +Soundness {.bPost} {.Skip} {bPost} (SkipRule .bPost) s1 s2 q1 q2 + = substId1 State {Level.zero} {State} {s1} {s2} (proj₂ q2) (SemCond bPost) q1 +Soundness {bPre} {.Abort} {bPost} (AbortRule .bPre .bPost) s1 s2 q1 () +Soundness (WeakeningRule {bPre} {bPre'} {cm} {bPost'} {bPost} tautPre pr tautPost) + s1 s2 q1 q2 + = let hyp : Satisfies bPre' cm bPost' + hyp = Soundness pr + r1 : SemCond bPre' s1 + r1 = tautValid bPre bPre' tautPre s1 q1 + r2 : SemCond bPost' s2 + r2 = hyp s1 s2 r1 q2 + in tautValid bPost' bPost tautPost s2 r2 +Soundness (SeqRule {bPre} {cm1} {bMid} {cm2} {bPost} pr1 pr2) + s1 s2 q1 q2 + = let hyp1 : Satisfies bPre cm1 bMid + hyp1 = Soundness pr1 + hyp2 : Satisfies bMid cm2 bPost + hyp2 = Soundness pr2 + sMid : State + sMid = proj₁ q2 + r1 : SemComm cm1 s1 sMid × SemComm cm2 sMid s2 + r1 = proj₂ q2 + r2 : SemComm cm1 s1 sMid + r2 = proj₁ r1 + r3 : SemComm cm2 sMid s2 + r3 = proj₂ r1 + r4 : SemCond bMid sMid + r4 = hyp1 s1 sMid q1 r2 + in hyp2 sMid s2 r4 r3 +Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse) + s1 s2 q1 q2 + = let hypThen : Satisfies (bPre /\ b) cmThen bPost + hypThen = Soundness pThen + hypElse : Satisfies (bPre /\ neg b) cmElse bPost + hypElse = Soundness pElse + rThen : RelOpState.comp + (RelOpState.delta (SemCond b)) + (SemComm cmThen) s1 s2 -> + SemCond bPost s2 + rThen = λ h -> + let t1 : SemCond b s1 × SemComm cmThen s1 s2 + t1 = (proj₂ (RelOpState.deltaRestPre + (SemCond b) + (SemComm cmThen) s1 s2)) h + t2 : SemCond (bPre /\ b) s1 + t2 = (proj₂ (respAnd bPre b s1)) + (q1 , proj₁ t1) + in hypThen s1 s2 t2 (proj₂ t1) + rElse : RelOpState.comp + (RelOpState.delta (NotP (SemCond b))) + (SemComm cmElse) s1 s2 -> + SemCond bPost s2 + rElse = λ h -> + let t10 : (NotP (SemCond b) s1) × + (SemComm cmElse s1 s2) + t10 = proj₂ (RelOpState.deltaRestPre + (NotP (SemCond b)) (SemComm cmElse) s1 s2) + h + t6 : SemCond (neg b) s1 + t6 = proj₂ (respNeg b s1) (proj₁ t10) + t7 : SemComm cmElse s1 s2 + t7 = proj₂ t10 + t8 : SemCond (bPre /\ neg b) s1 + t8 = proj₂ (respAnd bPre (neg b) s1) + (q1 , t6) + in hypElse s1 s2 t8 t7 + in when rThen rElse q2 +Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2 + = proj₂ (respAnd bInv (neg b) s2) t20 + where + hyp : Satisfies (bInv /\ b) cm' bInv + hyp = Soundness pr + n : ℕ + n = proj₁ q2 + Rel1 : ℕ -> Rel State (Level.zero) + Rel1 = λ m -> + RelOpState.repeat + m + (RelOpState.comp (RelOpState.delta (SemCond b)) + (SemComm cm')) + t1 : RelOpState.comp + (Rel1 n) + (RelOpState.delta (NotP (SemCond b))) s1 s2 + t1 = proj₂ q2 + t15 : (Rel1 n s1 s2) × (NotP (SemCond b) s2) + t15 = proj₂ (RelOpState.deltaRestPost + (NotP (SemCond b)) (Rel1 n) s1 s2) + t1 + t16 : Rel1 n s1 s2 + t16 = proj₁ t15 + t17 : NotP (SemCond b) s2 + t17 = proj₂ t15 + lem1 : (m : ℕ) -> (ss2 : State) -> Rel1 m s1 ss2 -> + SemCond bInv ss2 + lem1 ℕ.zero ss2 h + = substId1 State (proj₂ h) (SemCond bInv) q1 + lem1 (ℕ.suc n) ss2 h + = let hyp2 : (z : State) -> Rel1 n s1 z -> + SemCond bInv z + hyp2 = lem1 n + s20 : State + s20 = proj₁ h + t21 : Rel1 n s1 s20 + t21 = proj₁ (proj₂ h) + t22 : (SemCond b s20) × (SemComm cm' s20 ss2) + t22 = proj₂ (RelOpState.deltaRestPre + (SemCond b) (SemComm cm') s20 ss2) + (proj₂ (proj₂ h)) + t23 : SemCond (bInv /\ b) s20 + t23 = proj₂ (respAnd bInv b s20) + (hyp2 s20 t21 , proj₁ t22) + in hyp s20 ss2 t23 (proj₂ t22) + t20 : SemCond bInv s2 × SemCond (neg b) s2 + t20 = lem1 n s2 t16 , proj₂ (respNeg b s2) t17 diff -r 000000000000 -r f5705a66e9ea RelOp.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/RelOp.agda Tue Oct 13 18:01:42 2020 +0900 @@ -0,0 +1,81 @@ +{-# OPTIONS --universe-polymorphism #-} + +open import Level +open import Data.Empty +open import Data.Product +open import Data.Nat +open import Data.Sum +open import Data.Unit +open import Relation.Binary +open import Relation.Binary.Core +open import Relation.Nullary +open import utilities + +module RelOp (S : Set) where + +data Id {l} {X : Set} : Rel X l where + ref : {x : X} -> Id x x + +-- substId1 | x == y & P(x) => P(y) +substId1 : ∀ {l} -> {X : Set} -> {x y : X} -> + Id {l} x y -> (P : Pred X) -> P x -> P y +substId1 ref P q = q + +-- substId2 | x == y & P(y) => P(x) +substId2 : ∀ {l} -> {X : Set} -> {x y : X} -> + Id {l} x y -> (P : Pred X) -> P y -> P x +substId2 ref P q = q + +-- for X ⊆ S (formally, X : Pred S) +-- delta X = { (a, a) | a ∈ X } +delta : ∀ {l} -> Pred S -> Rel S l +delta X a b = X a × Id a b + +-- deltaGlob = delta S +deltaGlob : ∀ {l} -> Rel S l +deltaGlob = delta (λ (s : S) → ⊤) + +-- emptyRel = \varnothing +emptyRel : Rel S Level.zero +emptyRel a b = ⊥ + +-- comp R1 R2 = R2 ∘ R1 (= R1; R2) +comp : ∀ {l} -> Rel S l -> Rel S l -> Rel S l +comp R1 R2 a b = ∃ (λ (a' : S) → R1 a a' × R2 a' b) + +-- union R1 R2 = R1 ∪ R2 +union : ∀ {l} -> Rel S l -> Rel S l -> Rel S l +union R1 R2 a b = R1 a b ⊎ R2 a b + +-- repeat n R = R^n +repeat : ∀ {l} -> ℕ -> Rel S l -> Rel S l +repeat ℕ.zero R = deltaGlob +repeat (ℕ.suc m) R = comp (repeat m R) R + +-- unionInf f = ⋃_{n ∈ ω} f(n) +unionInf : ∀ {l} -> (ℕ -> Rel S l) -> Rel S l +unionInf f a b = ∃ (λ (n : ℕ) → f n a b) +-- restPre X R = { (s1,s2) ∈ R | s1 ∈ X } +restPre : ∀ {l} -> Pred S -> Rel S l -> Rel S l +restPre X R a b = X a × R a b + +-- restPost X R = { (s1,s2) ∈ R | s2 ∈ X } +restPost : ∀ {l} -> Pred S -> Rel S l -> Rel S l +restPost X R a b = R a b × X b + +deltaRestPre : (X : Pred S) -> (R : Rel S Level.zero) -> (a b : S) -> + Iff (restPre X R a b) (comp (delta X) R a b) +deltaRestPre X R a b + = (λ (h : restPre X R a b) → a , (proj₁ h , ref) , proj₂ h) , + λ (h : comp (delta X) R a b) → proj₁ (proj₁ (proj₂ h)) , + substId2 + (proj₂ (proj₁ (proj₂ h))) + (λ z → R z b) (proj₂ (proj₂ h)) + +deltaRestPost : (X : Pred S) -> (R : Rel S Level.zero) -> (a b : S) -> + Iff (restPost X R a b) (comp R (delta X) a b) +deltaRestPost X R a b + = (λ (h : restPost X R a b) → b , proj₁ h , proj₂ h , ref) , + λ (h : comp R (delta X) a b) → + substId1 (proj₂ (proj₂ (proj₂ h))) (R a) (proj₁ (proj₂ h)) , + substId1 (proj₂ (proj₂ (proj₂ h))) X (proj₁ (proj₂ (proj₂ h))) diff -r 000000000000 -r f5705a66e9ea gearswhile.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/gearswhile.agda Tue Oct 13 18:01:42 2020 +0900 @@ -0,0 +1,59 @@ +module gearswhile where + +open import Level renaming ( suc to succ ; zero to Zero ) +open import Data.Nat +open import Relation.Binary.PropositionalEquality +open import Data.Nat.Properties +open import Relation.Binary.Definitions +open import Data.Empty + +open import utilities +open _/\_ + +record Envc : Set (succ Zero) where + field + c10 : ℕ + varn : ℕ + vari : ℕ +open Envc + +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) + + +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 + ∎ diff -r 000000000000 -r f5705a66e9ea gearswhilehoare.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/gearswhilehoare.agda Tue Oct 13 18:01:42 2020 +0900 @@ -0,0 +1,239 @@ +module gearswhilehoare where + +open import Level renaming ( suc to succ ; zero to Zero ) +open import Data.Nat +open import Data.Empty +open import Data.Nat.Properties +open import Relation.Nullary using (¬_; Dec; yes; no) + +open import Agda.Builtin.Unit + +open import Relation.Binary +open import utilities +open _/\_ + +open import Relation.Binary.PropositionalEquality + + +record Envc : Set (succ Zero) where + field + c10 : ℕ + varn : ℕ + vari : ℕ +open Envc + +whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Envc → t) → t +whileTestP c10 next = next (record {varn = c10 ; vari = 0 ; c10 = 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 }) + +-- 停止するループ +loopP’ : {l : Level} {t : Set l} → Envc → (exit : Envc → t) → t +loopP’ record { c10 = c10 ; varn = zero ; vari = vari } exit = + exit (record { c10 = c10 ; varn = zero ; vari = vari }) +loopP’ record { c10 = c10 ; varn = (suc varn1) ; vari = vari } exit = whileLoopP' (record { c10 = c10 ; varn = (suc varn1) ; vari = vari }) (λ env → loopP’ (record { c10 = c10 ; varn = varn1 ; vari = vari }) exit ) exit + +whileTestPCall’ : (c10 : ℕ ) → Envc +whileTestPCall’ c10 = whileTestP {_} {_} c10 (λ env → loopP’ env (λ env → env)) + +-- 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)) + +-- whileTestPCall 10 +-- record { c10 = 10 ; varn = 0 ; vari = 10 } + +record Env : Set (succ Zero) where + field + varn : ℕ + vari : ℕ +open Env + +{-# TERMINATING #-} -- ↓PreCondition(Invaliant) +whileLoop' : {l : Level} {t : Set l} → (env : Env ) → {c10 : ℕ } → ((varn env) + (vari env) ≡ c10) → (Code : Env → 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} + 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 + ∎ + +-- +-- codeGears with states of condition +-- +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} → (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)) + + +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)) + + + +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 + ∎ + +{-# 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 + +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 + +whileTestPSem : (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)) diff -r 000000000000 -r f5705a66e9ea utilities.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/utilities.agda Tue Oct 13 18:01:42 2020 +0900 @@ -0,0 +1,171 @@ +{-# OPTIONS --allow-unsolved-metas #-} +module utilities where + +open import Function +open import Data.Nat +open import Data.Product +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 + +Pred : Set -> Set₁ +Pred X = X -> Set + +Imply : Set -> Set -> Set +Imply X Y = X -> Y + +Iff : Set -> Set -> Set +Iff X Y = Imply X Y × Imply Y X + +record _/\_ {n : Level } (a : Set n) (b : Set n): Set n where + field + pi1 : a + pi2 : b + +open _/\_ + +_-_ : ℕ → ℕ → ℕ +x - zero = x +zero - _ = zero +(suc x) - (suc y) = x - y + ++zero : { y : ℕ } → y + zero ≡ y ++zero {zero} = refl ++zero {suc y} = cong ( λ x → suc x ) ( +zero {y} ) + + ++-sym : { x y : ℕ } → x + y ≡ y + x ++-sym {zero} {zero} = refl ++-sym {zero} {suc y} = let open ≡-Reasoning in + begin + zero + suc y + ≡⟨⟩ + suc y + ≡⟨ sym +zero ⟩ + suc y + zero + ∎ ++-sym {suc x} {zero} = let open ≡-Reasoning in + begin + suc x + zero + ≡⟨ +zero ⟩ + suc x + ≡⟨⟩ + zero + suc x + ∎ ++-sym {suc x} {suc y} = cong ( λ z → suc z ) ( let open ≡-Reasoning in + begin + x + suc y + ≡⟨ +-sym {x} {suc y} ⟩ + suc (y + x) + ≡⟨ cong ( λ z → suc z ) (+-sym {y} {x}) ⟩ + suc (x + y) + ≡⟨ sym ( +-sym {y} {suc x}) ⟩ + y + suc x + ∎ ) + + +minus-plus : { x y : ℕ } → (suc x - 1) + (y + 1) ≡ suc x + y +minus-plus {zero} {y} = +-sym {y} {1} +minus-plus {suc x} {y} = cong ( λ z → suc z ) (minus-plus {x} {y}) + ++1≡suc : { x : ℕ } → x + 1 ≡ suc x ++1≡suc {zero} = refl ++1≡suc {suc x} = cong ( λ z → suc z ) ( +1≡suc {x} ) + +lt : ℕ → ℕ → Bool +lt x y with (suc x ) ≤? y +lt x y | yes p = true +lt x y | no ¬p = false + +predℕ : {n : ℕ } → lt 0 n ≡ true → ℕ +predℕ {zero} () +predℕ {suc n} refl = n + +predℕ+1=n : {n : ℕ } → (less : lt 0 n ≡ true ) → (predℕ less) + 1 ≡ n +predℕ+1=n {zero} () +predℕ+1=n {suc n} refl = +1≡suc + +suc-predℕ=n : {n : ℕ } → (less : lt 0 n ≡ true ) → suc (predℕ less) ≡ n +suc-predℕ=n {zero} () +suc-predℕ=n {suc n} refl = refl + +Equal : ℕ → ℕ → Bool +Equal x y with x ≟ y +Equal x y | yes p = true +Equal x y | no ¬p = false + +_⇒_ : Bool → Bool → Bool +false ⇒ _ = true +true ⇒ true = true +true ⇒ false = false + +⇒t : {x : Bool} → x ⇒ true ≡ true +⇒t {x} with x +⇒t {x} | false = refl +⇒t {x} | true = refl + +f⇒ : {x : Bool} → false ⇒ x ≡ true +f⇒ {x} with x +f⇒ {x} | false = refl +f⇒ {x} | true = refl + +∧-pi1 : { x y : Bool } → x ∧ y ≡ true → x ≡ true +∧-pi1 {x} {y} eq with x | y | eq +∧-pi1 {x} {y} eq | false | b | () +∧-pi1 {x} {y} eq | true | false | () +∧-pi1 {x} {y} eq | true | true | refl = refl + +∧-pi2 : { x y : Bool } → x ∧ y ≡ true → y ≡ true +∧-pi2 {x} {y} eq with x | y | eq +∧-pi2 {x} {y} eq | false | b | () +∧-pi2 {x} {y} eq | true | false | () +∧-pi2 {x} {y} eq | true | true | refl = refl + +∧true : { x : Bool } → x ∧ true ≡ x +∧true {x} with x +∧true {x} | false = refl +∧true {x} | true = refl + +true∧ : { x : Bool } → true ∧ x ≡ x +true∧ {x} with x +true∧ {x} | false = refl +true∧ {x} | true = refl +bool-case : ( x : Bool ) { p : Set } → ( x ≡ true → p ) → ( x ≡ false → p ) → p +bool-case x T F with x +bool-case x T F | false = F refl +bool-case x T F | true = T refl + +impl⇒ : {x y : Bool} → (x ≡ true → y ≡ true ) → x ⇒ y ≡ true +impl⇒ {x} {y} p = bool-case x (λ x=t → let open ≡-Reasoning in + begin + x ⇒ y + ≡⟨ cong ( λ z → x ⇒ z ) (p x=t ) ⟩ + x ⇒ true + ≡⟨ ⇒t ⟩ + true + ∎ + ) ( λ x=f → let open ≡-Reasoning in + begin + x ⇒ y + ≡⟨ cong ( λ z → z ⇒ y ) x=f ⟩ + true + ∎ + ) + +Equal→≡ : { x y : ℕ } → Equal x y ≡ true → x ≡ y +Equal→≡ {x} {y} eq with x ≟ y +Equal→≡ {x} {y} refl | yes refl = refl +Equal→≡ {x} {y} () | no ¬p + +Equal+1 : { x y : ℕ } → Equal x y ≡ Equal (suc x) (suc y) +Equal+1 {x} {y} with x ≟ y +Equal+1 {x} {.x} | yes refl = {!!} +Equal+1 {x} {y} | no ¬p = {!!} + +open import Data.Empty + +≡→Equal : { x y : ℕ } → x ≡ y → Equal x y ≡ true +≡→Equal {x} {.x} refl with x ≟ x +≡→Equal {x} {.x} refl | yes refl = refl +≡→Equal {x} {.x} refl | no ¬p = ⊥-elim ( ¬p refl ) diff -r 000000000000 -r f5705a66e9ea whileimple.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/whileimple.agda Tue Oct 13 18:01:42 2020 +0900 @@ -0,0 +1,109 @@ +module whilespecimple where + +open import Relation.Binary.PropositionalEquality +open import Data.Bool +open import Relation.Binary +open import Relation.Nullary using (¬_; Dec; yes; no) +open import Data.Empty +open import Agda.Builtin.Sigma +open import Data.Product +open import Data.Nat + + +open import utilities hiding ( _/\_ ) +open import whiletest +open import Hoare PrimComm Cond Axiom Tautology _and_ neg +open import whilespec + +State : Set +State = Env + +open import RelOp +module RelOpState = RelOp State + + +SemCond : Cond -> State -> Set +SemCond c p = c p ≡ true + +PrimSemComm : ∀ {l} -> PrimComm -> Rel State l +PrimSemComm prim s1 s2 = Id State (prim s1) s2 + +tautValid : (b1 b2 : Cond) -> Tautology b1 b2 -> (s : State) -> SemCond b1 s -> SemCond b2 s +tautValid b1 b2 taut s cond with b1 s | b2 s | taut s +tautValid b1 b2 taut s () | false | false | refl +tautValid b1 b2 taut s _ | false | true | refl = refl +tautValid b1 b2 taut s _ | true | false | () +tautValid b1 b2 taut s _ | true | true | refl = refl + + +axiomValid : ∀ {l} -> (bPre : Cond) -> (pcm : PrimComm) -> (bPost : Cond) -> + (ax : Axiom bPre pcm bPost) -> (s1 s2 : State) -> + SemCond bPre s1 -> PrimSemComm {l} pcm s1 s2 -> SemCond bPost s2 +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref with bPre s1 | bPost (pcm s1) | ax s1 +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) () ref | false | false | refl +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | false | true | refl = refl +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | false | () +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | true | refl = refl + + +respNeg : (b : Cond) -> (s : State) -> + Iff (SemCond (neg b) s) (¬ SemCond b s) +respNeg b s = ( left , right ) where + left : not (b s) ≡ true → (b s) ≡ true → ⊥ + left ne with b s + left refl | false = λ () + left () | true + right : ((b s) ≡ true → ⊥) → not (b s) ≡ true + right ne with b s + right ne | false = refl + right ne | true = ⊥-elim ( ne refl ) + +_/\_ : Cond -> Cond -> Cond +b1 /\ b2 = b1 and b2 + +_\/_ : Cond -> Cond -> Cond +b1 \/ b2 = neg (neg b1 /\ neg b2) + +respAnd : (b1 b2 : Cond) -> (s : State) -> + Iff (SemCond (b1 /\ b2) s) + ((SemCond b1 s) × (SemCond b2 s)) +respAnd b1 b2 s = ( left , right ) where + left : b1 s ∧ b2 s ≡ true → (b1 s ≡ true) × (b2 s ≡ true) + left and with b1 s | b2 s + left () | false | false + left () | false | true + left () | true | false + left refl | true | true = ( refl , refl ) + right : (b1 s ≡ true) × (b2 s ≡ true) → b1 s ∧ b2 s ≡ true + right ( x1 , x2 ) with b1 s | b2 s + right (() , ()) | false | false + right (() , _) | false | true + right (_ , ()) | true | false + right (refl , refl) | true | true = refl + + +open import HoareSoundness + Cond + PrimComm + neg + _and_ + Tautology + State + SemCond + tautValid + respNeg + respAnd + PrimSemComm + Axiom + axiomValid + +PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} -> + HTProof bPre cm bPost -> Satisfies bPre cm bPost +PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht + + +proofOfProgram : (c10 : ℕ) → (input output : Env ) + → initCond input ≡ true + → (SemComm (program c10) input output) + → termCond {c10} output ≡ true +proofOfProgram c10 input output ic sem = PrimSoundness (proof1 c10) input output ic sem diff -r 000000000000 -r f5705a66e9ea whileploof.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/whileploof.agda Tue Oct 13 18:01:42 2020 +0900 @@ -0,0 +1,164 @@ +module whilespecification where + +open import Function +open import Data.Nat +open import Data.Bool +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 Data.Nat.Properties + +open import utilities hiding ( _/\_ ) +open import whiletest + +open import Hoare PrimComm Cond Axiom Tautology _and_ neg + +open Env + +initCond : Cond +initCond env = true + +termCond : {c10 : ℕ} → Cond +termCond {c10} env = Equal (vari env) c10 + +stmt1Cond : {c10 : ℕ} → Cond +stmt1Cond {c10} env = Equal (varn env) c10 + +init-case : {c10 : ℕ} → (env : Env) → (( λ e → true ⇒ stmt1Cond {c10} e ) (record { varn = c10 ; vari = vari env }) ) ≡ true +init-case {c10} _ = impl⇒ ( λ cond → ≡→Equal refl ) + +stmt2Cond : {c10 : ℕ} → Cond +stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0) + +whileInv : {c10 : ℕ} → Cond +whileInv {c10} env = Equal ((varn env) + (vari env)) c10 + +whileInv' : {c10 : ℕ} → Cond +whileInv'{c10} env = Equal ((varn env) + (vari env)) (suc c10) ∧ lt zero (varn env) + +lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10}) +lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in + begin + (Equal (varn env) c10 ) ∧ true + ≡⟨ ∧true ⟩ + Equal (varn env) c10 + ≡⟨ cond ⟩ + true + ∎ ) + + +proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10}) +proof1 c10 = + SeqRule {λ e → true} ( PrimRule (init-case {c10} )) + $ SeqRule {λ e → Equal (varn e) c10} ( PrimRule lemma1 ) + $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)} lemma2 ( + WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10} + $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) + $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 + where + lemma21 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env ≡ c10 + lemma21 eq = Equal→≡ (∧-pi1 eq) + lemma22 : {env : Env } → {c10 : ℕ} → stmt2Cond {c10} env ≡ true → vari env ≡ 0 + lemma22 eq = Equal→≡ (∧-pi2 eq) + lemma23 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env + vari env ≡ c10 + lemma23 {env} {c10} eq = let open ≡-Reasoning in + begin + varn env + vari env + ≡⟨ cong ( \ x -> x + vari env ) (lemma21 eq ) ⟩ + c10 + vari env + ≡⟨ cong ( \ x -> c10 + x) (lemma22 {env} {c10} eq ) ⟩ + c10 + 0 + ≡⟨ +-sym {c10} {0} ⟩ + 0 + c10 + ≡⟨⟩ + c10 + ∎ + lemma2 : {c10 : ℕ} → Tautology stmt2Cond whileInv + lemma2 {c10} env = bool-case (stmt2Cond env) ( + λ eq → let open ≡-Reasoning in + begin + (stmt2Cond env) ⇒ (whileInv env) + ≡⟨⟩ + (stmt2Cond env) ⇒ ( Equal (varn env + vari env) c10 ) + ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ ( Equal x c10 ) ) ( lemma23 {env} eq ) ⟩ + (stmt2Cond env) ⇒ (Equal c10 c10) + ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ x ) (≡→Equal refl ) ⟩ + (stmt2Cond {c10} env) ⇒ true + ≡⟨ ⇒t ⟩ + true + ∎ + ) ( + λ ne → let open ≡-Reasoning in + begin + (stmt2Cond env) ⇒ (whileInv env) + ≡⟨ cong ( \ x -> x ⇒ (whileInv env) ) ne ⟩ + false ⇒ (whileInv {c10} env) + ≡⟨ f⇒ {whileInv {c10} env} ⟩ + true + ∎ + ) + lemma3 : Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv' + lemma3 env = impl⇒ ( λ cond → let open ≡-Reasoning in + begin + whileInv' (record { varn = varn env ; vari = vari env + 1 }) + ≡⟨⟩ + Equal (varn env + (vari env + 1)) (suc c10) ∧ (lt 0 (varn env) ) + ≡⟨ cong ( λ z → Equal (varn env + (vari env + 1)) (suc c10) ∧ z ) (∧-pi2 cond ) ⟩ + Equal (varn env + (vari env + 1)) (suc c10) ∧ true + ≡⟨ ∧true ⟩ + Equal (varn env + (vari env + 1)) (suc c10) + ≡⟨ cong ( \ x -> Equal x (suc c10) ) (sym (+-assoc (varn env) (vari env) 1)) ⟩ + Equal ((varn env + vari env) + 1) (suc c10) + ≡⟨ cong ( \ x -> Equal x (suc c10) ) +1≡suc ⟩ + Equal (suc (varn env + vari env)) (suc c10) + ≡⟨ sym Equal+1 ⟩ + Equal ((varn env + vari env) ) c10 + ≡⟨ ∧-pi1 cond ⟩ + true + ∎ ) + lemma41 : (env : Env ) → {c10 : ℕ} → (varn env + vari env) ≡ (suc c10) → lt 0 (varn env) ≡ true → Equal ((varn env - 1) + vari env) c10 ≡ true + lemma41 env {c10} c1 c2 = let open ≡-Reasoning in + begin + Equal ((varn env - 1) + vari env) c10 + ≡⟨ cong ( λ z → Equal ((z - 1 ) + vari env ) c10 ) (sym (suc-predℕ=n c2) ) ⟩ + Equal ((suc (predℕ {varn env} c2 ) - 1) + vari env) c10 + ≡⟨⟩ + Equal ((predℕ {varn env} c2 ) + vari env) c10 + ≡⟨ Equal+1 ⟩ + Equal ((suc (predℕ {varn env} c2 )) + vari env) (suc c10) + ≡⟨ cong ( λ z → Equal (z + vari env ) (suc c10) ) (suc-predℕ=n c2 ) ⟩ + Equal (varn env + vari env) (suc c10) + ≡⟨ cong ( λ z → (Equal z (suc c10) )) c1 ⟩ + Equal (suc c10) (suc c10) + ≡⟨ ≡→Equal refl ⟩ + true + ∎ + lemma4 : {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv + lemma4 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in + begin + whileInv (record { varn = varn env - 1 ; vari = vari env }) + ≡⟨⟩ + Equal ((varn env - 1) + vari env) c10 + ≡⟨ lemma41 env (Equal→≡ (∧-pi1 cond)) (∧-pi2 cond) ⟩ + true + ∎ + ) + lemma51 : (z : Env ) → neg (λ z → lt zero (varn z)) z ≡ true → varn z ≡ zero + lemma51 z cond with varn z + lemma51 z refl | zero = refl + lemma51 z () | suc x + lemma5 : {c10 : ℕ} → Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond + lemma5 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in + begin + termCond env + ≡⟨⟩ + Equal (vari env) c10 + ≡⟨⟩ + Equal (zero + vari env) c10 + ≡⟨ cong ( λ z → Equal (z + vari env) c10 ) (sym ( lemma51 env ( ∧-pi2 cond ) )) ⟩ + Equal (varn env + vari env) c10 + ≡⟨ ∧-pi1 cond ⟩ + true + ∎ + ) diff -r 000000000000 -r f5705a66e9ea whilespec.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/whilespec.agda Tue Oct 13 18:01:42 2020 +0900 @@ -0,0 +1,178 @@ +module whilespec where + +open import Function +open import Data.Nat +open import Data.Bool +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 Data.Nat.Properties + +open import utilities hiding ( _/\_ ) +open import whiletest + +open import Hoare PrimComm Cond Axiom Tautology _and_ neg + +open Env + +initCond : Cond +initCond env = true + +termCond : {c10 : ℕ} → Cond +termCond {c10} env = Equal (vari env) c10 + +stmt1Cond : {c10 : ℕ} → Cond +stmt1Cond {c10} env = Equal (varn env) c10 + +init-case : {c10 : ℕ} → (env : Env) → (( λ e → true ⇒ stmt1Cond {c10} e ) (record { varn = c10 ; vari = vari env }) ) ≡ true +init-case {c10} _ = impl⇒ ( λ cond → ≡→Equal refl ) + +stmt2Cond : {c10 : ℕ} → Cond +stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0) + +whileInv : {c10 : ℕ} → Cond +whileInv {c10} env = Equal ((varn env) + (vari env)) c10 + +whileInv' : {c10 : ℕ} → Cond +whileInv'{c10} env = (Equal ((varn env) + (vari env)) (suc c10)) ∧ lt zero (varn env) + +-- 事前条件が成り立つ場合に代入を行うと +-- 代入後の事後条件が成り立つ証明 +-- axiomはcondとprimcommとcondを受け取ってsetを返す +lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10}) +lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in + begin + (Equal (varn env) c10 ) ∧ true + ≡⟨ ∧true ⟩ + Equal (varn env) c10 + ≡⟨ cond ⟩ + true + ∎ ) + +-- proof1' : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10}) +-- proof1' c10 = SeqRule {!!} {!!} + +proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10}) +proof1 c10 = + SeqRule {λ e → true} ( PrimRule (init-case {c10} )) + $ SeqRule {λ e → Equal (varn e) c10} ( PrimRule lemma1 ) + $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)} lemma2 ( + WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10} + $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) + $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 + where + lemma21 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env ≡ c10 + lemma21 eq = Equal→≡ (∧-pi1 eq) + lemma22 : {env : Env } → {c10 : ℕ} → stmt2Cond {c10} env ≡ true → vari env ≡ 0 + lemma22 eq = Equal→≡ (∧-pi2 eq) + lemma23 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env + vari env ≡ c10 + lemma23 {env} {c10} eq = let open ≡-Reasoning in + begin + varn env + vari env + ≡⟨ cong ( \ x -> x + vari env ) (lemma21 eq ) ⟩ + c10 + vari env + ≡⟨ cong ( \ x -> c10 + x) (lemma22 {env} {c10} eq ) ⟩ + c10 + 0 + ≡⟨ +-sym {c10} {0} ⟩ + 0 + c10 + ≡⟨⟩ + c10 + ∎ + -- while loopに入る前のconditionからループ不変条件への変換の証明 + -- つまり状態の移動時の動作の証明を行なっている + lemma2 : {c10 : ℕ} → Tautology stmt2Cond whileInv + lemma2 {c10} env = bool-case (stmt2Cond env) ( + λ eq → let open ≡-Reasoning in + begin + (stmt2Cond env) ⇒ (whileInv env) + ≡⟨⟩ + (stmt2Cond env) ⇒ ( Equal (varn env + vari env) c10 ) + ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ ( Equal x c10 ) ) ( lemma23 {env} eq ) ⟩ + (stmt2Cond env) ⇒ (Equal c10 c10) + ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ x ) (≡→Equal refl ) ⟩ + (stmt2Cond {c10} env) ⇒ true + ≡⟨ ⇒t ⟩ + true + ∎ + ) ( + λ ne → let open ≡-Reasoning in + begin + (stmt2Cond env) ⇒ (whileInv env) + ≡⟨ cong ( \ x -> x ⇒ (whileInv env) ) ne ⟩ + false ⇒ (whileInv {c10} env) + ≡⟨ f⇒ {whileInv {c10} env} ⟩ + true + ∎ + ) + + -- While Loop内でのPCommの代入の証明 + -- ここで使っているwhileInvの引数が謎。引数はcondのはずなのにBoolが引数になっている気がする + lemma3 : Axiom (λ e → whileInv e ∧ lt zero (varn e)) + (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv' + lemma3 env = impl⇒ ( λ cond → let open ≡-Reasoning in + begin + whileInv' (record { varn = varn env ; vari = vari env + 1 }) + ≡⟨⟩ + Equal (varn env + (vari env + 1)) (suc c10) ∧ (lt 0 (varn env) ) + ≡⟨ cong ( λ z → Equal (varn env + (vari env + 1)) (suc c10) ∧ z ) (∧-pi2 cond ) ⟩ + Equal (varn env + (vari env + 1)) (suc c10) ∧ true + ≡⟨ ∧true ⟩ + Equal (varn env + (vari env + 1)) (suc c10) + ≡⟨ cong ( \ x -> Equal x (suc c10) ) (sym (+-assoc (varn env) (vari env) 1)) ⟩ + Equal ((varn env + vari env) + 1) (suc c10) + ≡⟨ cong ( \ x -> Equal x (suc c10) ) +1≡suc ⟩ + Equal (suc (varn env + vari env)) (suc c10) + ≡⟨ sym Equal+1 ⟩ + Equal ((varn env + vari env) ) c10 + ≡⟨ ∧-pi1 cond ⟩ + true + ∎ ) + lemma41 : (env : Env ) → {c10 : ℕ} → (varn env + vari env) ≡ (suc c10) → lt 0 (varn env) ≡ true → Equal ((varn env - 1) + vari env) c10 ≡ true + lemma41 env {c10} c1 c2 = let open ≡-Reasoning in + begin + Equal ((varn env - 1) + vari env) c10 + ≡⟨ cong ( λ z → Equal ((z - 1 ) + vari env ) c10 ) (sym (suc-predℕ=n c2) ) ⟩ + Equal ((suc (predℕ {varn env} c2 ) - 1) + vari env) c10 + ≡⟨⟩ + Equal ((predℕ {varn env} c2 ) + vari env) c10 + ≡⟨ Equal+1 ⟩ + Equal ((suc (predℕ {varn env} c2 )) + vari env) (suc c10) + ≡⟨ cong ( λ z → Equal (z + vari env ) (suc c10) ) (suc-predℕ=n c2 ) ⟩ + Equal (varn env + vari env) (suc c10) + ≡⟨ cong ( λ z → (Equal z (suc c10) )) c1 ⟩ + Equal (suc c10) (suc c10) + ≡⟨ ≡→Equal refl ⟩ + true + ∎ + -- While Loopを抜けた際のConditionの生合成の証明 + -- 抜けた際と言っているけどそれならvarnは0になり + lemma4 : {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv + lemma4 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in + begin + whileInv (record { varn = varn env - 1 ; vari = vari env }) + ≡⟨⟩ + Equal ((varn env - 1) + vari env) c10 + ≡⟨ lemma41 env (Equal→≡ (∧-pi1 cond)) (∧-pi2 cond) ⟩ + true + ∎ + ) + lemma51 : (z : Env ) → neg (λ z → lt zero (varn z)) z ≡ true → varn z ≡ zero + lemma51 z cond with varn z + lemma51 z refl | zero = refl + lemma51 z () | suc x + -- While Loopを抜けた後のループ不変条件からConditionへの変換とtermCondへの移行の整合性を保証している + lemma5 : {c10 : ℕ} → Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond + lemma5 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in + begin + termCond env + ≡⟨⟩ + Equal (vari env) c10 + ≡⟨⟩ + Equal (zero + vari env) c10 + ≡⟨ cong ( λ z → Equal (z + vari env) c10 ) (sym ( lemma51 env ( ∧-pi2 cond ) )) ⟩ + Equal (varn env + vari env) c10 + ≡⟨ ∧-pi1 cond ⟩ + true + ∎ + ) diff -r 000000000000 -r f5705a66e9ea whilespecification.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/whilespecification.agda Tue Oct 13 18:01:42 2020 +0900 @@ -0,0 +1,164 @@ +module whilespecification where + +open import Function +open import Data.Nat +open import Data.Bool +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 Data.Nat.Properties + +open import utilities hiding ( _/\_ ) +open import whiletest + +open import Hoare PrimComm Cond Axiom Tautology _and_ neg + +open Env + +initCond : Cond +initCond env = true + +termCond : {c10 : ℕ} → Cond +termCond {c10} env = Equal (vari env) c10 + +stmt1Cond : {c10 : ℕ} → Cond +stmt1Cond {c10} env = Equal (varn env) c10 + +init-case : {c10 : ℕ} → (env : Env) → (( λ e → true ⇒ stmt1Cond {c10} e ) (record { varn = c10 ; vari = vari env }) ) ≡ true +init-case {c10} _ = impl⇒ ( λ cond → ≡→Equal refl ) + +stmt2Cond : {c10 : ℕ} → Cond +stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0) + +whileInv : {c10 : ℕ} → Cond +whileInv {c10} env = Equal ((varn env) + (vari env)) c10 + +whileInv' : {c10 : ℕ} → Cond +whileInv'{c10} env = Equal ((varn env) + (vari env)) (suc c10) ∧ lt zero (varn env) + +lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10}) +lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in + begin + (Equal (varn env) c10 ) ∧ true + ≡⟨ ∧true ⟩ + Equal (varn env) c10 + ≡⟨ cond ⟩ + true + ∎ ) + + +proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10}) +proof1 c10 = + SeqRule {λ e → true} ( PrimRule (init-case {c10} )) + $ SeqRule {λ e → Equal (varn e) c10} ( PrimRule lemma1 ) + $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)} lemma2 ( + WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10} + $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) + $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 + where + lemma21 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env ≡ c10 + lemma21 eq = Equal→≡ (∧-pi1 eq) + lemma22 : {env : Env } → {c10 : ℕ} → stmt2Cond {c10} env ≡ true → vari env ≡ 0 + lemma22 eq = Equal→≡ (∧-pi2 eq) + lemma23 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env + vari env ≡ c10 + lemma23 {env} {c10} eq = let open ≡-Reasoning in + begin + varn env + vari env + ≡⟨ cong ( \ x -> x + vari env ) (lemma21 eq ) ⟩ + c10 + vari env + ≡⟨ cong ( \ x -> c10 + x) (lemma22 {env} {c10} eq ) ⟩ + c10 + 0 + ≡⟨ +-sym {c10} {0} ⟩ + 0 + c10 + ≡⟨⟩ + c10 + ∎ + lemma2 : {c10 : ℕ} → Tautology stmt2Cond whileInv + lemma2 {c10} env = bool-case (stmt2Cond env) ( + λ eq → let open ≡-Reasoning in + begin + (stmt2Cond env) ⇒ (whileInv env) + ≡⟨⟩ + (stmt2Cond env) ⇒ ( Equal (varn env + vari env) c10 ) + ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ ( Equal x c10 ) ) ( lemma23 {env} eq ) ⟩ + (stmt2Cond env) ⇒ (Equal c10 c10) + ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ x ) (≡→Equal refl ) ⟩ + (stmt2Cond {c10} env) ⇒ true + ≡⟨ ⇒t ⟩ + true + ∎ + ) ( + λ ne → let open ≡-Reasoning in + begin + (stmt2Cond env) ⇒ (whileInv env) + ≡⟨ cong ( \ x -> x ⇒ (whileInv env) ) ne ⟩ + false ⇒ (whileInv {c10} env) + ≡⟨ f⇒ {whileInv {c10} env} ⟩ + true + ∎ + ) + lemma3 : Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv' + lemma3 env = impl⇒ ( λ cond → let open ≡-Reasoning in + begin + whileInv' (record { varn = varn env ; vari = vari env + 1 }) + ≡⟨⟩ + Equal (varn env + (vari env + 1)) (suc c10) ∧ (lt 0 (varn env) ) + ≡⟨ cong ( λ z → Equal (varn env + (vari env + 1)) (suc c10) ∧ z ) (∧-pi2 cond ) ⟩ + Equal (varn env + (vari env + 1)) (suc c10) ∧ true + ≡⟨ ∧true ⟩ + Equal (varn env + (vari env + 1)) (suc c10) + ≡⟨ cong ( \ x -> Equal x (suc c10) ) (sym (+-assoc (varn env) (vari env) 1)) ⟩ + Equal ((varn env + vari env) + 1) (suc c10) + ≡⟨ cong ( \ x -> Equal x (suc c10) ) +1≡suc ⟩ + Equal (suc (varn env + vari env)) (suc c10) + ≡⟨ sym Equal+1 ⟩ + Equal ((varn env + vari env) ) c10 + ≡⟨ ∧-pi1 cond ⟩ + true + ∎ ) + lemma41 : (env : Env ) → {c10 : ℕ} → (varn env + vari env) ≡ (suc c10) → lt 0 (varn env) ≡ true → Equal ((varn env - 1) + vari env) c10 ≡ true + lemma41 env {c10} c1 c2 = let open ≡-Reasoning in + begin + Equal ((varn env - 1) + vari env) c10 + ≡⟨ cong ( λ z → Equal ((z - 1 ) + vari env ) c10 ) (sym (suc-predℕ=n c2) ) ⟩ + Equal ((suc (predℕ {varn env} c2 ) - 1) + vari env) c10 + ≡⟨⟩ + Equal ((predℕ {varn env} c2 ) + vari env) c10 + ≡⟨ Equal+1 ⟩ + Equal ((suc (predℕ {varn env} c2 )) + vari env) (suc c10) + ≡⟨ cong ( λ z → Equal (z + vari env ) (suc c10) ) (suc-predℕ=n c2 ) ⟩ + Equal (varn env + vari env) (suc c10) + ≡⟨ cong ( λ z → (Equal z (suc c10) )) c1 ⟩ + Equal (suc c10) (suc c10) + ≡⟨ ≡→Equal refl ⟩ + true + ∎ + lemma4 : {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv + lemma4 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in + begin + whileInv (record { varn = varn env - 1 ; vari = vari env }) + ≡⟨⟩ + Equal ((varn env - 1) + vari env) c10 + ≡⟨ lemma41 env (Equal→≡ (∧-pi1 cond)) (∧-pi2 cond) ⟩ + true + ∎ + ) + lemma51 : (z : Env ) → neg (λ z → lt zero (varn z)) z ≡ true → varn z ≡ zero + lemma51 z cond with varn z + lemma51 z refl | zero = refl + lemma51 z () | suc x + lemma5 : {c10 : ℕ} → Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond + lemma5 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in + begin + termCond env + ≡⟨⟩ + Equal (vari env) c10 + ≡⟨⟩ + Equal (zero + vari env) c10 + ≡⟨ cong ( λ z → Equal (z + vari env) c10 ) (sym ( lemma51 env ( ∧-pi2 cond ) )) ⟩ + Equal (varn env + vari env) c10 + ≡⟨ ∧-pi1 cond ⟩ + true + ∎ + ) diff -r 000000000000 -r f5705a66e9ea whilespecimple.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/whilespecimple.agda Tue Oct 13 18:01:42 2020 +0900 @@ -0,0 +1,108 @@ +module whilespecimple where + +open import Relation.Binary.PropositionalEquality +open import Data.Bool +open import Relation.Binary +open import Relation.Nullary using (¬_; Dec; yes; no) +open import Data.Empty +open import Agda.Builtin.Sigma +open import Data.Product +open import Data.Nat + + +open import utilities hiding ( _/\_ ) +open import whiletest +open import Hoare PrimComm Cond Axiom Tautology _and_ neg +open import whilespec + +State : Set +State = Env + +open import RelOp +module RelOpState = RelOp State + + +SemCond : Cond -> State -> Set +SemCond c p = c p ≡ true + +PrimSemComm : ∀ {l} -> PrimComm -> Rel State l +PrimSemComm prim s1 s2 = Id State (prim s1) s2 + +tautValid : (b1 b2 : Cond) -> Tautology b1 b2 -> (s : State) -> SemCond b1 s -> SemCond b2 s +tautValid b1 b2 taut s cond with b1 s | b2 s | taut s +tautValid b1 b2 taut s () | false | false | refl +tautValid b1 b2 taut s _ | false | true | refl = refl +tautValid b1 b2 taut s _ | true | false | () +tautValid b1 b2 taut s _ | true | true | refl = refl + + +axiomValid : ∀ {l} -> (bPre : Cond) -> (pcm : PrimComm) -> (bPost : Cond) -> + (ax : Axiom bPre pcm bPost) -> (s1 s2 : State) -> + SemCond bPre s1 -> PrimSemComm {l} pcm s1 s2 -> SemCond bPost s2 +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref with bPre s1 | bPost (pcm s1) | ax s1 +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) () ref | false | false | refl +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | false | true | refl = refl +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | false | () +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | true | refl = refl + + +respNeg : (b : Cond) -> (s : State) -> + Iff (SemCond (neg b) s) (¬ SemCond b s) +respNeg b s = ( left , right ) where + left : not (b s) ≡ true → (b s) ≡ true → ⊥ + left ne with b s + left refl | false = λ () + left () | true + right : ((b s) ≡ true → ⊥) → not (b s) ≡ true + right ne with b s + right ne | false = refl + right ne | true = ⊥-elim ( ne refl ) + +_/\_ : Cond -> Cond -> Cond +b1 /\ b2 = b1 and b2 + +_\/_ : Cond -> Cond -> Cond +b1 \/ b2 = neg (neg b1 /\ neg b2) + +respAnd : (b1 b2 : Cond) -> (s : State) -> + Iff (SemCond (b1 /\ b2) s) + ((SemCond b1 s) × (SemCond b2 s)) +respAnd b1 b2 s = ( left , right ) where + left : b1 s ∧ b2 s ≡ true → (b1 s ≡ true) × (b2 s ≡ true) + left and with b1 s | b2 s + left () | false | false + left () | false | true + left () | true | false + left refl | true | true = ( refl , refl ) + right : (b1 s ≡ true) × (b2 s ≡ true) → b1 s ∧ b2 s ≡ true + right ( x1 , x2 ) with b1 s | b2 s + right (() , ()) | false | false + right (() , _) | false | true + right (_ , ()) | true | false + right (refl , refl) | true | true = refl + + +open import HoareSoundness + Cond + PrimComm + neg + _and_ + Tautology + State + SemCond + tautValid + respNeg + respAnd + PrimSemComm + Axiom + axiomValid + +PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} -> + HTProof bPre cm bPost -> Satisfies bPre cm bPost +PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht + +proofOfProgram : (c10 : ℕ) → (input output : Env ) + → initCond input ≡ true + → (SemComm (program c10) input output) + → termCond {c10} output ≡ true +proofOfProgram c10 input output ic sem = PrimSoundness (proof1 c10) input output ic sem diff -r 000000000000 -r f5705a66e9ea whiletest.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/whiletest.agda Tue Oct 13 18:01:42 2020 +0900 @@ -0,0 +1,72 @@ +module whiletest where + +open import Data.Nat +open import Data.Bool +open import Function +open import Relation.Binary.PropositionalEquality + +open import utilities hiding ( _/\_ ) + +record Env : Set where + field + varn : ℕ + vari : ℕ +open Env + +-- Envのvariやvarnの代入を行う関数 +PrimComm : Set +PrimComm = Env → Env + +Cond : Set +Cond = (Env → Bool) + +-- ここから先のコメントがなかった + +Axiom : Cond -> PrimComm -> Cond -> Set +Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true + +Tautology : Cond -> Cond -> Set +Tautology pre post = ∀ (env : Env) → (pre env) ⇒ (post env) ≡ true + +_and_ : Cond -> Cond -> Cond +x and y = λ env → x env ∧ y env + +neg : Cond -> Cond +neg x = λ env → not ( x env ) + +open import Hoare PrimComm Cond Axiom Tautology _and_ neg + +-- 実装開始 +-- ここでは実行停止の定義などはしていない +-- numにループ回数をいれる感じか +program : ℕ → Comm +program loop_num = + Seq ( PComm (λ env → record env {varn = loop_num})) + $ Seq ( PComm (λ env → record env {vari = 0})) -- ここまで入力 + $ While (λ env → lt zero (varn env ) ) -- 大小比較をしている + (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) + $ PComm (λ env → record env {varn = ((varn env) - 1)} )) + +-- 実行するための定義 +-- この定義では停止しないのでTERMINATINGが必要 +-- コマンドがdata型なので全部の場合の記述をする +{-# TERMINATING #-} +interpret : Env → Comm → Env +interpret env Skip = env +interpret env Abort = env +interpret env (PComm x) = x env +interpret env (Seq comm comm1) = interpret (interpret env comm) comm1 +interpret env (If x then else) with x env +... | true = interpret env then +... | false = interpret env else +interpret env (While x comm) with x env +... | true = interpret (interpret env comm) (While x comm) +... | false = env + +-- 実行 +test : Env +test = interpret ( record { vari = 0 ; varn = 10 } ) (program 10) + +-- 実行はできた +-- 事前、事後条件を検証していく。これができるとHoare Logicを名乗っても良い +