module PLFA.Equality where


-- recap some definitions

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero    + n  =  n
(suc m) + n  =  suc (m + n)

-- equality is definable in Agda
-- Martin Löf equality

module equality-specialized-to-ℕ where
  data _≡_ (x : ℕ) : ℕ → Set where
    refl : x ≡ x

module alternative where
  -- definition where both arguments are indexes
  -- in theory the same, but the definition below is more efficient
  -- because Agda can assume that parameters remain fixed
  
  data _≡′_ {A : Set} : A → A → Set where
    refl : ∀ {x} → x ≡′ x

  sym′ : ∀ {A : Set} → {x y : A} → x ≡′ y → y ≡′ x
  sym′ refl = refl

-- full equality is parameterized over the type A 

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

-- equality is an equivalence relation (sym, trans)

-- symmetry
sym : ∀ {A : Set} → {x y : A} → x ≡ y → y ≡ x
sym refl = refl

trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl
-- alternative proof:
--trans refl y≡z = y≡z

-- and a congruence (cong, cong₂, cong-app)
cong : ∀ {A B : Set} → {x y : A} →
  (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl

cong₂ : ∀ {A B C : Set} → {x y : A} → {z w : B} →
  (f : A → B → C) → x ≡ y → z ≡ w → f x z ≡ f y w
cong₂ f refl refl = refl

cong-app : ∀ {A B : Set} → {f g : A → B} → {x : A} → 
  f ≡ g → f x ≡ g x
cong-app refl = refl

-- and closed under substitution (subst)

subst : ∀ {A : Set} {x y : A} {P : A → Set} → x ≡ y → P x → P y
subst refl Px = Px

-- P x could be x ≡ x


{- Question:
' (x : ℕ) : ℕ ' -> Set seems a bit redundant, why is X of Type ℕ of Type ℕ? When it takes two arguments, why isn't it written like (x : A) -> A -> Set ?
-}

-- equational reasoning (analogous to module in standard library)

module ≡-Reasoning {A : Set} where

  infix  1 begin_
  infixr 2 _≡⟨⟩_ _≡⟨_⟩_
  infix  3 _∎

  begin_ : ∀ {x y : A}
    → x ≡ y
      -----
    → x ≡ y
  begin x≡y  =  x≡y

  _≡⟨⟩_ : ∀ (x : A) {y : A}
    → x ≡ y
      -----
    → x ≡ y
  x ≡⟨⟩ x≡y  =  x≡y

  _≡⟨_⟩_ : ∀ (x : A) {y z : A}
    → x ≡ y
    → y ≡ z
      -----
    → x ≡ z
  x ≡⟨ x≡y ⟩ y≡z  =  trans x≡y y≡z

  _∎ : ∀ (x : A)
      -----
    → x ≡ x
  x ∎  =  refl

open ≡-Reasoning


+-assoc : ∀ m n p → (m + (n + p)) ≡ ((m + n) + p)
+-assoc zero n p = refl
+-assoc (suc m) n p = 
  begin
    suc (m + (n + p))
  ≡⟨ cong suc (+-assoc m n p) ⟩
    suc ((m + n) + p)
  ∎

-- reprove transitivity using ≡-Reasoning
trans′ : ∀ {A : Set} → {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans′ {A} {x} {y} {z} x≡y y≡z =
  begin
    x
  ≡⟨ x≡y ⟩
    y
  ≡⟨ y≡z ⟩
    z
  ∎


-- recall this definition
data even : ℕ → Set
data odd  : ℕ → Set

data even where

  even-zero : even zero

  even-suc : ∀ {n : ℕ}
    → odd n
      ------------
    → even (suc n)

data odd where
  odd-suc : ∀ {n : ℕ}
    → even n
      -----------
    → odd (suc n)


-- prove using rewrite
-- to tell Agda about our self-defined equality type we need to declare this:
{-# BUILTIN EQUALITY _≡_ #-}

-- instead of proving a lemma, we can also postulate it.
-- we assume it as given without proof.
-- * potentially dangerous because it's unchecked
-- * convenient to defer a proof obligation and carry on with a more interesting current proof
-- * ok if it refers to a previously proved statement
-- * ok if it is a generally accepted axiom that doesn't violate consistency

postulate
  +-comm : ∀ m n → (m + n) ≡ (n + m)


even-comm : ∀ m n → even (m + n) → even (n + m)
even-comm m n ev-m+n rewrite +-comm m n = ev-m+n

-- expand rewrite 
even-comm′ : ∀ m n → even (m + n) → even (n + m)
even-comm′ m n ev-m+n with (m + n) | +-comm m n
...                     | .(n + m) | refl       = ev-m+n

-- another notion of equality
-- Leibniz equality


_≐_ : ∀ {A : Set} (x y : A) → Set₁
_≐_ {A} x y = ∀ (P : A → Set) → P x → P y

-- show that Leibniz equality is also an equivalence

≐-refl : ∀ {A : Set} {x : A} →
  x ≐ x
≐-refl P Px = Px

module inlined-alternative where
  Q : {A : Set} {P : A → Set} (x z : A) → Set
  Q {A} {P} x z = P z → P x

  ≐-sym : ∀ {A : Set} {x y : A} → x ≐ y → y ≐ x
  ≐-sym {A} {x} x≐y P = x≐y (Q x) (≐-refl P)

≐-sym : ∀ {A : Set} {x y : A} → x ≐ y → y ≐ x
≐-sym {A} {x} {y} x=y P = Qy
  where Q = λ z → P z → P x
        Qx : Q x
        Qx = ≐-refl P
        Qy : Q y
        Qy = x=y Q Qx

-- end lecture June 3

-- the remaining proofs are straightforward

-- transitivity of Leibniz equality
≐-trans : ∀ {A : Set} {x y z : A} → x ≐ y → y ≐ z → x ≐ z
≐-trans x=y y=z = λ P x₁ → y=z P (x=y P x₁)

-- Leibnitz equality is a congruence (boils down to function composition P ∘ f)
≐-cong : ∀ {A B : Set} {x y : A} {f : A → B} → x ≐ y → f x ≐ f y
≐-cong {f = f} x≐y = λ P → x≐y (λ a → P (f a))

-- substitution holds for Leibnitz equality by definition
≐-subst : ∀ {A : Set} {x y : A} {P : A → Set} → x ≐ y → P x → P y
≐-subst x≐y = x≐y _

-- the final question: is Martin-Lof identity equivalent to Leibnitz equality?
≡->≐ : ∀ {A : Set} {x y : A} → x ≡ y → x ≐ y
≡->≐ refl = λ P z → z

≐->≡ : ∀ {A : Set} {x y : A} → x ≐ y → x ≡ y
≐->≡ {A} {x} x≐y = x≐y (_≡_ x) refl

-- the last proof has the same structure as ≐-sym
-- but by now, Agda finds it automatically (use ^C^A)