{-@$\#$@ 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 

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 )