--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/hoare.agda	Sat Feb 13 16:29:52 2021 +0900
@@ -0,0 +1,120 @@
+open import Level renaming ( suc to Suc ; zero to Zero )
+module hoare where
+
+open import Data.Nat
+open import Data.Bool hiding (_≤?_ ; _≤_)
+open import Data.Product renaming ( _×_ to _/\_ )
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary using (¬_; Dec; yes; no)
+
+record Env : Set (Suc Zero) where
+   field
+        varn : ℕ
+        vari : ℕ
+open Env
+
+Statement : Set (Suc Zero)
+Statement = {t : Set} → Env → (Env → t ) → t
+
+Cond : Set (Suc Zero)
+Cond = Env → Set
+
+whileTest :  {t : Set (Suc Zero) }  → (c10 : ℕ) → (Env → t) → t
+whileTest c10 next = next ( record {varn = c10 ; vari = 0 } )
+
+lt :  ℕ → ℕ → Bool
+lt zero zero = false
+lt (suc _) zero = false
+lt zero (suc _) = true
+lt (suc x) (suc y) = lt x y
+
+_-_ : ℕ → ℕ → ℕ
+zero - zero = zero
+zero - suc y = zero
+suc x - zero = suc x
+suc x - suc y = x - y
+
+{-# TERMINATING #-}
+whileLoop : {t : Set (Suc Zero)} → Env → (Env → t) → t
+whileLoop env next with lt 0 (varn env)
+whileLoop env next | false = next env
+whileLoop env next | true =
+   whileLoop (record env {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
+
+test1 : Env
+test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 ))
+
+assert1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
+assert1 = refl
+
+-- proof1 : (n : ℕ ) → whileTest n (λ env → whileLoop env (λ e → (vari e) ≡ n ))
+-- proof1 = {!!}
+
+{-# TERMINATING #-}
+whileLoop' : {l : Level} {t : Set l} → (env : Env ) → {c10 :  ℕ } → ((varn env) + (vari env) ≡ c10) → (Code : Env  → t) → t
+whileLoop' env proof next with  ( suc zero  ≤? (varn  env) )
+whileLoop' env proof next       | no p = next env
+whileLoop' env {c10} proof next | yes p = whileLoop' record env {varn = (varn  env) - 1 ; vari = (vari env) + 1} (proof3 proof p ) next
+    where
+          env1 = record env {varn = (varn  env) - 1 ; vari = (vari env) + 1}
+          proof3 : varn env + vari env ≡ c10 → (suc zero  ≤ (varn  env))  → varn env1 + vari env1 ≡ c10
+          proof3 = {!!}
+
+
+-- Condition to Invariant
+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
+conversion1 env {c10} p1 next = next env proof4
+   where
+      proof4 : varn env + vari env ≡ c10
+      proof4 = let open ≡-Reasoning  in
+          begin
+            varn env + vari env
+          ≡⟨ cong ( λ n → n + vari env ) {!!}  ⟩
+            c10 + vari env
+          ≡⟨ cong ( λ n → c10 + n ) {!!}  ⟩
+            c10 + 0
+          ≡⟨ {!!} ⟩
+            c10
+          ∎
+
+whileTest' : {l : Level} {t : Set l}  →  {c10 :  ℕ } → (Code : (env : Env )  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
+whileTest' {_} {_}  {c10} next = next env proof2
+  where
+    env : Env
+    env = record {vari = 0 ; varn = c10 }
+    proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition
+    proof2 = (refl , refl )
+
+-- all proofs are connected
+proofGears : {c10 :  ℕ } → Set
+proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 ))))
+
+-- proof2 : {c10 :  ℕ } → proofGears  {c10}
+-- proof2 {c10} = {!!}
+
+data _implies_ {l m : Level}  (A : Set l ) (B : Set m)  : Set (l Level.⊔  m) where
+    proof : ( A → B ) → A implies B
+--    ind1 : {Inv : ℕ → Set l} → A →  (∀(i : ℕ) → Inv i) → B  → A implies B
+
+data WhileTestState (c10 : ℕ) (env : Env)  : Set where
+  S1 : (vari env ≡ 0) /\ (varn env ≡ c10 ) → WhileTestState c10 env
+  S2 : varn env + vari env ≡ c10 → WhileTestState c10 env
+  Sf : vari env ≡ c10 → WhileTestState c10 env
+
+proofGears1 : {c10 : ℕ } →  whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 →
+    whileLoop' n1 p2 (λ n2 →  ( ( (vari n ≡ 0) /\ (varn n ≡ c10 )) implies (vari n2 ≡ c10 )))))
+proofGears1 {c10} = lemma3 where
+     lemma3 : whileTest' {Level.suc Level.zero} {_} {c10}
+            (λ n p1 →
+               conversion1 n p1
+               (λ n1 p2 →
+                  whileLoop' n1 p2
+                  (λ n2 → (vari n ≡ 0 /\ varn n ≡ c10) implies (vari n2 ≡ c10))))
+     lemma3 = {!!}
+     lemma2 : {n1 : {!!} } {p2 : {!!} } → (whileLoop' n1 p2 (λ n2 → {!!} implies (vari n2 ≡ c10 )))
+     lemma2 = {!!}
+     lemma1 : {n : {!!} } {p1 : {!!} } {p2 : {!!} } → conversion1 n p1 (λ n1 p2 → lemma2 )
+     lemma1 = {!!}
+     lemma0 :  whileTest' {_} {_} {c10} (λ n p1 → lemma1 )
+     lemma0 = {!!}