{-!$\#$! OPTIONS --allow-unsolved-metas !$\#$!-}
module utilities where

open import Function
open import Data.Nat
open import Data.Product
open import Data.Bool hiding ( _≟_  ; _!$\leq$!?_)
open import Level renaming ( suc to succ ; zero to Zero )
open import Relation.Nullary using (!$\neg$!_; Dec; yes; no)
open import Relation.Binary.PropositionalEquality

Pred : Set !$\rightarrow$! Set!$\_{1}$!
Pred X = X !$\rightarrow$! Set

Imply : Set !$\rightarrow$! Set !$\rightarrow$! Set
Imply X Y = X !$\rightarrow$! Y

Iff : Set !$\rightarrow$! Set !$\rightarrow$! Set
Iff X Y = Imply X Y !$\times$! Imply Y X

record _!$\wedge$!_ {n : Level } (a : Set n) (b : Set n): Set n where
  field
    pi1 : a
    pi2 : b

open  _!$\wedge$!_

_-_ : !$\mathbb{N}$! !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! !$\mathbb{N}$! 
x - zero  = x
zero - _  = zero
(suc x) - (suc y)  = x - y

+zero : { y : !$\mathbb{N}$! } !$\rightarrow$! y + zero  !$\equiv$! y
+zero {zero} = refl
+zero {suc y} = cong ( !$\lambda$! x !$\rightarrow$! suc x ) ( +zero {y} )


+-sym : { x y : !$\mathbb{N}$! } !$\rightarrow$! x + y !$\equiv$! y + x
+-sym {zero} {zero} = refl
+-sym {zero} {suc y} = let open !$\equiv$!-Reasoning  in
          begin
            zero + suc y 
          !$\equiv$!!$\langle$!!$\rangle$!
            suc y
          !$\equiv$!!$\langle$! sym +zero !$\rangle$!
            suc y + zero
          !$\blacksquare$!
+-sym {suc x} {zero} =  let open !$\equiv$!-Reasoning  in
          begin
            suc x + zero
          !$\equiv$!!$\langle$! +zero  !$\rangle$!
            suc x
          !$\equiv$!!$\langle$!!$\rangle$!
            zero + suc x
          !$\blacksquare$!
+-sym {suc x} {suc y} = cong ( !$\lambda$! z !$\rightarrow$! suc z ) (  let open !$\equiv$!-Reasoning  in
          begin
            x + suc y
          !$\equiv$!!$\langle$! +-sym {x} {suc y} !$\rangle$!
            suc (y + x)
          !$\equiv$!!$\langle$! cong ( !$\lambda$! z !$\rightarrow$! suc z )  (+-sym {y} {x}) !$\rangle$!
            suc (x + y)
          !$\equiv$!!$\langle$! sym ( +-sym {y} {suc x}) !$\rangle$!
            y + suc x
          !$\blacksquare$! )


minus-plus : { x y : !$\mathbb{N}$! } !$\rightarrow$! (suc x - 1) + (y + 1) !$\equiv$! suc x + y
minus-plus {zero} {y} = +-sym {y} {1}
minus-plus {suc x} {y} =  cong ( !$\lambda$! z !$\rightarrow$! suc z ) (minus-plus {x} {y})

+1!$\equiv$!suc : { x : !$\mathbb{N}$! } !$\rightarrow$! x + 1 !$\equiv$! suc x
+1!$\equiv$!suc {zero} = refl
+1!$\equiv$!suc {suc x} = cong ( !$\lambda$! z !$\rightarrow$! suc z ) ( +1!$\equiv$!suc {x} )

lt : !$\mathbb{N}$! !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! Bool
lt x y with (suc x ) !$\leq$!? y
lt x y | yes p = true
lt x y | no !$\neg$!p = false

pred!$\mathbb{N}$! : {n :  !$\mathbb{N}$! } !$\rightarrow$! lt 0 n !$\equiv$! true  !$\rightarrow$!  !$\mathbb{N}$!
pred!$\mathbb{N}$! {zero} ()
pred!$\mathbb{N}$! {suc n} refl = n

pred!$\mathbb{N}$!+1=n : {n :  !$\mathbb{N}$! } !$\rightarrow$! (less : lt 0 n !$\equiv$! true ) !$\rightarrow$! (pred!$\mathbb{N}$! less) + 1 !$\equiv$! n
pred!$\mathbb{N}$!+1=n {zero} ()
pred!$\mathbb{N}$!+1=n {suc n} refl = +1!$\equiv$!suc

suc-pred!$\mathbb{N}$!=n : {n :  !$\mathbb{N}$! } !$\rightarrow$! (less : lt 0 n !$\equiv$! true ) !$\rightarrow$! suc (pred!$\mathbb{N}$! less) !$\equiv$! n
suc-pred!$\mathbb{N}$!=n {zero} ()
suc-pred!$\mathbb{N}$!=n {suc n} refl = refl

Equal : !$\mathbb{N}$! !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! Bool
Equal x y with x ≟ y
Equal x y | yes p = true
Equal x y | no !$\neg$!p = false

_!$\Rightarrow$!_ : Bool !$\rightarrow$! Bool !$\rightarrow$! Bool
false  !$\Rightarrow$!  _ = true
true  !$\Rightarrow$!  true = true
true  !$\Rightarrow$!  false = false

!$\Rightarrow$!t : {x : Bool} !$\rightarrow$! x  !$\Rightarrow$! true  !$\equiv$! true
!$\Rightarrow$!t {x} with x
!$\Rightarrow$!t {x} | false = refl
!$\Rightarrow$!t {x} | true = refl

f!$\Rightarrow$! : {x : Bool} !$\rightarrow$! false  !$\Rightarrow$! x  !$\equiv$! true
f!$\Rightarrow$! {x} with x
f!$\Rightarrow$! {x} | false = refl
f!$\Rightarrow$! {x} | true = refl

!$\wedge$!-pi1 : { x y : Bool } !$\rightarrow$! x  !$\wedge$!  y  !$\equiv$! true  !$\rightarrow$! x  !$\equiv$! true
!$\wedge$!-pi1 {x} {y} eq with x | y | eq
!$\wedge$!-pi1 {x} {y} eq | false | b | ()
!$\wedge$!-pi1 {x} {y} eq | true | false | ()
!$\wedge$!-pi1 {x} {y} eq | true | true | refl = refl

!$\wedge$!-pi2 : { x y : Bool } !$\rightarrow$!  x  !$\wedge$!  y  !$\equiv$! true  !$\rightarrow$! y  !$\equiv$! true
!$\wedge$!-pi2 {x} {y} eq with x | y | eq
!$\wedge$!-pi2 {x} {y} eq | false | b | ()
!$\wedge$!-pi2 {x} {y} eq | true | false | ()
!$\wedge$!-pi2 {x} {y} eq | true | true | refl = refl

!$\wedge$!true : { x : Bool } !$\rightarrow$!  x  !$\wedge$!  true  !$\equiv$! x
!$\wedge$!true {x} with x
!$\wedge$!true {x} | false = refl
!$\wedge$!true {x} | true = refl

true!$\wedge$! : { x : Bool } !$\rightarrow$!  true  !$\wedge$!  x  !$\equiv$! x
true!$\wedge$! {x} with x
true!$\wedge$! {x} | false = refl
true!$\wedge$! {x} | true = refl
bool-case : ( x : Bool ) { p : Set } !$\rightarrow$! ( x !$\equiv$! true  !$\rightarrow$! p ) !$\rightarrow$! ( x !$\equiv$! false  !$\rightarrow$! p ) !$\rightarrow$! 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!$\Rightarrow$! :  {x y : Bool} !$\rightarrow$! (x  !$\equiv$! true !$\rightarrow$! y  !$\equiv$! true ) !$\rightarrow$! x  !$\Rightarrow$! y  !$\equiv$! true
impl!$\Rightarrow$! {x} {y} p = bool-case x (!$\lambda$! x=t !$\rightarrow$!   let open !$\equiv$!-Reasoning  in
          begin
            x  !$\Rightarrow$! y
          !$\equiv$!!$\langle$!  cong ( !$\lambda$! z !$\rightarrow$! x  !$\Rightarrow$! z ) (p x=t ) !$\rangle$!
            x  !$\Rightarrow$!  true
          !$\equiv$!!$\langle$! !$\Rightarrow$!t !$\rangle$!
            true
          !$\blacksquare$!
    ) ( !$\lambda$! x=f !$\rightarrow$!  let open !$\equiv$!-Reasoning  in
          begin
            x  !$\Rightarrow$!  y
          !$\equiv$!!$\langle$!  cong ( !$\lambda$! z !$\rightarrow$! z  !$\Rightarrow$!  y ) x=f !$\rangle$!
            true
          !$\blacksquare$!
  )
 
Equal!$\rightarrow$!!$\equiv$! : { x y : !$\mathbb{N}$! } !$\rightarrow$!  Equal x y !$\equiv$! true !$\rightarrow$! x !$\equiv$! y
Equal!$\rightarrow$!!$\equiv$! {x} {y} eq with x ≟ y
Equal!$\rightarrow$!!$\equiv$! {x} {y} refl | yes refl = refl
Equal!$\rightarrow$!!$\equiv$! {x} {y} () | no !$\neg$!p 

Equal+1 : { x y : !$\mathbb{N}$! } !$\rightarrow$!  Equal x y !$\equiv$! Equal (suc x) (suc y)
Equal+1 {x} {y} with  x ≟ y
Equal+1 {x} {.x} | yes refl = {!!}
Equal+1 {x} {y} | no !$\neg$!p = {!!}

open import Data.Empty 

!$\equiv$!!$\rightarrow$!Equal : { x y : !$\mathbb{N}$! } !$\rightarrow$! x !$\equiv$! y !$\rightarrow$!  Equal x y !$\equiv$! true 
!$\equiv$!!$\rightarrow$!Equal {x} {.x} refl with x ≟ x
!$\equiv$!!$\rightarrow$!Equal {x} {.x} refl | yes refl = refl
!$\equiv$!!$\rightarrow$!Equal {x} {.x} refl | no !$\neg$!p = !$\bot$!-elim ( !$\neg$!p refl )