--- a/Hoare.agda	Thu Dec 13 17:45:50 2018 +0900
+++ b/Hoare.agda	Thu Dec 13 19:05:43 2018 +0900
@@ -47,8 +47,8 @@
   While : Cond -> Comm -> Comm
 
 -- Hoare Triple
-data HT : Set where
-  ht : Cond -> Comm -> Cond -> HT
+-- data HT : Set where
+--   ht : Cond -> Comm -> Cond -> HT
 
 {-
                 prPre              pr              prPost

--- a/whileTest.agda	Thu Dec 13 17:45:50 2018 +0900
+++ b/whileTest.agda	Thu Dec 13 19:05:43 2018 +0900
@@ -5,8 +5,9 @@
 open import Data.Product
 open import Relation.Nullary
 open import Relation.Binary
+open import Relation.Binary.PropositionalEquality
 open import SET
-
+import Level
 
 record Env : Set where
   field
@@ -14,44 +15,55 @@
     vari : ℕ
 open Env
 
+PrimComm = Env → Env
+
+Cond = Env → Bool
+
 neg : (Env → Bool) → (Env → Bool)
 neg x e = not (x e)
-
+ 
 and : (Env → Bool) → (Env → Bool)  → (Env → Bool)
 and x y e = (x e) ∧ (y e)
 
-enveq : (Env → Bool) → (Env → Bool) → Set
-enveq x y = {!!}
-
-sem : (Env → Bool) → Pred Env
-sem x y = {!!}
-
-tautValid : (b1 b2 : Env → Bool) -> enveq b1 b2 ->
-                 (s : Env) -> sem b1 s -> sem b2 s
-tautValid = {!!}
-
-respNeg : (b : Env → Bool) -> (s : Env) ->
-               Iff (sem (neg b) s) (¬ sem b s)
-respNeg = {!!}               
+data Comm : Set where
+  Skip  : Comm
+  Abort : Comm
+  PComm : PrimComm -> Comm
+  Seq   : Comm -> Comm -> Comm
+  If    : Cond -> Comm -> Comm -> Comm
+  While : Cond -> Comm -> Comm
 
-respAnd : (b1 b2 : Env → Bool) -> (s : Env) ->
-               Iff (sem (and b1 b2) s)
-                   ((sem b1 s) ×  (sem b2 s))
-respAnd = {!!}
-
-PrimSemComm : ∀ {l} -> (Env → Env) -> Rel Env l
-PrimSemComm = {!!}
+data HTProof : Cond -> Comm -> Cond -> Set (Level.suc (Level.suc Level.zero)) where
+  PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
+             (pr :  Cond -> PrimComm -> Cond -> Set (Level.suc Level.zero)) ->
+             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} ->
+                bPre ≡ bPre' ->
+                HTProof bPre' cm bPost' ->
+                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 (and bPre b) cmThen bPost ->
+           HTProof (and bPre (neg b)) cmElse bPost ->
+           HTProof bPre (If b cmThen cmElse) bPost
+  WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
+              HTProof (and bInv b) cm bInv ->
+              HTProof bInv (While b cm) (and bInv (neg b))
+  Rule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} -> {w : Cond} ->
+              HTProof w cm bInv ->
+              HTProof bInv (While b cm) (and bInv (neg b))
 
-Axiom :( Env → Bool) -> (Env → Env) -> (Env → Bool) -> Set
-Axiom = {!!}
-
-axiomValid : ∀ {l} -> (bPre : Env → Bool ) -> (pcm : (Env → Env)) -> (bPost : Env → Bool) ->
-                  (ax : Axiom bPre pcm bPost) -> (s1 s2 : Env) ->
-                  sem bPre s1 -> PrimSemComm {l} pcm s1 s2 -> sem bPost s2
-axiomValid = {!!}
-
-open import Hoare (Env → Bool) (Env → Env) neg and enveq Env sem  tautValid
-                  respNeg respAnd PrimSemComm Axiom axiomValid
 
 lt : ℕ → ℕ → Bool
 lt x y with x <? y
@@ -98,7 +110,16 @@
 termCond : Env → Bool
 termCond env = (vari env) == 10
 
+iff : Bool → Bool → Bool
+iff true true = true
+iff false false = true
+iff _ _ = false
+
+proposition1 : Cond → PrimComm → Cond → Env → Set
+proposition1 pre cmd post = λ (env : Env) → {!!} -- iff (pre env) (post (cmd env))
 
 proof1 : HTProof initCond program termCond
-proof1 = {!!}
+proof1 = SeqRule (PrimRule {!!} )
+         (SeqRule (PrimRule {!!} )
+         (Rule {!!}  (WhileRule ?)))