### view utilities.agda @ 50:2edb44c5bf52

author ryokka Wed, 18 Dec 2019 20:08:58 +0900 a39a82820742 52d957db0222
line wrap: on
line source
```
{-# 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 )
```