Mercurial > hg > Members > soto > while_test

changeset 0:f5705a66e9ea default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
(none)
author soto@cr.ie.u-ryukyu.ac.jp
date Tue, 13 Oct 2020 18:01:42 +0900
parents
children
files .DS_Store Hoare.agda HoareSoundness.agda RelOp.agda gearswhile.agda gearswhilehoare.agda utilities.agda whileimple.agda whileploof.agda whilespec.agda whilespecification.agda whilespecimple.agda whiletest.agda
diffstat 13 files changed, 1631 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
Binary file .DS_Store has changed
--- /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)
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/HoareSoundness.agda	Tue Oct 13 18:01:42 2020 +0900
@@ -0,0 +1,210 @@
+{-# OPTIONS --universe-polymorphism #-}
+
+open import Level
+open import Data.Nat
+open import Data.Product
+open import Data.Bool
+open import Data.Empty
+open import Data.Sum
+open import Relation.Binary 
+open import Relation.Nullary
+open import Relation.Binary.Core
+open import Relation.Binary.PropositionalEquality
+open import RelOp 
+open import utilities 
+
+module HoareSoundness
+    (Cond : Set)
+    (PrimComm : Set)
+    (neg : Cond -> Cond)
+    (_/\_ : Cond -> Cond -> Cond)
+    (Tautology : Cond -> Cond -> Set)
+    (State : Set)
+    (SemCond : Cond -> State -> Set)
+    (tautValid : (b1 b2 : Cond) -> Tautology b1 b2 ->
+                 (s : State) -> SemCond b1 s -> SemCond b2 s)
+    (respNeg : (b : Cond) -> (s : State) ->
+               Iff (SemCond (neg b) s) (¬ SemCond b s))
+    (respAnd : (b1 b2 : Cond) -> (s : State) ->
+               Iff (SemCond (b1 /\ b2) s)
+                   ((SemCond b1 s) × (SemCond b2 s)))
+    (PrimSemComm : ∀ {l} -> PrimComm -> Rel State l)
+    (Axiom : Cond -> PrimComm -> Cond -> Set)
+    (axiomValid : ∀ {l} -> (bPre : Cond) -> (pcm : PrimComm) -> (bPost : Cond) ->
+                  (ax : Axiom bPre pcm bPost) -> (s1 s2 : State) ->
+                  SemCond bPre s1 -> PrimSemComm {l} pcm s1 s2 -> SemCond bPost s2) where
+
+open import Hoare PrimComm Cond Axiom Tautology _/\_ neg
+
+open import RelOp 
+module RelOpState = RelOp State
+
+NotP : {S : Set} -> Pred S -> Pred S
+NotP X s = ¬ X s
+
+_\/_ : Cond -> Cond -> Cond
+b1 \/ b2 = neg (neg b1 /\ neg b2)
+
+when : {X  Y  Z : Set} -> (X -> Z) -> (Y -> Z) ->
+       X ⊎ Y -> Z
+when f g (inj₁ x) = f x
+when f g (inj₂ y) = g y
+
+{-
+SemComm' : Comm -> Rel State (Level.zero)
+SemComm' Skip = {!!}
+SemComm' Abort = {!!}
+SemComm' (PComm pc) = {!!}
+SemComm' (Seq c1 c2) = {!!}
+SemComm' (If b c1 c2) = {!!}
+SemComm' (While b c) = {!!}
+-}
+
+-- 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))))
+
+-- 入力として入ってくるのは((s1 : State) -> (s2 : State) -> SemCond bPre s1 -> SemComm cm s1 s2)の部分
+-- 
+Satisfies : Cond -> Comm -> Cond -> Set
+Satisfies bPre cm bPost
+  = (s1 : State) -> (s2 : State) ->
+      SemCond bPre s1 -> SemComm cm s1 s2 -> SemCond bPost s2
+
+Soundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
+            HTProof bPre cm bPost -> Satisfies bPre cm bPost
+Soundness (PrimRule {bPre} {cm} {bPost} pr) s1 s2 q1 q2
+  = axiomValid bPre cm bPost pr s1 s2 q1 q2
+
+Soundness {.bPost} {.Skip} {bPost} (SkipRule .bPost) s1 s2 q1 q2
+  = substId1 State {Level.zero} {State} {s1} {s2} (proj₂ q2) (SemCond bPost) q1
+Soundness {bPre} {.Abort} {bPost} (AbortRule .bPre .bPost) s1 s2 q1 ()
+Soundness (WeakeningRule {bPre} {bPre'} {cm} {bPost'} {bPost} tautPre pr tautPost)
+          s1 s2 q1 q2
+  = let hyp : Satisfies bPre' cm bPost'
+        hyp = Soundness pr
+        r1 : SemCond bPre' s1
+        r1 = tautValid bPre bPre' tautPre s1 q1
+        r2 : SemCond bPost' s2
+        r2 = hyp s1 s2 r1 q2
+    in tautValid bPost' bPost tautPost s2 r2
+Soundness (SeqRule {bPre} {cm1} {bMid} {cm2} {bPost} pr1 pr2)
+           s1 s2 q1 q2
+  = let hyp1 : Satisfies bPre cm1 bMid
+        hyp1 = Soundness pr1
+        hyp2 : Satisfies bMid cm2 bPost
+        hyp2 = Soundness pr2
+        sMid : State
+        sMid = proj₁ q2
+        r1 : SemComm cm1 s1 sMid × SemComm cm2 sMid s2
+        r1 = proj₂ q2
+        r2 : SemComm cm1 s1 sMid
+        r2 = proj₁ r1
+        r3 : SemComm cm2 sMid s2
+        r3 = proj₂ r1
+        r4 : SemCond bMid sMid
+        r4 = hyp1 s1 sMid q1 r2
+    in hyp2 sMid s2 r4 r3
+Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse)
+          s1 s2 q1 q2
+  = let hypThen : Satisfies (bPre /\ b) cmThen bPost
+        hypThen = Soundness pThen
+        hypElse : Satisfies (bPre /\ neg b) cmElse bPost
+        hypElse = Soundness pElse
+        rThen : RelOpState.comp
+                  (RelOpState.delta (SemCond b))
+                  (SemComm cmThen) s1 s2 ->
+                SemCond bPost s2
+        rThen = λ h ->
+                  let t1 : SemCond b s1 × SemComm cmThen s1 s2
+                      t1 = (proj₂ (RelOpState.deltaRestPre
+                                     (SemCond b)
+                                     (SemComm cmThen) s1 s2)) h
+                      t2 : SemCond (bPre /\ b) s1
+                      t2 = (proj₂ (respAnd bPre b s1))
+                           (q1 , proj₁ t1)
+                  in hypThen s1 s2 t2 (proj₂ t1)
+        rElse : RelOpState.comp
+                  (RelOpState.delta (NotP (SemCond b)))
+                  (SemComm cmElse) s1 s2 ->
+                SemCond bPost s2
+        rElse = λ h ->
+                  let t10 : (NotP (SemCond b) s1) ×
+                            (SemComm cmElse s1 s2)
+                      t10 = proj₂ (RelOpState.deltaRestPre
+                                    (NotP (SemCond b)) (SemComm cmElse) s1 s2)
+                            h
+                      t6 : SemCond (neg b) s1
+                      t6 = proj₂ (respNeg b s1) (proj₁ t10)
+                      t7 : SemComm cmElse s1 s2
+                      t7 = proj₂ t10
+                      t8 : SemCond (bPre /\ neg b) s1
+                      t8 = proj₂ (respAnd bPre (neg b) s1)
+                           (q1 , t6)
+                  in hypElse s1 s2 t8 t7
+    in when rThen rElse q2
+Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2
+  = proj₂ (respAnd bInv (neg b) s2) t20
+    where
+      hyp : Satisfies (bInv /\ b) cm' bInv
+      hyp = Soundness pr
+      n : ℕ
+      n = proj₁ q2
+      Rel1 : ℕ -> Rel State (Level.zero)
+      Rel1 = λ m ->
+               RelOpState.repeat
+                 m
+                 (RelOpState.comp (RelOpState.delta (SemCond b))
+                                  (SemComm cm'))
+      t1 : RelOpState.comp
+             (Rel1 n)
+             (RelOpState.delta (NotP (SemCond b))) s1 s2
+      t1 = proj₂ q2
+      t15 : (Rel1 n s1 s2) × (NotP (SemCond b) s2)
+      t15 = proj₂ (RelOpState.deltaRestPost
+                    (NotP (SemCond b)) (Rel1 n) s1 s2)
+              t1
+      t16 : Rel1 n s1 s2
+      t16 = proj₁ t15
+      t17 : NotP (SemCond b) s2
+      t17 = proj₂ t15
+      lem1 : (m : ℕ) -> (ss2 : State) -> Rel1 m s1 ss2 ->
+             SemCond bInv ss2
+      lem1 ℕ.zero ss2 h
+        = substId1 State (proj₂ h) (SemCond bInv) q1
+      lem1 (ℕ.suc n) ss2 h
+        = let hyp2 : (z : State) -> Rel1 n s1 z ->
+                     SemCond bInv z
+              hyp2 = lem1 n
+              s20 : State
+              s20 = proj₁ h
+              t21 : Rel1 n s1 s20
+              t21 = proj₁ (proj₂ h)
+              t22 : (SemCond b s20) × (SemComm cm' s20 ss2)
+              t22 = proj₂ (RelOpState.deltaRestPre
+                            (SemCond b) (SemComm cm') s20 ss2)
+                    (proj₂ (proj₂ h))
+              t23 : SemCond (bInv /\ b) s20
+              t23 = proj₂ (respAnd bInv b s20)
+                    (hyp2 s20 t21 , proj₁ t22)
+          in hyp s20 ss2 t23 (proj₂ t22)
+      t20 : SemCond bInv s2 × SemCond (neg b) s2
+      t20 = lem1 n s2 t16 , proj₂ (respNeg b s2) t17
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/RelOp.agda	Tue Oct 13 18:01:42 2020 +0900
@@ -0,0 +1,81 @@
+{-# OPTIONS --universe-polymorphism #-}
+
+open import Level
+open import Data.Empty
+open import Data.Product
+open import Data.Nat
+open import Data.Sum
+open import Data.Unit
+open import Relation.Binary
+open import Relation.Binary.Core
+open import Relation.Nullary
+open import utilities
+
+module RelOp (S : Set) where
+
+data Id {l} {X : Set} : Rel X l where
+  ref : {x : X} -> Id x x
+
+-- substId1 | x == y & P(x) => P(y)
+substId1 :  ∀ {l} -> {X : Set} -> {x y : X} ->
+           Id {l} x y -> (P : Pred X) -> P x -> P y
+substId1 ref P q = q
+
+-- substId2 | x == y & P(y) => P(x)
+substId2 :  ∀ {l} -> {X : Set} -> {x y : X} ->
+           Id {l} x  y -> (P : Pred X) -> P y -> P x
+substId2 ref P q = q
+
+-- for X ⊆ S (formally, X : Pred S)
+-- delta X = { (a, a) | a ∈ X }
+delta : ∀ {l} -> Pred S -> Rel S l
+delta X a b = X a × Id a b 
+
+-- deltaGlob = delta S
+deltaGlob : ∀ {l} -> Rel S l
+deltaGlob = delta (λ (s : S) → ⊤)
+
+-- emptyRel = \varnothing
+emptyRel : Rel S Level.zero
+emptyRel a b = ⊥
+
+-- comp R1 R2 = R2 ∘ R1 (= R1; R2)
+comp : ∀ {l} -> Rel S l -> Rel S l -> Rel S l
+comp R1 R2 a b = ∃ (λ (a' : S) → R1 a a' × R2 a' b)
+
+-- union R1 R2 = R1 ∪ R2
+union : ∀ {l} -> Rel S l -> Rel S l -> Rel S l
+union R1 R2 a b = R1 a b ⊎ R2 a b
+
+-- repeat n R = R^n
+repeat : ∀ {l} -> ℕ -> Rel S l -> Rel S l
+repeat ℕ.zero R = deltaGlob
+repeat (ℕ.suc m) R = comp (repeat m R) R
+
+-- unionInf f = ⋃_{n ∈ ω} f(n)
+unionInf : ∀ {l} -> (ℕ -> Rel S l) -> Rel S l
+unionInf f a b = ∃ (λ (n : ℕ) → f n a b)
+-- restPre X R = { (s1,s2) ∈ R | s1 ∈ X }
+restPre : ∀ {l} -> Pred S -> Rel S l -> Rel S l
+restPre X R a b = X a × R a b
+
+-- restPost X R = { (s1,s2) ∈ R | s2 ∈ X }
+restPost : ∀ {l} -> Pred S -> Rel S l -> Rel S l
+restPost X R a b = R a b × X b
+
+deltaRestPre : (X : Pred S) -> (R : Rel S Level.zero) -> (a b : S) ->
+               Iff (restPre X R a b) (comp (delta X) R a b)
+deltaRestPre X R a b
+  = (λ (h : restPre X R a b) → a , (proj₁ h , ref) , proj₂ h) ,
+     λ (h : comp (delta X) R a b) → proj₁ (proj₁ (proj₂ h)) ,
+       substId2
+         (proj₂ (proj₁ (proj₂ h)))
+         (λ z → R z b) (proj₂ (proj₂ h))
+
+deltaRestPost : (X : Pred S) -> (R : Rel S Level.zero) -> (a b : S) ->
+                Iff (restPost X R a b) (comp R (delta X) a b)
+deltaRestPost X R a b
+  = (λ (h : restPost X R a b) → b , proj₁ h , proj₂ h , ref) ,
+     λ (h : comp R (delta X) a b) →
+       substId1 (proj₂ (proj₂ (proj₂ h))) (R a) (proj₁ (proj₂ h)) ,
+       substId1 (proj₂ (proj₂ (proj₂ h))) X (proj₁ (proj₂ (proj₂ h)))
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/gearswhile.agda	Tue Oct 13 18:01:42 2020 +0900
@@ -0,0 +1,59 @@
+module gearswhile where
+
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Nat
+open import Relation.Binary.PropositionalEquality
+open import Data.Nat.Properties
+open import Relation.Binary.Definitions 
+open import Data.Empty
+
+open import utilities
+open  _/\_
+
+record Envc : Set (succ Zero) where
+  field
+    c10 : ℕ
+    varn : ℕ
+    vari : ℕ
+open Envc
+
+data whileTestState  : Set where
+  s1 : whileTestState
+  s2 : whileTestState
+  sf : whileTestState
+
+whileTestStateP : whileTestState → Envc →  Set
+whileTestStateP s1 env = (vari env ≡ 0) /\ (varn env ≡ c10 env)
+whileTestStateP s2 env = (varn env + vari env ≡ c10 env)
+whileTestStateP sf env = (vari env ≡ c10 env)
+
+
+whileLoopPwP : {l : Level} {t : Set l}   → (env : Envc ) → whileTestStateP s2 env
+    → (next : (env : Envc ) → whileTestStateP s2 env  → t)
+    → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
+whileLoopPwP env s next exit with <-cmp 0 (varn env)
+whileLoopPwP env s next exit | tri≈ ¬a b ¬c = exit env (lem (sym b) s)
+  where
+    lem : (varn env ≡ 0) → (varn env + vari env ≡ c10 env) → vari env ≡ c10 env
+    lem refl refl = refl
+whileLoopPwP env s next exit | tri< a ¬b ¬c  = next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) (proof5 a)
+  where
+    1<0 : 1 ≤ zero → ⊥
+    1<0 ()
+    proof5 : (suc zero  ≤ (varn  env))  → (varn env - 1) + (vari env + 1) ≡ c10 env
+    proof5 (s≤s lt) with varn  env
+    proof5 (s≤s z≤n) | zero = ⊥-elim (1<0 a)
+    proof5 (s≤s (z≤n {n'}) ) | suc n = let open ≡-Reasoning in
+      begin
+        n' + (vari env + 1)
+      ≡⟨ cong ( λ z → n' + z ) ( +-sym  {vari env} {1} )  ⟩
+        n' + (1 + vari env )
+      ≡⟨ sym ( +-assoc (n')  1 (vari env) ) ⟩
+        (n' + 1) + vari env
+      ≡⟨ cong ( λ z → z + vari env )  +1≡suc  ⟩
+        (suc n' ) + vari env
+      ≡⟨⟩
+        varn env + vari env
+      ≡⟨ s  ⟩
+         c10 env
+      ∎
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/gearswhilehoare.agda	Tue Oct 13 18:01:42 2020 +0900
@@ -0,0 +1,239 @@
+module gearswhilehoare where
+
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Nat
+open import Data.Empty
+open import Data.Nat.Properties
+open import Relation.Nullary using (¬_; Dec; yes; no)
+
+open import Agda.Builtin.Unit
+
+open import Relation.Binary
+open import utilities
+open  _/\_
+
+open import Relation.Binary.PropositionalEquality
+
+
+record Envc : Set (succ Zero) where
+  field
+    c10 : ℕ
+    varn : ℕ
+    vari : ℕ
+open Envc
+
+whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Envc → t) → t
+whileTestP c10 next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } )
+
+-- equivalent of whileLoopP but it looks like an induction on varn
+whileLoopP' : {l : Level} {t : Set l} → Envc → (next : Envc → t) → (exit : Envc → t) → t
+whileLoopP' env@record { c10 = c10 ; varn = zero ; vari = vari } _ exit = exit env
+whileLoopP' record { c10 = c10 ; varn = suc varn1 ; vari = vari } next _ =
+  next (record {c10 = c10 ; varn = varn1 ; vari = suc vari })
+
+-- 停止するループ
+loopP’ : {l : Level} {t : Set l} → Envc → (exit : Envc → t) → t
+loopP’ record { c10 = c10 ; varn = zero ; vari = vari } exit =
+  exit (record { c10 = c10 ; varn = zero ; vari = vari })
+loopP’ record { c10 = c10 ; varn = (suc varn1) ; vari = vari } exit = whileLoopP' (record { c10 = c10 ; varn = (suc varn1) ; vari = vari }) (λ env → loopP’ (record { c10 = c10 ; varn = varn1 ; vari = vari }) exit ) exit
+
+whileTestPCall’ : (c10 : ℕ ) → Envc
+whileTestPCall’ c10 = whileTestP {_} {_} c10 (λ env → loopP’ env (λ env → env))
+
+-- normal loop without termination
+{-# TERMINATING #-}
+loopP : {l : Level} {t : Set l} → Envc → (exit : Envc → t) → t
+loopP env exit = whileLoopP' env (λ env → loopP env exit ) exit
+
+whileTestPCall : (c10 :  ℕ ) → Envc
+whileTestPCall c10 = whileTestP {_} {_} c10 (λ env → loopP env (λ env →  env))
+
+-- whileTestPCall 10
+-- record { c10 = 10 ; varn = 0 ; vari = 10 }
+
+record Env : Set (succ Zero) where
+  field
+    varn : ℕ
+    vari : ℕ
+open Env
+
+{-# TERMINATING #-} --                                                  ↓PreCondition(Invaliant)
+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' env1 (proof3 p ) next
+    where
+      env1 = record env {varn = (varn  env) - 1 ; vari = (vari env) + 1}
+      1<0 : 1 ≤ zero → ⊥
+      1<0 ()
+      proof3 : (suc zero  ≤ (varn  env))  → varn env1 + vari env1 ≡ c10
+      proof3 (s≤s lt) with varn  env
+      proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p)
+      proof3 (s≤s (z≤n {n'}) ) | suc n =  let open ≡-Reasoning  in
+          begin
+             n' + (vari env + 1)
+          ≡⟨ cong ( λ z → n' + z ) ( +-sym  {vari env} {1} )  ⟩
+             n' + (1 + vari env )
+          ≡⟨ sym ( +-assoc (n')  1 (vari env) ) ⟩
+             (n' + 1) + vari env
+          ≡⟨ cong ( λ z → z + vari env )  +1≡suc  ⟩
+             (suc n' ) + vari env
+          ≡⟨⟩
+             varn env + vari env
+          ≡⟨ proof  ⟩
+             c10
+          ∎
+
+--
+-- codeGears with states of condition
+--
+data whileTestState  : Set where
+  s1 : whileTestState
+  s2 : whileTestState
+  sf : whileTestState
+
+whileTestStateP : whileTestState → Envc →  Set
+whileTestStateP s1 env = (vari env ≡ 0) /\ (varn env ≡ c10 env)
+whileTestStateP s2 env = (varn env + vari env ≡ c10 env)
+whileTestStateP sf env = (vari env ≡ c10 env)
+
+whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) → ((env : Envc ) → whileTestStateP s1 env → t) → t
+whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
+   env : Envc
+   env = whileTestP c10 ( λ env → env )
+
+whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env
+  → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env  → t)
+  → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
+whileLoopPwP' zero env refl refl next exit = exit env refl
+whileLoopPwP' (suc n) env refl refl next exit = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env))
+
+
+loopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
+loopPwP' zero env refl refl exit = exit env refl
+loopPwP' (suc n) env refl refl exit  = whileLoopPwP' (suc n) env refl refl (λ env x y → loopPwP' n env x y exit) exit
+
+loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) → (seq : whileTestStateP s2 env) → loopPwP' n env (sym eq) seq λ env₁ x → (vari env₁ ≡ c10 env₁)
+loopHelper zero env eq refl rewrite eq = refl
+loopHelper (suc n) env eq refl rewrite eq = loopHelper n (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) refl (+-suc n (vari env))
+
+
+
+whileLoopPwP : {l : Level} {t : Set l}   → (env : Envc ) → whileTestStateP s2 env
+    → (next : (env : Envc ) → whileTestStateP s2 env  → t)
+    → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
+whileLoopPwP env s next exit with <-cmp 0 (varn env)
+whileLoopPwP env s next exit | tri≈ ¬a b ¬c = exit env (lem (sym b) s)
+  where
+    lem : (varn env ≡ 0) → (varn env + vari env ≡ c10 env) → vari env ≡ c10 env
+    lem refl refl = refl
+whileLoopPwP env s next exit | tri< a ¬b ¬c  = next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) (proof5 a)
+  where
+    1<0 : 1 ≤ zero → ⊥
+    1<0 ()
+    proof5 : (suc zero  ≤ (varn  env))  → (varn env - 1) + (vari env + 1) ≡ c10 env
+    proof5 (s≤s lt) with varn  env
+    proof5 (s≤s z≤n) | zero = ⊥-elim (1<0 a)
+    proof5 (s≤s (z≤n {n'}) ) | suc n = let open ≡-Reasoning in
+      begin
+        n' + (vari env + 1)
+      ≡⟨ cong ( λ z → n' + z ) ( +-sym  {vari env} {1} )  ⟩
+        n' + (1 + vari env )
+      ≡⟨ sym ( +-assoc (n')  1 (vari env) ) ⟩
+        (n' + 1) + vari env
+      ≡⟨ cong ( λ z → z + vari env )  +1≡suc  ⟩
+        (suc n' ) + vari env
+      ≡⟨⟩
+        varn env + vari env
+      ≡⟨ s  ⟩
+         c10 env
+      ∎
+
+{-# TERMINATING #-}
+loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
+loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit
+
+whileTestPCallwP : (c :  ℕ ) → Set
+whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c10 env )  ) where
+   conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
+   conv e record { pi1 = refl ; pi2 = refl } = +zero
+
+
+whileTestPCallwP' : (c :  ℕ ) → Set
+whileTestPCallwP' c = whileTestPwP {_} {_} c (λ env s → loopPwP' (varn env) env refl (conv env s) ( λ env s → vari env ≡ c10 env )  ) where
+  conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
+  conv e record { pi1 = refl ; pi2 = refl } = +zero
+
+helperCallwP : (c : ℕ) → whileTestPCallwP' c
+helperCallwP c = whileTestPwP {_} {_} c (λ env s → loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero)
+
+
+
+--
+-- Using imply relation to make soundness explicit
+-- termination is shown by induction on varn
+--
+
+data _implies_  (A B : Set ) : Set (succ Zero) where
+    proof : ( A → B ) → A implies B
+
+implies2p : {A B : Set } → A implies B  → A → B
+implies2p (proof x) = x
+
+whileTestPSem :  (c : ℕ) → whileTestP c ( λ env → ⊤ implies (whileTestStateP s1 env) )
+whileTestPSem c = proof ( λ _ → record { pi1 = refl ; pi2 = refl } )
+
+SemGears : (f : {l : Level } {t : Set l } → (e0 : Envc ) → ((e : Envc) → t)  → t ) → Set (succ Zero)
+SemGears f = Envc → Envc → Set
+
+GearsUnitSound : (e0 e1 : Envc) {pre : Envc → Set} {post : Envc → Set}
+   → (f : {l : Level } {t : Set l } → (e0 : Envc ) → (Envc → t)  → t )
+   → (fsem : (e0 : Envc ) → f e0 ( λ e1 → (pre e0) implies (post e1)))
+   → f e0 (λ e1 → pre e0 implies post e1)
+GearsUnitSound e0 e1 f fsem = fsem e0
+
+whileTestPSemSound : (c : ℕ ) (output : Envc ) → output ≡ whileTestP c (λ e → e) → ⊤ implies ((vari output ≡ 0) /\ (varn output ≡ c))
+whileTestPSemSound c output refl = whileTestPSem c
+
+
+whileConvPSemSound : {l : Level} → (input : Envc) → (whileTestStateP s1 input ) implies (whileTestStateP s2 input)
+whileConvPSemSound input = proof λ x → (conv input x) where
+  conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
+  conv e record { pi1 = refl ; pi2 = refl } = +zero
+
+loopPP : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
+loopPP zero input refl = input
+loopPP (suc n) input refl =
+    loopPP n (record input { varn = pred (varn input) ; vari = suc (vari input)}) refl
+
+whileLoopPSem : {l : Level} {t : Set l}   → (input : Envc ) → whileTestStateP s2 input
+  → (next : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output)  → t)
+  → (exit : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output)  → t) → t
+whileLoopPSem env s next exit with varn env | s
+... | zero | _ = exit env (proof (λ z → z))
+... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } ) (proof λ x → +-suc varn (vari env) )
+
+loopPPSem : (input output : Envc ) →  output ≡ loopPP (varn input)  input refl
+  → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output)
+loopPPSem input output refl s2p = loopPPSemInduct (varn input) input  refl refl s2p
+  where
+    lem : (n : ℕ) → (env : Envc) → n + suc (vari env) ≡ suc (n + vari env)
+    lem n env = +-suc (n) (vari env)
+    loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) →  (loopeq : output ≡ loopPP n current eq)
+      → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output)
+    loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl)
+    loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) =
+        whileLoopPSem current refl
+            (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
+            (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
+
+whileLoopPSemSound : {l : Level} → (input output : Envc )
+   → whileTestStateP s2 input
+   →  output ≡ loopPP (varn input) input refl
+   → (whileTestStateP s2 input ) implies ( whileTestStateP sf output )
+whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre
+
+
+
+-- whileTestSound : {l : Level} (c : ℕ) → (output : Envc) → ⊤ →  whileTestStateP sf output
+-- whileTestSound {l} c record { c10 = c10 ; varn = varn ; vari = vari } top = implies2p (whileLoopPSemSound {l} (record { c10 = c ; varn = c ; vari = zero }) (record { c10 = c10 ; varn = c ; vari = vari}) (+zero) {!!}) (implies2p (whileConvPSemSound {l} (record { c10 = c ; varn = c ; vari = zero })) (implies2p (whileTestPSemSound c (whileTestP c (λ e → e)) refl) top))
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/utilities.agda	Tue Oct 13 18:01:42 2020 +0900
@@ -0,0 +1,171 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+module utilities where
+
+open import Function
+open import Data.Nat
+open import Data.Product
+open import Data.Bool hiding ( _≟_  ; _≤?_)
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Relation.Binary.PropositionalEquality
+
+Pred : Set -> Set₁
+Pred X = X -> Set
+
+Imply : Set -> Set -> Set
+Imply X Y = X -> Y
+
+Iff : Set -> Set -> Set
+Iff X Y = Imply X Y × Imply Y X
+
+record _/\_ {n : Level } (a : Set n) (b : Set n): Set n where
+  field
+    pi1 : a
+    pi2 : b
+
+open  _/\_
+
+_-_ : ℕ → ℕ → ℕ 
+x - zero  = x
+zero - _  = zero
+(suc x) - (suc y)  = x - y
+
++zero : { y : ℕ } → y + zero  ≡ y
++zero {zero} = refl
++zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
+
+
++-sym : { x y : ℕ } → x + y ≡ y + x
++-sym {zero} {zero} = refl
++-sym {zero} {suc y} = let open ≡-Reasoning  in
+          begin
+            zero + suc y 
+          ≡⟨⟩
+            suc y
+          ≡⟨ sym +zero ⟩
+            suc y + zero
+          ∎
++-sym {suc x} {zero} =  let open ≡-Reasoning  in
+          begin
+            suc x + zero
+          ≡⟨ +zero  ⟩
+            suc x
+          ≡⟨⟩
+            zero + suc x
+          ∎
++-sym {suc x} {suc y} = cong ( λ z → suc z ) (  let open ≡-Reasoning  in
+          begin
+            x + suc y
+          ≡⟨ +-sym {x} {suc y} ⟩
+            suc (y + x)
+          ≡⟨ cong ( λ z → suc z )  (+-sym {y} {x}) ⟩
+            suc (x + y)
+          ≡⟨ sym ( +-sym {y} {suc x}) ⟩
+            y + suc x
+          ∎ )
+
+
+minus-plus : { x y : ℕ } → (suc x - 1) + (y + 1) ≡ suc x + y
+minus-plus {zero} {y} = +-sym {y} {1}
+minus-plus {suc x} {y} =  cong ( λ z → suc z ) (minus-plus {x} {y})
+
++1≡suc : { x : ℕ } → x + 1 ≡ suc x
++1≡suc {zero} = refl
++1≡suc {suc x} = cong ( λ z → suc z ) ( +1≡suc {x} )
+
+lt : ℕ → ℕ → Bool
+lt x y with (suc x ) ≤? y
+lt x y | yes p = true
+lt x y | no ¬p = false
+
+predℕ : {n :  ℕ } → lt 0 n ≡ true  →  ℕ
+predℕ {zero} ()
+predℕ {suc n} refl = n
+
+predℕ+1=n : {n :  ℕ } → (less : lt 0 n ≡ true ) → (predℕ less) + 1 ≡ n
+predℕ+1=n {zero} ()
+predℕ+1=n {suc n} refl = +1≡suc
+
+suc-predℕ=n : {n :  ℕ } → (less : lt 0 n ≡ true ) → suc (predℕ less) ≡ n
+suc-predℕ=n {zero} ()
+suc-predℕ=n {suc n} refl = refl
+
+Equal : ℕ → ℕ → Bool
+Equal x y with x ≟ y
+Equal x y | yes p = true
+Equal x y | no ¬p = false
+
+_⇒_ : Bool → Bool → Bool
+false  ⇒  _ = true
+true  ⇒  true = true
+true  ⇒  false = false
+
+⇒t : {x : Bool} → x  ⇒ true  ≡ true
+⇒t {x} with x
+⇒t {x} | false = refl
+⇒t {x} | true = refl
+
+f⇒ : {x : Bool} → false  ⇒ x  ≡ true
+f⇒ {x} with x
+f⇒ {x} | false = refl
+f⇒ {x} | true = refl
+
+∧-pi1 : { x y : Bool } → x  ∧  y  ≡ true  → x  ≡ true
+∧-pi1 {x} {y} eq with x | y | eq
+∧-pi1 {x} {y} eq | false | b | ()
+∧-pi1 {x} {y} eq | true | false | ()
+∧-pi1 {x} {y} eq | true | true | refl = refl
+
+∧-pi2 : { x y : Bool } →  x  ∧  y  ≡ true  → y  ≡ true
+∧-pi2 {x} {y} eq with x | y | eq
+∧-pi2 {x} {y} eq | false | b | ()
+∧-pi2 {x} {y} eq | true | false | ()
+∧-pi2 {x} {y} eq | true | true | refl = refl
+
+∧true : { x : Bool } →  x  ∧  true  ≡ x
+∧true {x} with x
+∧true {x} | false = refl
+∧true {x} | true = refl
+
+true∧ : { x : Bool } →  true  ∧  x  ≡ x
+true∧ {x} with x
+true∧ {x} | false = refl
+true∧ {x} | true = refl
+bool-case : ( x : Bool ) { p : Set } → ( x ≡ true  → p ) → ( x ≡ false  → p ) → p
+bool-case x T F with x
+bool-case x T F | false = F refl
+bool-case x T F | true = T refl
+
+impl⇒ :  {x y : Bool} → (x  ≡ true → y  ≡ true ) → x  ⇒ y  ≡ true
+impl⇒ {x} {y} p = bool-case x (λ x=t →   let open ≡-Reasoning  in
+          begin
+            x  ⇒ y
+          ≡⟨  cong ( λ z → x  ⇒ z ) (p x=t ) ⟩
+            x  ⇒  true
+          ≡⟨ ⇒t ⟩
+            true
+          ∎
+    ) ( λ x=f →  let open ≡-Reasoning  in
+          begin
+            x  ⇒  y
+          ≡⟨  cong ( λ z → z  ⇒  y ) x=f ⟩
+            true
+          ∎
+  )
+ 
+Equal→≡ : { x y : ℕ } →  Equal x y ≡ true → x ≡ y
+Equal→≡ {x} {y} eq with x ≟ y
+Equal→≡ {x} {y} refl | yes refl = refl
+Equal→≡ {x} {y} () | no ¬p 
+
+Equal+1 : { x y : ℕ } →  Equal x y ≡ Equal (suc x) (suc y)
+Equal+1 {x} {y} with  x ≟ y
+Equal+1 {x} {.x} | yes refl = {!!}
+Equal+1 {x} {y} | no ¬p = {!!}
+
+open import Data.Empty 
+
+≡→Equal : { x y : ℕ } → x ≡ y →  Equal x y ≡ true 
+≡→Equal {x} {.x} refl with x ≟ x
+≡→Equal {x} {.x} refl | yes refl = refl
+≡→Equal {x} {.x} refl | no ¬p = ⊥-elim ( ¬p refl )
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/whileimple.agda	Tue Oct 13 18:01:42 2020 +0900
@@ -0,0 +1,109 @@
+module whilespecimple where
+
+open import Relation.Binary.PropositionalEquality
+open import Data.Bool
+open import Relation.Binary
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Data.Empty
+open import Agda.Builtin.Sigma
+open import Data.Product
+open import Data.Nat
+
+
+open import utilities hiding ( _/\_ )
+open import whiletest
+open import Hoare PrimComm Cond Axiom Tautology _and_ neg
+open import whilespec
+
+State : Set
+State = Env
+
+open import RelOp 
+module RelOpState = RelOp State
+
+
+SemCond : Cond -> State -> Set
+SemCond c p = c p ≡ true
+
+PrimSemComm : ∀ {l} -> PrimComm -> Rel State l
+PrimSemComm prim s1 s2 =  Id State (prim s1) s2
+
+tautValid : (b1 b2 : Cond) -> Tautology b1 b2 -> (s : State) -> SemCond b1 s -> SemCond b2 s
+tautValid b1 b2 taut s cond with b1 s | b2 s | taut s
+tautValid b1 b2 taut s () | false | false | refl
+tautValid b1 b2 taut s _ | false | true | refl = refl
+tautValid b1 b2 taut s _ | true | false | ()
+tautValid b1 b2 taut s _ | true | true | refl = refl
+
+
+axiomValid : ∀ {l} -> (bPre : Cond) -> (pcm : PrimComm) -> (bPost : Cond) ->
+                  (ax : Axiom bPre pcm bPost) -> (s1 s2 : State) ->
+                  SemCond bPre s1 -> PrimSemComm {l} pcm s1 s2 -> SemCond bPost s2 
+axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref with bPre s1 | bPost (pcm s1) | ax s1
+axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) () ref | false | false | refl
+axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | false | true | refl = refl
+axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | false | ()
+axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | true | refl = refl
+
+
+respNeg : (b : Cond) -> (s : State) ->
+               Iff (SemCond (neg b) s) (¬ SemCond b s)
+respNeg b s = ( left , right ) where
+    left : not (b s) ≡ true → (b s) ≡ true → ⊥
+    left ne with b s
+    left refl | false = λ ()
+    left () | true
+    right : ((b s) ≡ true → ⊥) → not (b s) ≡ true
+    right ne with b s
+    right ne | false = refl
+    right ne | true = ⊥-elim ( ne refl )
+
+_/\_ : Cond -> Cond -> Cond
+b1 /\ b2 = b1 and b2
+
+_\/_ : Cond -> Cond -> Cond
+b1 \/ b2 = neg (neg b1 /\ neg b2)
+
+respAnd : (b1 b2 : Cond) -> (s : State) ->
+               Iff (SemCond (b1 /\ b2) s)
+                   ((SemCond b1 s) × (SemCond b2 s))
+respAnd b1 b2 s = ( left , right ) where
+     left : b1 s ∧ b2 s ≡ true → (b1 s ≡ true)  ×  (b2 s ≡ true)
+     left and with b1 s | b2 s
+     left () | false | false 
+     left () | false | true 
+     left () | true | false 
+     left refl | true | true = ( refl , refl )
+     right :  (b1 s ≡ true)  ×  (b2 s ≡ true) →  b1 s ∧ b2 s ≡ true
+     right ( x1 , x2 ) with b1 s | b2 s
+     right (() , ()) | false | false 
+     right (() , _) | false | true 
+     right (_ , ()) | true | false 
+     right (refl , refl) | true | true = refl
+
+
+open import HoareSoundness
+    Cond 
+    PrimComm 
+    neg 
+    _and_ 
+    Tautology 
+    State 
+    SemCond 
+    tautValid 
+    respNeg 
+    respAnd 
+    PrimSemComm 
+    Axiom 
+    axiomValid
+
+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/whileploof.agda	Tue Oct 13 18:01:42 2020 +0900
@@ -0,0 +1,164 @@
+module whilespecification where
+
+open import Function
+open import Data.Nat
+open import Data.Bool
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Relation.Binary.PropositionalEquality
+
+open import Data.Nat.Properties
+
+open import utilities hiding ( _/\_ )
+open import whiletest
+
+open import Hoare PrimComm Cond Axiom Tautology _and_ neg
+
+open Env
+
+initCond : Cond
+initCond env = true
+
+termCond : {c10 : ℕ} → Cond
+termCond {c10} env = Equal (vari env) c10
+
+stmt1Cond : {c10 : ℕ} → Cond
+stmt1Cond {c10} env = Equal (varn env) c10
+
+init-case : {c10 :  ℕ} → (env : Env) → (( λ e → true  ⇒ stmt1Cond {c10} e ) (record { varn = c10 ; vari = vari env }) ) ≡ true 
+init-case {c10} _ = impl⇒ ( λ cond → ≡→Equal refl )
+
+stmt2Cond : {c10 : ℕ} → Cond
+stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)
+
+whileInv : {c10 : ℕ} → Cond
+whileInv {c10} env = Equal ((varn env) + (vari env)) c10
+
+whileInv' : {c10 : ℕ} → Cond
+whileInv'{c10}  env = Equal ((varn env) + (vari env)) (suc c10) ∧ lt zero (varn env)
+
+lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
+lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
+  begin
+    (Equal (varn env) c10 ) ∧ true
+  ≡⟨ ∧true ⟩
+    Equal (varn env) c10 
+  ≡⟨ cond ⟩
+    true
+  ∎ )
+
+
+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
+  where
+     lemma21 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env ≡ c10
+     lemma21 eq = Equal→≡ (∧-pi1 eq)
+     lemma22 : {env : Env } → {c10 : ℕ} → stmt2Cond {c10} env ≡ true → vari env ≡ 0
+     lemma22 eq = Equal→≡ (∧-pi2 eq)
+     lemma23 :  {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env + vari env ≡ c10
+     lemma23 {env} {c10} eq = let open ≡-Reasoning  in
+          begin
+            varn env + vari env
+          ≡⟨ cong ( \ x -> x + vari env ) (lemma21 eq  ) ⟩
+            c10 + vari env
+          ≡⟨ cong ( \ x -> c10 + x) (lemma22 {env} {c10} eq ) ⟩
+            c10 + 0
+          ≡⟨ +-sym {c10} {0} ⟩
+            0 + c10 
+          ≡⟨⟩
+            c10 
+          ∎
+     lemma2 :  {c10 : ℕ} → Tautology stmt2Cond whileInv
+     lemma2 {c10} env = bool-case (stmt2Cond env) (
+        λ eq → let open ≡-Reasoning  in
+          begin
+            (stmt2Cond env)  ⇒  (whileInv env)
+          ≡⟨⟩
+            (stmt2Cond env)  ⇒ ( Equal (varn env + vari env) c10 )
+          ≡⟨  cong ( \ x -> (stmt2Cond  {c10} env)  ⇒ ( Equal x c10 ) ) ( lemma23 {env} eq ) ⟩
+            (stmt2Cond env)  ⇒ (Equal c10 c10)
+          ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ x ) (≡→Equal refl )  ⟩
+            (stmt2Cond {c10} env)  ⇒  true
+          ≡⟨ ⇒t ⟩
+            true
+          ∎
+        ) (
+         λ ne → let open ≡-Reasoning  in
+          begin
+            (stmt2Cond env)  ⇒  (whileInv env)
+          ≡⟨ cong ( \ x -> x  ⇒  (whileInv env) ) ne ⟩
+             false  ⇒  (whileInv {c10} env)
+          ≡⟨ f⇒ {whileInv {c10} env} ⟩
+            true
+          ∎
+        ) 
+     lemma3 :   Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv'
+     lemma3 env = impl⇒ ( λ cond →  let open ≡-Reasoning  in
+          begin
+            whileInv' (record { varn = varn env ; vari = vari env + 1 }) 
+          ≡⟨⟩
+             Equal (varn env + (vari env + 1)) (suc c10) ∧ (lt 0 (varn env) )
+          ≡⟨ cong ( λ z → Equal (varn env + (vari env + 1)) (suc c10) ∧ z ) (∧-pi2 cond )  ⟩
+             Equal (varn env + (vari env + 1)) (suc c10) ∧ true
+          ≡⟨ ∧true ⟩
+            Equal (varn env + (vari env + 1)) (suc c10)
+          ≡⟨ cong ( \ x -> Equal x (suc c10) ) (sym (+-assoc (varn env) (vari env) 1)) ⟩
+            Equal ((varn env + vari env) + 1) (suc c10)
+          ≡⟨ cong ( \ x -> Equal x (suc c10) ) +1≡suc ⟩
+            Equal (suc (varn env + vari env)) (suc c10)
+          ≡⟨ sym Equal+1 ⟩
+            Equal ((varn env + vari env) ) c10
+          ≡⟨ ∧-pi1  cond ⟩
+            true
+          ∎ )
+     lemma41 : (env : Env ) → {c10 : ℕ} → (varn env + vari env) ≡ (suc c10) → lt 0 (varn env) ≡ true  → Equal ((varn env - 1) + vari env) c10 ≡ true
+     lemma41 env {c10} c1 c2 =  let open ≡-Reasoning  in
+          begin
+            Equal ((varn env - 1) + vari env) c10
+          ≡⟨ cong ( λ z → Equal ((z - 1 ) +  vari env ) c10 ) (sym (suc-predℕ=n c2) )  ⟩
+            Equal ((suc (predℕ {varn env} c2 ) - 1) + vari env) c10
+          ≡⟨⟩
+            Equal ((predℕ {varn env} c2 ) + vari env) c10
+          ≡⟨  Equal+1 ⟩
+            Equal ((suc (predℕ {varn env} c2 )) + vari env) (suc c10)
+          ≡⟨ cong ( λ z → Equal (z  +  vari env ) (suc c10) ) (suc-predℕ=n c2 )  ⟩
+            Equal (varn env + vari env) (suc c10)
+          ≡⟨ cong ( λ z → (Equal z (suc c10) )) c1 ⟩
+            Equal (suc c10) (suc c10)
+          ≡⟨ ≡→Equal refl ⟩
+            true
+          ∎
+     lemma4 :  {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv
+     lemma4 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
+          begin
+            whileInv (record { varn = varn env - 1 ; vari = vari env })
+          ≡⟨⟩
+            Equal ((varn env - 1) + vari env) c10
+          ≡⟨ lemma41 env (Equal→≡ (∧-pi1  cond)) (∧-pi2  cond) ⟩
+            true
+          ∎
+        )
+     lemma51 : (z : Env ) → neg (λ z → lt zero (varn z)) z ≡ true → varn z ≡ zero
+     lemma51 z cond with varn z
+     lemma51 z refl | zero = refl
+     lemma51 z () | suc x
+     lemma5 : {c10 : ℕ} →  Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond
+     lemma5 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
+         begin
+            termCond env
+          ≡⟨⟩
+             Equal (vari env) c10 
+          ≡⟨⟩
+             Equal (zero + vari env) c10 
+          ≡⟨ cong ( λ z →  Equal (z + vari env) c10 )  (sym ( lemma51 env ( ∧-pi2  cond ) )) ⟩
+             Equal (varn env + vari env) c10 
+          ≡⟨ ∧-pi1  cond  ⟩
+             true
+          ∎
+        )
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/whilespec.agda	Tue Oct 13 18:01:42 2020 +0900
@@ -0,0 +1,178 @@
+module whilespec where
+
+open import Function
+open import Data.Nat
+open import Data.Bool
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Relation.Binary.PropositionalEquality
+
+open import Data.Nat.Properties
+
+open import utilities hiding ( _/\_ )
+open import whiletest
+
+open import Hoare PrimComm Cond Axiom Tautology _and_ neg
+
+open Env
+
+initCond : Cond
+initCond env = true
+
+termCond : {c10 : ℕ} → Cond
+termCond {c10} env = Equal (vari env) c10
+
+stmt1Cond : {c10 : ℕ} → Cond
+stmt1Cond {c10} env = Equal (varn env) c10
+
+init-case : {c10 :  ℕ} → (env : Env) → (( λ e → true  ⇒ stmt1Cond {c10} e ) (record { varn = c10 ; vari = vari env }) ) ≡ true 
+init-case {c10} _ = impl⇒ ( λ cond → ≡→Equal refl )
+
+stmt2Cond : {c10 : ℕ} → Cond
+stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)
+
+whileInv : {c10 : ℕ} → Cond
+whileInv {c10} env = Equal ((varn env) + (vari env)) c10
+
+whileInv' : {c10 : ℕ} → Cond
+whileInv'{c10}  env = (Equal ((varn env) + (vari env)) (suc c10)) ∧ lt zero (varn env)
+
+-- 事前条件が成り立つ場合に代入を行うと
+-- 代入後の事後条件が成り立つ証明
+-- axiomはcondとprimcommとcondを受け取ってsetを返す
+lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
+lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
+  begin
+    (Equal (varn env) c10 ) ∧ true
+  ≡⟨ ∧true ⟩
+    Equal (varn env) c10
+  ≡⟨ cond ⟩
+    true
+  ∎ )
+
+-- proof1' : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10})
+-- proof1' c10 = SeqRule {!!} {!!} 
+
+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
+  where
+     lemma21 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env ≡ c10
+     lemma21 eq = Equal→≡ (∧-pi1 eq)
+     lemma22 : {env : Env } → {c10 : ℕ} → stmt2Cond {c10} env ≡ true → vari env ≡ 0
+     lemma22 eq = Equal→≡ (∧-pi2 eq)
+     lemma23 :  {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env + vari env ≡ c10
+     lemma23 {env} {c10} eq = let open ≡-Reasoning  in
+          begin
+            varn env + vari env
+          ≡⟨ cong ( \ x -> x + vari env ) (lemma21 eq  ) ⟩
+            c10 + vari env
+          ≡⟨ cong ( \ x -> c10 + x) (lemma22 {env} {c10} eq ) ⟩
+            c10 + 0
+          ≡⟨ +-sym {c10} {0} ⟩
+            0 + c10 
+          ≡⟨⟩
+            c10 
+          ∎
+     -- while loopに入る前のconditionからループ不変条件への変換の証明
+     -- つまり状態の移動時の動作の証明を行なっている
+     lemma2 :  {c10 : ℕ} → Tautology stmt2Cond whileInv
+     lemma2 {c10} env = bool-case (stmt2Cond env) (
+        λ eq → let open ≡-Reasoning  in
+          begin
+            (stmt2Cond env)  ⇒  (whileInv env)
+          ≡⟨⟩
+            (stmt2Cond env)  ⇒ ( Equal (varn env + vari env) c10 )
+          ≡⟨  cong ( \ x -> (stmt2Cond  {c10} env)  ⇒ ( Equal x c10 ) ) ( lemma23 {env} eq ) ⟩
+            (stmt2Cond env)  ⇒ (Equal c10 c10)
+          ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ x ) (≡→Equal refl )  ⟩
+            (stmt2Cond {c10} env)  ⇒  true
+          ≡⟨ ⇒t ⟩
+            true
+          ∎
+        ) (
+         λ ne → let open ≡-Reasoning  in
+          begin
+            (stmt2Cond env)  ⇒  (whileInv env)
+          ≡⟨ cong ( \ x -> x  ⇒  (whileInv env) ) ne ⟩
+             false  ⇒  (whileInv {c10} env)
+          ≡⟨ f⇒ {whileInv {c10} env} ⟩
+            true
+          ∎
+        )
+        
+     -- While Loop内でのPCommの代入の証明
+     -- ここで使っているwhileInvの引数が謎。引数はcondのはずなのにBoolが引数になっている気がする
+     lemma3 : Axiom (λ e → whileInv e ∧ lt zero (varn e))
+              (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv'
+     lemma3 env = impl⇒ ( λ cond →  let open ≡-Reasoning  in
+          begin
+            whileInv' (record { varn = varn env ; vari = vari env + 1 }) 
+          ≡⟨⟩
+             Equal (varn env + (vari env + 1)) (suc c10) ∧ (lt 0 (varn env) )
+          ≡⟨ cong ( λ z → Equal (varn env + (vari env + 1)) (suc c10) ∧ z ) (∧-pi2 cond )  ⟩
+             Equal (varn env + (vari env + 1)) (suc c10) ∧ true
+          ≡⟨ ∧true ⟩
+            Equal (varn env + (vari env + 1)) (suc c10)
+          ≡⟨ cong ( \ x -> Equal x (suc c10) ) (sym (+-assoc (varn env) (vari env) 1)) ⟩
+            Equal ((varn env + vari env) + 1) (suc c10)
+          ≡⟨ cong ( \ x -> Equal x (suc c10) ) +1≡suc ⟩
+            Equal (suc (varn env + vari env)) (suc c10)
+          ≡⟨ sym Equal+1 ⟩
+            Equal ((varn env + vari env) ) c10
+          ≡⟨ ∧-pi1  cond ⟩
+            true
+          ∎ )
+     lemma41 : (env : Env ) → {c10 : ℕ} → (varn env + vari env) ≡ (suc c10) → lt 0 (varn env) ≡ true  → Equal ((varn env - 1) + vari env) c10 ≡ true
+     lemma41 env {c10} c1 c2 =  let open ≡-Reasoning  in
+          begin
+            Equal ((varn env - 1) + vari env) c10
+          ≡⟨ cong ( λ z → Equal ((z - 1 ) +  vari env ) c10 ) (sym (suc-predℕ=n c2) )  ⟩
+            Equal ((suc (predℕ {varn env} c2 ) - 1) + vari env) c10
+          ≡⟨⟩
+            Equal ((predℕ {varn env} c2 ) + vari env) c10
+          ≡⟨  Equal+1 ⟩
+            Equal ((suc (predℕ {varn env} c2 )) + vari env) (suc c10)
+          ≡⟨ cong ( λ z → Equal (z  +  vari env ) (suc c10) ) (suc-predℕ=n c2 )  ⟩
+            Equal (varn env + vari env) (suc c10)
+          ≡⟨ cong ( λ z → (Equal z (suc c10) )) c1 ⟩
+            Equal (suc c10) (suc c10)
+          ≡⟨ ≡→Equal refl ⟩
+            true
+          ∎
+     -- While Loopを抜けた際のConditionの生合成の証明
+     -- 抜けた際と言っているけどそれならvarnは0になり
+     lemma4 :  {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv
+     lemma4 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
+          begin
+            whileInv (record { varn = varn env - 1 ; vari = vari env })
+          ≡⟨⟩
+            Equal ((varn env - 1) + vari env) c10
+          ≡⟨ lemma41 env (Equal→≡ (∧-pi1  cond)) (∧-pi2  cond) ⟩
+            true
+          ∎
+        )
+     lemma51 : (z : Env ) → neg (λ z → lt zero (varn z)) z ≡ true → varn z ≡ zero
+     lemma51 z cond with varn z
+     lemma51 z refl | zero = refl
+     lemma51 z () | suc x
+     -- While Loopを抜けた後のループ不変条件からConditionへの変換とtermCondへの移行の整合性を保証している
+     lemma5 : {c10 : ℕ} →  Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond
+     lemma5 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
+         begin
+            termCond env
+          ≡⟨⟩
+             Equal (vari env) c10 
+          ≡⟨⟩
+             Equal (zero + vari env) c10 
+          ≡⟨ cong ( λ z →  Equal (z + vari env) c10 )  (sym ( lemma51 env ( ∧-pi2  cond ) )) ⟩
+             Equal (varn env + vari env) c10 
+          ≡⟨ ∧-pi1  cond  ⟩
+             true
+          ∎
+        )
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/whilespecification.agda	Tue Oct 13 18:01:42 2020 +0900
@@ -0,0 +1,164 @@
+module whilespecification where
+
+open import Function
+open import Data.Nat
+open import Data.Bool
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Relation.Binary.PropositionalEquality
+
+open import Data.Nat.Properties
+
+open import utilities hiding ( _/\_ )
+open import whiletest
+
+open import Hoare PrimComm Cond Axiom Tautology _and_ neg
+
+open Env
+
+initCond : Cond
+initCond env = true
+
+termCond : {c10 : ℕ} → Cond
+termCond {c10} env = Equal (vari env) c10
+
+stmt1Cond : {c10 : ℕ} → Cond
+stmt1Cond {c10} env = Equal (varn env) c10
+
+init-case : {c10 :  ℕ} → (env : Env) → (( λ e → true  ⇒ stmt1Cond {c10} e ) (record { varn = c10 ; vari = vari env }) ) ≡ true 
+init-case {c10} _ = impl⇒ ( λ cond → ≡→Equal refl )
+
+stmt2Cond : {c10 : ℕ} → Cond
+stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)
+
+whileInv : {c10 : ℕ} → Cond
+whileInv {c10} env = Equal ((varn env) + (vari env)) c10
+
+whileInv' : {c10 : ℕ} → Cond
+whileInv'{c10}  env = Equal ((varn env) + (vari env)) (suc c10) ∧ lt zero (varn env)
+
+lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
+lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
+  begin
+    (Equal (varn env) c10 ) ∧ true
+  ≡⟨ ∧true ⟩
+    Equal (varn env) c10 
+  ≡⟨ cond ⟩
+    true
+  ∎ )
+
+
+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
+  where
+     lemma21 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env ≡ c10
+     lemma21 eq = Equal→≡ (∧-pi1 eq)
+     lemma22 : {env : Env } → {c10 : ℕ} → stmt2Cond {c10} env ≡ true → vari env ≡ 0
+     lemma22 eq = Equal→≡ (∧-pi2 eq)
+     lemma23 :  {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env + vari env ≡ c10
+     lemma23 {env} {c10} eq = let open ≡-Reasoning  in
+          begin
+            varn env + vari env
+          ≡⟨ cong ( \ x -> x + vari env ) (lemma21 eq  ) ⟩
+            c10 + vari env
+          ≡⟨ cong ( \ x -> c10 + x) (lemma22 {env} {c10} eq ) ⟩
+            c10 + 0
+          ≡⟨ +-sym {c10} {0} ⟩
+            0 + c10 
+          ≡⟨⟩
+            c10 
+          ∎
+     lemma2 :  {c10 : ℕ} → Tautology stmt2Cond whileInv
+     lemma2 {c10} env = bool-case (stmt2Cond env) (
+        λ eq → let open ≡-Reasoning  in
+          begin
+            (stmt2Cond env)  ⇒  (whileInv env)
+          ≡⟨⟩
+            (stmt2Cond env)  ⇒ ( Equal (varn env + vari env) c10 )
+          ≡⟨  cong ( \ x -> (stmt2Cond  {c10} env)  ⇒ ( Equal x c10 ) ) ( lemma23 {env} eq ) ⟩
+            (stmt2Cond env)  ⇒ (Equal c10 c10)
+          ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ x ) (≡→Equal refl )  ⟩
+            (stmt2Cond {c10} env)  ⇒  true
+          ≡⟨ ⇒t ⟩
+            true
+          ∎
+        ) (
+         λ ne → let open ≡-Reasoning  in
+          begin
+            (stmt2Cond env)  ⇒  (whileInv env)
+          ≡⟨ cong ( \ x -> x  ⇒  (whileInv env) ) ne ⟩
+             false  ⇒  (whileInv {c10} env)
+          ≡⟨ f⇒ {whileInv {c10} env} ⟩
+            true
+          ∎
+        ) 
+     lemma3 :   Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv'
+     lemma3 env = impl⇒ ( λ cond →  let open ≡-Reasoning  in
+          begin
+            whileInv' (record { varn = varn env ; vari = vari env + 1 }) 
+          ≡⟨⟩
+             Equal (varn env + (vari env + 1)) (suc c10) ∧ (lt 0 (varn env) )
+          ≡⟨ cong ( λ z → Equal (varn env + (vari env + 1)) (suc c10) ∧ z ) (∧-pi2 cond )  ⟩
+             Equal (varn env + (vari env + 1)) (suc c10) ∧ true
+          ≡⟨ ∧true ⟩
+            Equal (varn env + (vari env + 1)) (suc c10)
+          ≡⟨ cong ( \ x -> Equal x (suc c10) ) (sym (+-assoc (varn env) (vari env) 1)) ⟩
+            Equal ((varn env + vari env) + 1) (suc c10)
+          ≡⟨ cong ( \ x -> Equal x (suc c10) ) +1≡suc ⟩
+            Equal (suc (varn env + vari env)) (suc c10)
+          ≡⟨ sym Equal+1 ⟩
+            Equal ((varn env + vari env) ) c10
+          ≡⟨ ∧-pi1  cond ⟩
+            true
+          ∎ )
+     lemma41 : (env : Env ) → {c10 : ℕ} → (varn env + vari env) ≡ (suc c10) → lt 0 (varn env) ≡ true  → Equal ((varn env - 1) + vari env) c10 ≡ true
+     lemma41 env {c10} c1 c2 =  let open ≡-Reasoning  in
+          begin
+            Equal ((varn env - 1) + vari env) c10
+          ≡⟨ cong ( λ z → Equal ((z - 1 ) +  vari env ) c10 ) (sym (suc-predℕ=n c2) )  ⟩
+            Equal ((suc (predℕ {varn env} c2 ) - 1) + vari env) c10
+          ≡⟨⟩
+            Equal ((predℕ {varn env} c2 ) + vari env) c10
+          ≡⟨  Equal+1 ⟩
+            Equal ((suc (predℕ {varn env} c2 )) + vari env) (suc c10)
+          ≡⟨ cong ( λ z → Equal (z  +  vari env ) (suc c10) ) (suc-predℕ=n c2 )  ⟩
+            Equal (varn env + vari env) (suc c10)
+          ≡⟨ cong ( λ z → (Equal z (suc c10) )) c1 ⟩
+            Equal (suc c10) (suc c10)
+          ≡⟨ ≡→Equal refl ⟩
+            true
+          ∎
+     lemma4 :  {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv
+     lemma4 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
+          begin
+            whileInv (record { varn = varn env - 1 ; vari = vari env })
+          ≡⟨⟩
+            Equal ((varn env - 1) + vari env) c10
+          ≡⟨ lemma41 env (Equal→≡ (∧-pi1  cond)) (∧-pi2  cond) ⟩
+            true
+          ∎
+        )
+     lemma51 : (z : Env ) → neg (λ z → lt zero (varn z)) z ≡ true → varn z ≡ zero
+     lemma51 z cond with varn z
+     lemma51 z refl | zero = refl
+     lemma51 z () | suc x
+     lemma5 : {c10 : ℕ} →  Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond
+     lemma5 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
+         begin
+            termCond env
+          ≡⟨⟩
+             Equal (vari env) c10 
+          ≡⟨⟩
+             Equal (zero + vari env) c10 
+          ≡⟨ cong ( λ z →  Equal (z + vari env) c10 )  (sym ( lemma51 env ( ∧-pi2  cond ) )) ⟩
+             Equal (varn env + vari env) c10 
+          ≡⟨ ∧-pi1  cond  ⟩
+             true
+          ∎
+        )
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/whilespecimple.agda	Tue Oct 13 18:01:42 2020 +0900
@@ -0,0 +1,108 @@
+module whilespecimple where
+
+open import Relation.Binary.PropositionalEquality
+open import Data.Bool
+open import Relation.Binary
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Data.Empty
+open import Agda.Builtin.Sigma
+open import Data.Product
+open import Data.Nat
+
+
+open import utilities hiding ( _/\_ )
+open import whiletest
+open import Hoare PrimComm Cond Axiom Tautology _and_ neg
+open import whilespec
+
+State : Set
+State = Env
+
+open import RelOp 
+module RelOpState = RelOp State
+
+
+SemCond : Cond -> State -> Set
+SemCond c p = c p ≡ true
+
+PrimSemComm : ∀ {l} -> PrimComm -> Rel State l
+PrimSemComm prim s1 s2 =  Id State (prim s1) s2
+
+tautValid : (b1 b2 : Cond) -> Tautology b1 b2 -> (s : State) -> SemCond b1 s -> SemCond b2 s
+tautValid b1 b2 taut s cond with b1 s | b2 s | taut s
+tautValid b1 b2 taut s () | false | false | refl
+tautValid b1 b2 taut s _ | false | true | refl = refl
+tautValid b1 b2 taut s _ | true | false | ()
+tautValid b1 b2 taut s _ | true | true | refl = refl
+
+
+axiomValid : ∀ {l} -> (bPre : Cond) -> (pcm : PrimComm) -> (bPost : Cond) ->
+                  (ax : Axiom bPre pcm bPost) -> (s1 s2 : State) ->
+                  SemCond bPre s1 -> PrimSemComm {l} pcm s1 s2 -> SemCond bPost s2 
+axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref with bPre s1 | bPost (pcm s1) | ax s1
+axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) () ref | false | false | refl
+axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | false | true | refl = refl
+axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | false | ()
+axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | true | refl = refl
+
+
+respNeg : (b : Cond) -> (s : State) ->
+               Iff (SemCond (neg b) s) (¬ SemCond b s)
+respNeg b s = ( left , right ) where
+    left : not (b s) ≡ true → (b s) ≡ true → ⊥
+    left ne with b s
+    left refl | false = λ ()
+    left () | true
+    right : ((b s) ≡ true → ⊥) → not (b s) ≡ true
+    right ne with b s
+    right ne | false = refl
+    right ne | true = ⊥-elim ( ne refl )
+
+_/\_ : Cond -> Cond -> Cond
+b1 /\ b2 = b1 and b2
+
+_\/_ : Cond -> Cond -> Cond
+b1 \/ b2 = neg (neg b1 /\ neg b2)
+
+respAnd : (b1 b2 : Cond) -> (s : State) ->
+               Iff (SemCond (b1 /\ b2) s)
+                   ((SemCond b1 s) × (SemCond b2 s))
+respAnd b1 b2 s = ( left , right ) where
+     left : b1 s ∧ b2 s ≡ true → (b1 s ≡ true)  ×  (b2 s ≡ true)
+     left and with b1 s | b2 s
+     left () | false | false 
+     left () | false | true 
+     left () | true | false 
+     left refl | true | true = ( refl , refl )
+     right :  (b1 s ≡ true)  ×  (b2 s ≡ true) →  b1 s ∧ b2 s ≡ true
+     right ( x1 , x2 ) with b1 s | b2 s
+     right (() , ()) | false | false 
+     right (() , _) | false | true 
+     right (_ , ()) | true | false 
+     right (refl , refl) | true | true = refl
+
+
+open import HoareSoundness
+    Cond 
+    PrimComm 
+    neg 
+    _and_ 
+    Tautology 
+    State 
+    SemCond 
+    tautValid 
+    respNeg 
+    respAnd 
+    PrimSemComm 
+    Axiom 
+    axiomValid
+
+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/whiletest.agda	Tue Oct 13 18:01:42 2020 +0900
@@ -0,0 +1,72 @@
+module whiletest where
+
+open import Data.Nat
+open import Data.Bool
+open import Function
+open import Relation.Binary.PropositionalEquality
+
+open import utilities hiding ( _/\_ )
+
+record Env : Set where
+  field
+    varn : ℕ
+    vari : ℕ
+open Env
+
+-- Envのvariやvarnの代入を行う関数
+PrimComm : Set
+PrimComm = Env → Env
+
+Cond : Set
+Cond = (Env → Bool) 
+
+-- ここから先のコメントがなかった
+
+Axiom : Cond -> PrimComm -> Cond -> Set
+Axiom pre comm post = ∀ (env : Env) →  (pre env) ⇒ ( post (comm env)) ≡ true
+
+Tautology : Cond -> Cond -> Set
+Tautology pre post = ∀ (env : Env) →  (pre env)  ⇒ (post env) ≡ true
+
+_and_ :  Cond -> Cond -> Cond
+x and y =  λ env → x env ∧ y env 
+
+neg :  Cond -> Cond
+neg x  =  λ env → not ( x env )
+
+open import Hoare PrimComm Cond Axiom Tautology _and_ neg
+
+-- 実装開始
+-- ここでは実行停止の定義などはしていない
+-- numにループ回数をいれる感じか
+program : ℕ → Comm
+program loop_num  =
+  Seq ( PComm (λ env → record env {varn = loop_num}))
+    $ Seq ( PComm (λ env → record env {vari = 0})) -- ここまで入力
+    $ While (λ env → lt zero (varn env ) ) -- 大小比較をしている
+      (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
+        $ PComm (λ env → record env {varn = ((varn env) - 1)} ))
+        
+-- 実行するための定義
+-- この定義では停止しないのでTERMINATINGが必要
+-- コマンドがdata型なので全部の場合の記述をする
+{-# 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
+
+-- 実行
+test : Env
+test = interpret ( record { vari = 0 ; varn = 10 } ) (program 10)
+
+-- 実行はできた
+-- 事前、事後条件を検証していく。これができるとHoare Logicを名乗っても良い
+