module Miercoles where
open import Data.Product
open import Data.Sum
open import Relation.Binary.PropositionalEquality hiding (sym ; trans ; cong ; subst )
sym : {A : Set} → {a b : A} → a ≡ b → b ≡ a
sym refl = refl
trans : {A : Set}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans p refl = p
cong : {A B : Set}(f : A → B){a b : A} → a ≡ b → f a ≡ f b
cong f refl = refl
subst : {A : Set}(P : A → Set) → {a b : A} → a ≡ b → P a → P b
subst P refl p = p
sym' : {A : Set} → {a b : A} → a ≡ b → b ≡ a
sym' {A} {a} p = subst (λ x → x ≡ a) p refl
trans' : {A : Set}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans' {A} {a} p q = subst (λ x → a ≡ x) q p
uip : {A : Set}{a b : A}(p q : a ≡ b) → p ≡ q
uip refl refl = refl
open import Data.Nat
0+ : (n : ℕ) → zero + n ≡ n
0+ n = refl
+0 : (n : ℕ) → n + zero ≡ n
+0 zero = refl
+0 (suc n) = cong suc (+0 n)
suc+ : (m n : ℕ) → (suc m) + n ≡ suc (m + n)
suc+ m n = refl
+suc : (m n : ℕ) → m + (suc n) ≡ suc (m + n)
+suc zero n = refl
+suc (suc m) n = cong suc (+suc m n)
+-comm : (m n : ℕ) → m + n ≡ n + m
+-comm m zero = +0 m
+-comm m (suc n) = trans (+suc m n) (cong suc (+-comm m n))
open ≡-Reasoning
open import Data.Product
+-comm' : (m n : ℕ) → m + n ≡ n + m
+-comm' m zero = +0 m
+-comm' m (suc n) = begin
m + suc n ≡⟨ +suc m n ⟩
suc (m + n) ≡⟨ cong suc (+-comm m n) ⟩
suc n + m ∎
+-assoc : (i j k : ℕ) → (i + j) + k ≡ i + (j + k)
+-assoc zero j k = refl
+-assoc (suc i) j k = cong suc (+-assoc i j k)
*-zero : (n : ℕ) → 0 ≡ n * 0
*-zero zero = refl
*-zero (suc n) = *-zero n
*-suc : (m n : ℕ) → m + (m * n) ≡ m * (suc n)
*-suc zero n = refl
*-suc (suc n) n' = cong suc (begin
n + (n' + n * n') ≡⟨ sym (+-assoc n n' (n * n')) ⟩
(n + n') + n * n' ≡⟨ cong (λ x → x + n * n') (+-comm n n') ⟩
(n' + n) + n * n' ≡⟨ +-assoc n' n (n * n') ⟩
n' + (n + n * n') ≡⟨ cong (λ x → n' + x) (*-suc n n') ⟩
n' + n * suc n' ∎)
*-comm : (m n : ℕ) → m * n ≡ n * m
*-comm zero n = *-zero n
*-comm (suc n) n' = begin
suc n * n' ≡⟨ refl ⟩ n' + (n * n')
≡⟨ cong (λ x → n' + x) (*-comm n n') ⟩ n' + (n' * n)
≡⟨ *-suc n' n ⟩ n' * suc n ∎
ℕelim : (P : ℕ → Set) →
P zero →
((n : ℕ) → P n → P (suc n)) →
(n : ℕ) → P n
ℕelim P z s zero = z
ℕelim P z s (suc n) = s n (ℕelim P z s n)
ℕrec : (A : Set) → A → (ℕ → A → A) → ℕ → A
ℕrec A = ℕelim (λ _ → A)
_+R_ : ℕ → ℕ → ℕ
_+R_ = ℕrec (ℕ → ℕ) (λ n → n) (λ m m+ n → suc (m+ n))
_*R_ : ℕ → ℕ → ℕ
_*R_ = ℕrec (ℕ → ℕ) (λ n → 0) (λ m m* n → n + (m* n))
+0' : (n : ℕ) → n + zero ≡ n
+0' = ℕelim (λ n' → n' + zero ≡ n') refl (λ n +0n → cong suc +0n)
open import Data.Bool
_≡b_ : ℕ → ℕ → Bool
zero ≡b zero = true
zero ≡b suc n = false
suc n ≡b zero = false
suc n ≡b suc m = n ≡b m
_≡bR_ : ℕ → ℕ → Bool
_≡bR_ = ℕrec (ℕ → Bool) (ℕrec Bool true (λ x x' → false))
(λ m eqm → ℕrec Bool false (λ x x' → eqm x))
open import Relation.Nullary
_≡?_ : (m n : ℕ) → Dec (m ≡ n)
zero ≡? zero = yes refl
zero ≡? suc n = no (λ ())
suc n ≡? zero = no (λ ())
suc n ≡? suc m with n ≡? m
suc n ≡? suc m | yes p = yes (cong suc p)
suc n ≡? suc m | no ¬p = no (λ sn≡sm → ¬p (cong pred sn≡sm))
data BT : Set where
leaf : BT
node : BT → BT → BT
injL : {l l' r r' : BT} → node l r ≡ node l' r' → l ≡ l'
injL refl = refl
injR : {l l' r r' : BT} → node l r ≡ node l' r' → r ≡ r'
injR refl = refl
_≡BT?_ : (m n : BT) → Dec (m ≡ n)
leaf ≡BT? leaf = yes refl
leaf ≡BT? node y y' = no (λ ())
node y y' ≡BT? leaf = no (λ ())
node l r ≡BT? node l' r' with l ≡BT? l'
node .l' r ≡BT? node l' r' | yes refl with r ≡BT? r'
node .l' .r' ≡BT? node _ r' | yes refl | yes refl = yes refl
... | no ¬p = no (λ x → ¬p (injR x))
node l r ≡BT? node l' r' | no ¬p = no (λ x → ¬p (injL x))
mod₂ : ℕ → ℕ
mod₂ zero = 0
mod₂ (suc zero) = 1
mod₂ (suc (suc n)) = mod₂ n
div₂ : ℕ → ℕ
div₂ zero = zero
div₂ (suc zero) = zero
div₂ (suc (suc n)) = suc (div₂ n)
mod₂Lem : (n : ℕ) → mod₂ n ≡ 0 ⊎ mod₂ n ≡ 1
mod₂Lem zero = inj₁ refl
mod₂Lem (suc zero) = inj₂ refl
mod₂Lem (suc (suc n)) = mod₂Lem n
s2* : ∀{n} → 2 * (suc n) ≡ 2 + 2 * n
s2* {n} = begin
2 * (suc n) ≡⟨ *-comm 2 (suc n) ⟩
(suc n) * 2 ≡⟨ refl ⟩
2 + n * 2 ≡⟨ cong (_+_ 2) (*-comm n 2) ⟩
2 + 2 * n
∎
div₂Lem : ∀ {n} → 2 * (div₂ n) + mod₂ n ≡ n
div₂Lem {zero} = refl
div₂Lem {suc zero} = refl
div₂Lem {suc (suc n)} = begin
2 * div₂ (suc (suc n)) + mod₂ (suc (suc n)) ≡⟨ refl ⟩
2 * suc (div₂ n) + mod₂ n ≡⟨ cong (λ x → x + mod₂ n) (s2* {div₂ n}) ⟩
2 + (2 * div₂ n + mod₂ n) ≡⟨ cong (_+_ 2) div₂Lem ⟩
suc (suc n)
∎
_≡₂_ : ℕ → ℕ → Set
m ≡₂ n = mod₂ m ≡ mod₂ n
_≡₂?_ : (m n : ℕ) → Dec (m ≡₂ n)
zero ≡₂? zero = yes refl
zero ≡₂? suc zero = no (λ ())
zero ≡₂? suc (suc n) = zero ≡₂? n
suc zero ≡₂? zero = no (λ ())
suc zero ≡₂? suc zero = yes refl
suc zero ≡₂? suc (suc n) = suc zero ≡₂? n
suc (suc n) ≡₂? n' = n ≡₂? n'