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

notation, basic datatypes and type classes
-/
prelude

notation `Prop` := Sort 0
notation f ` $ `:1 a:0 := f a

/- Logical operations and relations -/

reserve prefix `¬`:40
reserve prefix `~`:40
reserve infixr ` ∧ `:35
reserve infixr ` /\ `:35
reserve infixr ` \/ `:30
reserve infixr ` ∨ `:30
reserve infix ` <-> `:20
reserve infix ` ↔ `:20
reserve infix ` = `:50
reserve infix ` == `:50
reserve infix ` != `:50
reserve infix ` ~= `:50
reserve infix ` ≅ `:50
reserve infix ` ≠ `:50
reserve infix ` ≈ `:50
reserve infix ` ~ `:50
reserve infix ` ≡ `:50
reserve infixl ` ⬝ `:75
reserve infixr ` ▸ `:75
reserve infixr ` ▹ `:75

/- types and Type constructors -/

reserve infixr ` ⊕ `:30
reserve infixr ` × `:35

/- arithmetic operations -/

reserve infixl ` + `:65
reserve infixl ` - `:65
reserve infixl ` * `:70
reserve infixl ` / `:70
reserve infixl ` % `:70
reserve infixl ` %ₙ `:70
reserve prefix `-`:100
reserve infixr ` ^ `:80

reserve infixr ` ∘ `:90

reserve infix ` <= `:50
reserve infix ` ≤ `:50
reserve infix ` < `:50
reserve infix ` >= `:50
reserve infix ` ≥ `:50
reserve infix ` > `:50

/- boolean operations -/

reserve prefix `!`:40
reserve infixl ` && `:35
reserve infixl ` || `:30

/- set operations -/

reserve infix ` ∈ `:50
reserve infix ` ∉ `:50
reserve infixl ` ∩ `:70
reserve infixl ` ∪ `:65
reserve infix ` ⊆ `:50
reserve infix ` ⊇ `:50
reserve infix ` ⊂ `:50
reserve infix ` ⊃ `:50
reserve infix ` \ `:70

/- other symbols -/

reserve infix ` ∣ `:50
reserve infixl ` ++ `:65
reserve infixr ` :: `:67

/- Control -/
reserve infixr ` <|> `:2
reserve infixr `; `   :3
reserve infixr ` >>= `:55
reserve infixr ` >=> `:55
reserve infixl ` <*> `:60
reserve infixl ` <* ` :60
reserve infixr ` *> ` :60
reserve infixr ` >> ` :60
reserve infixr ` <$> `:100
reserve infixr ` <$ ` :100
reserve infixr ` $> ` :100
reserve infixl ` <&> `:100

universes u v w

/-- Auxiliary unsafe constant used by the Compiler when erasing proofs from code. -/
unsafe axiom lcProof {α : Prop} : α
/-- Auxiliary unsafe constant used by the Compiler to mark unreachable code. -/
unsafe axiom lcUnreachable {α : Sort u} : α

@[inline] def id {α : Sort u} (a : α) : α := a

def inline {α : Sort u} (a : α) : α := a

@[inline] def flip {α : Sort u} {β : Sort v} {φ : Sort w} (f : α → β → φ) : β → α → φ :=
λ b a, f a b

/-
The kernel definitional equality test (t =?= s) has special support for idDelta applications.
It implements the following rules

   1)   (idDelta t) =?= t
   2)   t =?= (idDelta t)
   3)   (idDelta t) =?= s  IF (unfoldOf t) =?= s
   4)   t =?= idDelta s    IF t =?= (unfoldOf s)

This is mechanism for controlling the delta reduction (aka unfolding) used in the kernel.

We use idDelta applications to address performance problems when Type checking
theorems generated by the equation Compiler.
-/
@[inline] def idDelta {α : Sort u} (a : α) : α :=
a

/-- Gadget for optional parameter support. -/
@[reducible] def optParam (α : Sort u) (default : α) : Sort u :=
α

/-- Gadget for marking output parameters in type classes. -/
@[reducible] def outParam (α : Sort u) : Sort u := α

/-- Auxiliary Declaration used to implement the notation (a : α) -/
@[reducible] def typedExpr (α : Sort u) (a : α) : α := a

/- `idRhs` is an auxiliary Declaration used in the equation Compiler to address performance
   issues when proving equational theorems. The equation Compiler uses it as a marker. -/
@[macroInline] abbrev idRhs (α : Sort u) (a : α) : α := a

inductive PUnit : Sort u
| unit : PUnit

/-- An abbreviation for `PUnit.{0}`, its most common instantiation.
    This Type should be preferred over `PUnit` where possible to avoid
    unnecessary universe parameters. -/
abbrev Unit : Type := PUnit

@[pattern] abbrev Unit.unit : Unit := PUnit.unit

/- Remark: thunks have an efficient implementation in the runtime. -/
structure Thunk (α : Type u) : Type u :=
(fn : Unit → α)

attribute [extern cpp inline "lean::mk_thunk(#2)"] Thunk.mk

@[noinline, extern cpp inline "lean::thunk_pure(#2)"]
protected def Thunk.pure {α : Type u} (a : α) : Thunk α :=
⟨λ _, a⟩
@[noinline, extern cpp inline "lean::thunk_get_own(#2)"]
protected def Thunk.get {α : Type u} (x : @& Thunk α) : α :=
x.fn ()
@[noinline, extern cpp inline "lean::thunk_map(#3, #4)"]
protected def Thunk.map {α : Type u} {β : Type v} (f : α → β) (x : Thunk α) : Thunk β :=
⟨λ _, f x.get⟩
@[noinline, extern cpp inline "lean::thunk_bind(#3, #4)"]
protected def Thunk.bind {α : Type u} {β : Type v} (x : Thunk α) (f : α → Thunk β) : Thunk β :=
⟨λ _, (f x.get).get⟩

/- Remark: tasks have an efficient implementation in the runtime. -/
structure Task (α : Type u) : Type u :=
(fn : Unit → α)

attribute [extern cpp inline "lean::mk_task(#2)"] Task.mk

@[noinline, extern cpp inline "lean::task_pure(#2)"]
protected def Task.pure {α : Type u} (a : α) : Task α :=
⟨λ _, a⟩
@[noinline, extern cpp inline "lean::task_get(#2)"]
protected def Task.get {α : Type u} (x : @& Task α) : α :=
x.fn ()
@[noinline, extern cpp inline "lean::task_map(#3, #4)"]
protected def Task.map {α : Type u} {β : Type v} (f : α → β) (x : Task α) : Task β :=
⟨λ _, f x.get⟩
@[noinline, extern cpp inline "lean::task_bind(#3, #4)"]
protected def Task.bind {α : Type u} {β : Type v} (x : Task α) (f : α → Task β) : Task β :=
⟨λ _, (f x.get).get⟩

inductive True : Prop
| intro : True

inductive False : Prop

inductive Empty : Type

def Not (a : Prop) : Prop := a → False
prefix `¬` := Not

inductive Eq {α : Sort u} (a : α) : α → Prop
| refl : Eq a

@[elabAsEliminator, inline, reducible]
def {u1 u2} Eq.ndrec {α : Sort u2} {a : α} {C : α → Sort u1} (m : C a) {b : α} (h : Eq a b) : C b :=
@Eq.rec α a (λ α _, C α) m b h

@[elabAsEliminator, inline, reducible]
def {u1 u2} Eq.ndrecOn {α : Sort u2} {a : α} {C : α → Sort u1} {b : α} (h : Eq a b) (m : C a) : C b :=
@Eq.rec α a (λ α _, C α) m b h

/-
Initialize the Quotient Module, which effectively adds the following definitions:

constant Quot {α : Sort u} (r : α → α → Prop) : Sort u

constant Quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : Quot r

constant Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
  (∀ a b : α, r a b → Eq (f a) (f b)) → Quot r → β

constant Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} :
  (∀ a : α, β (Quot.mk r a)) → ∀ q : Quot r, β q
-/
initQuot

inductive Heq {α : Sort u} (a : α) : Π {β : Sort u}, β → Prop
| refl : Heq a

structure Prod (α : Type u) (β : Type v) :=
(fst : α) (snd : β)

/-- Similar to `Prod`, but α and β can be propositions.
   We use this Type internally to automatically generate the brecOn recursor. -/
structure PProd (α : Sort u) (β : Sort v) :=
(fst : α) (snd : β)

structure And (a b : Prop) : Prop :=
intro :: (left : a) (right : b)

structure Iff (a b : Prop) : Prop :=
intro :: (mp : a → b) (mpr : b → a)

/- Eq basic support -/

infix = := Eq

@[pattern] def rfl {α : Sort u} {a : α} : a = a := Eq.refl a

@[elabAsEliminator]
theorem Eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b :=
Eq.ndrec h₂ h₁

infixr ▸ := Eq.subst

theorem Eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c :=
h₂ ▸ h₁

theorem Eq.symm {α : Sort u} {a b : α} (h : a = b) : b = a :=
h ▸ rfl

infix ~= := Heq
infix ≅ := Heq

@[pattern] def Heq.rfl {α : Sort u} {a : α} : a ≅ a := Heq.refl a

