/-
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 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
reserve infixl `; `:1

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
lemmas 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 lemmas. The equation Compiler uses it as a marker. -/
@[macroInline] abbrev idRhs (α : Sort u) (a : α) : α := a

inductive Punit : Sort u
| star : 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.star : Unit := Punit.star

/- 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(#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)

def And.elimLeft {a b : Prop} (h : And a b) : a := h.1

def And.elimRight {a b : Prop} (h : And a b) : b := h.2

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

attribute [ppAnonymousCtor] Sigma Psigma Subtype Pprod And

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
notation `[` l:(foldr `, ` (h t, List.cons h t) List.nil `]`) := l

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 HasDvd      (α : Type u) := (dvd : α → α → Prop)
class HasMod      (α : Type u) := (mod : α → α → α)
class HasModn     (α : Type u) := (modn : α → Nat → α)
class HasLe       (α : Type u) := (le : α → α → Prop)
class HasLt       (α : Type u) := (lt : α → α → Prop)
class HasBeq      (α : Type u) := (beq : α → α → Bool)
class HasAppend   (α : Type u) := (append : α → α → α)
class HasAndthen  (α : Type u) (β : Type v) (σ : outParam $ Type w) := (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 ∣        := HasDvd.dvd
infix %        := HasMod.mod
infix %ₙ       := HasModn.modn
prefix -       := HasNeg.neg
infix <=       := HasLe.le
infix ≤        := HasLe.le
infix <        := HasLt.lt
infix ==       := HasBeq.beq
infix ++       := HasAppend.append
infix ;        := andthen
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

export HasAppend (append)

@[reducible] def ge {α : Type u} [HasLe α] (a b : α) : Prop := HasLe.le b a
@[reducible] def gt {α : Type u} [HasLt α] (a b : α) : Prop := HasLt.lt b a

infix >=       := ge
infix ≥        := ge
infix >        := gt

@[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⟩

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

/- sizeof -/

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

export HasSizeof (sizeof)

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

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

/- Combinator calculus -/
namespace Combinator
universes u₁ u₂ u₃
def I {α : Type u₁} (a : α) := a
def K {α : Type u₁} {β : Type u₂} (a : α) (b : β) := a
def S {α : Type u₁} {β : Type u₂} {γ : Type u₃} (x : α → β → γ) (y : α → β) (z : α) := x z (y z)
end Combinator

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

/-- Auxiliary datatype for #[ ... ] notation.
    #[1, 2, 3, 4] is notation for

    BinTree.Node
      (BinTree.Node (BinTree.leaf 1) (BinTree.leaf 2))
      (BinTree.Node (BinTree.leaf 3) (BinTree.leaf 4))

    We use this notation to input long sequences without exhausting the System stack space.
    Later, we define a coercion from `BinTree` into `List`.
-/
inductive BinTree (α : Type u)
| Empty {}       : BinTree
| leaf (val : α) : BinTree
| Node (left right : BinTree) : BinTree

attribute [elabSimple] BinTree.Node BinTree.leaf

/-- 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 bor : Bool → Bool → Bool
| true  _  := true
| false b  := b

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

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

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

prefix ! := bnot
infix || := bor
infix && := band

/- 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 not.intro {a : Prop} (h : a → False) : ¬ a := h

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 eqFfOfNeTt : ∀ {b : Bool}, b ≠ true → b = false
| true h := False.elim (h rfl)
| false h := rfl

theorem eqTtOfNeFf : ∀ {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 heqOfEqRecLeft {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a = a') (h₂ : (Eq.recOn e p₁ : φ a') = p₂), p₁ ≅ p₂
| a _ p₁ p₂ rfl h := Eq.recOn h (Heq.refl p₁)

theorem heqOfEqRecRight {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a' = a) (h₂ : p₁ = Eq.recOn e p₂), p₁ ≅ p₂
| a _ p₁ p₂ rfl h :=
  have p₁ = p₂, from h,
  this ▸ 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 nonContradictoryEm (a : Prop) : ¬¬(a ∨ ¬a) :=
assume notEm : ¬(a ∨ ¬a),
  have negA : ¬a, from
    assume posA : a, absurd (Or.inl posA) notEm,
  absurd (Or.inr negA) notEm

def notNotEm := nonContradictoryEm

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) := (a ∧ ¬ b) ∨ (b ∧ ¬ a)

@[recursor 5]
theorem Iff.elim (h₁ : (a → b) → (b → a) → c) (h₂ : a ↔ b) : c :=
Iff.rec h₁ h₂

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

theorem Iff.elimRight : (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.elimRight h) (Iff.elimLeft 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.elimRight h₁ hb))
 (assume (hnb : ¬ b) (ha : a), hnb (Iff.elimLeft 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 impCongr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a → b) ↔ (c → d) :=
Iff.intro
  (λ hab hc, Iff.mp h₂ (hab (Iff.mpr h₁ hc)))
  (λ hcd ha, Iff.mpr h₂ (hcd (Iff.mp h₁ ha)))

theorem impCongrCtx (h₁ : a ↔ c) (h₂ : c → (b ↔ d)) : (a → b) ↔ (c → d) :=
Iff.intro
  (λ hab hc, have ha : a, from Iff.mpr h₁ hc,
             have hb : b, from hab ha,
             Iff.mp (h₂ hc) hb)
  (λ hcd ha, have hc : c, from Iff.mp h₁ ha,
             have hd : d, from hcd hc,
Iff.mpr (h₂ hc) hd)

theorem impCongrRight (h : a → (b ↔ c)) : (a → b) ↔ (a → c) :=
Iff.intro
  (assume hab ha, Iff.elimLeft (h ha) (hab ha))
  (assume hab ha, Iff.elimRight (h ha) (hab ha))

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

theorem notOfNotNotNot (h : ¬¬¬a) : ¬a :=
λ ha, absurd (notNotIntro ha) h

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

def notTrueIff := notTrue

theorem notFalseIff : (¬ False) ↔ True :=
iffTrueIntro notFalse

theorem notCongr (h : a ↔ b) : ¬a ↔ ¬b :=
Iff.intro (λ h₁ h₂, h₁ (Iff.mpr h h₂)) (λ h₁ h₂, h₁ (Iff.mp h h₂))

theorem neSelfIffFalse {α : Sort u} (a : α) : (not (a = a)) ↔ False :=
Iff.intro falseOfNe False.elim

theorem eqSelfIffTrue {α : Sort u} (a : α) : (a = a) ↔ True :=
iffTrueIntro rfl

theorem heqSelfIffTrue {α : Sort u} (a : α) : (a ≅ a) ↔ True :=
iffTrueIntro (Heq.refl a)

theorem iffNotSelf (a : Prop) : (a ↔ ¬a) ↔ False :=
iffFalseIntro (λ h,
   have h' : ¬a, from (λ ha, (Iff.mp h ha) ha),
   h' (Iff.mpr h h'))

theorem notIffSelf (a : Prop) : (¬a ↔ a) ↔ False :=
iffFalseIntro (λ h,
   have h' : ¬a, from (λ ha, (Iff.mpr h ha) ha),
   h' (Iff.mp h h'))

theorem trueIffFalse : (True ↔ False) ↔ False :=
iffFalseIntro (λ h, Iff.mp h trivial)

theorem falseIffTrue : (False ↔ True) ↔ False :=
iffFalseIntro (λ h, Iff.mpr h trivial)

theorem falseOfTrueIffFalse : (True ↔ False) → False :=
assume h, Iff.mp h trivial

theorem falseOfTrueEqFalse : (True = False) → False :=
assume h, h ▸ trivial

theorem trueEqFalseOfFalse : False → (True = False) :=
False.elim

theorem eqComm {α : Sort u} {a b : α} : a = b ↔ b = a :=
⟨Eq.symm, Eq.symm⟩

/- and simp rules -/
theorem and.imp (hac : a → c) (hbd : b → d) : a ∧ b → c ∧ d :=
assume ⟨ha, hb⟩, ⟨hac ha, hbd hb⟩

def andImplies := @and.imp

theorem andCongr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ∧ b) ↔ (c ∧ d) :=
Iff.intro (and.imp (Iff.mp h₁) (Iff.mp h₂)) (and.imp (Iff.mpr h₁) (Iff.mpr h₂))

