/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura

In the standard library we cannot assume the univalence axiom.
We say two types are equivalent if they are isomorphic.
-/
import data.sum data.nat
open function

structure equiv [class] (A B : Type) :=
  (to_fun    : A → B)
  (inv       : B → A)
  (left_inv  : left_inverse inv to_fun)
  (right_inv : right_inverse inv to_fun)

namespace equiv
infix `≃`:50 := equiv

namespace ops
  attribute equiv.to_fun [coercion]
  definition inverse [reducible] {A B : Type} [h : A ≃ B] : B → A :=
  λ b, @equiv.inv A B h b
  postfix `⁻¹` := inverse
end ops

protected theorem refl [refl] (A : Type) : A ≃ A :=
mk (@id A) (@id A) (λ x, rfl) (λ x, rfl)

protected theorem symm [symm] {A B : Type} : A ≃ B → B ≃ A
| (mk f g h₁ h₂) := mk g f h₂ h₁

protected theorem trans [trans] {A B C : Type} : A ≃ B → B ≃ C → A ≃ C
| (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) :=
  mk (f₂ ∘ f₁) (g₁ ∘ g₂)
   (show ∀ x, g₁ (g₂ (f₂ (f₁ x))) = x, by intros; rewrite [l₂, l₁])
   (show ∀ x, f₂ (f₁ (g₁ (g₂ x))) = x, by intros; rewrite [r₁, r₂])

lemma false_equiv_empty : empty ≃ false :=
mk (λ e, empty.rec _ e) (λ h, false.rec _ h) (λ e, empty.rec _ e) (λ h, false.rec _ h)

lemma arrow_congr {A₁ B₁ A₂ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ → B₁) ≃ (A₂ → B₂)
| (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) :=
  mk
   (λ (h : A₁ → B₁) (a : A₂), f₂ (h (g₁ a)))
   (λ (h : A₂ → B₂) (a : A₁), g₂ (h (f₁ a)))
   (λ h, funext (λ a, by rewrite [l₁, l₂]))
   (λ h, funext (λ a, by rewrite [r₁, r₂]))

section
open unit
lemma arrow_unit_equiv_unit (A : Type) : (A → unit) ≃ unit :=
mk (λ f, star) (λ u, (λ f, star))
   (λ f, funext (λ x, by cases (f x); reflexivity))
   (λ u, by cases u; reflexivity)

lemma unit_arrow_equiv (A : Type) : (unit → A) ≃ A :=
mk (λ f, f star) (λ a, (λ u, a))
   (λ f, funext (λ x, by cases x; reflexivity))
   (λ u, rfl)

lemma empty_arrow_equiv_unit (A : Type) : (empty → A) ≃ unit :=
mk (λ f, star) (λ u, λ e, empty.rec _ e)
   (λ f, funext (λ x, empty.rec _ x))
   (λ u, by cases u; reflexivity)

lemma false_arrow_equiv_unit (A : Type) : (false → A) ≃ unit :=
calc (false → A) ≃ (empty → A) : arrow_congr false_equiv_empty !equiv.refl
             ... ≃ unit        : empty_arrow_equiv_unit
end

lemma prod_congr {A₁ B₁ A₂ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ × B₁) ≃ (A₂ × B₂)
| (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) :=
  mk
    (λ p, match p with (a₁, b₁) := (f₁ a₁, f₂ b₁) end)
    (λ p, match p with (a₂, b₂) := (g₁ a₂, g₂ b₂) end)
    (λ p, begin cases p, esimp, rewrite [l₁, l₂] end)
    (λ p, begin cases p, esimp, rewrite [r₁, r₂] end)

lemma prod_comm (A B : Type) : (A × B) ≃ (B × A) :=
mk (λ p, match p with (a, b) := (b, a) end)
   (λ p, match p with (b, a) := (a, b) end)
   (λ p, begin cases p, esimp end)
   (λ p, begin cases p, esimp end)

lemma prod_assoc (A B C : Type) : ((A × B) × C) ≃ (A × (B × C)) :=
mk (λ t, match t with ((a, b), c) := (a, (b, c)) end)
   (λ t, match t with (a, (b, c)) := ((a, b), c) end)
   (λ t, begin cases t with ab c, cases ab, esimp end)
   (λ t, begin cases t with a bc, cases bc, esimp end)

section
open unit prod.ops
lemma prod_unit_right (A : Type) : (A × unit) ≃ A :=
mk (λ p, p.1)
   (λ a, (a, star))
   (λ p, begin cases p with a u, cases u, esimp end)
   (λ a, rfl)