theorem eqOfHeq {α : Sort u} {a a' : α} (h : a ≅ a') : a = a' :=
have ∀ (α' : Sort u) (a' : α') (h₁ : @Heq α a α' a') (h₂ : α = α'), (Eq.recOn h₂ a : α') = a', from
  λ (α' : Sort u) (a' : α') (h₁ : @Heq α a α' a'), Heq.recOn h₁ (λ h₂ : α = α, rfl),
show (Eq.ndrecOn (Eq.refl α) a : α) = a', from
  this α a' h (Eq.refl α)

inductive Sum (α : Type u) (β : Type v)
| inl {} (val : α) : Sum
| inr {} (val : β) : Sum

inductive PSum (α : Sort u) (β : Sort v)
| inl {} (val : α) : PSum
| inr {} (val : β) : PSum

inductive Or (a b : Prop) : Prop
| inl {} (h : a) : Or
| inr {} (h : b) : Or

def Or.introLeft {a : Prop} (b : Prop) (ha : a) : Or a b :=
Or.inl ha

def Or.introRight (a : Prop) {b : Prop} (hb : b) : Or a b :=
Or.inr hb

structure Sigma {α : Type u} (β : α → Type v) :=
mk :: (fst : α) (snd : β fst)

structure PSigma {α : Sort u} (β : α → Sort v) :=
mk :: (fst : α) (snd : β fst)

inductive Bool : Type
| false : Bool
| true : Bool

/- Remark: Subtype must take a Sort instead of Type because of the axiom strongIndefiniteDescription. -/
structure Subtype {α : Sort u} (p : α → Prop) :=
(val : α) (property : p val)

inductive Exists {α : Sort u} (p : α → Prop) : Prop
| intro (w : α) (h : p w) : Exists

class inductive Decidable (p : Prop)
| isFalse (h : ¬p) : Decidable
| isTrue  (h : p) : Decidable

@[reducible] def DecidablePred {α : Sort u} (r : α → Prop) :=
Π (a : α), Decidable (r a)

@[reducible] def DecidableRel {α : Sort u} (r : α → α → Prop) :=
Π (a b : α), Decidable (r a b)

class DecidableEq (α : Sort u) :=
{decEq : Π a b : α, Decidable (a = b)}

export DecidableEq (decEq)

@[inline] instance decidableOfDecidableEq {α : Sort u} (a b : α) [DecidableEq α] : Decidable (a = b) :=
decEq a b

inductive Option (α : Type u)
| none {} : Option
| some (val : α) : Option

export Option (none some)
export Bool (false true)

inductive List (T : Type u)
| nil {} : List
| cons (hd : T) (tl : List) : List

infixr :: := List.cons

inductive Nat
| zero : Nat
| succ (n : Nat) : Nat

/- Auxiliary axiom used to implement `sorry`.
   TODO: add this theorem on-demand. That is,
   we should only add it if after the first error. -/
unsafe axiom sorryAx (α : Sort u) (synthetic := true) : α

/- Declare builtin and reserved notation -/

class HasZero     (α : Type u) := (zero : α)
class HasOne      (α : Type u) := (one : α)
class HasAdd      (α : Type u) := (add : α → α → α)
class HasMul      (α : Type u) := (mul : α → α → α)
class HasNeg      (α : Type u) := (neg : α → α)
class HasSub      (α : Type u) := (sub : α → α → α)
class HasDiv      (α : Type u) := (div : α → α → α)
class HasDivides  (α : Type u) := (Divides : α → α → Prop)
class HasMod      (α : Type u) := (mod : α → α → α)
class HasModn     (α : Type u) := (modn : α → Nat → α)
class HasLessEq   (α : Type u) := (LessEq : α → α → Prop)
class HasLess     (α : Type u) := (Less : α → α → Prop)
class HasBeq      (α : Type u) := (beq : α → α → Bool)
class HasAppend   (α : Type u) := (append : α → α → α)
class HasOrelse   (α : Type u) := (orelse  : α → α → α)
class HasAndthen  (α : Type u) := (andthen : α → α → α)
class HasUnion    (α : Type u) := (union : α → α → α)
class HasInter    (α : Type u) := (inter : α → α → α)
class HasSDiff    (α : Type u) := (sdiff : α → α → α)
class HasEquiv    (α : Sort u) := (Equiv : α → α → Prop)
class HasSubset   (α : Type u) := (Subset : α → α → Prop)
class HasSSubset  (α : Type u) := (SSubset : α → α → Prop)
/- Type classes HasEmptyc and HasInsert are
   used to implement polymorphic notation for collections.
   Example: {a, b, c}. -/
class HasEmptyc   (α : Type u) := (emptyc : α)
class HasInsert   (α : outParam $ Type u) (γ : Type v) := (insert : α → γ → γ)
/- Type class used to implement the notation { a ∈ c | p a } -/
class HasSep (α : outParam $ Type u) (γ : Type v) :=
(sep : (α → Prop) → γ → γ)
/- Type class for set-like membership -/
class HasMem (α : outParam $ Type u) (γ : Type v) := (mem : α → γ → Prop)

class HasPow (α : Type u) (β : Type v) :=
(pow : α → β → α)

export HasAndthen (andthen)
export HasPow (pow)

infix ∈        := HasMem.mem
notation a ` ∉ ` s := ¬ HasMem.mem a s
infix +        := HasAdd.add
infix *        := HasMul.mul
infix -        := HasSub.sub
infix /        := HasDiv.div
infix ∣        := HasDivides.Divides
infix %        := HasMod.mod
infix %ₙ       := HasModn.modn
prefix -       := HasNeg.neg
infix <=       := HasLessEq.LessEq
infix ≤        := HasLessEq.LessEq
infix <        := HasLess.Less
infix ==       := HasBeq.beq
infix ++       := HasAppend.append
notation `∅`   := HasEmptyc.emptyc _
infix ∪        := HasUnion.union
infix ∩        := HasInter.inter
infix ⊆        := HasSubset.Subset
infix ⊂        := HasSSubset.SSubset
infix \        := HasSDiff.sdiff
infix ≈        := HasEquiv.Equiv
infixr ^       := HasPow.pow
infixr /\      := And
infixr ∧       := And
infixr \/      := Or
infixr ∨       := Or
infix <->      := Iff
infix ↔        := Iff
-- notation `exists` binders `, ` r:(scoped P, Exists P) := r
-- notation `∃` binders `, ` r:(scoped P, Exists P) := r
infixr <|>     := HasOrelse.orelse
infixr >>      := HasAndthen.andthen

export HasAppend (append)

@[reducible] def GreaterEq {α : Type u} [HasLessEq α] (a b : α) : Prop := HasLessEq.LessEq b a
@[reducible] def Greater {α : Type u} [HasLess α] (a b : α) : Prop     := HasLess.Less b a

infix >=       := GreaterEq
infix ≥        := GreaterEq
infix >        := Greater

@[reducible] def Superset {α : Type u} [HasSubset α] (a b : α) : Prop := HasSubset.Subset b a
@[reducible] def SSuperset {α : Type u} [HasSSubset α] (a b : α) : Prop := HasSSubset.SSubset b a

infix ⊇        := Superset
infix ⊃        := SSuperset

@[inline] def bit0 {α : Type u} [s  : HasAdd α] (a  : α)                 : α := a + a
@[inline] def bit1 {α : Type u} [s₁ : HasOne α] [s₂ : HasAdd α] (a : α) : α := (bit0 a) + 1

attribute [pattern] HasZero.zero HasOne.one bit0 bit1 HasAdd.add HasNeg.neg

export HasInsert (insert)

/- The Empty collection -/
@[inline] def singleton {α : Type u} {γ : Type v} [HasEmptyc γ] [HasInsert α γ] (a : α) : γ :=
HasInsert.insert a ∅

/- Nat basic instances -/
@[extern cpp "lean::nat_add"]
protected def Nat.add : (@& Nat) → (@& Nat) → Nat
| a  Nat.zero     := a
| a  (Nat.succ b) := Nat.succ (Nat.add a b)

/- We mark the following definitions as pattern to make sure they can be used in recursive equations,
   and reduced by the equation Compiler. -/
attribute [pattern] Nat.add Nat.add._main

instance : HasZero Nat := ⟨Nat.zero⟩

instance : HasOne Nat := ⟨Nat.succ (Nat.zero)⟩

instance : HasAdd Nat := ⟨Nat.add⟩

/- Auxiliary constant used by equation compiler. -/
constant hugeFuel : Nat := 10000

def std.priority.default : Nat := 1000
def std.priority.max     : Nat := 0xFFFFFFFF

protected def Nat.prio := std.priority.default + 100

/-
  Global declarations of right binding strength

  If a Module reassigns these, it will be incompatible with other modules that adhere to these
  conventions.

  When hovering over a symbol, use "C-c C-k" to see how to input it.
-/
def std.prec.max   : Nat := 1024 -- the strength of application, identifiers, (, [, etc.
def std.prec.arrow : Nat := 25

/-
The next def is "max + 10". It can be used e.g. for postfix operations that should
be stronger than application.
-/

def std.prec.maxPlus : Nat := std.prec.max + 10

infixr × := Prod
-- notation for n-ary tuples

/- Some type that is not a scalar value in our runtime.
   TODO: mark opaque -/
structure NonScalar :=
(val : Nat)

/- sizeof -/

class HasSizeof (α : Sort u) :=
(sizeof : α → Nat)

export HasSizeof (sizeof)

/-
Declare sizeof instances and theorems for types declared before HasSizeof.
From now on, the inductive Compiler will automatically generate sizeof instances and theorems.
-/

/- Every Type `α` has a default HasSizeof instance that just returns 0 for every element of `α` -/
protected def default.sizeof (α : Sort u) : α → Nat
| a := 0

instance defaultHasSizeof (α : Sort u) : HasSizeof α :=
⟨default.sizeof α⟩

protected def Nat.sizeof : Nat → Nat
| n := n

instance : HasSizeof Nat :=
⟨Nat.sizeof⟩

protected def Prod.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof β] : (Prod α β) → Nat
| ⟨a, b⟩ := 1 + sizeof a + sizeof b

instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Prod α β) :=
⟨Prod.sizeof⟩

protected def Sum.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof β] : (Sum α β) → Nat
| (Sum.inl a) := 1 + sizeof a
| (Sum.inr b) := 1 + sizeof b

instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Sum α β) :=
⟨Sum.sizeof⟩