theorem andComm : a ∧ b ↔ b ∧ a :=
Iff.intro and.swap and.swap

theorem andAssoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
Iff.intro
  (assume ⟨⟨ha, hb⟩, hc⟩, ⟨ha, ⟨hb, hc⟩⟩)
  (assume ⟨ha, ⟨hb, hc⟩⟩, ⟨⟨ha, hb⟩, hc⟩)

theorem andLeftComm : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) :=
Iff.trans (Iff.symm andAssoc) (Iff.trans (andCongr andComm (Iff.refl c)) andAssoc)

theorem andTrue (a : Prop) : a ∧ True ↔ a :=
Iff.intro And.left (λ ha, ⟨ha, trivial⟩)

theorem trueAnd (a : Prop) : True ∧ a ↔ a :=
Iff.intro And.right (λ h, ⟨trivial, h⟩)

theorem andFalse (a : Prop) : a ∧ False ↔ False :=
iffFalseIntro And.right

theorem falseAnd (a : Prop) : False ∧ a ↔ False :=
iffFalseIntro And.left

theorem notAndSelf (a : Prop) : (¬a ∧ a) ↔ False :=
iffFalseIntro (λ h, and.elim h (λ h₁ h₂, absurd h₂ h₁))

theorem andNotSelf (a : Prop) : (a ∧ ¬a) ↔ False :=
iffFalseIntro (assume ⟨h₁, h₂⟩, absurd h₁ h₂)

