--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/WhileTest.agda	Thu Feb 11 17:23:49 2021 +0900
@@ -0,0 +1,71 @@
+open import Level renaming (suc to Suc ; zero to Zero )
+module WhileTest  where
+
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Core
+open import Data.Nat hiding (compare)
+open import Data.Maybe
+open import Data.List
+open import Function
+open import logic
+
+--open import Data.Bool hiding ( _≟_ ) -- ; _≤?_ ; _≤_ ; _<_)
+--open import Relation.Binary.PropositionalEquality
+open import Agda.Builtin.Unit
+
+record Env : Set (Suc Zero) where
+  field
+    varn : ℕ
+    vari : ℕ
+open Env
+
+data _implies_  (A B : Set ) : Set (Suc Zero) where
+    proof : ( A → B ) → A implies B
+
+data whileTestState  : Set where
+  s1 : whileTestState
+  s2 : whileTestState
+  sf : whileTestState
+
+whileTestStateP : whileTestState → Env → ℕ → Set
+whileTestStateP s1 env c10 = (vari env ≡ 0) ∧ (varn env ≡ c10)
+whileTestStateP s2 env c10 = (varn env + vari env ≡ c10 )
+whileTestStateP sf env c10 = (vari env ≡ c10)
+
+record WhileTest {m : Level }  {t : Set m }  : Set (Suc m) where
+  field
+    env : Env
+  whileInit :  {m : Level }  {t : Set m } → (c10 : ℕ) → (Env → t) → t
+  whileInit c10 next = next (record {varn = c10 ; vari = 0 } )
+  whileInit-imple : (c10 : ℕ) → whileInit c10 (λ env → ⊤ implies (whileTestStateP s1 env c10) )
+  whileInit-imple c = proof ( λ _ → record { proj1 = refl ; proj2 = refl } )
+  whileLoop : Env → (Code : Env → t) → t
+  whileLoop env next = whileLoop1 (varn env) env where
+      whileLoop1 : ℕ → Env → t
+      whileLoop1 zero env =  next env
+      whileLoop1 (suc t ) env = whileLoop1 t (record env {varn = t ; vari = (vari env) + 1})
+  whileTest : (c10 : ℕ) → (Env → t) → t
+  whileTest c10 next = whileInit c10 $ λ env → whileLoop env next
+
+open WhileTest
+
+createWhileTest : {m : Level} {t : Set m }  → WhileTest {m} {t}
+createWhileTest  = record { env = record { varn = 0; vari = 0 } }
+
+test2 : ℕ
+test2 = whileTest createWhileTest 10 $ λ e → vari e
+
+---
+
+{-
+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)
+
+whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Envc → t) → t
+whileTestP c10 next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } )
+
+whileTestPSem :  (c : ℕ) → whileTestP c ( λ env → ⊤ implies (whileTestStateP s1 env) )
+whileTestPSem c = proof ( λ _ → record { pi1 = refl ; pi2 = refl } )
+-}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/logic.agda	Thu Feb 11 17:23:49 2021 +0900
@@ -0,0 +1,152 @@
+module logic where
+
+open import Level
+open import Relation.Nullary
+open import Relation.Binary hiding(_⇔_)
+open import Data.Empty
+
+
+data Bool : Set where
+    true : Bool
+    false : Bool
+
+record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   field
+      proj1 : A
+      proj2 : B
+
+data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   case1 : A → A ∨ B
+   case2 : B → A ∨ B
+
+_⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
+_⇔_ A B =  ( A → B ) ∧ ( B → A )
+
+contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
+contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a )
+
+double-neg : {n  : Level } {A : Set n} → A → ¬ ¬ A
+double-neg A notnot = notnot A
+
+double-neg2 : {n  : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
+double-neg2 notnot A = notnot ( double-neg A )
+
+de-morgan : {n  : Level } {A B : Set n} →  A ∧ B  → ¬ ( (¬ A ) ∨ (¬ B ) )
+de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
+de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
+
+dont-or :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ A → B
+dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
+dont-or {A} {B} (case2 b) ¬A = b
+
+dont-orb :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ B → A
+dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
+dont-orb {A} {B} (case1 a) ¬B = a
+
+
+
+infixr  130 _∧_
+infixr  140 _∨_
+infixr  150 _⇔_
+
+_/\_ : Bool → Bool → Bool 
+true /\ true = true
+_ /\ _ = false
+
+_\/_ : Bool → Bool → Bool 
+false \/ false = false
+_ \/ _ = true
+
+not_ : Bool → Bool 
+not true = false
+not false = true 
+
+_<=>_ : Bool → Bool → Bool  
+true <=> true = true
+false <=> false = true
+_ <=> _ = false
+
+infixr  130 _\/_
+infixr  140 _/\_
+
+open import Relation.Binary.PropositionalEquality
+
+
+≡-Bool-func : {A B : Bool } → ( A ≡ true → B ≡ true ) → ( B ≡ true → A ≡ true ) → A ≡ B
+≡-Bool-func {true} {true} a→b b→a = refl
+≡-Bool-func {false} {true} a→b b→a with b→a refl
+... | ()
+≡-Bool-func {true} {false} a→b b→a with a→b refl
+... | ()
+≡-Bool-func {false} {false} a→b b→a = refl
+
+bool-≡-? : (a b : Bool) → Dec ( a ≡ b )
+bool-≡-? true true = yes refl
+bool-≡-? true false = no (λ ())
+bool-≡-? false true = no (λ ())
+bool-≡-? false false = yes refl
+
+¬-bool-t : {a : Bool} →  ¬ ( a ≡ true ) → a ≡ false
+¬-bool-t {true} ne = ⊥-elim ( ne refl )
+¬-bool-t {false} ne = refl
+
+¬-bool-f : {a : Bool} →  ¬ ( a ≡ false ) → a ≡ true
+¬-bool-f {true} ne = refl
+¬-bool-f {false} ne = ⊥-elim ( ne refl )
+
+¬-bool : {a : Bool} →  a ≡ false  → a ≡ true → ⊥
+¬-bool refl ()
+
+lemma-∧-0 : {a b : Bool} → a /\ b ≡ true → a ≡ false → ⊥
+lemma-∧-0 {true} {true} refl ()
+lemma-∧-0 {true} {false} ()
+lemma-∧-0 {false} {true} ()
+lemma-∧-0 {false} {false} ()
+
+lemma-∧-1 : {a b : Bool} → a /\ b ≡ true → b ≡ false → ⊥
+lemma-∧-1 {true} {true} refl ()
+lemma-∧-1 {true} {false} ()
+lemma-∧-1 {false} {true} ()
+lemma-∧-1 {false} {false} ()
+
+bool-and-tt : {a b : Bool} → a ≡ true → b ≡ true → ( a /\ b ) ≡ true
+bool-and-tt refl refl = refl
+
+bool-∧→tt-0 : {a b : Bool} → ( a /\ b ) ≡ true → a ≡ true 
+bool-∧→tt-0 {true} {true} refl = refl
+bool-∧→tt-0 {false} {_} ()
+
+bool-∧→tt-1 : {a b : Bool} → ( a /\ b ) ≡ true → b ≡ true 
+bool-∧→tt-1 {true} {true} refl = refl
+bool-∧→tt-1 {true} {false} ()
+bool-∧→tt-1 {false} {false} ()
+
+bool-or-1 : {a b : Bool} → a ≡ false → ( a \/ b ) ≡ b 
+bool-or-1 {false} {true} refl = refl
+bool-or-1 {false} {false} refl = refl
+bool-or-2 : {a b : Bool} → b ≡ false → (a \/ b ) ≡ a 
+bool-or-2 {true} {false} refl = refl
+bool-or-2 {false} {false} refl = refl
+
+bool-or-3 : {a : Bool} → ( a \/ true ) ≡ true 
+bool-or-3 {true} = refl
+bool-or-3 {false} = refl
+
+bool-or-31 : {a b : Bool} → b ≡ true  → ( a \/ b ) ≡ true 
+bool-or-31 {true} {true} refl = refl
+bool-or-31 {false} {true} refl = refl
+
+bool-or-4 : {a : Bool} → ( true \/ a ) ≡ true 
+bool-or-4 {true} = refl
+bool-or-4 {false} = refl
+
+bool-or-41 : {a b : Bool} → a ≡ true  → ( a \/ b ) ≡ true 
+bool-or-41 {true} {b} refl = refl
+
+bool-and-1 : {a b : Bool} →  a ≡ false → (a /\ b ) ≡ false
+bool-and-1 {false} {b} refl = refl
+bool-and-2 : {a b : Bool} →  b ≡ false → (a /\ b ) ≡ false
+bool-and-2 {true} {false} refl = refl
+bool-and-2 {false} {false} refl = refl
+
+