protected def PSum.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof β] : (PSum α β) → Nat
| (PSum.inl a) := 1 + sizeof a
| (PSum.inr b) := 1 + sizeof b

instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (PSum α β) :=
⟨PSum.sizeof⟩

protected def Sigma.sizeof {α : Type u} {β : α → Type v} [HasSizeof α] [∀ a, HasSizeof (β a)] : Sigma β → Nat
| ⟨a, b⟩ := 1 + sizeof a + sizeof b

instance (α : Type u) (β : α → Type v) [HasSizeof α] [∀ a, HasSizeof (β a)] : HasSizeof (Sigma β) :=
⟨Sigma.sizeof⟩

protected def PSigma.sizeof {α : Type u} {β : α → Type v} [HasSizeof α] [∀ a, HasSizeof (β a)] : PSigma β → Nat
| ⟨a, b⟩ := 1 + sizeof a + sizeof b

instance (α : Type u) (β : α → Type v) [HasSizeof α] [∀ a, HasSizeof (β a)] : HasSizeof (PSigma β) :=
⟨PSigma.sizeof⟩

protected def PUnit.sizeof : PUnit → Nat
| u := 1

instance : HasSizeof PUnit := ⟨PUnit.sizeof⟩

protected def Bool.sizeof : Bool → Nat
| b := 1

instance : HasSizeof Bool := ⟨Bool.sizeof⟩

protected def Option.sizeof {α : Type u} [HasSizeof α] : Option α → Nat
| none     := 1
| (some a) := 1 + sizeof a

instance (α : Type u) [HasSizeof α] : HasSizeof (Option α) :=
⟨Option.sizeof⟩

protected def List.sizeof {α : Type u} [HasSizeof α] : List α → Nat
| List.nil        := 1
| (List.cons a l) := 1 + sizeof a + List.sizeof l

instance (α : Type u) [HasSizeof α] : HasSizeof (List α) :=
⟨List.sizeof⟩

protected def Subtype.sizeof {α : Type u} [HasSizeof α] {p : α → Prop} : Subtype p → Nat
| ⟨a, _⟩ := sizeof a

instance {α : Type u} [HasSizeof α] (p : α → Prop) : HasSizeof (Subtype p) :=
⟨Subtype.sizeof⟩

theorem natAddZero (n : Nat) : n + 0 = n := rfl

theorem optParamEq (α : Sort u) (default : α) : optParam α default = α := rfl

/-- Like `by applyInstance`, but not dependent on the tactic framework. -/
@[reducible] def inferInstance {α : Type u} [i : α] : α := i
@[reducible, elabSimple] def inferInstanceAs (α : Type u) [i : α] : α := i

/- Boolean operators -/

@[macroInline] def cond {a : Type u} : Bool → a → a → a
| true  x y := x
| false x y := y

@[macroInline] def or : Bool → Bool → Bool
| true  _  := true
| false b  := b

@[macroInline] def and : Bool → Bool → Bool
| false _  := false
| true  b  := b

@[macroInline] def not : Bool → Bool
| true  := false
| false := true

@[macroInline] def xor : Bool → Bool → Bool
| true  b := not b
| false b := b

prefix ! := not
infix || := or
infix && := and

@[extern cpp inline "#1 || #2"] def strictOr  (b₁ b₂ : Bool) := b₁ || b₂
@[extern cpp inline "#1 && #2"] def strictAnd (b₁ b₂ : Bool) := b₁ && b₂

@[inline] def bne {α : Type u} [HasBeq α] (a b : α) : Bool :=
!(a == b)

infix != := bne

/- Logical connectives an equality -/

def implies (a b : Prop) := a → b

theorem implies.trans {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) : implies p r :=
assume hp, h₂ (h₁ hp)

def trivial : True := ⟨⟩

@[macroInline] def False.elim {C : Sort u} (h : False) : C :=
False.rec (λ _, C) h

@[macroInline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : ¬a) : b :=
False.elim (h₂ h₁)

theorem mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a := assume ha : a, h₂ (h₁ ha)

theorem notFalse : ¬False := id

-- proof irrelevance is built in
theorem proofIrrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ := rfl

theorem id.def {α : Sort u} (a : α) : id a = a := rfl

@[macroInline] def Eq.mp {α β : Sort u} (h₁ : α = β) (h₂ : α) : β :=
Eq.recOn h₁ h₂

@[macroInline] def Eq.mpr {α β : Sort u} : (α = β) → β → α :=
λ h₁ h₂, Eq.recOn (Eq.symm h₁) h₂

@[elabAsEliminator]
theorem Eq.substr {α : Sort u} {p : α → Prop} {a b : α} (h₁ : b = a) (h₂ : p a) : p b :=
Eq.subst (Eq.symm h₁) h₂