theorem andSelf (a : Prop) : a ∧ a ↔ a :=
Iff.intro And.left (assume h, ⟨h, h⟩)

/- or simp rules -/

theorem orCongr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ∨ b) ↔ (c ∨ d) :=
Iff.intro (λ h, Or.elim h (λ h, Or.inl (Iff.mp h₁ h)) (λ h, Or.inr (Iff.mp h₂ h)))
          (λ h, Or.elim h (λ h, Or.inl (Iff.mpr h₁ h)) (λ h, Or.inr (Iff.mpr h₂ h)))

theorem orComm : a ∨ b ↔ b ∨ a := Iff.intro Or.swap Or.swap

theorem orAssoc : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) :=
Iff.intro (λ h, Or.elim h (λ h, Or.elim h Or.inl (λ h, Or.inr (Or.inl h))) (λ h, Or.inr (Or.inr h)))
          (λ h, Or.elim h (λ h, Or.inl (Or.inl h)) (λ h, Or.elim h (λ h, Or.inl (Or.inr h)) Or.inr))

theorem orLeftComm : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c) :=
Iff.trans (Iff.symm orAssoc) (Iff.trans (orCongr orComm (Iff.refl c)) orAssoc)

theorem orTrue (a : Prop) : a ∨ True ↔ True :=
iffTrueIntro (Or.inr trivial)

theorem trueOr (a : Prop) : True ∨ a ↔ True :=
iffTrueIntro (Or.inl trivial)

theorem orFalse (a : Prop) : a ∨ False ↔ a :=
Iff.intro (λ h, Or.elim h id False.elim) Or.inl

theorem falseOr (a : Prop) : False ∨ a ↔ a :=
Iff.trans orComm (orFalse a)

theorem orSelf (a : Prop) : a ∨ a ↔ a :=
Iff.intro (λ h, Or.elim h id id) Or.inl

theorem notOr {a b : Prop} : ¬ a → ¬ b → ¬ (a ∨ b)
| hna hnb (Or.inl ha) := absurd ha hna
| hna hnb (Or.inr hb) := absurd hb hnb

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

/- Iff simp rules -/

theorem iffTrue (a : Prop) : (a ↔ True) ↔ a :=
Iff.intro (assume h, Iff.mpr h trivial) iffTrueIntro

theorem trueIff (a : Prop) : (True ↔ a) ↔ a :=
Iff.trans Iff.comm (iffTrue a)

theorem iffFalse (a : Prop) : (a ↔ False) ↔ ¬ a :=
Iff.intro Iff.mp iffFalseIntro

theorem falseIff (a : Prop) : (False ↔ a) ↔ ¬ a :=
Iff.trans Iff.comm (iffFalse a)

theorem iffSelf (a : Prop) : (a ↔ a) ↔ True :=
iffTrueIntro Iff.rfl

