# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1613228963 -32400
# Node ID 250c1d4e683b07162355db34361fe4400ef0116c
# Parent  69dc3096fa721162d1d677195e8e102f1ed6baeb
...

diff -r 69dc3096fa72 -r 250c1d4e683b hoare.agda
--- a/hoare.agda	Sat Feb 13 16:29:52 2021 +0900
+++ b/hoare.agda	Sun Feb 14 00:09:23 2021 +0900
@@ -2,10 +2,12 @@
 module hoare where
 
 open import Data.Nat
-open import Data.Bool hiding (_≤?_ ; _≤_)
-open import Data.Product renaming ( _×_ to _/\_ )
+open import Data.Nat.Properties
+-- open import Data.Bool hiding (_≤?_ ; _≤_)
+-- open import Data.Product renaming ( _×_ to _/\_ )
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary using (¬_; Dec; yes; no)
+open import logic
 
 record Env : Set (Suc Zero) where
    field
@@ -28,11 +30,12 @@
 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
+open import nat 
+-- _-_ : ℕ → ℕ → ℕ
+-- 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
@@ -58,11 +61,19 @@
     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 = {!!}
+          proof3 n+i=c 0<n = begin
+              varn env1 + vari env1 ≡⟨⟩
+              (varn env - 1) + (vari env + 1) ≡⟨ cong (λ k → (varn env - 1 ) + k ) (+-comm _ 1 ) ⟩
+              (varn env - 1) + (1 + vari env ) ≡⟨ sym (+-assoc _ 1 _) ⟩ -- 1 ≤ varn env
+              ((varn env - 1) + 1 )+ vari env  ≡⟨ cong (λ k → k + vari env) (minus+n {_} {1} (s≤s p)) ⟩
+              varn env + vari env ≡⟨ proof ⟩
+              c10
+            ∎ where open ≡-Reasoning  
 
+open _∧_
 
 -- Condition to Invariant
-conversion1 : {l : Level} {t : Set l } → (env : Env ) → {c10 :  ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
+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
@@ -70,21 +81,21 @@
       proof4 = let open ≡-Reasoning  in
           begin
             varn env + vari env
-          ≡⟨ cong ( λ n → n + vari env ) {!!}  ⟩
+          ≡⟨ cong ( λ n → n + vari env ) (proj2 p1) ⟩
             c10 + vari env
-          ≡⟨ cong ( λ n → c10 + n ) {!!}  ⟩
+          ≡⟨ cong ( λ n → c10 + n ) (proj1 p1) ⟩
             c10 + 0
-          ≡⟨ {!!} ⟩
+          ≡⟨ +-comm _ 0 ⟩
             c10
           ∎
 
-whileTest' : {l : Level} {t : Set l}  →  {c10 :  ℕ } → (Code : (env : Env )  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
+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 )
+    proof2 : ((vari env) ≡ 0) ∧ ((varn env) ≡ c10) -- PostCondition
+    proof2 = record { proj1 = refl ; proj2 =  refl }
 
 -- all proofs are connected
 proofGears : {c10 :  ℕ } → Set
@@ -95,26 +106,25 @@
 
 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
 
+-- step : {l m n : Level} {t : Set l} {A : Set l } {B : Set m} {C : Set n} (F : A → (B → t) → t ) →  
+-- step = ?
+
 data WhileTestState (c10 : ℕ) (env : Env)  : Set where
-  S1 : (vari env ≡ 0) /\ (varn env ≡ c10 ) → WhileTestState c10 env
+  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 = {!!}
+proofGears1 : {c10 : ℕ } →
+    whileTest' {_} {_} {c10} (λ n p1 →
+    conversion1 n p1 (λ n1 p2 →
+    whileLoop' n1 p2 (λ n2 →  vari n2 ≡ c10 )))
+proofGears1 {c10} = {!!} where
+     lemma2 : whileTest' {Level.suc Level.zero} {_} {c10} (λ n p1 → (vari n ≡ 0) ∧ (varn n ≡ c10 ))
+     lemma2 = record { proj1 = refl ; proj2 =  refl }
+     lemma4 : {n : Env} → (p2 : ((varn n) + (vari n) ≡ c10)) → whileLoop' n p2 (λ n2 →  vari n2 ≡ c10)
+     lemma4 {record { varn = zero ; vari = i }} p2 = p2
+     lemma4 {record { varn = suc n ; vari = i }} p2 with lemma4 {record { varn = n - 0; vari = i + 1 }} {!!} 
+     ... | t = {!!}
diff -r 69dc3096fa72 -r 250c1d4e683b logic.agda
--- a/logic.agda	Sat Feb 13 16:29:52 2021 +0900
+++ b/logic.agda	Sun Feb 14 00:09:23 2021 +0900
@@ -2,7 +2,7 @@
 
 open import Level
 open import Relation.Nullary
-open import Relation.Binary
+open import Relation.Binary hiding (_⇔_)
 open import Data.Empty
 
 
diff -r 69dc3096fa72 -r 250c1d4e683b nat.agda
--- a/nat.agda	Sat Feb 13 16:29:52 2021 +0900
+++ b/nat.agda	Sun Feb 14 00:09:23 2021 +0900
@@ -8,7 +8,7 @@
 open import  Relation.Binary.PropositionalEquality
 open import  Relation.Binary.Core
 open import  logic
--- open import Relation.Binary.Definitions
+open import Relation.Binary.Definitions
 
 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
 nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x