Mercurial > hg > Members > soto > while_test
view whilespecimple.agda @ 0:f5705a66e9ea default tip
(none)
author | soto@cr.ie.u-ryukyu.ac.jp |
---|---|
date | Tue, 13 Oct 2020 18:01:42 +0900 |
parents | |
children |
line wrap: on
line source
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