theorem iffCongr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ↔ b) ↔ (c ↔ d) :=
(iffIffImpliesAndImplies a b).trans
  ((andCongr (impCongr h₁ h₂) (impCongr h₂ h₁)).trans
    (iffIffImpliesAndImplies c d).symm)

/- implies simp rule -/
theorem impliesTrueIff (α : Sort u) : (α → True) ↔ True :=
Iff.intro (λ h, trivial) (λ ha h, trivial)

theorem falseImpliesIff (a : Prop) : (False → a) ↔ True :=
Iff.intro (λ h, trivial) (λ ha h, False.elim h)

theorem trueImpliesIff (α : Prop) : (True → α) ↔ α :=
Iff.intro (λ h, h trivial) (λ h h', h)

/- exists -/

@[pattern]
def exists.intro := @Exists.intro

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

/- exists and forall congruences -/
theorem forallCongr {α : Sort u} {p q : α → Prop} (h : ∀ a, (p a ↔ q a)) : (∀ a, p a) ↔ ∀ a, q a :=
Iff.intro (λ p a, Iff.mp (h a) (p a)) (λ q a, Iff.mpr (h a) (q a))

theorem existsImpExists {α : Sort u} {p q : α → Prop} (h : ∀ a, (p a → q a)) (p : ∃ a, p a) : ∃ a, q a :=
exists.elim p (λ a hp, ⟨a, h a hp⟩)

theorem existsCongr {α : Sort u} {p q : α → Prop} (h : ∀ a, (p a ↔ q a)) : (Exists p) ↔ ∃ a, q a :=
Iff.intro
  (existsImpExists (λ a, Iff.mp (h a)))
  (existsImpExists (λ a, Iff.mpr (h a)))

theorem forallNotOfNotExists {α : Sort u} {p : α → Prop} : ¬(∃ x, p x) → (∀ x, ¬p x) :=
λ hne x hp, hne ⟨x, hp⟩

/- Decidable -/

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

export Decidable (isTrue isFalse toBool)

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

theorem toBoolFalseEqFf (h : Decidable False) : @toBool 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))

theorem notOrIffAndNot (p q) [d₁ : Decidable p] [d₂ : Decidable q] : ¬ (p ∨ q) ↔ ¬ p ∧ ¬ q :=
Iff.intro
  (λ h, match d₁ with
        | isTrue h₁  := False.elim $ h (Or.inl h₁)
        | isFalse h₁ :=
          match d₂ with
          | isTrue h₂  := False.elim $ h (Or.inr h₂)
          | isFalse h₂ := ⟨h₁, h₂⟩)
  (λ ⟨np, nq⟩ h, Or.elim h np nq)
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

@[macroInline]
protected def or.byCases [Decidable p] [Decidable q] {α : Sort u}
                          (h : p ∨ q) (h₁ : p → α) (h₂ : q → α) : α :=
if hp : p then h₁ hp else
  if hq : q then h₂ hq else
    False.rec _ (Or.elim h hp hq)
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)))

instance existsPropDecidable {p} (P : p → Prop) [Decidable p] [s : ∀ h, Decidable (P h)] : Decidable (∃ h, P h) :=
if h : p then decidableOfDecidableOfIff (s h)
  ⟨λ h2, ⟨h, h2⟩, λ ⟨h', h2⟩, h2⟩ else isFalse (mt (λ ⟨h, _⟩, h) h)

instance forallPropDecidable {p} (P : p → Prop)
  [Dp : Decidable p] [DP : ∀ h, Decidable (P h)] : Decidable (∀ h, P h) :=
if h : p then decidableOfDecidableOfIff (DP h)
  ⟨λ h2 _, h2, λal, al h⟩ else isTrue (λ h2, absurd h2 h)
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

def isDecEq {α : Sort u} (p : α → α → Bool) : Prop   := ∀ ⦃x y : α⦄, p x y = true → x = y
def isDecRefl {α : Sort u} (p : α → α → Bool) : Prop := ∀ x, p x x = true

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}

@[inline]
def decidableEqOfBoolPred {α : Sort u} {p : α → α → Bool} (h₁ : isDecEq p) (h₂ : isDecRefl p) : DecidableEq α :=
{decEq := λ x y : α,
 if hp : p x y = true then isTrue (h₁ hp)
 else isFalse (assume hxy : x = y, absurd (h₂ y) (@Eq.recOn _ _ (λ z _, ¬p z y = true) _ hxy hp))}

