# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1545694875 -32400
# Node ID 3968822b96930c81b019c468c344242f393e1ea2
# Parent  e88ad1d70faf9dded983b7936f31cdadcdd9de41
separate prim program

diff -r e88ad1d70faf -r 3968822b9693 whileTestPrim.agda
--- a/whileTestPrim.agda	Tue Dec 25 08:24:54 2018 +0900
+++ b/whileTestPrim.agda	Tue Dec 25 08:41:15 2018 +0900
@@ -72,260 +72,3 @@
 tests : Env
 tests =  interpret ( record { vari = 0  ; varn = 0 } ) (simple 10)
 
-
-empty-case : (env : Env) → (( λ e → true ) env ) ≡ true 
-empty-case _ = refl
-
-
-
-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)
-
-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
-
-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
-  ∎ )
-
-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
-
-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 Hoare
-    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
diff -r e88ad1d70faf -r 3968822b9693 whileTestPrimProof.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/whileTestPrimProof.agda	Tue Dec 25 08:41:15 2018 +0900
@@ -0,0 +1,281 @@
+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 HoareData 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 Hoare
+    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