module Miercoles where

{- Basic constructions in Type Theory -}

{- Π - types -}

{- built in : (x : A) → B -}

{- Σ - types -}

open import Data.Product

{- disjoint union (⊎) -}

open import Data.Sum

{- Equality -}

open import Relation.Binary.PropositionalEquality hiding (sym ; trans ; cong ; subst )

{- Using pattern matching we can prove that ≡ is symmetric & transitive
   and hence an equivalence relation (because refl proves reflexivity)/ -}

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

{- Any function respects equality: -}

cong : {A B : Set}(f : A → B){a b : A} → a ≡ b → f a ≡ f b
cong f refl = refl

{- But not every function is injective. -}

{-
cong' : {A B : Set}{f : A → B}{a b : A} →  f a ≡ f b → a ≡ b
cong' p = ?
-}

{- Agda rejects the attempt to pattern match on f a ≡ f b. 
   While it is correct that refl is the only proof of this 
   type, we cannot conclude that a ≡ b. -}

{- We prove a very general property: substitutivity.
   The other properties we have mentioned are derivable 
   from this one. -}

subst : {A : Set}(P : A → Set) → {a b : A} → a ≡ b → P a → P b
subst P refl p = p 

{- Derive sym and trans using subst -}

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

{- uniqueness of identity proofs -}

uip : {A : Set}{a b : A}(p q : a ≡ b) → p ≡ q
uip refl refl = refl

{- Induction and recursion -}

open import Data.Nat 

{- It is obvious that zero is left neutral, indeed this 
   follows from the 1st line of the definition of +. Hence the prove
   is also trivial. "By definition" translates to "refl".
-}
0+ : (n : ℕ) → zero + n ≡ n
0+ n = refl

{- While it is true that zero is also right neutral, it is less
   obvious. It doesn't follow from the definition. Indeed, if we try

+0 : (n : ℕ) → n + zero ≡ n
+0 n    = refl

  Agda complaints by saying: n + 0 != n ? This means that n + 0 isn't
  definitionally equal to n. However they are propositionally equal
  (≡), which we can prove using pattern matching and recursion.

-}

+0 : (n : ℕ) → n + zero ≡ n
+0 zero    = refl
+0 (suc n) = cong suc (+0 n)

{- In the suc case we use 
   cong f :  m ≡ n → f m ≡ f n
   which we proved in the previous lecture (but called it resp).
   "cong" stands for congruence. This and other gadgets to reason
   about equality are defined in Relation.Binary.PropositionalEquality -}

{- Let's look at the interaction of + and suc -}

{- suc in the first argument commutes with + and this follows from the
   definition. -}
suc+ : (m n : ℕ) → (suc m) + n ≡ suc (m + n)
suc+ m n = refl

{- suc also commutes with + in the 2nd argument, but as before for +0 
   this requires a recursive proof. -}

+suc : (m n : ℕ) → m + (suc n) ≡ suc (m + n)
+suc zero n = refl
+suc (suc m) n = cong suc (+suc m n)

{- We have now all the pieces together to prove commutativity of addition. 
   Basically we do yet another recursion and in each case exploit the lemmas 
   we have proven previously.
-}

+-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))

{- nicer way to write proofs -}

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  ∎

{- some more proofs about arithmetic (ℕ,0,+,1,*) is a comm. semiring. -}

+-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 : ℕ) →  ≡ n * 
*-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  ∎


{- induction and recursion -}

{- All the constructions using ℕ can be reduced to a basic combinator: -}

ℕ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)

{- from ℕelim we can derive primitive recursion -}

ℕ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 → ) (λ m m* n → n + (m* n))

+0' : (n : ℕ) → n + zero ≡ n
+0' = ℕelim (λ n' → n' + zero ≡ n') refl (λ n +0n → cong suc +0n) 

{- Each datatype in Type Theory comes with its own eliminator.
   However, eliminators are inconvenient to program with.
-}

{- 
  Decidabililty 

  Equality on natural numbers is decidable, i.e. we can implement a
  boolean function which returns true if two numbers are equal, and
  false otherwise.
-}

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

{- implement ≡b just using ℕrec -}

_≡bR_ : ℕ → ℕ → Bool
_≡bR_ = ℕrec (ℕ → Bool) (ℕrec Bool true (λ x x' → false)) 
                        (λ m eqm → ℕrec Bool false (λ x x' → eqm x))

-- 3 ≡bR 3
-- 3 ≡bR 4

open import Relation.Nullary 

{- We prove that ≡ is "decidable", i.e. for every m,n : ℕ we can 
   decide m ≡ n.
-}

_≡?_ : (m n : ℕ) → Dec (m ≡ n)
zero ≡? zero = yes refl
zero ≡? suc n = no (λ ()) -- use the "impossible pattern" in a λ-abstraction.
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))

-- 3 ≡? 3
-- 3 ≡? 4

{- The similarity with ≡b should be obvious. The difference is that ≡?
   doesn't just say "yes" or "no" corresponding to "true" and "false"
   but it also provides the evidence why it is ok to give this answer.

   Also we should note that ≡? is at the same time a program and a proof. 
-}

{- another example decidability for the equality of binary trees -}

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))

{- but beware not all equalities are decidable, e.g. ℕ → ℕ hasn't got a decidable equality. -}

{- Example : mod₂ -}

{- Define functions,
   mod₂ : remainder of division by 2
   div₂ : division by two 
-}
mod₂ : ℕ → ℕ 
mod₂ zero = 
mod₂ (suc zero) = 
mod₂ (suc (suc n)) = mod₂ n

div₂ : ℕ → ℕ
div₂ zero = zero
div₂ (suc zero) = zero
div₂ (suc (suc n)) = suc (div₂ n)

{- And prove the following properties: -}

mod₂Lem : (n : ℕ) → mod₂ n ≡  ⊎ mod₂ n ≡ 
mod₂Lem zero = inj₁ refl
mod₂Lem (suc zero) = inj₂ refl
mod₂Lem (suc (suc n)) = mod₂Lem n

s2* : ∀{n} →  * (suc n) ≡  +  * n
s2* {n} =  begin 
   * (suc n) ≡⟨ *-comm  (suc n) ⟩
  (suc n) *  ≡⟨ refl ⟩
   + n *  ≡⟨ cong (_+_ ) (*-comm n ) ⟩
   +  * n
  ∎

div₂Lem : ∀ {n} →  * (div₂ n) + mod₂ n ≡ n
div₂Lem {zero} = refl
div₂Lem {suc zero} = refl
div₂Lem {suc (suc n)} = begin 
   * div₂ (suc (suc n)) + mod₂ (suc (suc n))    ≡⟨ refl ⟩
   * suc (div₂ n) + mod₂ n    ≡⟨ cong (λ x → x + mod₂ n) (s2* {div₂ n}) ⟩
   + ( * div₂ n + mod₂ n)    ≡⟨ cong (_+_ ) div₂Lem ⟩
  suc (suc n)
  ∎

{- Show that equality modulo 2 is decidable. -}

_≡₂_ : ℕ → ℕ → 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'