theorem decidableEqInlRefl {α : Sort u} [DecidableEq α] (a : α) : decEq a a = isTrue (Eq.refl a) :=
match (decEq a a) with
| (isTrue e)  := rfl
| (isFalse n) := absurd rfl n

theorem decidableEqInrNeg {α : Sort u} [DecidableEq α] {a b : α} : Π n : a ≠ b, decEq a b = isFalse n :=
assume n,
match decEq a b with
| isTrue e   := absurd e n
| isFalse n₁ := proofIrrel n n₁ ▸ Eq.refl (isFalse n)

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

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

theorem ifCtxCongr {α : Sort u} {b c : Prop} [decB : Decidable b] [decC : Decidable c]
                   {x y u v : α}
                   (hC : b ↔ c) (hT : c → x = u) (hE : ¬c → y = v) :
        ite b x y = ite c u v :=
match decB, decC with
| (isFalse h₁), (isFalse h₂) := hE h₂
| (isTrue h₁),  (isTrue h₂)  := hT h₂
| (isFalse h₁), (isTrue h₂)  := absurd h₂ (Iff.mp (notIffNotOfIff hC) h₁)
| (isTrue h₁),  (isFalse h₂) := absurd h₁ (Iff.mpr (notIffNotOfIff hC) h₂)

theorem ifCongr {α : Sort u} {b c : Prop} [decB : Decidable b] [decC : Decidable c]
               {x y u v : α}
               (hC : b ↔ c) (hT : x = u) (hE : y = v) :
        ite b x y = ite c u v :=
@ifCtxCongr α b c decB decC x y u v hC (λ h, hT) (λ h, hE)

theorem ifCtxSimpCongr {α : Sort u} {b c : Prop} [decB : Decidable b] {x y u v : α}
                        (hC : b ↔ c) (hT : c → x = u) (hE : ¬c → y = v) :
        ite b x y = (@ite c (decidableOfDecidableOfIff decB hC) α u v) :=
@ifCtxCongr α b c decB (decidableOfDecidableOfIff decB hC) x y u v hC hT hE

theorem ifSimpCongr {α : Sort u} {b c : Prop} [decB : Decidable b] {x y u v : α}
                    (hC : b ↔ c) (hT : x = u) (hE : y = v) :
        ite b x y = (@ite c (decidableOfDecidableOfIff decB hC) α u v) :=
@ifCtxSimpCongr α b c decB x y u v hC (λ h, hT) (λ h, hE)

theorem ifTrue {α : Sort u} {h : Decidable True} (t e : α) : (@ite True h α t e) = t :=
ifPos trivial

theorem ifFalse {α : Sort u} {h : Decidable False} (t e : α) : (@ite False h α t e) = e :=
ifNeg notFalse

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

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