lemma prod_unit_left (A : Type) : (unit × A) ≃ A :=
calc (unit × A) ≃ (A × unit) : prod_comm
            ... ≃ A          : prod_unit_right

lemma prod_empty_right (A : Type) : (A × empty) ≃ empty :=
mk (λ p, empty.rec _ p.2) (λ e, empty.rec _ e) (λ p, empty.rec _ p.2)  (λ e, empty.rec _ e)

lemma prod_empty_left (A : Type) : (empty × A) ≃ empty :=
calc (empty × A) ≃ (A × empty) : prod_comm
             ... ≃ empty       : prod_empty_right
end

section
open sum
lemma sum_congr {A₁ B₁ A₂ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ + B₁) ≃ (A₂ + B₂)
| (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) :=
  mk
   (λ s, match s with inl a₁ := inl (f₁ a₁) | inr b₁ := inr (f₂ b₁) end)
   (λ s, match s with inl a₂ := inl (g₁ a₂) | inr b₂ := inr (g₂ b₂) end)
   (λ s, begin cases s, {esimp, rewrite l₁}, {esimp, rewrite l₂} end)
   (λ s, begin cases s, {esimp, rewrite r₁}, {esimp, rewrite r₂} end)

open bool unit
lemma bool_equiv_unit_sum_unit : bool ≃ (unit + unit) :=
mk (λ b, match b with tt := inl star | ff := inr star end)
   (λ s, match s with inl star := tt | inr star := ff end)
   (λ b, begin cases b, esimp, esimp end)
   (λ s, begin cases s with u u, {cases u, esimp}, {cases u, esimp} end)

lemma sum_comm (A B : Type) : (A + B) ≃ (B + A) :=
mk (λ s, match s with inl a := inr a | inr b := inl b end)
   (λ s, match s with inl b := inr b | inr a := inl a end)
   (λ s, begin cases s, esimp, esimp end)
   (λ s, begin cases s, esimp, esimp end)

lemma sum_assoc (A B C : Type) : ((A + B) + C) ≃ (A + (B + C)) :=
mk (λ s, match s with inl (inl a) := inl a | inl (inr b) := inr (inl b) | inr c := inr (inr c) end)
   (λ s, match s with inl a := inl (inl a) | inr (inl b) := inl (inr b) | inr (inr c) := inr c end)
   (λ s, begin cases s with ab c, cases ab, repeat esimp end)
   (λ s, begin cases s with a bc, esimp, cases bc, repeat esimp end)

lemma sum_empty_right (A : Type) : (A + empty) ≃ A :=
mk (λ s, match s with inl a := a | inr e := empty.rec _ e end)
   (λ a, inl a)
   (λ s, begin cases s with a e, esimp, exact empty.rec _ e end)
   (λ a, rfl)

lemma sum_empty_left (A : Type) : (empty + A) ≃ A :=
calc (empty + A) ≃ (A + empty) : sum_comm
          ...    ≃ A           : sum_empty_right
end

section
open prod.ops
lemma arrow_prod_equiv_prod_arrow (A B C : Type) : (C → A × B) ≃ ((C → A) × (C → B)) :=
mk (λ f, (λ c, (f c).1, λ c, (f c).2))
   (λ p, λ c, (p.1 c, p.2 c))
   (λ f, funext (λ c, begin esimp, cases f c, esimp end))
   (λ p, begin cases p, esimp end)

lemma arrow_arrow_equiv_prod_arrow (A B C : Type) : (A → B → C) ≃ (A × B → C) :=
mk (λ f, λ p, f p.1 p.2)
   (λ f, λ a b, f (a, b))
   (λ f, rfl)
   (λ f, funext (λ p, begin cases p, esimp end))

open sum
lemma sum_arrow_equiv_prod_arrow (A B C : Type) : ((A + B) → C) ≃ ((A → C) × (B → C)) :=
mk (λ f, (λ a, f (inl a), λ b, f (inr b)))
   (λ p, (λ s, match s with inl a := p.1 a | inr b := p.2 b end))
   (λ f, funext (λ s, begin cases s, esimp, esimp end))
   (λ p, begin cases p, esimp end)

