--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Readme.md	Sat Apr 08 07:49:41 2023 +0900
@@ -0,0 +1,145 @@
+-title: Hoare Logic
+
+-- files
+
+    Hoare.agda                   Hoare logic data structre
+    HoareSoundness.agda          Hoare logic soundness
+    RelOp.agda                   Set theoretic operation
+    whileTestPrim.agda           definition of simple program and conditions as a Hoare logic command
+    whileTestPrimProof.agda      proof using HoareSoundness
+
+    whileTestGears.agda          Gears form of proof
+    simple.agda
+    utilities.agda
+
+-- Hoare logic Programm commands
+
+    data Comm : Set where
+      Skip  : Comm
+      Abort : Comm
+      PComm : PrimComm -> Comm
+      Seq   : Comm -> Comm -> Comm
+      If    : Cond -> Comm -> Comm -> Comm
+      While : Cond -> Comm -> Comm
+
+-- Example
+
+    record Env : Set where
+      field
+        varn : ℕ
+        vari : ℕ
+
+    program : ℕ → Comm
+    program c10 = 
+        Seq ( PComm (λ env → record env {varn = c10}))                     ---    n = c10 ;
+        $ Seq ( PComm (λ env → record env {vari = 0}))                     ---    i = 0 ;
+        $ While (λ env → lt zero (varn env ) )                             ---    while ( 0 < n ) {
+          (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))     ---        i = i + 1
+            $ PComm (λ env → record env {varn = ((varn env) - 1)} ))       ---        n = n - 1 }
+
+This is a syntax tree of a program.
+
+-- Interpretation of the example
+
+    {-# TERMINATING #-}
+    interpret : Env → Comm → Env
+    interpret env Skip = env
+    interpret env Abort = env
+    interpret env (PComm x) = x env
+    interpret env (Seq comm comm1) = interpret (interpret env comm) comm1
+    interpret env (If x then else) with x env
+    ... | true = interpret env then
+    ... | false = interpret env else
+    interpret env (While x comm) with x env
+    ... | true = interpret (interpret env comm) (While x comm)
+    ... | false = env
+
+-- Hoare logic Programm commands with Post and Pre conditions
+
+A syntax tree of a program with conditions.
+
+    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)
+
+-- Example of proposition
+
+    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
+
+This defines a connected sequence of conditions.
+
+-- Semantics of commands
+
+    SemComm : Comm -> Rel State (Level.zero)
+    SemComm Skip = RelOpState.deltaGlob
+    SemComm Abort = RelOpState.emptyRel
+    SemComm (PComm pc) = PrimSemComm pc
+    SemComm (Seq c1 c2) = RelOpState.comp (SemComm c1) (SemComm c2)
+    SemComm (If b c1 c2)
+      = RelOpState.union
+          (RelOpState.comp (RelOpState.delta (SemCond b))
+                           (SemComm c1))
+          (RelOpState.comp (RelOpState.delta (NotP (SemCond b)))
+                           (SemComm c2))
+    SemComm (While b c)
+      = RelOpState.unionInf
+          (λ (n : ℕ) ->
+            RelOpState.comp (RelOpState.repeat n
+                           (RelOpState.comp (RelOpState.delta (SemCond b)) (SemComm c))) (RelOpState.delta (NotP (SemCond b))))
+
+This defines a proposition of Hoare conditions. It is not proved yet.
+
+The semantics of while-command is defined as any countable sequence of the body.
+
+-- Soundness
+
+    Soundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
+                HTProof bPre cm bPost -> Satisfies bPre cm bPost
+
+The proof of the soundness of the semantics of HTProof.
+
+-- An example of the soundness
+
+    proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10})
+
+    PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
+                HTProof bPre cm bPost -> Satisfies bPre cm bPost
+    PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht
+
+    proofOfProgram : (c10 : ℕ) → (input output : Env )
+      → initCond input ≡ true
+      → (SemComm (program c10) input output)
+      → termCond {c10} output ≡ true
+    proofOfProgram c10 input output ic sem  = PrimSoundness (proof1 c10) input output ic sem
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ReadmeGears.md	Sat Apr 08 07:49:41 2023 +0900
@@ -0,0 +1,70 @@
+-title: GearsAgda
+
+-- files
+
+    whileTestGears.agda          Gears form of proof
+
+-- Continuation form makes Hoare logic simple
+
+Write a program in Gears form, which is a lightweight continuation style.
+
+   code : {t : Set} -> (next : t -> t ) -> t
+
+-- Gears version of a program
+
+    record Env  : Set where
+      field
+        varn : ℕ
+        vari : ℕ
+    open Env
+
+    {-# TERMINATING #-}
+    whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
+    whileLoop env next with lt 0 (varn env)
+    whileLoop env next | false = next env
+    whileLoop env next | true =
+        whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
+
+We need TERMINATING, because Agda does not understand the termination.
+
+-- A Segmented code gear with a condition
+
+    whileLoopSeg : {l : Level} {t : Set l} → {c10 :  ℕ } → (env : Env) → ((varn env) + (vari env) ≡ c10)
+       → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t)     -- next with PostCondition
+       → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t
+
+It includes a reduction sequence "varn e1 < varn env → t)".
+
+The invariant is directly described in the program, we don't need sytax tree of a code nor a code with conditions.
+
+-- Specification
+
+    whileTestSpec1 : (c10 : ℕ) →  (e1 : Env ) → vari e1 ≡ c10 → ⊤
+    whileTestSpec1 _ _ x = tt
+
+This is the condition to be proved.
+
+-- while loop in GearsAgda
+
+    TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → {Invraiant : Index → Set } → ( reduce : Index → ℕ)
+       → (loop : (r : Index)  → Invraiant r → (next : (r1 : Index)  → Invraiant r1 → reduce r1 < reduce r  → t ) → t)
+       → (r : Index) → (p : Invraiant r)  → t 
+
+TerminatingLoopS defines a loop connective, which define the loop and it also gives a correctness of exit condition.
+
+    whileTest' : {l : Level} {t : Set l}  → {c10 :  ℕ } → (Code : (env : Env)  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
+
+    conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 :  ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
+                   → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t
+
+    proofGearsTermS : {c10 :  ℕ } → ⊤
+    proofGearsTermS {c10} = whileTest' {_} {_}  {c10} (λ n p →  conversion1 n p (λ n1 p1 →
+        TerminatingLoopS Env (λ env → varn env)
+            (λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 )) 
+
+This a proof, because it is a value not a type. whileTestSpec get a proof of specification.
+
+
+
+
+

--- a/Todo	Tue Nov 02 07:30:50 2021 +0900
+++ b/Todo	Sat Apr 08 07:49:41 2023 +0900
@@ -1,3 +1,7 @@
+Sat Apr  8 07:48:50 JST 2023
+
+    Invariant と 実際の入力をわけない
+
 Sun Dec 16 07:32:06 JST 2018
 
     Gears の方に term condition を入れる

--- a/whileTestGears.agda	Tue Nov 02 07:30:50 2021 +0900
+++ b/whileTestGears.agda	Sat Apr 08 07:49:41 2023 +0900
@@ -103,7 +103,7 @@
 
 --                                                                      ↓PreCondition(Invaliant)
 whileLoopSeg : {l : Level} {t : Set l} → {c10 :  ℕ } → (env : Env) → ((varn env) + (vari env) ≡ c10)
-   → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t) 
+   → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t)     -- next with PostCondition
    → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t
 whileLoopSeg env proof next exit with  ( suc zero  ≤? (varn  env) )
 whileLoopSeg {_} {_} {c10} env proof next exit | no p = exit env ( begin