{-# 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 

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 )