import tactic.basic

import logic.is_empty

universes u v w

variables {α : Sort u} {β : Sort v} {γ : Sort w}

structure unique (α : Sort u) extends inhabited α :=

(uniq : ∀ a : α, a = default)

attribute [class] unique

lemma unique_iff_exists_unique (α : Sort u) : nonempty (unique α) ↔ ∃! a : α, true :=

⟨λ ⟨u⟩, ⟨u.default, trivial, λ a _, u.uniq a⟩, λ ⟨a,_,h⟩, ⟨⟨⟨a⟩, λ _, h _ trivial⟩⟩⟩

lemma unique_subtype_iff_exists_unique {α} (p : α → Prop) :

nonempty (unique (subtype p)) ↔ ∃! a, p a :=

⟨λ ⟨u⟩, ⟨u.default.1, u.default.2, λ a h, congr_arg subtype.val (u.uniq ⟨a,h⟩)⟩,

λ ⟨a,ha,he⟩, ⟨⟨⟨⟨a,ha⟩⟩, λ ⟨b,hb⟩, by { congr, exact he b hb }⟩⟩⟩

@[reducible] def unique_of_subsingleton {α : Sort*} [subsingleton α] (a : α) : unique α :=

{ default := a,

uniq := λ _, subsingleton.elim _ _ }

instance punit.unique : unique punit.{u} :=

{ default := punit.star,

uniq := λ x, punit_eq x _ }

@[simp] lemma punit.default_eq_star : (default : punit) = punit.star := rfl

def unique_prop {p : Prop} (h : p) : unique p :=

{ default := h, uniq := λ x, rfl }

instance : unique true := unique_prop trivial

lemma fin.eq_zero : ∀ n : fin 1, n = 0

| ⟨n, hn⟩ := fin.eq_of_veq (nat.eq_zero_of_le_zero (nat.le_of_lt_succ hn))

instance {n : ℕ} : inhabited (fin n.succ) := ⟨0⟩

instance inhabited_fin_one_add (n : ℕ) : inhabited (fin (1 + n)) := ⟨⟨0, nat.zero_lt_one_add n⟩⟩

@[simp] lemma fin.default_eq_zero (n : ℕ) : (default : fin n.succ) = 0 := rfl

instance fin.unique : unique (fin 1) :=

{ uniq := fin.eq_zero, .. fin.inhabited }

namespace unique

open function

variables [unique α]

@[priority 100] -- see Note [lower instance priority]

instance : inhabited α := to_inhabited ‹unique α›

lemma eq_default (a : α) : a = default := uniq _ a

lemma default_eq (a : α) : default = a := (uniq _ a).symm

@[priority 100] -- see Note [lower instance priority]

instance : subsingleton α := subsingleton_of_forall_eq _ eq_default

lemma forall_iff {p : α → Prop} : (∀ a, p a) ↔ p default :=

⟨λ h, h _, λ h x, by rwa [unique.eq_default x]⟩

lemma exists_iff {p : α → Prop} : Exists p ↔ p default :=

⟨λ ⟨a, ha⟩, eq_default a ▸ ha, exists.intro default⟩

@[ext] protected lemma subsingleton_unique' : ∀ (h₁ h₂ : unique α), h₁ = h₂

| ⟨⟨x⟩, h⟩ ⟨⟨y⟩, _⟩ := by congr; rw [h x, h y]

instance subsingleton_unique : subsingleton (unique α) :=

⟨unique.subsingleton_unique'⟩

@[reducible] def mk' (α : Sort u) [h₁ : inhabited α] [subsingleton α] : unique α :=

{ uniq := λ x, subsingleton.elim _ _, .. h₁ }

end unique

lemma unique_iff_subsingleton_and_nonempty (α : Sort u) :

nonempty (unique α) ↔ subsingleton α ∧ nonempty α :=

⟨λ ⟨u⟩, by split; exactI infer_instance,

λ ⟨hs, hn⟩, ⟨by { resetI, inhabit α, exact unique.mk' α }⟩⟩

@[simp] lemma pi.default_def {β : α → Sort v} [Π a, inhabited (β a)] :

@default (Π a, β a) _ = λ a : α, @default (β a) _ := rfl

lemma pi.default_apply {β : α → Sort v} [Π a, inhabited (β a)] (a : α) :

@default (Π a, β a) _ a = default := rfl

instance pi.unique {β : α → Sort v} [Π a, unique (β a)] : unique (Π a, β a) :=

{ uniq := λ f, funext $ λ x, unique.eq_default _,

.. pi.inhabited α }

instance pi.unique_of_is_empty [is_empty α] (β : α → Sort v) :

unique (Π a, β a) :=

{ default := is_empty_elim,

uniq := λ f, funext is_empty_elim }

lemma eq_const_of_unique [unique α] (f : α → β) : f = function.const α (f default) :=

by { ext x, rw subsingleton.elim x default }

lemma heq_const_of_unique [unique α] {β : α → Sort v}

(f : Π a, β a) : f == function.const α (f default) :=

function.hfunext rfl $ λ i _ _, by rw subsingleton.elim i default

namespace function

variable {f : α → β}

protected lemma injective.subsingleton (hf : injective f) [subsingleton β] :

subsingleton α :=

⟨λ x y, hf $ subsingleton.elim _ _⟩

protected lemma surjective.subsingleton [subsingleton α] (hf : surjective f) :

subsingleton β :=

⟨hf.forall₂.2 $ λ x y, congr_arg f $ subsingleton.elim x y⟩

protected def surjective.unique (hf : surjective f) [unique α] : unique β :=

@unique.mk' _ ⟨f default⟩ hf.subsingleton

protected def injective.unique [inhabited α] [subsingleton β] (hf : injective f) : unique α :=

@unique.mk' _ _ hf.subsingleton

def surjective.unique_of_surjective_const (α : Type*) {β : Type*} (b : β)

(h : function.surjective (function.const α b)) : unique β :=

@unique_of_subsingleton _ (subsingleton_of_forall_eq b $ h.forall.mpr (λ _, rfl)) b

end function

lemma unique.bijective {A B} [unique A] [unique B] {f : A → B} : function.bijective f :=

rw function.bijective_iff_has_inverse,

refine ⟨default, _, _⟩; intro x; simp

namespace option

lemma subsingleton_iff_is_empty {α} : subsingleton (option α) ↔ is_empty α :=

⟨λ h, ⟨λ x, option.no_confusion $ @subsingleton.elim _ h x none⟩,

λ h, ⟨λ x y, option.cases_on x (option.cases_on y rfl (λ x, h.elim x)) (λ x, h.elim x)⟩⟩

instance {α} [is_empty α] : unique (option α) := @unique.mk' _ _ (subsingleton_iff_is_empty.2 ‹_›)

end option

section subtype

instance unique.subtype_eq (y : α) : unique {x // x = y} :=

{ default := ⟨y, rfl⟩,

uniq := λ ⟨x, hx⟩, by simpa using hx }

instance unique.subtype_eq' (y : α) : unique {x // y = x} :=

{ default := ⟨y, rfl⟩,

uniq := λ ⟨x, hx⟩, by simpa using hx.symm }

end subtype