--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Hoare.agda	Tue Oct 13 18:01:42 2020 +0900
@@ -0,0 +1,76 @@
+module Hoare
+        (PrimComm : Set)
+        (Cond : Set)
+        (Axiom : Cond -> PrimComm -> Cond -> Set)
+        (Tautology : Cond -> Cond -> Set)
+        (_and_ :  Cond -> Cond -> Cond)
+        (neg :  Cond -> Cond )
+  where
+
+-- Hoare Logicでのコマンドを表しているらしい
+data Comm : Set where
+  Skip : Comm　-- 何もしない。
+  Abort : Comm -- 中断
+  PComm : PrimComm → Comm -- PrimCommを受けてコマンドを返す
+  Seq : Comm → Comm → Comm -- コマンドの実行結果をさらに次のコマンドの引数として渡す
+  If : Cond → Comm → Comm → Comm -- Condにより実行するコマンドを分岐する
+  While : Cond → Comm → Comm -- Condとコマンドを受け取り、Condがtrueである間コマンドを繰り返し実行するコマンド
+
+{-
+                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 /\ c} cm1 {bPost}  {bPre /\ neg c} cm2 {bPost}
+If: ------------------------------------------------------
+     {bPre} If c then cm1 else cm2 fi {bPost}
+
+                          pr
+                 -------------------
+                 {inv /\ c} cm {inv}
+While: ---------------------------------------
+        {inv} while c do cm od {inv /\ neg c}
+-}
+
+
+data HTProof : Cond -> Comm -> Cond -> Set where
+  PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
+             (pr : Axiom bPre pcm bPost) ->
+             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} ->
+                Tautology bPre bPre' ->
+                HTProof bPre' cm bPost' ->
+                Tautology 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 (bPre and b) cmThen bPost ->
+           HTProof (bPre and neg b) cmElse bPost ->
+           HTProof bPre (If b cmThen cmElse) bPost
+  WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
+              HTProof (bInv and b) cm bInv ->
+              HTProof bInv (While b cm) (bInv and neg b)
+