lemma sum_prod_distrib (A B C : Type) : ((A + B) × C) ≃ ((A × C) + (B × C)) :=
mk (λ p, match p with (inl a, c) := inl (a, c) | (inr b, c) := inr (b, c) end)
   (λ s, match s with inl (a, c) := (inl a, c) | inr (b, c) := (inr b, c) end)
   (λ p, begin cases p with ab c, cases ab, repeat esimp end)
   (λ s, begin cases s with ac bc, cases ac, esimp, cases bc, esimp end)

lemma prod_sum_distrib (A B C : Type) : (A × (B + C)) ≃ ((A × B) + (A × C)) :=
calc (A × (B + C)) ≃ ((B + C) × A)       : prod_comm
             ...   ≃ ((B × A) + (C × A)) : sum_prod_distrib
             ...   ≃ ((A × B) + (A × C)) : sum_congr !prod_comm !prod_comm
end

section
open sum nat unit prod.ops
lemma nat_equiv_nat_sum_unit : nat ≃ (nat + unit) :=
mk (λ n, match n with 0 := inr star | succ a := inl a end)
   (λ s, match s with inl n := succ n | inr star := zero end)
   (λ n, begin cases n, repeat esimp end)
   (λ s, begin cases s with a u, esimp, {cases u, esimp} end)

lemma nat_sum_unit_equiv_nat : (nat + unit) ≃ nat :=
equiv.symm nat_equiv_nat_sum_unit

lemma nat_prod_nat_equiv_nat : (nat × nat) ≃ nat :=
mk (λ p, mkpair p.1 p.2)
   (λ n, unpair n)
   (λ p, begin cases p, apply unpair_mkpair end)
   (λ n, mkpair_unpair n)

lemma nat_sum_bool_equiv_nat : (nat + bool) ≃ nat :=
calc (nat + bool) ≃ (nat + (unit + unit)) : sum_congr !equiv.refl bool_equiv_unit_sum_unit
             ...  ≃ ((nat + unit) + unit) : sum_assoc
             ...  ≃ (nat + unit)          : sum_congr nat_sum_unit_equiv_nat !equiv.refl
             ...  ≃ nat                   : nat_sum_unit_equiv_nat

open decidable
lemma nat_sum_nat_equiv_nat : (nat + nat) ≃ nat :=
mk (λ s, match s with inl n := 2*n | inr n := 2*n+1 end)
   (λ n, if even n then inl (n div 2) else inr ((n - 1) div 2))
   (λ s, begin
           have two_gt_0 : 2 > 0, from dec_trivial,
           cases s,
             {esimp, rewrite [if_pos (even_two_mul _), mul_div_cancel_left _ two_gt_0]},
             {esimp, rewrite [if_neg (not_even_two_mul_plus_one _), add_sub_cancel, mul_div_cancel_left _ two_gt_0]}
         end)
   (λ n, by_cases
          (λ h : even n, begin rewrite [if_pos h], esimp, rewrite [mul_div_cancel' (dvd_of_even h)]  end)
          (λ h : ¬ even n,
            begin
              rewrite [if_neg h], esimp,
              cases n,
                {exact absurd even_zero h},
                {rewrite [-add_one, add_sub_cancel,
                          mul_div_cancel' (dvd_of_even (even_of_odd_succ (odd_of_not_even h)))]}
            end))
end

section
open decidable
definition decidable_eq_of_equiv {A B : Type} [h : decidable_eq A] : A ≃ B → decidable_eq B
| (mk f g l r) :=
  take b₁ b₂, match h (g b₁) (g b₂) with
  | inl he := inl (assert aux : f (g b₁) = f (g b₂), from congr_arg f he,
                   begin rewrite *r at aux, exact aux end)
  | inr hn := inr (λ b₁eqb₂, by subst b₁eqb₂; exact absurd rfl hn)
  end
end

definition inhabited_of_equiv {A B : Type} [h : inhabited A] : A ≃ B → inhabited B
| (mk f g l r) := inhabited.mk (f (inhabited.value h))

section
open subtype
override equiv.ops
definition subtype_equiv_of_subtype {A B : Type} {p : A → Prop} : A ≃ B → {a : A | p a} ≃ {b : B | p (b⁻¹)}
| (mk f g l r) :=
  mk (λ s, match s with tag v h := tag (f v) (eq.rec_on (eq.symm (l v)) h) end)
     (λ s, match s with tag v h := tag (g v) (eq.rec_on (eq.symm (r v)) h) end)
     (λ s, begin cases s, esimp, congruence, rewrite l, reflexivity end)
     (λ s, begin cases s, esimp, congruence, rewrite r, reflexivity end)
end
end equiv