theorem congr {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : f₁ = f₂) (h₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=
Eq.subst h₁ (Eq.subst h₂ rfl)

theorem congrFun {α : Sort u} {β : α → Sort v} {f g : Π x, β x} (h : f = g) (a : α) : f a = g a :=
Eq.subst h (Eq.refl (f a))

theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂ :=
congr rfl h

theorem transRelLeft {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c :=
h₂ ▸ h₁

theorem transRelRight {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : a = b) (h₂ : r b c) : r a c :=
h₁.symm ▸ h₂

theorem ofEqTrue {p : Prop} (h : p = True) : p :=
h.symm ▸ trivial

theorem notOfEqFalse {p : Prop} (h : p = False) : ¬p :=
assume hp, h ▸ hp

@[macroInline] def cast {α β : Sort u} (h : α = β) (a : α) : β :=
Eq.rec a h

theorem castProofIrrel {α β : Sort u} (h₁ h₂ : α = β) (a : α) : cast h₁ a = cast h₂ a := rfl

theorem castEq {α : Sort u} (h : α = α) (a : α) : cast h a = a := rfl

@[reducible] def Ne {α : Sort u} (a b : α) := ¬(a = b)
infix ≠ := Ne

theorem Ne.def {α : Sort u} (a b : α) : a ≠ b = ¬ (a = b) := rfl

section Ne
variable {α : Sort u}
variables {a b : α} {p : Prop}

theorem Ne.intro (h : a = b → False) : a ≠ b := h

theorem Ne.elim (h : a ≠ b) : a = b → False := h

theorem Ne.irrefl (h : a ≠ a) : False := h rfl

theorem Ne.symm (h : a ≠ b) : b ≠ a :=
assume (h₁ : b = a), h (h₁.symm)

theorem falseOfNe : a ≠ a → False := Ne.irrefl

theorem neFalseOfSelf : p → p ≠ False :=
assume (hp : p) (Heq : p = False), Heq ▸ hp

theorem neTrueOfNot : ¬p → p ≠ True :=
assume (hnp : ¬p) (Heq : p = True), (Heq ▸ hnp) trivial

theorem trueNeFalse : ¬True = False :=
neFalseOfSelf trivial
end Ne

theorem eqFalseOfNeTrue : ∀ {b : Bool}, b ≠ true → b = false
| true h := False.elim (h rfl)
| false h := rfl

theorem eqTrueOfNeFalse : ∀ {b : Bool}, b ≠ false → b = true
| true h := rfl
| false h := False.elim (h rfl)

section
variables {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}

@[elabAsEliminator]
theorem {u1 u2} Heq.ndrec {α : Sort u2} {a : α} {C : Π {β : Sort u2}, β → Sort u1} (m : C a) {β : Sort u2} {b : β} (h : a ≅ b) : C b :=
@Heq.rec α a (λ β b _, C b) m β b h

@[elabAsEliminator]
theorem {u1 u2} Heq.ndrecOn {α : Sort u2} {a : α} {C : Π {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : C a) : C b :=
@Heq.rec α a (λ β b _, C b) m β b h

theorem Heq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b :=
Eq.recOn (eqOfHeq h₁) h₂

theorem Heq.subst {p : ∀ T : Sort u, T → Prop} (h₁ : a ≅ b) (h₂ : p α a) : p β b :=
Heq.ndrecOn h₁ h₂

theorem Heq.symm (h : a ≅ b) : b ≅ a :=
Heq.ndrecOn h (Heq.refl a)

theorem heqOfEq (h : a = a') : a ≅ a' :=
Eq.subst h (Heq.refl a)

theorem Heq.trans (h₁ : a ≅ b) (h₂ : b ≅ c) : a ≅ c :=
Heq.subst h₂ h₁

theorem heqOfHeqOfEq (h₁ : a ≅ b) (h₂ : b = b') : a ≅ b' :=
Heq.trans h₁ (heqOfEq h₂)

theorem heqOfEqOfHeq (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b :=
Heq.trans (heqOfEq h₁) h₂

def typeEqOfHeq (h : a ≅ b) : α = β :=
Heq.ndrecOn h (Eq.refl α)
end

theorem eqRecHeq {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} (h : a = a') (p : φ a), (Eq.recOn h p : φ a') ≅ p
| a _ rfl p := Heq.refl p

theorem ofHeqTrue {a : Prop} (h : a ≅ True) : a :=
ofEqTrue (eqOfHeq h)

theorem castHeq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a
| α _ rfl a := Heq.refl a

variables {a b c d : Prop}

theorem And.elim (h₁ : a ∧ b) (h₂ : a → b → c) : c :=
And.rec h₂ h₁

theorem And.swap : a ∧ b → b ∧ a :=
assume ⟨ha, hb⟩, ⟨hb, ha⟩

def And.symm := @And.swap

theorem Or.elim (h₁ : a ∨ b) (h₂ : a → c) (h₃ : b → c) : c :=
Or.rec h₂ h₃ h₁

theorem Or.swap (h : a ∨ b) : b ∨ a :=
Or.elim h Or.inr Or.inl

def Or.symm := @Or.swap

/- xor -/
def Xor (a b : Prop) : Prop := (a ∧ ¬ b) ∨ (b ∧ ¬ a)

theorem Iff.elim (h₁ : (a → b) → (b → a) → c) (h₂ : a ↔ b) : c :=
Iff.rec h₁ h₂

theorem Iff.left : (a ↔ b) → a → b := Iff.mp

theorem Iff.right : (a ↔ b) → b → a := Iff.mpr

theorem iffIffImpliesAndImplies (a b : Prop) : (a ↔ b) ↔ (a → b) ∧ (b → a) :=
Iff.intro (λ h, And.intro h.mp h.mpr) (λ h, Iff.intro h.left h.right)

theorem Iff.refl (a : Prop) : a ↔ a :=
Iff.intro (assume h, h) (assume h, h)

theorem Iff.rfl {a : Prop} : a ↔ a :=
Iff.refl a

theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=
Iff.intro
  (assume ha, Iff.mp h₂ (Iff.mp h₁ ha))
  (assume hc, Iff.mpr h₁ (Iff.mpr h₂ hc))

theorem Iff.symm (h : a ↔ b) : b ↔ a :=
Iff.intro (Iff.right h) (Iff.left h)

theorem Iff.comm : (a ↔ b) ↔ (b ↔ a) :=
Iff.intro Iff.symm Iff.symm

theorem Eq.toIff {a b : Prop} (h : a = b) : a ↔ b :=
Eq.recOn h Iff.rfl

theorem neqOfNotIff {a b : Prop} : ¬(a ↔ b) → a ≠ b :=
λ h₁ h₂,
have a ↔ b, from Eq.subst h₂ (Iff.refl a),
absurd this h₁

theorem notIffNotOfIff (h₁ : a ↔ b) : ¬a ↔ ¬b :=
Iff.intro
 (assume (hna : ¬ a) (hb : b), hna (Iff.right h₁ hb))
 (assume (hnb : ¬ b) (ha : a), hnb (Iff.left h₁ ha))

theorem ofIffTrue (h : a ↔ True) : a :=
Iff.mp (Iff.symm h) trivial

theorem notOfIffFalse : (a ↔ False) → ¬a := Iff.mp

theorem iffTrueIntro (h : a) : a ↔ True :=
Iff.intro
  (λ hl, trivial)
  (λ hr, h)

theorem iffFalseIntro (h : ¬a) : a ↔ False :=
Iff.intro h (False.rec (λ _, a))

theorem notNotIntro (ha : a) : ¬¬a :=
assume hna : ¬a, hna ha

theorem notTrue : (¬ True) ↔ False :=
iffFalseIntro (notNotIntro trivial)

/- or resolution rulses -/

theorem resolveLeft {a b : Prop} (h : a ∨ b) (na : ¬ a) : b :=
Or.elim h (λ ha, absurd ha na) id

theorem negResolveLeft {a b : Prop} (h : ¬ a ∨ b) (ha : a) : b :=
Or.elim h (λ na, absurd ha na) id

theorem resolveRight {a b : Prop} (h : a ∨ b) (nb : ¬ b) : a :=
Or.elim h id (λ hb, absurd hb nb)

theorem negResolveRight {a b : Prop} (h : a ∨ ¬ b) (hb : b) : a :=
Or.elim h id (λ nb, absurd hb nb)

/- Exists -/

theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop}
   (h₁ : Exists (λ x, p x)) (h₂ : ∀ (a : α), p a → b) : b :=
Exists.rec h₂ h₁

/- Decidable -/

@[inlineIfReduce, nospecialize] def Decidable.decide (p : Prop) [h : Decidable p] : Bool :=
Decidable.casesOn h (λ h₁, false) (λ h₂, true)

export Decidable (isTrue isFalse decide)

instance beqOfEq {α : Type u} [DecidableEq α] : HasBeq α :=
⟨λ a b, decide (a = b)⟩

theorem decideTrueEqTrue (h : Decidable True) : @decide True h = true :=
Decidable.casesOn h (λ h, False.elim (Iff.mp notTrue h)) (λ _, rfl)

theorem decideFalseEqFalse (h : Decidable False) : @decide False h = false :=
Decidable.casesOn h (λ h, rfl) (λ h, False.elim h)

instance : Decidable True :=
isTrue trivial

instance : Decidable False :=
isFalse notFalse

-- We use "dependent" if-then-else to be able to communicate the if-then-else condition
-- to the branches
@[macroInline] def dite (c : Prop) [h : Decidable c] {α : Sort u} : (c → α) → (¬ c → α) → α :=
λ t e, Decidable.casesOn h e t

/- if-then-else -/

@[macroInline] def ite (c : Prop) [h : Decidable c] {α : Sort u} (t e : α) : α :=
Decidable.casesOn h (λ hnc, e) (λ hc, t)

namespace Decidable
variables {p q : Prop}

def recOnTrue [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : p) (h₄ : h₁ h₃)
    : (Decidable.recOn h h₂ h₁ : Sort u) :=
Decidable.casesOn h (λ h, False.rec _ (h h₃)) (λ h, h₄)

def recOnFalse [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : ¬p) (h₄ : h₂ h₃)
    : (Decidable.recOn h h₂ h₁ : Sort u) :=
Decidable.casesOn h (λ h, h₄) (λ h, False.rec _ (h₃ h))

@[macroInline] def byCases {q : Sort u} [s : Decidable p] (h1 : p → q) (h2 : ¬p → q) : q :=
match s with
| isTrue h  := h1 h
| isFalse h := h2 h

theorem em (p : Prop) [Decidable p] : p ∨ ¬p :=
byCases Or.inl Or.inr

theorem byContradiction [Decidable p] (h : ¬p → False) : p :=
byCases id (λ np : ¬p, False.elim (h np))

theorem ofNotNot [Decidable p] : ¬ ¬ p → p :=
λ hnn, byContradiction (λ hn, absurd hn hnn)

theorem notNotIff (p) [Decidable p] : (¬ ¬ p) ↔ p :=
Iff.intro ofNotNot notNotIntro

theorem notAndIffOrNot (p q : Prop) [d₁ : Decidable p] [d₂ : Decidable q] : ¬ (p ∧ q) ↔ ¬ p ∨ ¬ q :=
Iff.intro
(λ h, match d₁, d₂ with
      | isTrue h₁,  isTrue h₂  := absurd (And.intro h₁ h₂) h
      | _,           isFalse h₂ := Or.inr h₂
      | isFalse h₁, _           := Or.inl h₁)
(λ h ⟨hp, hq⟩, Or.elim h (λ h, h hp) (λ h, h hq))

end Decidable

section
variables {p q : Prop}
@[inline] def  decidableOfDecidableOfIff (hp : Decidable p) (h : p ↔ q) : Decidable q :=
if hp : p then isTrue (Iff.mp h hp)
else isFalse (Iff.mp (notIffNotOfIff h) hp)

@[inline] def  decidableOfDecidableOfEq (hp : Decidable p) (h : p = q) : Decidable q :=
decidableOfDecidableOfIff hp h.toIff
end

section
variables {p q : Prop}

@[macroInline] instance [Decidable p] [Decidable q] : Decidable (p ∧ q) :=
if hp : p then
  if hq : q then isTrue ⟨hp, hq⟩
  else isFalse (assume h : p ∧ q, hq (And.right h))
else isFalse (assume h : p ∧ q, hp (And.left h))

@[macroInline] instance [Decidable p] [Decidable q] : Decidable (p ∨ q) :=
if hp : p then isTrue (Or.inl hp) else
  if hq : q then isTrue (Or.inr hq) else
    isFalse (λ h, Or.elim h hp hq)

instance [Decidable p] : Decidable (¬p) :=
if hp : p then isFalse (absurd hp) else isTrue hp

@[macroInline] instance implies.Decidable [Decidable p] [Decidable q] : Decidable (p → q) :=
if hp : p then
  if hq : q then isTrue (assume h, hq)
  else isFalse (assume h : p → q, absurd (h hp) hq)
else isTrue (assume h, absurd h hp)

instance [Decidable p] [Decidable q] : Decidable (p ↔ q) :=
if hp : p then
  if hq : q then isTrue ⟨λ_, hq, λ_, hp⟩
  else isFalse $ λh, hq (h.1 hp)
else
  if hq : q then isFalse $ λh, hp (h.2 hq)
  else isTrue $ ⟨λh, absurd h hp, λh, absurd h hq⟩

instance [Decidable p] [Decidable q] : Decidable (Xor p q) :=
if hp : p then
  if hq : q then isFalse (λ h, Or.elim h (λ ⟨_, h⟩, h hq : ¬(p ∧ ¬ q)) (λ ⟨_, h⟩, h hp : ¬(q ∧ ¬ p)))
  else isTrue $ Or.inl ⟨hp, hq⟩
else
  if hq : q then isTrue $ Or.inr ⟨hq, hp⟩
  else isFalse (λ h, Or.elim h (λ ⟨h, _⟩, hp h : ¬(p ∧ ¬ q)) (λ ⟨h, _⟩, hq h : ¬(q ∧ ¬ p)))

end

@[inline] instance {α : Sort u} [DecidableEq α] (a b : α) : Decidable (a ≠ b) :=
match decEq a b with
| isTrue h := isFalse $ λ h', absurd h h'
| isFalse h := isTrue h

theorem Bool.falseNeTrue (h : false = true) : False :=
Bool.noConfusion h

instance : DecidableEq Bool :=
{decEq := λ a b, match a, b with
 | false, false := isTrue rfl
 | false, true  := isFalse Bool.falseNeTrue
 | true, false  := isFalse (Ne.symm Bool.falseNeTrue)
 | true, true   := isTrue rfl}

/- if-then-else expression theorems -/

theorem ifPos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t e : α} : (ite c t e) = t :=
match h with
| (isTrue  hc)  := rfl
| (isFalse hnc) := absurd hc hnc

theorem ifNeg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t e : α} : (ite c t e) = e :=
match h with
| (isTrue hc)   := absurd hc hnc
| (isFalse hnc) := rfl

-- Remark: dite and ite are "defally equal" when we ignore the proofs.
theorem difEqIf (c : Prop) [h : Decidable c] {α : Sort u} (t : α) (e : α) : dite c (λ h, t) (λ h, e) = ite c t e :=
match h with
| (isTrue hc)   := rfl
| (isFalse hnc) := rfl

instance {c t e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] : Decidable (if c then t else e)  :=
match dC with
| (isTrue hc)  := dT
| (isFalse hc) := dE

instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : ∀ h, Decidable (t h)] [dE : ∀ h, Decidable (e h)] : Decidable (if h : c then t h else e h)  :=
match dC with
| (isTrue hc)  := dT hc
| (isFalse hc) := dE hc

/-- Universe lifting operation -/
structure {r s} ULift (α : Type s) : Type (max s r) :=
up :: (down : α)

namespace ULift
/- Bijection between α and ULift.{v} α -/
theorem upDown {α : Type u} : ∀ (b : ULift.{v} α), up (down b) = b
| (up a) := rfl

theorem downUp {α : Type u} (a : α) : down (up.{v} a) = a := rfl
end ULift

/-- Universe lifting operation from Sort to Type -/
structure PLift (α : Sort u) : Type u :=
up :: (down : α)

namespace PLift
/- Bijection between α and PLift α -/
theorem upDown {α : Sort u} : ∀ (b : PLift α), up (down b) = b
| (up a) := rfl

theorem downUp {α : Sort u} (a : α) : down (up a) = a := rfl
end PLift

/- pointed types -/
structure PointedType :=
(type : Type u) (val : type)

/- Inhabited -/

class Inhabited (α : Sort u) :=
(default : α)

constant default (α : Sort u) [Inhabited α] : α :=
Inhabited.default α

@[inline, irreducible] def arbitrary (α : Sort u) [Inhabited α] : α :=
default α

instance Prop.Inhabited : Inhabited Prop :=
⟨True⟩

instance Fun.Inhabited (α : Sort u) {β : Sort v} [h : Inhabited β] : Inhabited (α → β) :=
Inhabited.casesOn h (λ b, ⟨λ a, b⟩)

instance Pi.Inhabited (α : Sort u) {β : α → Sort v} [Π x, Inhabited (β x)] : Inhabited (Π x, β x) :=
⟨λ a, default (β a)⟩

instance : Inhabited Bool := ⟨false⟩

instance : Inhabited True := ⟨trivial⟩

instance : Inhabited Nat := ⟨0⟩

instance : Inhabited NonScalar := ⟨⟨default _⟩⟩

instance : Inhabited PointedType := ⟨{type := PUnit, val := ⟨⟩}⟩

class inductive Nonempty (α : Sort u) : Prop
| intro (val : α) : Nonempty

protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p :=
Nonempty.rec h₂ h₁

instance nonemptyOfInhabited {α : Sort u} [Inhabited α] : Nonempty α :=
⟨default α⟩

theorem nonemptyOfExists {α : Sort u} {p : α → Prop} : Exists (λ x, p x) → Nonempty α
| ⟨w, h⟩ := ⟨w⟩

/- Subsingleton -/

class inductive Subsingleton (α : Sort u) : Prop
| intro (h : ∀ a b : α, a = b) : Subsingleton

protected def Subsingleton.elim {α : Sort u} [h : Subsingleton α] : ∀ (a b : α), a = b :=
Subsingleton.casesOn h (λ p, p)

protected def Subsingleton.helim {α β : Sort u} [h : Subsingleton α] (h : α = β) : ∀ (a : α) (b : β), a ≅ b :=
Eq.recOn h (λ a b : α, heqOfEq (Subsingleton.elim a b))

instance subsingletonProp (p : Prop) : Subsingleton p :=
⟨λ a b, proofIrrel a b⟩

instance (p : Prop) : Subsingleton (Decidable p) :=
Subsingleton.intro (λ d₁,
  match d₁ with
  | (isTrue t₁) := (λ d₂,
    match d₂ with
    | (isTrue t₂) := Eq.recOn (proofIrrel t₁ t₂) rfl
    | (isFalse f₂) := absurd t₁ f₂)
  | (isFalse f₁) := (λ d₂,
    match d₂ with
    | (isTrue t₂) := absurd t₂ f₁
    | (isFalse f₂) := Eq.recOn (proofIrrel f₁ f₂) rfl))

protected theorem recSubsingleton {p : Prop} [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u}
                                 [h₃ : Π (h : p), Subsingleton (h₁ h)] [h₄ : Π (h : ¬p), Subsingleton (h₂ h)]
                                 : Subsingleton (Decidable.casesOn h h₂ h₁) :=
match h with
| (isTrue h)  := h₃ h
| (isFalse h) := h₄ h

section relation
variables {α : Sort u} {β : Sort v} (r : β → β → Prop)

def Reflexive := ∀ x, r x x

def Symmetric := ∀ {x y}, r x y → r y x

def Transitive := ∀ {x y z}, r x y → r y z → r x z

def Equivalence := Reflexive r ∧ Symmetric r ∧ Transitive r

def Total := ∀ x y, r x y ∨ r y x

def mkEquivalence (rfl : Reflexive r) (symm : Symmetric r) (trans : Transitive r) : Equivalence r :=
⟨rfl, @symm, @trans⟩

def Irreflexive := ∀ x, ¬ r x x

def AntiSymmetric := ∀ {x y}, r x y → r y x → x = y

def emptyRelation := λ a₁ a₂ : α, False

def Subrelation (q r : β → β → Prop) := ∀ {x y}, q x y → r x y

def InvImage (f : α → β) : α → α → Prop :=
λ a₁ a₂, r (f a₁) (f a₂)

theorem InvImage.Transitive (f : α → β) (h : Transitive r) : Transitive (InvImage r f) :=
λ (a₁ a₂ a₃ : α) (h₁ : InvImage r f a₁ a₂) (h₂ : InvImage r f a₂ a₃), h h₁ h₂

theorem InvImage.Irreflexive (f : α → β) (h : Irreflexive r) : Irreflexive (InvImage r f) :=
λ (a : α) (h₁ : InvImage r f a a), h (f a) h₁

inductive TC {α : Sort u} (r : α → α → Prop) : α → α → Prop
| base  : ∀ a b, r a b → TC a b
| trans : ∀ a b c, TC a b → TC b c → TC a c

@[elabAsEliminator]
theorem {u1 u2} TC.ndrec {α : Sort u} {r : α → α → Prop} {C : α → α → Prop}
                (m₁ : ∀ (a b : α), r a b → C a b)
                (m₂ : ∀ (a b c : α), TC r a b → TC r b c → C a b → C b c → C a c)
                {a b : α} (h : TC r a b) : C a b :=
@TC.rec α r (λ a b _, C a b) m₁ m₂ a b h

@[elabAsEliminator]
theorem {u1 u2} TC.ndrecOn {α : Sort u} {r : α → α → Prop} {C : α → α → Prop}
                {a b : α} (h : TC r a b)
                (m₁ : ∀ (a b : α), r a b → C a b)
                (m₂ : ∀ (a b c : α), TC r a b → TC r b c → C a b → C b c → C a c)
                : C a b :=
@TC.rec α r (λ a b _, C a b) m₁ m₂ a b h

end relation

section Binary
variables {α : Type u} {β : Type v}
variable f : α → α → α

def Commutative        := ∀ a b, f a b = f b a
def Associative        := ∀ a b c, f (f a b) c = f a (f b c)
def RightCommutative (h : β → α → β) := ∀ b a₁ a₂, h (h b a₁) a₂ = h (h b a₂) a₁
def LeftCommutative  (h : α → β → β) := ∀ a₁ a₂ b, h a₁ (h a₂ b) = h a₂ (h a₁ b)

theorem leftComm : Commutative f → Associative f → LeftCommutative f :=
assume hcomm hassoc, assume a b c,
((Eq.symm (hassoc a b c)).trans (hcomm a b ▸ rfl : f (f a b) c = f (f b a) c)).trans (hassoc b a c)

theorem rightComm : Commutative f → Associative f → RightCommutative f :=
assume hcomm hassoc, assume a b c,
((hassoc a b c).trans (hcomm b c ▸ rfl : f a (f b c) = f a (f c b))).trans (Eq.symm (hassoc a c b))

end Binary

/- Subtype -/

namespace Subtype
def existsOfSubtype {α : Type u} {p : α → Prop} : { x // p x } → Exists (λ x, p x)
| ⟨a, h⟩ := ⟨a, h⟩

variables {α : Type u} {p : α → Prop}

theorem tagIrrelevant {a : α} (h1 h2 : p a) : mk a h1 = mk a h2 :=
rfl

protected theorem eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
| ⟨x, h1⟩ ⟨.(x), h2⟩ rfl := rfl

theorem eta (a : {x // p x}) (h : p (val a)) : mk (val a) h = a :=
Subtype.eq rfl

instance {α : Type u} {p : α → Prop} {a : α} (h : p a) : Inhabited {x // p x} :=
⟨⟨a, h⟩⟩

instance {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
{decEq := λ ⟨a, h₁⟩ ⟨b, h₂⟩,
  if h : a = b then isTrue (Subtype.eq h)
  else isFalse (λ h', Subtype.noConfusion h' (λ h', absurd h' h))}
end Subtype

/- Sum -/

infixr ⊕ := Sum

section
variables {α : Type u} {β : Type v}

instance Sum.inhabitedLeft [h : Inhabited α] : Inhabited (α ⊕ β) :=
⟨Sum.inl (default α)⟩

instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (α ⊕ β) :=
⟨Sum.inr (default β)⟩

instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (α ⊕ β) :=
{decEq := λ a b,
 match a, b with
 | (Sum.inl a), (Sum.inl b) := if h : a = b then isTrue (h ▸ rfl)
                               else isFalse (λ h', Sum.noConfusion h' (λ h', absurd h' h))
 | (Sum.inr a), (Sum.inr b) := if h : a = b then isTrue (h ▸ rfl)
                               else isFalse (λ h', Sum.noConfusion h' (λ h', absurd h' h))
 | (Sum.inr a), (Sum.inl b) := isFalse (λ h, Sum.noConfusion h)
 | (Sum.inl a), (Sum.inr b) := isFalse (λ h, Sum.noConfusion h)}
end

/- Product -/

section
variables {α : Type u} {β : Type v}

instance [Inhabited α] [Inhabited β] : Inhabited (Prod α β) :=
⟨(default α, default β)⟩

instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
{decEq := λ ⟨a, b⟩ ⟨a', b'⟩,
  match (decEq a a') with
  | (isTrue e₁) :=
    (match (decEq b b') with
     | (isTrue e₂)  := isTrue (Eq.recOn e₁ (Eq.recOn e₂ rfl))
     | (isFalse n₂) := isFalse (assume h, Prod.noConfusion h (λ e₁' e₂', absurd e₂' n₂)))
  | (isFalse n₁) := isFalse (assume h, Prod.noConfusion h (λ e₁' e₂', absurd e₁' n₁))}

instance [HasLess α] [HasLess β] : HasLess (α × β) :=
⟨λ s t, s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)⟩

instance prodHasDecidableLt
         [HasLess α] [HasLess β] [DecidableEq α] [DecidableEq β]
         [Π a b : α, Decidable (a < b)] [Π a b : β, Decidable (a < b)]
         : Π s t : α × β, Decidable (s < t) :=
λ t s, Or.Decidable

theorem Prod.ltDef [HasLess α] [HasLess β] (s t : α × β) : (s < t) = (s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)) :=
rfl
end

def {u₁ u₂ v₁ v₂} Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂}
  (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
| (a, b) := (f a, g b)

/- Dependent products -/

-- notation `Σ` binders `, ` r:(scoped p, Sigma p) := r
-- notation `Σ'` binders `, ` r:(scoped p, PSigma p) := r

theorem exOfPsig {α : Type u} {p : α → Prop} : (PSigma (λ x, p x)) → Exists (λ x, p x)
| ⟨x, hx⟩ := ⟨x, hx⟩

section
variables {α : Type u} {β : α → Type v}

protected theorem Sigma.eq : ∀ {p₁ p₂ : Sigma (λ a : α, β a)} (h₁ : p₁.1 = p₂.1), (Eq.recOn h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂
| ⟨a, b⟩ ⟨.(a), .(b)⟩ rfl rfl := rfl
end

section
variables {α : Sort u} {β : α → Sort v}

protected theorem PSigma.eq : ∀ {p₁ p₂ : PSigma β} (h₁ : p₁.1 = p₂.1), (Eq.recOn h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂
| ⟨a, b⟩ ⟨.(a), .(b)⟩ rfl rfl := rfl
end

/- Universe polymorphic unit -/

theorem punitEq (a b : PUnit) : a = b :=
PUnit.recOn a (PUnit.recOn b rfl)

theorem punitEqPUnit (a : PUnit) : a = () :=
punitEq a ()

instance : Subsingleton PUnit :=
Subsingleton.intro punitEq

instance : Inhabited PUnit :=
⟨⟨⟩⟩

instance : DecidableEq PUnit :=
{decEq := λ a b, isTrue (punitEq a b)}

/- Setoid -/

class Setoid (α : Sort u) :=
(r : α → α → Prop) (iseqv : Equivalence r)

instance setoidHasEquiv {α : Sort u} [Setoid α] : HasEquiv α :=
⟨Setoid.r⟩

namespace Setoid
variables {α : Sort u} [Setoid α]

theorem refl (a : α) : a ≈ a :=
match Setoid.iseqv α with
| ⟨hRefl, hSymm, hTrans⟩ := hRefl a

theorem symm {a b : α} (hab : a ≈ b) : b ≈ a :=
match Setoid.iseqv α with
| ⟨hRefl, hSymm, hTrans⟩ := hSymm hab

theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c :=
match Setoid.iseqv α with
| ⟨hRefl, hSymm, hTrans⟩ := hTrans hab hbc
end Setoid

/- Propositional extensionality -/

axiom propext {a b : Prop} : (a ↔ b) → a = b

theorem eqTrueIntro {a : Prop} (h : a) : a = True :=
propext (iffTrueIntro h)

theorem eqFalseIntro {a : Prop} (h : ¬a) : a = False :=
propext (iffFalseIntro h)

/- Quotients -/

-- Iff can now be used to do substitutions in a calculation
theorem iffSubst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) : p b :=
Eq.subst (propext h₁) h₂

namespace Quot
axiom sound : Π {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r b

attribute [elabAsEliminator] lift ind

protected theorem liftBeta {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) (c : ∀ a b, r a b → f a = f b) (a : α) : lift f c (Quot.mk r a) = f a :=
rfl

protected theorem indBeta {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} (p : ∀ a, β (Quot.mk r a)) (a : α) : (ind p (Quot.mk r a) : β (Quot.mk r a)) = p a :=
rfl

@[reducible, elabAsEliminator, inline]
protected def liftOn {α : Sort u} {β : Sort v} {r : α → α → Prop} (q : Quot r) (f : α → β) (c : ∀ a b, r a b → f a = f b) : β :=
lift f c q

@[elabAsEliminator]
protected theorem inductionOn {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} (q : Quot r) (h : ∀ a, β (Quot.mk r a)) : β q :=
ind h q

theorem existsRep {α : Sort u} {r : α → α → Prop} (q : Quot r) : Exists (λ a : α, (Quot.mk r a) = q) :=
Quot.inductionOn q (λ a, ⟨a, rfl⟩)

section
variable {α : Sort u}
variable {r : α → α → Prop}
variable {β : Quot r → Sort v}

@[reducible, macroInline]
protected def indep (f : Π a, β (Quot.mk r a)) (a : α) : PSigma β :=
⟨Quot.mk r a, f a⟩

protected theorem indepCoherent (f : Π a, β (Quot.mk r a))
                     (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β (Quot.mk r b)) = f b)
                     : ∀ a b, r a b → Quot.indep f a = Quot.indep f b  :=
λ a b e, PSigma.eq (sound e) (h a b e)

protected theorem liftIndepPr1
  (f : Π a, β (Quot.mk r a)) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β (Quot.mk r b)) = f b)
  (q : Quot r) : (lift (Quot.indep f) (Quot.indepCoherent f h) q).1 = q  :=
Quot.ind (λ (a : α), Eq.refl (Quot.indep f a).1) q

@[reducible, elabAsEliminator, inline]
protected def rec
   (f : Π a, β (Quot.mk r a)) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β (Quot.mk r b)) = f b)
   (q : Quot r) : β q :=
Eq.ndrecOn (Quot.liftIndepPr1 f h q) ((lift (Quot.indep f) (Quot.indepCoherent f h) q).2)

@[reducible, elabAsEliminator, inline]
protected def recOn
   (q : Quot r) (f : Π a, β (Quot.mk r a)) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β (Quot.mk r b)) = f b) : β q :=
Quot.rec f h q

@[reducible, elabAsEliminator, inline]
protected def recOnSubsingleton
   [h : ∀ a, Subsingleton (β (Quot.mk r a))] (q : Quot r) (f : Π a, β (Quot.mk r a)) : β q :=
Quot.rec f (λ a b h, Subsingleton.elim _ (f b)) q

@[reducible, elabAsEliminator, inline]
protected def hrecOn
   (q : Quot r) (f : Π a, β (Quot.mk r a)) (c : ∀ (a b : α) (p : r a b), f a ≅ f b) : β q :=
Quot.recOn q f $
  λ a b p, eqOfHeq $
    have p₁ : (Eq.rec (f a) (sound p) : β (Quot.mk r b)) ≅ f a, from eqRecHeq (sound p) (f a),
    Heq.trans p₁ (c a b p)

end
end Quot

def Quotient {α : Sort u} (s : Setoid α) :=
@Quot α Setoid.r

namespace Quotient

@[inline]
protected def mk {α : Sort u} [s : Setoid α] (a : α) : Quotient s :=
Quot.mk Setoid.r a

notation `⟦`:max a `⟧`:0 := Quotient.mk a

def sound {α : Sort u} [s : Setoid α] {a b : α} : a ≈ b → ⟦a⟧ = ⟦b⟧ :=
Quot.sound

@[reducible, elabAsEliminator]
protected def lift {α : Sort u} {β : Sort v} [s : Setoid α] (f : α → β) : (∀ a b, a ≈ b → f a = f b) → Quotient s → β :=
Quot.lift f

@[elabAsEliminator]
protected theorem ind {α : Sort u} [s : Setoid α] {β : Quotient s → Prop} : (∀ a, β ⟦a⟧) → ∀ q, β q :=
Quot.ind

@[reducible, elabAsEliminator, inline]
protected def liftOn {α : Sort u} {β : Sort v} [s : Setoid α] (q : Quotient s) (f : α → β) (c : ∀ a b, a ≈ b → f a = f b) : β :=
Quot.liftOn q f c

@[elabAsEliminator]
protected theorem inductionOn {α : Sort u} [s : Setoid α] {β : Quotient s → Prop} (q : Quotient s) (h : ∀ a, β ⟦a⟧) : β q :=
Quot.inductionOn q h

theorem existsRep {α : Sort u} [s : Setoid α] (q : Quotient s) : Exists (λ a : α, ⟦a⟧ = q) :=
Quot.existsRep q

section
variable {α : Sort u}
variable [s : Setoid α]
variable {β : Quotient s → Sort v}

@[inline]
protected def rec
   (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : a ≈ b), (Eq.rec (f a) (Quotient.sound p) : β ⟦b⟧) = f b)
   (q : Quotient s) : β q :=
Quot.rec f h q

@[reducible, elabAsEliminator, inline]
protected def recOn
   (q : Quotient s) (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : a ≈ b), (Eq.rec (f a) (Quotient.sound p) : β ⟦b⟧) = f b) : β q :=
Quot.recOn q f h

@[reducible, elabAsEliminator, inline]
protected def recOnSubsingleton
   [h : ∀ a, Subsingleton (β ⟦a⟧)] (q : Quotient s) (f : Π a, β ⟦a⟧) : β q :=
@Quot.recOnSubsingleton _ _ _ h q f

@[reducible, elabAsEliminator, inline]
protected def hrecOn
   (q : Quotient s) (f : Π a, β ⟦a⟧) (c : ∀ (a b : α) (p : a ≈ b), f a ≅ f b) : β q :=
Quot.hrecOn q f c
end

section
universes uA uB uC
variables {α : Sort uA} {β : Sort uB} {φ : Sort uC}
variables [s₁ : Setoid α] [s₂ : Setoid β]
include s₁ s₂

@[reducible, elabAsEliminator, inline]
protected def lift₂
   (f : α → β → φ)(c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂)
   (q₁ : Quotient s₁) (q₂ : Quotient s₂) : φ :=
Quotient.lift
  (λ (a₁ : α), Quotient.lift (f a₁) (λ (a b : β), c a₁ a a₁ b (Setoid.refl a₁)) q₂)
  (λ (a b : α) (h : a ≈ b),
     @Quotient.ind β s₂
       (λ (a1 : Quotient s₂),
          (Quotient.lift (f a) (λ (a1 b : β), c a a1 a b (Setoid.refl a)) a1)
          =
          (Quotient.lift (f b) (λ (a b1 : β), c b a b b1 (Setoid.refl b)) a1))
       (λ (a' : β), c a a' b a' h (Setoid.refl a'))
       q₂)
  q₁

@[reducible, elabAsEliminator, inline]
protected def liftOn₂
  (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : α → β → φ) (c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) : φ :=
Quotient.lift₂ f c q₁ q₂

@[elabAsEliminator]
protected theorem ind₂ {φ : Quotient s₁ → Quotient s₂ → Prop} (h : ∀ a b, φ ⟦a⟧ ⟦b⟧) (q₁ : Quotient s₁) (q₂ : Quotient s₂) : φ q₁ q₂ :=
Quotient.ind (λ a₁, Quotient.ind (λ a₂, h a₁ a₂) q₂) q₁

@[elabAsEliminator]
protected theorem inductionOn₂
   {φ : Quotient s₁ → Quotient s₂ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (h : ∀ a b, φ ⟦a⟧ ⟦b⟧) : φ q₁ q₂ :=
Quotient.ind (λ a₁, Quotient.ind (λ a₂, h a₁ a₂) q₂) q₁

@[elabAsEliminator]
protected theorem inductionOn₃
   [s₃ : Setoid φ]
   {δ : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (q₃ : Quotient s₃) (h : ∀ a b c, δ ⟦a⟧ ⟦b⟧ ⟦c⟧)
   : δ q₁ q₂ q₃ :=
Quotient.ind (λ a₁, Quotient.ind (λ a₂, Quotient.ind (λ a₃, h a₁ a₂ a₃) q₃) q₂) q₁
end

section Exact
variable   {α : Sort u}
variable   [s : Setoid α]
include s

private def rel (q₁ q₂ : Quotient s) : Prop :=
Quotient.liftOn₂ q₁ q₂
  (λ a₁ a₂, a₁ ≈ a₂)
  (λ a₁ a₂ b₁ b₂ a₁b₁ a₂b₂,
    propext (Iff.intro
      (λ a₁a₂, Setoid.trans (Setoid.symm a₁b₁) (Setoid.trans a₁a₂ a₂b₂))
      (λ b₁b₂, Setoid.trans a₁b₁ (Setoid.trans b₁b₂ (Setoid.symm a₂b₂)))))

private theorem rel.refl : ∀ q : Quotient s, rel q q :=
λ q, Quot.inductionOn q (λ a, Setoid.refl a)

private theorem eqImpRel {q₁ q₂ : Quotient s} : q₁ = q₂ → rel q₁ q₂ :=
assume h, Eq.ndrecOn h (rel.refl q₁)

theorem exact {a b : α} : ⟦a⟧ = ⟦b⟧ → a ≈ b :=
assume h, eqImpRel h
end Exact

section
universes uA uB uC
variables {α : Sort uA} {β : Sort uB}
variables [s₁ : Setoid α] [s₂ : Setoid β]
include s₁ s₂

@[reducible, elabAsEliminator]
protected def recOnSubsingleton₂
   {φ : Quotient s₁ → Quotient s₂ → Sort uC} [h : ∀ a b, Subsingleton (φ ⟦a⟧ ⟦b⟧)]
   (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : Π a b, φ ⟦a⟧ ⟦b⟧) : φ q₁ q₂:=
@Quotient.recOnSubsingleton _ s₁ (λ q, φ q q₂) (λ a, Quotient.ind (λ b, h a b) q₂) q₁
  (λ a, Quotient.recOnSubsingleton q₂ (λ b, f a b))

end
end Quotient

section
variable {α : Type u}
variable (r : α → α → Prop)

inductive EqvGen : α → α → Prop
| rel {} : Π x y, r x y → EqvGen x y
| refl {} : Π x, EqvGen x x
| symm {} : Π x y, EqvGen x y → EqvGen y x
| trans {} : Π x y z, EqvGen x y → EqvGen y z → EqvGen x z

theorem EqvGen.isEquivalence : Equivalence (@EqvGen α r) :=
mkEquivalence _ EqvGen.refl EqvGen.symm EqvGen.trans

def EqvGen.Setoid : Setoid α :=
Setoid.mk _ (EqvGen.isEquivalence r)

theorem Quot.exact {a b : α} (H : Quot.mk r a = Quot.mk r b) : EqvGen r a b :=
@Quotient.exact _ (EqvGen.Setoid r) a b (@congrArg _ _ _ _
  (Quot.lift (@Quotient.mk _ (EqvGen.Setoid r)) (λx y h, Quot.sound (EqvGen.rel x y h))) H)

theorem Quot.eqvGenSound {r : α → α → Prop} {a b : α} (H : EqvGen r a b) : Quot.mk r a = Quot.mk r b :=
EqvGen.recOn H
  (λ x y h, Quot.sound h)
  (λ x, rfl)
  (λ x y _ IH, Eq.symm IH)
  (λ x y z _ _ IH₁ IH₂, Eq.trans IH₁ IH₂)
end

instance {α : Sort u} {s : Setoid α} [d : ∀ a b : α, Decidable (a ≈ b)] : DecidableEq (Quotient s) :=
{decEq := λ q₁ q₂ : Quotient s,
  Quotient.recOnSubsingleton₂ q₁ q₂
    (λ a₁ a₂,
      match (d a₁ a₂) with
      | (isTrue h₁)  := isTrue (Quotient.sound h₁)
      | (isFalse h₂) := isFalse (λ h, absurd (Quotient.exact h) h₂))}

/- Function extensionality -/

namespace Function
variables {α : Sort u} {β : α → Sort v}

def Equiv (f₁ f₂ : Π x : α, β x) : Prop := ∀ x, f₁ x = f₂ x

protected theorem Equiv.refl (f : Π x : α, β x) : Equiv f f := assume x, rfl

protected theorem Equiv.symm {f₁ f₂ : Π x: α, β x} : Equiv f₁ f₂ → Equiv f₂ f₁ :=
λ h x, Eq.symm (h x)

protected theorem Equiv.trans {f₁ f₂ f₃ : Π x: α, β x} : Equiv f₁ f₂ → Equiv f₂ f₃ → Equiv f₁ f₃ :=
λ h₁ h₂ x, Eq.trans (h₁ x) (h₂ x)

protected theorem Equiv.isEquivalence (α : Sort u) (β : α → Sort v) : Equivalence (@Function.Equiv α β) :=
mkEquivalence (@Function.Equiv α β) (@Equiv.refl α β) (@Equiv.symm α β) (@Equiv.trans α β)
end Function

section
open Quotient
variables {α : Sort u} {β : α → Sort v}

@[instance]
private def funSetoid (α : Sort u) (β : α → Sort v) : Setoid (Π x : α, β x) :=
Setoid.mk (@Function.Equiv α β) (Function.Equiv.isEquivalence α β)

private def extfunApp (f : Quotient $ funSetoid α β) : Π x : α, β x :=
assume x,
Quot.liftOn f
  (λ f : Π x : α, β x, f x)
  (λ f₁ f₂ h, h x)

theorem funext {f₁ f₂ : Π x : α, β x} (h : ∀ x, f₁ x = f₂ x) : f₁ = f₂ :=
show extfunApp ⟦f₁⟧ = extfunApp ⟦f₂⟧, from
congrArg extfunApp (sound h)
end

instance Pi.Subsingleton {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] : Subsingleton (Π a, β a) :=
⟨λ f₁ f₂, funext (λ a, Subsingleton.elim (f₁ a) (f₂ a))⟩

/- General operations on functions -/
namespace Function
universes u₁ u₂ u₃ u₄
variables {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} {ζ : Sort u₁}

@[inline, reducible] def comp (f : β → φ) (g : α → β) : α → φ :=
λ x, f (g x)

infixr  ` ∘ `      := Function.comp

@[inline, reducible] def onFun (f : β → β → φ) (g : α → β) : α → α → φ :=
λ x y, f (g x) (g y)

@[inline, reducible] def combine (f : α → β → φ) (op : φ → δ → ζ) (g : α → β → δ)
  : α → β → ζ :=
λ x y, op (f x y) (g x y)

@[inline, reducible] def const (β : Sort u₂) (a : α) : β → α :=
λ x, a

@[inline, reducible] def swap {φ : α → β → Sort u₃} (f : Π x y, φ x y) : Π y x, φ x y :=
λ y x, f x y

infixl  ` on `:2         := onFun
notation f ` -[` op `]- ` g  := combine f op g

end Function

/- Classical reasoning support -/

namespace Classical

axiom choice {α : Sort u} : Nonempty α → α

noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop)
  (h : Exists (λ x, p x)) : {x // p x} :=
choice $ let ⟨x, px⟩ := h in ⟨⟨x, px⟩⟩

noncomputable def choose {α : Sort u} {p : α → Prop} (h : Exists (λ x, p x)) : α :=
(indefiniteDescription p h).val

theorem chooseSpec {α : Sort u} {p : α → Prop} (h : Exists (λ x, p x)) : p (choose h) :=
(indefiniteDescription p h).property

/- Diaconescu's theorem: excluded middle from choice, Function extensionality and propositional extensionality. -/
theorem em (p : Prop) : p ∨ ¬p :=
let U (x : Prop) : Prop := x = True ∨ p in
let V (x : Prop) : Prop := x = False ∨ p in
have exU : Exists (λ x, U x), from ⟨True, Or.inl rfl⟩,
have exV : Exists (λ x, V x), from ⟨False, Or.inl rfl⟩,
let u : Prop := choose exU in
let v : Prop := choose exV in
have uDef : U u, from chooseSpec exU,
have vDef : V v, from chooseSpec exV,
have notUvOrP : u ≠ v ∨ p, from
  Or.elim uDef
    (assume hut : u = True,
      Or.elim vDef
        (assume hvf : v = False,
          have hne : u ≠ v, from hvf.symm ▸ hut.symm ▸ trueNeFalse,
          Or.inl hne)
        Or.inr)
    Or.inr,
have pImpliesUv : p → u = v, from
  assume hp : p,
  have hpred : U = V, from
    funext $ assume x : Prop,
      have hl : (x = True ∨ p) → (x = False ∨ p), from
        assume a, Or.inr hp,
      have hr : (x = False ∨ p) → (x = True ∨ p), from
        assume a, Or.inr hp,
      show (x = True ∨ p) = (x = False ∨ p), from
        propext (Iff.intro hl hr),
  have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV, from
    hpred ▸ λ exU exV, rfl,
  show u = v, from h₀ _ _,
Or.elim notUvOrP
  (assume hne : u ≠ v, Or.inr (mt pImpliesUv hne))
  Or.inl

theorem existsTrueOfNonempty {α : Sort u} : Nonempty α → Exists (λ x : α, True)
| ⟨x⟩ := ⟨x, trivial⟩

noncomputable def inhabitedOfNonempty {α : Sort u} (h : Nonempty α) : Inhabited α :=
⟨choice h⟩

noncomputable def inhabitedOfExists {α : Sort u} {p : α → Prop} (h : Exists (λ x, p x)) :
  Inhabited α :=
inhabitedOfNonempty (Exists.elim h (λ w hw, ⟨w⟩))

/- all propositions are Decidable -/
noncomputable def propDecidable (a : Prop) : Decidable a :=
choice $ Or.elim (em a)
  (assume ha, ⟨isTrue ha⟩)
  (assume hna, ⟨isFalse hna⟩)
local attribute [instance] propDecidable

noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) :=
⟨propDecidable a⟩
local attribute [instance] decidableInhabited

noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
{decEq := λ x y, propDecidable (x = y)}

noncomputable def typeDecidable (α : Sort u) : PSum α (α → False) :=
match (propDecidable (Nonempty α)) with
| (isTrue hp)  := PSum.inl (@Inhabited.default _ (inhabitedOfNonempty hp))
| (isFalse hn) := PSum.inr (λ a, absurd (Nonempty.intro a) hn)

noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop)
  (h : Nonempty α) : {x : α // Exists (λ y : α, p y) → p x} :=
if hp : Exists (λ x : α, p x) then
  let xp := indefiniteDescription _ hp in
  ⟨xp.val, λ h', xp.property⟩
else ⟨choice h, λ h, absurd h hp⟩

/- the Hilbert epsilon Function -/

noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α :=
(strongIndefiniteDescription p h).val

theorem epsilonSpecAux {α : Sort u} (h : Nonempty α) (p : α → Prop)
  : Exists (λ y, p y) → p (@epsilon α h p) :=
(strongIndefiniteDescription p h).property

theorem epsilonSpec {α : Sort u} {p : α → Prop} (hex : Exists (λ y, p y)) :
    p (@epsilon α (nonemptyOfExists hex) p) :=
epsilonSpecAux (nonemptyOfExists hex) p hex

theorem epsilonSingleton {α : Sort u} (x : α) : @epsilon α ⟨x⟩ (λ y, y = x) = x :=
@epsilonSpec α (λ y, y = x) ⟨x, rfl⟩

/- the axiom of choice -/

theorem axiomOfChoice {α : Sort u} {β : α → Sort v} {r : Π x, β x → Prop} (h : ∀ x, Exists (λ y, r x y)) :
  Exists (λ (f : Π x, β x), ∀ x, r x (f x)) :=
⟨_, λ x, chooseSpec (h x)⟩

theorem skolem {α : Sort u} {b : α → Sort v} {p : Π x, b x → Prop} :
  (∀ x, Exists (λ y, p x y)) ↔ Exists (λ (f : Π x, b x), ∀ x, p x (f x)) :=
⟨axiomOfChoice, λ ⟨f, hw⟩ x, ⟨f x, hw x⟩⟩

theorem propComplete (a : Prop) : a = True ∨ a = False :=
Or.elim (em a)
  (λ t, Or.inl (eqTrueIntro t))
  (λ f, Or.inr (eqFalseIntro f))

-- this supercedes byCases in Decidable
theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
Decidable.byCases hpq hnpq

-- this supercedes byContradiction in Decidable
theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
Decidable.byContradiction h

end Classical