theorem difCtxCongr {α : Sort u} {b c : Prop} [decB : Decidable b] [decC : Decidable c]
                    {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
                    (hC : b ↔ c)
                    (hT : ∀ (h : c),    x (Iff.mpr hC h)                      = u h)
                    (hE : ∀ (h : ¬c),   y (Iff.mpr (notIffNotOfIff hC) h) = v h) :
        (@dite b decB α x y) = (@dite c decC α u v) :=
match decB, decC with
| (isFalse h₁), (isFalse h₂) := hE h₂
| (isTrue h₁),  (isTrue h₂)  := hT h₂
| (isFalse h₁), (isTrue h₂)  := absurd h₂ (Iff.mp (notIffNotOfIff hC) h₁)
| (isTrue h₁),  (isFalse h₂) := absurd h₁ (Iff.mpr (notIffNotOfIff hC) h₂)

theorem difCtxSimpCongr {α : Sort u} {b c : Prop} [decB : Decidable b]
                         {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
                         (hC : b ↔ c)
                         (hT : ∀ (h : c),    x (Iff.mpr hC h)                      = u h)
                         (hE : ∀ (h : ¬c),   y (Iff.mpr (notIffNotOfIff hC) h) = v h) :
        (@dite b decB α x y) = (@dite c (decidableOfDecidableOfIff decB hC) α u v) :=
@difCtxCongr α b c decB (decidableOfDecidableOfIff decB hC) x u y v hC hT hE

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

def asTrue (c : Prop) [Decidable c] : Prop :=
if c then True else False

def asFalse (c : Prop) [Decidable c] : Prop :=
if c then False else True

def ofAsTrue {c : Prop} [h₁ : Decidable c] (h₂ : asTrue c) : c :=
match h₁, h₂ with
| (isTrue hC),  h₂ := hC
| (isFalse hC), h₂ := False.elim h₂

/-- 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 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} : (∃ 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

/- Equalities for rewriting let-expressions -/
theorem letValueEq {α : Sort u} {β : Sort v} {a₁ a₂ : α} (b : α → β) :
                   a₁ = a₂ → (let x : α := a₁ in b x) = (let x : α := a₂ in b x) :=
λ h, Eq.ndrecOn h rfl

theorem letValueHeq {α : Sort v} {β : α → Sort u} {a₁ a₂ : α} (b : Π x : α, β x) :
                    a₁ = a₂ → (let x : α := a₁ in b x) ≅ (let x : α := a₂ in b x) :=
λ h, Eq.ndrecOn h (Heq.refl (b a₁))

theorem letBodyEq {α : Sort v} {β : α → Sort u} (a : α) {b₁ b₂ : Π x : α, β x} :
                  (∀ x, b₁ x = b₂ x) → (let x : α := a in b₁ x) = (let x : α := a in b₂ x) :=
λ h, h a

theorem letEq {α : Sort v} {β : Sort u} {a₁ a₂ : α} {b₁ b₂ : α → β} :
             a₁ = a₂ → (∀ x, b₁ x = b₂ x) → (let x : α := a₁ in b₁ x) = (let x : α := a₂ in b₂ x) :=
λ h₁ h₂, Eq.ndrecOn h₁ (h₂ a₁)

section relation
variables {α : Sort u} {β : Sort v} (r : β → β → Prop)
local infix `≺`:50 := r

def reflexive := ∀ x, x ≺ x

def symmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x

def transitive := ∀ ⦃x y z⦄, x ≺ y → y ≺ z → x ≺ z

def equivalence := reflexive r ∧ symmetric r ∧ transitive r

def total := ∀ x y, x ≺ y ∨ y ≺ x

def mkEquivalence (rfl : reflexive r) (symm : symmetric r) (trans : transitive r) : equivalence r :=
⟨rfl, symm, trans⟩

def irreflexive := ∀ x, ¬ x ≺ x

def antiSymmetric := ∀ ⦃x y⦄, x ≺ y → 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₂, f a₁ ≺ f a₂

theorem InvImage.trans (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 : α → α → α
variable inv : α → α
variable one : α
local infix * := f
local postfix `⁻¹`:max := inv
variable g : α → α → α
local infix + := g

def commutative        := ∀ a b, a * b = b * a
def associative        := ∀ a b c, (a * b) * c = a * (b * c)
def leftIdentity      := ∀ a, one * a = a
def rightIdentity     := ∀ a, a * one = a
def rightInverse      := ∀ a, a * a⁻¹ = one
def leftCancelative   := ∀ a b c, a * b = a * c → b = c
def rightCancelative  := ∀ a b c, a * b = c * b → a = c
def leftDistributive  := ∀ a b c, a * (b + c) = a * b + a * c
def rightDistributive := ∀ a b c, (a + b) * c = a * c + 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)

local infix `◾`:50 := Eq.trans

theorem leftComm : commutative f → associative f → leftCommutative f :=
assume hcomm hassoc, assume a b c,
  Eq.symm (hassoc a b c)
◾ (hcomm a b ▸ rfl : (a*b)*c = (b*a)*c)
◾ hassoc b a c

theorem rightComm : commutative f → associative f → rightCommutative f :=
assume hcomm hassoc, assume a b c,
  hassoc a b c
◾ (hcomm b c ▸ rfl : a*(b*c) = a*(c*b))
◾ Eq.symm (hassoc a c b)

end binary

/- Subtype -/

namespace Subtype
def existsOfSubtype {α : Type u} {p : α → Prop} : { x // p x } → ∃ 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}

theorem Prod.mk.eta : ∀{p : α × β}, (p.1, p.2) = p
| (a, b) := rfl

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 [HasLt α] [HasLt β] : HasLt (α × β) :=
⟨λ s t, s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)⟩

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

theorem Prod.ltDef [HasLt α] [HasLt β] (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} : (Σ' x, p x) → ∃ x, p x
| ⟨x, hx⟩ := ⟨x, hx⟩

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

protected theorem Sigma.Eq : ∀ {p₁ p₂ : Σ 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

/- Additional congruence theorems. -/

theorem forallCongrEq {a : Sort u} {p q : a → Prop} (h : ∀ x, p x = q x) : (∀ x, p x) = ∀ x, q x :=
propext (forallCongr (λ a, (h a).toIff))

theorem impCongrEq {a b c d : Prop} (h₁ : a = c) (h₂ : b = d) : (a → b) = (c → d) :=
propext (impCongr h₁.toIff h₂.toIff)

theorem impCongrCtxEq {a b c d : Prop} (h₁ : a = c) (h₂ : c → (b = d)) : (a → b) = (c → d) :=
propext (impCongrCtx h₁.toIff (λ hc, (h₂ hc).toIff))

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

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

theorem Iff.toEq {a b : Prop} (h : a ↔ b) : a = b :=
propext h

theorem iffEqEq {a b : Prop} : (a ↔ b) = (a = b) :=
propext (Iff.intro
  (assume h, Iff.toEq h)
  (assume h, h.toIff))

theorem eqFalse {a : Prop} : (a = False) = (¬ a) :=
have (a ↔ False) = (¬ a), from propext (iffFalse a),
Eq.subst (@iffEqEq a False) this

theorem eqTrue {a : Prop} : (a = True) = a :=
have (a ↔ True) = a, from propext (iffTrue a),
Eq.subst (@iffEqEq a True) this

/- 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) : ∃ a : α, (Quot.mk r a) = q :=
Quot.inductionOn q (λ a, ⟨a, rfl⟩)

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

local notation `⟦`:max a `⟧` := Quot.mk r a

@[reducible, macroInline]
protected def indep (f : Π a, β ⟦a⟧) (a : α) : Psigma β :=
⟨⟦a⟧, f a⟩

protected theorem indepCoherent (f : Π a, β ⟦a⟧)
                     (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β ⟦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, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β ⟦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, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β ⟦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, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β ⟦b⟧) = f b) : β q :=
Quot.rec f h q

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

@[reducible, elabAsEliminator, inline]
protected def hrecOn
   (q : Quot r) (f : Π a, β ⟦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) : β ⟦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) : ∃ 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₂)))))

