### view whileTestPrimProof.agda @ 50:2edb44c5bf52

author ryokka Wed, 18 Dec 2019 20:08:58 +0900 e668962ac31a 62dcb0ae2c94
line wrap: on
line source
```
module whileTestPrimProof where

open import Function
open import Data.Nat
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 hiding ( _/\_ )
open import whileTestPrim

open import Hoare PrimComm Cond Axiom Tautology _and_ neg

open Env

initCond : Cond
initCond env = true

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 )

init-type : {c10 :  ℕ} → Axiom (λ env → true) (λ env → record { varn = c10 ; vari = vari env }) (stmt1Cond {c10})
init-type {c10} env = init-case env

stmt2Cond : {c10 : ℕ} → Cond
stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)

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
∎ )

-- simple : ℕ → Comm
-- simple c10 =
--     Seq ( PComm (λ env → record env {varn = c10}))
--     \$  PComm (λ env → record env {vari = 0})

proofs : (c10 : ℕ) → HTProof initCond (simple c10) (stmt2Cond {c10})
proofs c10 =
SeqRule {initCond} ( PrimRule (init-case {c10} ))
\$ PrimRule {stmt1Cond} {_} {stmt2Cond} (lemma1 {c10})

open import Data.Empty

open import Data.Nat.Properties

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)

termCond : {c10 : ℕ} → Cond
termCond {c10} env = Equal (vari env) c10

--  program : ℕ → Comm
--  program c10 =
--      Seq ( PComm (λ env → record env {varn = c10}))
--      \$ 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)} ))

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
∎
)

--- necessary definitions for Hoare.agda ( Soundness )

State : Set
State = Env

open import RelOp
module RelOpState = RelOp State

open import Data.Product
open import Relation.Binary

NotP : {S : Set} -> Pred S -> Pred S
NotP X s = ¬ X s

_/\_ : Cond -> Cond -> Cond
b1 /\ b2 = b1 and b2

_\/_ : Cond -> Cond -> Cond
b1 \/ b2 = neg (neg b1 /\ neg b2)

_==>_ : Cond -> Cond -> Cond
b1 ==> b2 = neg (b1 \/ b2)

SemCond : Cond -> State -> Set
SemCond c p = c p ≡ true

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

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 )

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

PrimSemComm : ∀ {l} -> PrimComm -> Rel State l
PrimSemComm prim s1 s2 =  Id State (prim s1) s2

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

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
```