module day where

open import Relation.Binary.PropositionalEquality

data day : Set where
  monday : day
  tuesday : day
  wednesday : day
  thursday : day
  friday : day
  saturday : day
  sunday : day

-- ↑はただのデータ

nextWeekday : day → day
nextWeekday monday = tuesday
nextWeekday tuesday = wednesday
nextWeekday wednesday = thursday
nextWeekday thursday = friday
nextWeekday friday = monday
nextWeekday saturday = monday
nextWeekday sunday = monday

hoge : day → day
hoge x = nextWeekday x

data bool : Set where
  true : bool
  false : bool

negb : bool → bool
negb true = false
negb false = true

andb : bool → bool → bool
-- andb true true = true
-- andb true false = false
-- andb false true = false
-- andb false false = false
andb true b = b
andb false _ = false

orb : (x y : bool) → bool
orb true _ = true
orb false y = y

-- data _≡_  {a} { A : Set a} ( x : A ) : A → Set a where
--  refl : x ≡ x

testOrb1 : (orb true false) ≡ true
testOrb1 = refl

data nat : Set where
  O :  nat
  Succ : nat → nat

pred : nat → nat
pred O = O
pred (Succ x) = x

minustwo : nat → nat
minustwo x = pred (pred x)

evenb : nat → bool
evenb O = true
evenb (Succ O) = false
evenb (Succ (Succ x)) = evenb x

open import Data.Nat.Base

factorial : ℕ → ℕ
factorial zero = 1
factorial (suc x) = x * (factorial (x))

beqNat : ℕ  → ℕ  → bool
beqNat zero zero = true
beqNat zero (suc y) = false 
beqNat (suc x) zero = false 
beqNat (suc x) (suc y) = beqNat x y

-- beqNat x y with x | y 
-- beqNat x y | zero | zero = true
-- beqNat x y | zero | suc a = false
-- beqNat x y | suc z | zero = false
-- beqNat x y | suc z | suc a = beqNat z a 

open import Data.Nat.Properties 
open import Data.Empty

n+0 : ( n : ℕ ) →  ( n + 0 ) ≡ n
n+0 zero = refl
n+0 (suc x) rewrite  (  +-comm (suc x) 0 ) = refl

andbTrueElim2 : ( b c : bool ) →  (andb b c ) ≡ true → c ≡ true
-- andbTrueElim2 true c d with d
-- andbTrueElim2 true .true d | refl = refl
andbTrueElim2 _ true d = refl
andbTrueElim2 false false ()
andbTrueElim2 true false ()

mult0r : ( n : ℕ ) → ( n * zero) ≡ zero
mult0r zero = refl
-- mult0r (suc n) = mult0r n
mult0r (suc n) rewrite ( *-comm (suc n) 0 ) = refl

double : (n : ℕ ) → ℕ
double zero = zero
double (suc x) = suc ( suc ( double x))

sucEqPlus1 : ( n : ℕ ) → (n + 1) ≡(suc n)
sucEqPlus1 x rewrite (+-comm x 1 ) = refl


plusNSm : (n m : ℕ ) →  (suc ( n + m)) ≡ (n + suc (m))
plusNSm zero zero =  refl
plusNSm zero (suc y) = refl
plusNSm (suc x) zero rewrite sucEqPlus1 x  | n+0 x = refl
plusNSm (suc x) (suc y) = cong (suc) (plusNSm x (suc y))

doublePlus : (n : ℕ ) → (double n) ≡ (n + n)
doublePlus zero = refl
doublePlus (suc n) rewrite (doublePlus n) | plusNSm n n = refl

plusSwap : ( n m p : ℕ ) → ( n + (m + p)) ≡ ( m + (n + p))
plusSwap zero y z = refl
plusSwap (suc x) y z rewrite sym (plusNSm (y) (x + z)) | plusSwap x y z = refl