Mercurial > hg > Members > ryokka > HoareLogic

annotate HoareSoundness.agda @ 79:52d957db0222

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author ryokka
date Mon, 30 Dec 2019 20:53:00 +0900
parents 222dd3869ab0
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 {-# OPTIONS --universe-polymorphism #-}
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Level
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Data.Nat
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Data.Product
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Data.Bool
20
fe7d6c90e435 Hoare and Relop done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
7 open import Data.Empty
21
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
8 open import Data.Sum
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Relation.Binary
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Relation.Nullary
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Relation.Binary.Core
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
12 open import Relation.Binary.PropositionalEquality
21
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
13 open import RelOp
22
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
14 open import utilities
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
24
e668962ac31a rename modules
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
16 module HoareSoundness
22
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
17 (Cond : Set)
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
18 (PrimComm : Set)
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
19 (neg : Cond -> Cond)
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
20 (_/\_ : Cond -> Cond -> Cond)
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
21 (Tautology : Cond -> Cond -> Set)
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
22 (State : Set)
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
23 (SemCond : Cond -> State -> Set)
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
24 (tautValid : (b1 b2 : Cond) -> Tautology b1 b2 ->
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
25 (s : State) -> SemCond b1 s -> SemCond b2 s)
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
26 (respNeg : (b : Cond) -> (s : State) ->
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
27 Iff (SemCond (neg b) s) (¬ SemCond b s))
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
28 (respAnd : (b1 b2 : Cond) -> (s : State) ->
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
29 Iff (SemCond (b1 /\ b2) s)
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
30 ((SemCond b1 s) × (SemCond b2 s)))
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
31 (PrimSemComm : ∀ {l} -> PrimComm -> Rel State l)
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
32 (Axiom : Cond -> PrimComm -> Cond -> Set)
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
33 (axiomValid : ∀ {l} -> (bPre : Cond) -> (pcm : PrimComm) -> (bPost : Cond) ->
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
34 (ax : Axiom bPre pcm bPost) -> (s1 s2 : State) ->
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
35 SemCond bPre s1 -> PrimSemComm {l} pcm s1 s2 -> SemCond bPost s2) where
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36
24
e668962ac31a rename modules
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
37 open import Hoare PrimComm Cond Axiom Tautology _/\_ neg
22
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
38
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
39 open import RelOp
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
40 module RelOpState = RelOp State
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
41
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
42 NotP : {S : Set} -> Pred S -> Pred S
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
43 NotP X s = ¬ X s
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
44
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
45 _\/_ : Cond -> Cond -> Cond
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
46 b1 \/ b2 = neg (neg b1 /\ neg b2)
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
47
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
48 when : {X Y Z : Set} -> (X -> Z) -> (Y -> Z) ->
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
49 X ⊎ Y -> Z
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
50 when f g (inj₁ x) = f x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
51 when f g (inj₂ y) = g y
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 -- semantics of commands
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
54 SemComm : Comm -> Rel State (Level.zero)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
55 SemComm Skip = RelOpState.deltaGlob
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
56 SemComm Abort = RelOpState.emptyRel
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 SemComm (PComm pc) = PrimSemComm pc
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
58 SemComm (Seq c1 c2) = RelOpState.comp (SemComm c1) (SemComm c2)
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 SemComm (If b c1 c2)
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
60 = RelOpState.union
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
61 (RelOpState.comp (RelOpState.delta (SemCond b))
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 (SemComm c1))
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
63 (RelOpState.comp (RelOpState.delta (NotP (SemCond b)))
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 (SemComm c2))
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 SemComm (While b c)
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
66 = RelOpState.unionInf
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 (λ (n : ℕ) ->
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
68 RelOpState.comp (RelOpState.repeat
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 n
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
70 (RelOpState.comp
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
71 (RelOpState.delta (SemCond b))
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 (SemComm c)))
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
73 (RelOpState.delta (NotP (SemCond b))))
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 Satisfies : Cond -> Comm -> Cond -> Set
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 Satisfies bPre cm bPost
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 = (s1 : State) -> (s2 : State) ->
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
78 SemCond bPre s1 -> SemComm cm s1 s2 -> SemCond bPost s2
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 Soundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 HTProof bPre cm bPost -> Satisfies bPre cm bPost
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 Soundness (PrimRule {bPre} {cm} {bPost} pr) s1 s2 q1 q2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 = axiomValid bPre cm bPost pr s1 s2 q1 q2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 Soundness {.bPost} {.Skip} {bPost} (SkipRule .bPost) s1 s2 q1 q2
20
fe7d6c90e435 Hoare and Relop done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
85 = substId1 State {Level.zero} {State} {s1} {s2} (proj₂ q2) (SemCond bPost) q1
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 Soundness {bPre} {.Abort} {bPost} (AbortRule .bPre .bPost) s1 s2 q1 ()
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 Soundness (WeakeningRule {bPre} {bPre'} {cm} {bPost'} {bPost} tautPre pr tautPost)
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 s1 s2 q1 q2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 = let hyp : Satisfies bPre' cm bPost'
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 hyp = Soundness pr
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 r1 : SemCond bPre' s1
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 r1 = tautValid bPre bPre' tautPre s1 q1
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 r2 : SemCond bPost' s2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 r2 = hyp s1 s2 r1 q2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 in tautValid bPost' bPost tautPost s2 r2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 Soundness (SeqRule {bPre} {cm1} {bMid} {cm2} {bPost} pr1 pr2)
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 s1 s2 q1 q2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 = let hyp1 : Satisfies bPre cm1 bMid
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 hyp1 = Soundness pr1
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 hyp2 : Satisfies bMid cm2 bPost
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 hyp2 = Soundness pr2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 sMid : State
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 sMid = proj₁ q2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 r1 : SemComm cm1 s1 sMid × SemComm cm2 sMid s2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 r1 = proj₂ q2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 r2 : SemComm cm1 s1 sMid
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 r2 = proj₁ r1
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 r3 : SemComm cm2 sMid s2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 r3 = proj₂ r1
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 r4 : SemCond bMid sMid
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 r4 = hyp1 s1 sMid q1 r2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 in hyp2 sMid s2 r4 r3
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse)
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 s1 s2 q1 q2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 = let hypThen : Satisfies (bPre /\ b) cmThen bPost
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116 hypThen = Soundness pThen
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117 hypElse : Satisfies (bPre /\ neg b) cmElse bPost
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118 hypElse = Soundness pElse
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
119 rThen : RelOpState.comp
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
120 (RelOpState.delta (SemCond b))
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 (SemComm cmThen) s1 s2 ->
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122 SemCond bPost s2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123 rThen = λ h ->
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 let t1 : SemCond b s1 × SemComm cmThen s1 s2
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
125 t1 = (proj₂ (RelOpState.deltaRestPre
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 (SemCond b)
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 (SemComm cmThen) s1 s2)) h
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 t2 : SemCond (bPre /\ b) s1
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 t2 = (proj₂ (respAnd bPre b s1))
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 (q1 , proj₁ t1)
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 in hypThen s1 s2 t2 (proj₂ t1)
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
132 rElse : RelOpState.comp
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
133 (RelOpState.delta (NotP (SemCond b)))
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 (SemComm cmElse) s1 s2 ->
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 SemCond bPost s2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136 rElse = λ h ->
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137 let t10 : (NotP (SemCond b) s1) ×
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138 (SemComm cmElse s1 s2)
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
139 t10 = proj₂ (RelOpState.deltaRestPre
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140 (NotP (SemCond b)) (SemComm cmElse) s1 s2)
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141 h
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142 t6 : SemCond (neg b) s1
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143 t6 = proj₂ (respNeg b s1) (proj₁ t10)
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144 t7 : SemComm cmElse s1 s2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145 t7 = proj₂ t10
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 t8 : SemCond (bPre /\ neg b) s1
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 t8 = proj₂ (respAnd bPre (neg b) s1)
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148 (q1 , t6)
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149 in hypElse s1 s2 t8 t7
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150 in when rThen rElse q2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151 Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152 = proj₂ (respAnd bInv (neg b) s2) t20
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153 where
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
154 hyp : Satisfies (bInv /\ b) cm' bInv
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
155 hyp = Soundness pr
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
156 n : ℕ
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
157 n = proj₁ q2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
158 Rel1 : ℕ -> Rel State (Level.zero)
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
159 Rel1 = λ m ->
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
160 RelOpState.repeat
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
161 m
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
162 (RelOpState.comp (RelOpState.delta (SemCond b))
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
163 (SemComm cm'))
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
164 t1 : RelOpState.comp
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
165 (Rel1 n)
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
166 (RelOpState.delta (NotP (SemCond b))) s1 s2
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
167 t1 = proj₂ q2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
168 t15 : (Rel1 n s1 s2) × (NotP (SemCond b) s2)
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
169 t15 = proj₂ (RelOpState.deltaRestPost
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
170 (NotP (SemCond b)) (Rel1 n) s1 s2)
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
171 t1
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
172 t16 : Rel1 n s1 s2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
173 t16 = proj₁ t15
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
174 t17 : NotP (SemCond b) s2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
175 t17 = proj₂ t15
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
176 lem1 : (m : ℕ) -> (ss2 : State) -> Rel1 m s1 ss2 ->
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
177 SemCond bInv ss2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
178 lem1 ℕ.zero ss2 h
20
fe7d6c90e435 Hoare and Relop done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
179 = substId1 State (proj₂ h) (SemCond bInv) q1
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
180 lem1 (ℕ.suc n) ss2 h
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
181 = let hyp2 : (z : State) -> Rel1 n s1 z ->
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
182 SemCond bInv z
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
183 hyp2 = lem1 n
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
184 s20 : State
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
185 s20 = proj₁ h
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
186 t21 : Rel1 n s1 s20
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
187 t21 = proj₁ (proj₂ h)
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
188 t22 : (SemCond b s20) × (SemComm cm' s20 ss2)
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
189 t22 = proj₂ (RelOpState.deltaRestPre
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
190 (SemCond b) (SemComm cm') s20 ss2)
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
191 (proj₂ (proj₂ h))
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
192 t23 : SemCond (bInv /\ b) s20
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
193 t23 = proj₂ (respAnd bInv b s20)
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
194 (hyp2 s20 t21 , proj₁ t22)
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
195 in hyp s20 ss2 t23 (proj₂ t22)
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
196 t20 : SemCond bInv s2 × SemCond (neg b) s2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
197 t20 = lem1 n s2 t16 , proj₂ (respNeg b s2) t17