lean4-htt/src/Init/Core.lean

/-
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
reserve infixr ` $ `:1
notation f ` $ ` a := f a

/- Logical operations and relations -/

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 infixr ` ▸ `:75

/- types and Type constructors -/

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

/- other symbols -/

reserve infixl ` ++ `:65
reserve infixr ` :: `:67

/- Control -/
reserve infixr ` <|> `:2
reserve infixl ` >>= `:55
reserve infixr ` >=> `:55
reserve infixl ` <*> `:60
reserve infixl ` <* ` :60
reserve infixr ` *> ` :60
reserve infixr ` >> ` :60
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 : α → β → φ) : β → α → φ :=
fun 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, reducible] def idRhs (α : Sort u) (a : α) : α := a

/-- Auxiliary Declaration used to implement the named patterns `x@p` -/
@[reducible] def namedPattern {α : Sort u} (x 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

@[matchPattern] 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 "lean_mk_thunk"] Thunk.mk

@[noinline, extern "lean_thunk_pure"]
protected def Thunk.pure {α : Type u} (a : α) : Thunk α :=
⟨fun _ => a⟩
@[noinline, extern "lean_thunk_get_own"]
protected def Thunk.get {α : Type u} (x : @& Thunk α) : α :=
x.fn ()
@[noinline, extern "lean_thunk_map"]
protected def Thunk.map {α : Type u} {β : Type v} (f : α → β) (x : Thunk α) : Thunk β :=
⟨fun _ => f x.get⟩
@[noinline, extern "lean_thunk_bind"]
protected def Thunk.bind {α : Type u} {β : Type v} (x : Thunk α) (f : α → Thunk β) : Thunk β :=
⟨fun _ => (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 Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {C : α → Sort u1} (m : C a) {b : α} (h : Eq a b) : C b :=
@Eq.rec α a (fun α _ => C α) m b h

@[elabAsEliminator, inline, reducible]
def Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {C : α → Sort u1} {b : α} (h : Eq a b) (m : C a) : C b :=
@Eq.rec α a (fun α _ => 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
-/
init_quot

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

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

attribute [unbox] Prod

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

/-- Similar to `Prod`, but `α` and `β` are in the same universe. -/
structure MProd (α β : Type u) :=
(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

@[matchPattern] 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

@[matchPattern] 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' :=
  fun (α' : Sort u) (a' : α') (h₁ : @HEq α a α' a') => HEq.recOn h₁ (fun (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)

attribute [unbox] Sigma

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

/- Auxiliary type used to compile `for x in xs` notation. -/
inductive ForInStep (α : Type u)
| done  : α → ForInStep
| yield : α → ForInStep

/- Auxiliary type used to compile `do` notation. -/
inductive DoResultPRBC (α β σ : Type u)
| «pure»     : α → σ → DoResultPRBC
| «return»   : β → σ → DoResultPRBC
| «break»    : σ → DoResultPRBC
| «continue» : σ → DoResultPRBC

/- Auxiliary type used to compile `do` notation. -/
inductive DoResultPR (α β σ : Type u)
| «pure»     : α → σ → DoResultPR
| «return»   : β → σ → DoResultPR

/- Auxiliary type used to compile `do` notation. -/
inductive DoResultBC (σ : Type u)
| «break»    : σ → DoResultBC
| «continue» : σ → DoResultBC

/- Auxiliary type used to compile `do` notation. -/
inductive DoResultSBC (α σ : Type u)
| «pureReturn» : α → σ → DoResultSBC
| «break»      : σ → DoResultSBC
| «continue»   : σ → DoResultSBC

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

abbrev DecidablePred {α : Sort u} (r : α → Prop) :=
∀ (a : α), Decidable (r a)

abbrev DecidableRel {α : Sort u} (r : α → α → Prop) :=
∀ (a b : α), Decidable (r a b)

abbrev DecidableEq (α : Sort u) :=
∀ (a b : α), Decidable (a = b)

def decEq {α : Sort u} [s : DecidableEq α] (a b : α) : Decidable (a = b) :=
s a b

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

attribute [unbox] 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. -/
axiom sorryAx (α : Sort u) (synthetic := true) : α

/- Declare builtin and reserved notation -/

class HasZero     (α : Type u) := mk {} :: (zero : α)
class HasOne      (α : Type u) := mk {} :: (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 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 HasEquiv    (α : Sort u) := (Equiv : α → α → Prop)
class HasEmptyc   (α : Type u) := (emptyc : α)

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

infix `+`        := HasAdd.add
infix `*`        := HasMul.mul
infix `-`        := HasSub.sub
infix `/`        := HasDiv.div
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 `≈`        := 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

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

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

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

/- Nat basic instances -/
@[extern "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 [matchPattern] 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

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

attribute [extern "lean_task_pure"] Task.pure
attribute [extern "lean_task_get_own"] Task.get

namespace Task
/-- Task priority. Tasks with higher priority will always be scheduled before ones with lower priority. -/
abbrev Priority := Nat
def Priority.default : Priority := 0
-- see `LEAN_MAX_PRIO`
def Priority.max : Priority := 8
/--
  Any priority higher than `Task.Priority.max` will result in the task being scheduled immediately on a dedicated thread.
  This is particularly useful for long-running and/or I/O-bound tasks since Lean will by default allocate no more
  non-dedicated workers than the number of cores to reduce context switches. -/
def Priority.dedicated : Priority := 9

@[noinline, extern "lean_task_spawn"]
protected def spawn {α : Type u} (fn : Unit → α) (prio := Priority.default) : Task α :=
⟨fn ()⟩
@[noinline, extern "lean_task_map"]
protected def map {α : Type u} {β : Type v} (f : α → β) (x : Task α) (prio := Priority.default) : Task β :=
⟨f x.get⟩
@[noinline, extern "lean_task_bind"]
protected def bind {α : Type u} {β : Type v} (x : Task α) (f : α → Task β) (prio := Priority.default) : Task β :=
⟨(f x.get).get⟩

end Task

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

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

/- Some type that is not a scalar value in our runtime and is universe polymorphic. -/
inductive PNonScalar : Type u
| mk (v : Nat) : PNonScalar

/- For numeric literals notation -/
class HasOfNat (α : Type u) :=
(ofNat : Nat → α)

export HasOfNat (ofNat)

instance : HasOfNat Nat :=
⟨id⟩

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

@[inline] def condEq {β : Sort u} (b : Bool) (h₁ : b = true → β) (h₂ : b = false → β) : β :=
@Bool.casesOn (λ x => b = x → β) b h₂ h₁ rfl

@[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 c inline "#1 || #2"] def strictOr  (b₁ b₂ : Bool) := b₁ || b₂
@[extern c 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 :=
fun hp => h₂ (h₁ hp)

def trivial : True := ⟨⟩

@[macroInline] def False.elim {C : Sort u} (h : False) : C :=
False.rec (fun _ => 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 :=
fun ha => 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} : (α = β) → β → α :=
fun 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 :=
fun 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 :=
fun h₁ => h (h₁.symm)

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

theorem neFalseOfSelf : p → p ≠ False :=
fun (hp : p) (h : p = False) => h ▸ hp

theorem neTrueOfNot : ¬p → p ≠ True :=
fun (hnp : ¬p) (h : p = True) => (h ▸ 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)

theorem neFalseOfEqTrue : ∀ {b : Bool}, b = true → b ≠ false
| true, _  => fun h => Bool.noConfusion h
| false, h => Bool.noConfusion h

theorem neTrueOfEqFalse : ∀ {b : Bool}, b = false → b ≠ true
| true, h  => Bool.noConfusion h
| false, _ => fun h => Bool.noConfusion h

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

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

@[elabAsEliminator]
theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {C : ∀ {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : C a) : C b :=
@HEq.rec α a (fun β 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 :=
fun ⟨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)

@[recursor 5]
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 (fun h => And.intro h.mp h.mpr) (fun h => Iff.intro h.left h.right)

theorem Iff.refl (a : Prop) : a ↔ a :=
Iff.intro (fun h => h) (fun 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
  (fun ha => Iff.mp h₂ (Iff.mp h₁ ha))
  (fun 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 :=
fun h₁ h₂ =>
have a ↔ b from Eq.subst h₂ (Iff.refl a);
absurd this h₁

theorem notIffNotOfIff (h₁ : a ↔ b) : ¬a ↔ ¬b :=
Iff.intro
 (fun (hna : ¬ a) (hb : b) => hna (Iff.right h₁ hb))
 (fun (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
  (fun hl => trivial)
  (fun hr => h)

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

theorem notNotIntro (ha : a) : ¬¬a :=
fun hna => 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 (fun ha => absurd ha na) id

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

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

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

/- Exists -/

theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop}
   (h₁ : Exists (fun 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 (fun h₁ => false) (fun h₂ => true)

export Decidable (isTrue isFalse decide)

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

theorem decideTrueEqTrue (h : Decidable True) : @decide True h = true :=
match h with
| isTrue h  => rfl
| isFalse h => False.elim (Iff.mp notTrue h)

theorem decideFalseEqFalse (h : Decidable False) : @decide False h = false :=
match h with
| isFalse h => rfl
| isTrue h  => False.elim h

theorem decideEqTrue : ∀ {p : Prop} [s : Decidable p], p → decide p = true
| _, isTrue  _, _   => rfl
| _, isFalse h₁, h₂ => absurd h₂ h₁

theorem decideEqFalse : ∀ {p : Prop} [s : Decidable p], ¬p → decide p = false
| _, isTrue  h₁, h₂ => absurd h₁ h₂
| _, isFalse h, _   => rfl

theorem ofDecideEqTrue {p : Prop} [s : Decidable p] : decide p = true → p :=
fun h => match s with
  | isTrue  h₁ => h₁
  | isFalse h₁ => absurd h (neTrueOfEqFalse (decideEqFalse h₁))

theorem ofDecideEqFalse {p : Prop} [s : Decidable p] : decide p = false → ¬p :=
fun h => match s with
  | isTrue  h₁ => absurd h (neFalseOfEqTrue (decideEqTrue h₁))
  | isFalse h₁ => h₁

/-- Similar to `decide`, but uses an explicit instance -/
@[inline] def toBoolUsing {p : Prop} (d : Decidable p) : Bool :=
@decide p d

theorem toBoolUsingEqTrue {p : Prop} (d : Decidable p) (h : p) : toBoolUsing d = true :=
@decideEqTrue _ d h

theorem ofBoolUsingEqTrue {p : Prop} {d : Decidable p} (h : toBoolUsing d = true) : p :=
@ofDecideEqTrue _ d h

theorem ofBoolUsingEqFalse {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) : ¬ p :=
@ofDecideEqFalse _ d 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 {α : Sort u} (c : Prop) [h : Decidable c] : (c → α) → (¬ c → α) → α :=
fun t e => Decidable.casesOn h e t

/- if-then-else -/

@[macroInline] def ite {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α :=
Decidable.casesOn h (fun hnc => e) (fun 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 (fun h => False.rec _ (h h₃)) (fun 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 (fun h => h₄) (fun 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 (fun np => False.elim (h np))

theorem ofNotNot [Decidable p] : ¬ ¬ p → p :=
fun hnn => byContradiction (fun 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
(fun 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₁)
(fun (h) ⟨hp, hq⟩ => Or.elim h (fun h => h hp) (fun 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 (fun h => hq (And.right h))
else isFalse (fun h => 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 (fun 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 (fun h => hq)
  else isFalse (fun h => absurd (h hp) hq)
else isTrue (fun h => absurd h hp)

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

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

end

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

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

@[inline] instance : DecidableEq Bool :=
fun 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

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

-- 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 (fun h => t) (fun 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 ULift.{r, s} (α : 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) :=
mk {} :: (default : α)

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

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

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

instance Forall.Inhabited (α : Sort u) {β : α → Sort v} [∀ x, Inhabited (β x)] : Inhabited (∀ x, β x) :=
⟨fun a => arbitrary (β a)⟩

instance : Inhabited Bool := ⟨false⟩

instance : Inhabited True := ⟨trivial⟩

instance : Inhabited Nat := ⟨0⟩

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

instance : Inhabited PNonScalar.{u} := ⟨⟨arbitrary _⟩⟩

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 α :=
⟨arbitrary α⟩

theorem nonemptyOfExists {α : Sort u} {p : α → Prop} : Exists (fun 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 (fun p => p)

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

instance subsingletonProp (p : Prop) : Subsingleton p :=
⟨fun a b => proofIrrel a b⟩

instance (p : Prop) : Subsingleton (Decidable p) :=
Subsingleton.intro $ fun d₁ =>
  match d₁ with
  | (isTrue t₁) => fun d₂ =>
    match d₂ with
    | (isTrue t₂)  => Eq.recOn (proofIrrel t₁ t₂) rfl
    | (isFalse f₂) => absurd t₁ f₂
  | (isFalse f₁) => fun 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₂ : α) : Prop := False

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

def InvImage (f : α → β) : α → α → Prop :=
fun a₁ a₂ => r (f a₁) (f a₂)

theorem InvImage.Transitive (f : α → β) (h : Transitive r) : Transitive (InvImage r f) :=
fun (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) :=
fun (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 TC.ndrec.{u1, u2} {α : 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 (fun a b _ => C a b) m₁ m₂ a b h

@[elabAsEliminator]
theorem TC.ndrecOn.{u1, u2} {α : 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 (fun 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 :=
fun hcomm hassoc 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 :=
fun hcomm hassoc 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 (fun 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} :=
fun ⟨a, h₁⟩ ⟨b, h₂⟩ =>
  if h : a = b then isTrue (Subtype.eq h)
  else isFalse (fun h' => Subtype.noConfusion h' (fun h' => absurd h' h))
end Subtype

/- Sum -/

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

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

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

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

/- Product -/

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

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

instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
fun ⟨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 (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₂' n₂))
  | (isFalse n₁) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₁' n₁))

instance [HasBeq α] [HasBeq β] : HasBeq (α × β) :=
⟨fun ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ => a₁ == a₂ && b₁ == b₂⟩

instance [HasLess α] [HasLess β] : HasLess (α × β) :=
⟨fun 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) :=
fun 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 Prod.map.{u₁, u₂, v₁, v₂} {α₁ : 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 (fun x => p x)) → Exists (fun x => p x)
| ⟨x, hx⟩ => ⟨x, hx⟩

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

protected theorem Sigma.eq : ∀ {p₁ p₂ : Sigma (fun 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 :=
fun 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 (fun a => (Quot.mk r a) = q) :=
Quot.inductionOn q (fun 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  :=
fun 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 (fun (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 (fun 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 $
  fun a b p => eqOfHEq $
    have p₁ : (Eq.rec (f a) (sound p) : β (Quot.mk r b)) ≅ f a := 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

def sound {α : Sort u} [s : Setoid α] {a b : α} : a ≈ b → Quotient.mk a = Quotient.mk 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, β (Quotient.mk 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, β (Quotient.mk a)) : β q :=
Quot.inductionOn q h

theorem existsRep {α : Sort u} [s : Setoid α] (q : Quotient s) : Exists (fun (a : α) => Quotient.mk a = q) :=
Quot.existsRep q

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

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

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

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

@[reducible, elabAsEliminator, inline]
protected def hrecOn
   (q : Quotient s) (f : ∀ a, β (Quotient.mk 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 β]

@[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
  (fun (a₁ : α) => Quotient.lift (f a₁) (fun (a b : β) => c a₁ a a₁ b (Setoid.refl a₁)) q₂)
  (fun (a b : α) (h : a ≈ b) =>
     @Quotient.ind β s₂
       (fun (a1 : Quotient s₂) =>
          (Quotient.lift (f a) (fun (a1 b : β) => c a a1 a b (Setoid.refl a)) a1)
          =
          (Quotient.lift (f b) (fun (a b1 : β) => c b a b b1 (Setoid.refl b)) a1))
       (fun (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, φ (Quotient.mk a) (Quotient.mk b)) (q₁ : Quotient s₁) (q₂ : Quotient s₂) : φ q₁ q₂ :=
Quotient.ind (fun a₁ => Quotient.ind (fun a₂ => h a₁ a₂) q₂) q₁

@[elabAsEliminator]
protected theorem inductionOn₂
   {φ : Quotient s₁ → Quotient s₂ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (h : ∀ a b, φ (Quotient.mk a) (Quotient.mk b)) : φ q₁ q₂ :=
Quotient.ind (fun a₁ => Quotient.ind (fun 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, δ (Quotient.mk a) (Quotient.mk b) (Quotient.mk c))
   : δ q₁ q₂ q₃ :=
Quotient.ind (fun a₁ => Quotient.ind (fun a₂ => Quotient.ind (fun a₃ => h a₁ a₂ a₃) q₃) q₂) q₁
end

section Exact
variable   {α : Sort u}

private def rel [s : Setoid α] (q₁ q₂ : Quotient s) : Prop :=
Quotient.liftOn₂ q₁ q₂
  (fun a₁ a₂ => a₁ ≈ a₂)
  (fun a₁ a₂ b₁ b₂ a₁b₁ a₂b₂ =>
    propext (Iff.intro
      (fun a₁a₂ => Setoid.trans (Setoid.symm a₁b₁) (Setoid.trans a₁a₂ a₂b₂))
      (fun b₁b₂ => Setoid.trans a₁b₁ (Setoid.trans b₁b₂ (Setoid.symm a₂b₂)))))

private theorem rel.refl [s : Setoid α] : ∀ (q : Quotient s), rel q q :=
fun q => Quot.inductionOn q (fun a => Setoid.refl a)

private theorem eqImpRel [s : Setoid α] {q₁ q₂ : Quotient s} : q₁ = q₂ → rel q₁ q₂ :=
fun h => Eq.ndrecOn h (rel.refl q₁)

theorem exact [s : Setoid α] {a b : α} : Quotient.mk a = Quotient.mk b → a ≈ b :=
fun h => eqImpRel h
end Exact

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

@[reducible, elabAsEliminator]
protected def recOnSubsingleton₂
   {φ : Quotient s₁ → Quotient s₂ → Sort uC} [h : ∀ a b, Subsingleton (φ (Quotient.mk a) (Quotient.mk b))]
   (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : ∀ a b, φ (Quotient.mk a) (Quotient.mk b)) : φ q₁ q₂:=
@Quotient.recOnSubsingleton _ s₁ (fun q => φ q q₂) (fun a => Quotient.ind (fun b => h a b) q₂) q₁
  (fun a => Quotient.recOnSubsingleton q₂ (fun 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)) (fun 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
  (fun x y h => Quot.sound h)
  (fun x => rfl)
  (fun x y _ IH => Eq.symm IH)
  (fun x y z _ _ IH₁ IH₂ => Eq.trans IH₁ IH₂)
end

instance {α : Sort u} {s : Setoid α} [d : ∀ (a b : α), Decidable (a ≈ b)] : DecidableEq (Quotient s) :=
fun (q₁ q₂ : Quotient s) =>
  Quotient.recOnSubsingleton₂ q₁ q₂
    (fun a₁ a₂ =>
      match (d a₁ a₂) with
      | (isTrue h₁)  => isTrue (Quotient.sound h₁)
      | (isFalse h₂) => isFalse (fun 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 :=
fun x => rfl

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

protected theorem Equiv.trans {f₁ f₂ f₃ : ∀ (x : α), β x} : Equiv f₁ f₂ → Equiv f₂ f₃ → Equiv f₁ f₃ :=
fun 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 :=
fun x =>
Quot.liftOn f
  (fun (f : ∀ (x : α), β x) => f x)
  (fun f₁ f₂ h => h x)

theorem funext {f₁ f₂ : ∀ (x : α), β x} (h : ∀ x, f₁ x = f₂ x) : f₁ = f₂ :=
show extfunApp (Quotient.mk f₁) = extfunApp (Quotient.mk f₂) from
congrArg extfunApp (sound h)
end

instance Forall.Subsingleton {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] : Subsingleton (∀ a, β a) :=
⟨fun f₁ f₂ => funext (fun 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 : α → β) : α → φ :=
fun x => f (g x)

infixr  ` ∘ `      := Function.comp

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

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

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

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

end Function

/- Squash -/

def Squash (α : Type u) := Quot (fun (a b : α) => True)

def Squash.mk {α : Type u} (x : α) : Squash α := Quot.mk _ x

theorem Squash.ind {α : Type u} {β : Squash α → Prop} (h : ∀ (a : α), β (Squash.mk a)) : ∀ (q : Squash α), β q :=
Quot.ind h

@[inline] def Squash.lift {α β} [Subsingleton β] (s : Squash α) (f : α → β) : β :=
Quot.lift f (fun a b _ => Subsingleton.elim _ _) s

instance Squash.Subsingleton {α} : Subsingleton (Squash α) :=
⟨Squash.ind (fun (a : α) => Squash.ind (fun (b : α) => Quot.sound trivial))⟩

namespace Lean
/- Kernel reduction hints -/

/--
  When the kernel tries to reduce a term `Lean.reduceBool c`, it will invoke the Lean interpreter to evaluate `c`.
  The kernel will not use the interpreter if `c` is not a constant.
  This feature is useful for performing proofs by reflection.

  Remark: the Lean frontend allows terms of the from `Lean.reduceBool t` where `t` is a term not containing
  free variables. The frontend automatically declares a fresh auxiliary constant `c` and replaces the term with
  `Lean.reduceBool c`. The main motivation is that the code for `t` will be pre-compiled.

  Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base.
  This is extra 30k lines of code. More importantly, you will probably not be able to check your developement using
  external type checkers (e.g., Trepplein) that do not implement this feature.
  Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
  So, you are mainly losing the capability of type checking your developement using external checkers.

  Recall that the compiler trusts the correctness of all `[implementedBy ...]` and `[extern ...]` annotations.
  If an extern function is executed, then the trusted code base will also include the implementation of the associated
  foreign function.
-/
constant reduceBool (b : Bool) : Bool := b

/--
  Similar to `Lean.reduceBool` for closed `Nat` terms.

  Remark: we do not have plans for supporting a generic `reduceValue {α} (a : α) : α := a`.
  The main issue is that it is non-trivial to convert an arbitrary runtime object back into a Lean expression.
  We believe `Lean.reduceBool` enables most interesting applications (e.g., proof by reflection). -/
constant reduceNat (n : Nat) : Nat := n

axiom ofReduceBool (a b : Bool) (h : reduceBool a = b) : a = b
axiom ofReduceNat (a b : Nat) (h : reduceNat a = b)    : a = b

end Lean

/- Classical reasoning support -/

namespace Classical

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

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

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

theorem chooseSpec {α : Sort u} {p : α → Prop} (h : Exists (fun 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;
let V (x : Prop) : Prop := x = False ∨ p;
have exU : Exists (fun x => U x) from ⟨True, Or.inl rfl⟩;
have exV : Exists (fun x => V x) from ⟨False, Or.inl rfl⟩;
let u : Prop := choose exU;
let v : Prop := choose exV;
have uDef : U u from chooseSpec exU;
have vDef : V v from chooseSpec exV;
have notUvOrP : u ≠ v ∨ p from
  Or.elim uDef
    (fun hut =>
      Or.elim vDef
        (fun hvf =>
          have hne : u ≠ v from hvf.symm ▸ hut.symm ▸ trueNeFalse;
          Or.inl hne)
        Or.inr)
    Or.inr;
have pImpliesUv : p → u = v from
  fun hp =>
  have hpred : U = V from
    funext $ fun x =>
      have hl : (x = True ∨ p) → (x = False ∨ p) from
        fun a => Or.inr hp;
      have hr : (x = False ∨ p) → (x = True ∨ p) from
        fun 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 ▸ fun exU exV => rfl;
  show u = v from h₀ _ _;
Or.elim notUvOrP
  (fun (hne : u ≠ v) => Or.inr (mt pImpliesUv hne))
  Or.inl

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

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

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

/- all propositions are Decidable -/
noncomputable def propDecidable (a : Prop) : Decidable a :=
choice $ Or.elim (em a)
  (fun ha => ⟨isTrue ha⟩)
  (fun hna => ⟨isFalse hna⟩)

noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) :=
⟨propDecidable a⟩

noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
fun x y => propDecidable (x = y)

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

noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop)
  (h : Nonempty α) : {x : α // Exists (fun (y : α) => p y) → p x} :=
@dite _ (Exists (fun (x : α) => p x)) (propDecidable _)
  (fun (hp : Exists (fun (x : α) => p x)) =>
    show {x : α // Exists (fun (y : α) => p y) → p x} from
    let xp := indefiniteDescription _ hp;
    ⟨xp.val, fun h' => xp.property⟩)
  (fun hp => ⟨choice h, fun 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 (fun y => p y) → p (@epsilon α h p) :=
(strongIndefiniteDescription p h).property

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

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

/- the axiom of choice -/

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

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

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

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

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

end Classical