--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Hoare.agda.replaced	Tue Sep 08 18:38:08 2020 +0900
@@ -0,0 +1,79 @@
+module Hoare
+        (PrimComm : Set)
+        (Cond : Set)
+        (Axiom : Cond @$\rightarrow$@ PrimComm @$\rightarrow$@ Cond @$\rightarrow$@ Set)
+        (Tautology : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Set)
+        (_and_ :  Cond @$\rightarrow$@ Cond @$\rightarrow$@ Cond)
+        (neg :  Cond @$\rightarrow$@ Cond )
+  where
+
+data Comm : Set where
+  Skip  : Comm
+  Abort : Comm
+  PComm : PrimComm @$\rightarrow$@ Comm
+  Seq   : Comm @$\rightarrow$@ Comm @$\rightarrow$@ Comm
+  If    : Cond @$\rightarrow$@ Comm @$\rightarrow$@ Comm @$\rightarrow$@ Comm
+  While : Cond @$\rightarrow$@ Comm @$\rightarrow$@ Comm
+
+-- Hoare Triple
+data HT : Set where
+  ht : Cond @$\rightarrow$@ Comm @$\rightarrow$@ Cond @$\rightarrow$@ HT
+
+{-
+                prPre              pr              prPost
+             -------------  ------------------  ----------------
+             bPre => bPre'  {bPre'} c {bPost'}  bPost' => bPost
+Weakening : ----------------------------------------------------
+                       {bPre} c {bPost}
+
+Assign: ----------------------------
+         {bPost[v<-e]} v:=e {bPost}
+
+             pr1                pr2
+      -----------------  ------------------
+      {bPre} cm1 {bMid}  {bMid} cm2 {bPost}
+Seq: ---------------------------------------
+      {bPre} cm1 ; cm2 {bPost}
+
+               pr1                         pr2
+     -----------------------  ---------------------------
+     {bPre @$\wedge$@ c} cm1 {bPost}  {bPre @$\wedge$@ neg c} cm2 {bPost}
+If: ------------------------------------------------------
+     {bPre} If c then cm1 else cm2 fi {bPost}
+
+                          pr
+                 -------------------
+                 {inv @$\wedge$@ c} cm {inv}
+While: ---------------------------------------
+        {inv} while c do cm od {inv @$\wedge$@ neg c}
+-}
+
+
+data HTProof : Cond @$\rightarrow$@ Comm @$\rightarrow$@ Cond @$\rightarrow$@ Set where
+  PrimRule : {bPre : Cond} @$\rightarrow$@ {pcm : PrimComm} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@
+             (pr : Axiom bPre pcm bPost) @$\rightarrow$@
+             HTProof bPre (PComm pcm) bPost
+  SkipRule : (b : Cond) @$\rightarrow$@ HTProof b Skip b
+  AbortRule : (bPre : Cond) @$\rightarrow$@ (bPost : Cond) @$\rightarrow$@
+              HTProof bPre Abort bPost
+  WeakeningRule : {bPre : Cond} @$\rightarrow$@ {bPre' : Cond} @$\rightarrow$@ {cm : Comm} @$\rightarrow$@
+                {bPost' : Cond} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@
+                Tautology bPre bPre' @$\rightarrow$@
+                HTProof bPre' cm bPost' @$\rightarrow$@
+                Tautology bPost' bPost @$\rightarrow$@
+                HTProof bPre cm bPost
+  SeqRule : {bPre : Cond} @$\rightarrow$@ {cm1 : Comm} @$\rightarrow$@ {bMid : Cond} @$\rightarrow$@
+            {cm2 : Comm} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@
+            HTProof bPre cm1 bMid @$\rightarrow$@
+            HTProof bMid cm2 bPost @$\rightarrow$@
+            HTProof bPre (Seq cm1 cm2) bPost
+  IfRule : {cmThen : Comm} @$\rightarrow$@ {cmElse : Comm} @$\rightarrow$@
+           {bPre : Cond} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@
+           {b : Cond} @$\rightarrow$@
+           HTProof (bPre and b) cmThen bPost @$\rightarrow$@
+           HTProof (bPre and neg b) cmElse bPost @$\rightarrow$@
+           HTProof bPre (If b cmThen cmElse) bPost
+  WhileRule : {cm : Comm} @$\rightarrow$@ {bInv : Cond} @$\rightarrow$@ {b : Cond} @$\rightarrow$@
+              HTProof (bInv and b) cm bInv @$\rightarrow$@
+              HTProof bInv (While b cm) (bInv and neg b)
+