local infix `~` := rel

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

private theorem eqImpRel {q₁ q₂ : Quotient s} : q₁ = q₂ → 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}

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

local infix `~` := Function.equiv

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

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

protected theorem equiv.trans {f₁ f₂ f₃ : Π x: α, β x} : f₁ ~ f₂ → f₂ ~ f₃ → 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 extfun (α : Sort u) (β : α → Sort v) : Sort (imax u v) :=
Quotient (funSetoid α β)

private def funToExtfun (f : Π x : α, β x) : extfun α β :=
⟦f⟧
private def extfunApp (f : extfun α β) : Π 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

local infix `~` := Function.equiv

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

/- Classical reasoning support -/

namespace Classical

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

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

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

theorem chooseSpec {α : Sort u} {p : α → Prop} (h : ∃ 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 : ∃ x, U x, from ⟨True, Or.inl rfl⟩,
have exV : ∃ 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 α → ∃ x : α, True
| ⟨x⟩ := ⟨x, trivial⟩

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

noncomputable def inhabitedOfExists {α : Sort u} {p : α → Prop} (h : ∃ 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 : α // (∃ y : α, p y) → p x} :=
if hp : ∃ 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)
  : (∃ y, p y) → p (@epsilon α h p) :=
(strongIndefiniteDescription p h).property

theorem epsilonSpec {α : Sort u} {p : α → Prop} (hex : ∃ 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, ∃ y, r x y) :
  ∃ (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, ∃ y, p x y) ↔ ∃ (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
def 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