--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/utilities.agda	Sat Dec 15 17:24:35 2018 +0900
@@ -0,0 +1,154 @@
+module utilities where
+
+open import Function
+open import Data.Nat
+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
+
+
+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 = refl
+Equal+1 {x} {y} | no ¬p = refl
+