lean4-htt/library/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
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 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 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

@[inline] def id {α : 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 id_delta applications.
It implements the following rules

   1)   (id_delta t) =?= t
   2)   t =?= (id_delta t)
   3)   (id_delta t) =?= s  IF (unfold_of t) =?= s
   4)   t =?= id_delta s    IF t =?= (unfold_of s)

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

We use id_delta applications to address performance problems when type checking
lemmas generated by the equation compiler.
-/
@[inline] def id_delta {α : Sort u} (a : α) : α :=
a

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

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

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

/-
  id_rhs 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.
-/
abbreviation id_rhs (α : 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. -/
abbreviation unit : Type := punit

@[pattern] abbreviation unit.star : unit := punit.star

/--
Gadget for defining thunks, thunk parameters have special treatment.
Example: given
      def f (s : string) (t : thunk nat) : nat
an application
     f "hello" 10
 is converted into
     f "hello" (λ _, 10)
-/
@[reducible] def thunk (α : Type u) : Type u :=
unit → α

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

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

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 brec_on recursor. -/
structure pprod (α : Sort u) (β : Sort v) :=
(fst : α) (snd : β)

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

def and.elim_left {a b : Prop} (h : and a b) : a := h.1

def and.elim_right {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

attribute [refl] eq.refl

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

@[elab_as_eliminator, subst]
theorem eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b :=
eq.rec h₂ h₁

notation h1 ▸ h2 := eq.subst h1 h2

@[trans] theorem eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c :=
h₂ ▸ h₁

@[symm] theorem eq.symm {α : Sort u} {a b : α} (h : a = b) : b = a :=
h ▸ rfl

infix == := heq

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

theorem eq_of_heq {α : Sort u} {a a' : α} (h : a == a') : a = a' :=
have ∀ (α' : Sort u) (a' : α') (h₁ : @heq α a α' a') (h₂ : α = α'), (eq.rec_on h₂ a : α') = a', from
  λ (α' : Sort u) (a' : α') (h₁ : @heq α a α' a'), heq.rec_on h₁ (λ h₂ : α = α, rfl),
show (eq.rec_on (eq.refl α) a : α) = a', from
  this α a' h (eq.refl α)

/- The following four lemmas could not be automatically generated when the
   structures were declared, so we prove them manually here. -/
theorem prod.mk.inj {α : Type u} {β : Type v} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β}
  : (x₁, y₁) = (x₂, y₂) → and (x₁ = x₂) (y₁ = y₂) :=
λ h, prod.no_confusion h (λ h₁ h₂, ⟨h₁, h₂⟩)

theorem prod.mk.inj_arrow {α : Type u} {β : Type v} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β}
  : (x₁, y₁) = (x₂, y₂) → Π ⦃P : Sort w⦄, (x₁ = x₂ → y₁ = y₂ → P) → P :=
λ h₁ _ h₂, prod.no_confusion h₁ h₂

theorem pprod.mk.inj {α : Sort u} {β : Sort v} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β}
  : pprod.mk x₁ y₁ = pprod.mk x₂ y₂ → and (x₁ = x₂) (y₁ = y₂) :=
λ h, pprod.no_confusion h (λ h₁ h₂, ⟨h₁, h₂⟩)

theorem pprod.mk.inj_arrow {α : Type u} {β : Type v} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β}
  : (x₁, y₁) = (x₂, y₂) → Π ⦃P : Sort w⦄, (x₁ = x₂ → y₁ = y₂ → P) → P :=
λ h₁ _ h₂, prod.no_confusion h₁ h₂

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.intro_left {a : Prop} (b : Prop) (ha : a) : or a b :=
or.inl ha

def or.intro_right (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
| ff : bool
| tt : bool

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

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

def exists_unique {α : Sort u} (p : α → Prop) :=
Exists (λ x, and (p x) (∀ y, p y → y = x))

attribute [pp_using_anonymous_constructor] sigma psigma subtype pprod and

class inductive decidable (p : Prop)
| is_false (h : ¬p) : decidable
| is_true  (h : p) : decidable

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

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

@[reducible]
def decidable_eq (α : Sort u) :=
decidable_rel (@eq α)

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

export option (none some)
export bool (ff tt)

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

notation h :: t  := list.cons h t
notation `[` l:(foldr `, ` (h t, list.cons h t) list.nil `]`) := l

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

/- Declare builtin and reserved notation -/

class has_zero     (α : Type u) := (zero : α)
class has_one      (α : Type u) := (one : α)
class has_add      (α : Type u) := (add : α → α → α)
class has_mul      (α : Type u) := (mul : α → α → α)
class has_inv      (α : Type u) := (inv : α → α)
class has_neg      (α : Type u) := (neg : α → α)
class has_sub      (α : Type u) := (sub : α → α → α)
class has_div      (α : Type u) := (div : α → α → α)
class has_dvd      (α : Type u) := (dvd : α → α → Prop)
class has_mod      (α : Type u) := (mod : α → α → α)
class has_le       (α : Type u) := (le : α → α → Prop)
class has_lt       (α : Type u) := (lt : α → α → Prop)
class has_append   (α : Type u) := (append : α → α → α)
class has_andthen  (α : Type u) (β : Type v) (σ : out_param $ Type w) := (andthen : α → β → σ)
class has_union    (α : Type u) := (union : α → α → α)
class has_inter    (α : Type u) := (inter : α → α → α)
class has_sdiff    (α : Type u) := (sdiff : α → α → α)
class has_equiv    (α : Sort u) := (equiv : α → α → Prop)
class has_subset   (α : Type u) := (subset : α → α → Prop)
class has_ssubset  (α : Type u) := (ssubset : α → α → Prop)
/- Type classes has_emptyc and has_insert are
   used to implement polymorphic notation for collections.
   Example: {a, b, c}. -/
class has_emptyc   (α : Type u) := (emptyc : α)
class has_insert   (α : out_param $ Type u) (γ : Type v) := (insert : α → γ → γ)
/- Type class used to implement the notation { a ∈ c | p a } -/
class has_sep (α : out_param $ Type u) (γ : Type v) :=
(sep : (α → Prop) → γ → γ)
/- Type class for set-like membership -/
class has_mem (α : out_param $ Type u) (γ : Type v) := (mem : α → γ → Prop)

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

export has_andthen (andthen)
export has_pow (pow)

infix ∈        := has_mem.mem
notation a ∉ s := ¬ has_mem.mem a s
infix +        := has_add.add
infix *        := has_mul.mul
infix -        := has_sub.sub
infix /        := has_div.div
infix ∣        := has_dvd.dvd
infix %        := has_mod.mod
prefix -       := has_neg.neg
infix <=       := has_le.le
infix ≤        := has_le.le
infix <        := has_lt.lt
infix ++       := has_append.append
infix ;        := andthen
notation `∅`   := has_emptyc.emptyc _
infix ∪        := has_union.union
infix ∩        := has_inter.inter
infix ⊆        := has_subset.subset
infix ⊂        := has_ssubset.ssubset
infix \        := has_sdiff.sdiff
infix ≈        := has_equiv.equiv
infixr ^       := has_pow.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
notation `∃!` binders `, ` r:(scoped P, exists_unique P) := r

export has_append (append)

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

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

@[reducible] def superset {α : Type u} [has_subset α] (a b : α) : Prop := has_subset.subset b a
@[reducible] def ssuperset {α : Type u} [has_ssubset α] (a b : α) : Prop := has_ssubset.ssubset b a

infix ⊇        := superset
infix ⊃        := ssuperset

def bit0 {α : Type u} [s  : has_add α] (a  : α)                 : α := a + a
def bit1 {α : Type u} [s₁ : has_one α] [s₂ : has_add α] (a : α) : α := (bit0 a) + 1

attribute [pattern] has_zero.zero has_one.one bit0 bit1 has_add.add has_neg.neg

def insert {α : Type u} {γ : Type v} [has_insert α γ] : α → γ → γ :=
has_insert.insert

/- The empty collection -/
def singleton {α : Type u} {γ : Type v} [has_emptyc γ] [has_insert α γ] (a : α) : γ :=
has_insert.insert a ∅

/- nat basic instances -/
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 : has_zero nat := ⟨nat.zero⟩

instance : has_one nat := ⟨nat.succ (nat.zero)⟩

instance : has_add 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.max_plus : nat := std.prec.max + 10

reserve postfix `⁻¹`:std.prec.max_plus  -- input with \sy or \-1 or \inv
postfix ⁻¹     := has_inv.inv

notation α × β := prod α β
-- notation for n-ary tuples

/- sizeof -/

class has_sizeof (α : Sort u) :=
(sizeof : α → nat)

def sizeof {α : Sort u} [s : has_sizeof α] : α → nat :=
has_sizeof.sizeof

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

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

instance default_has_sizeof (α : Sort u) : has_sizeof α :=
⟨default.sizeof α⟩

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

instance : has_sizeof nat :=
⟨nat.sizeof⟩

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

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

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

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

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

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

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

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

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

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

protected def punit.sizeof : punit → nat
| u := 1

instance : has_sizeof punit := ⟨punit.sizeof⟩

protected def bool.sizeof : bool → nat
| b := 1

instance : has_sizeof bool := ⟨bool.sizeof⟩

protected def option.sizeof {α : Type u} [has_sizeof α] : option α → nat
| none     := 1
| (some a) := 1 + sizeof a

instance (α : Type u) [has_sizeof α] : has_sizeof (option α) :=
⟨option.sizeof⟩

protected def list.sizeof {α : Type u} [has_sizeof α] : list α → nat
| list.nil        := 1
| (list.cons a l) := 1 + sizeof a + list.sizeof l

instance (α : Type u) [has_sizeof α] : has_sizeof (list α) :=
⟨list.sizeof⟩

protected def subtype.sizeof {α : Type u} [has_sizeof α] {p : α → Prop} : subtype p → nat
| ⟨a, _⟩ := sizeof a

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

theorem nat_add_zero (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

@[simp] theorem opt_param_eq (α : Sort u) (default : α) : opt_param α default = α := rfl

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

    bin_tree.node
      (bin_tree.node (bin_tree.leaf 1) (bin_tree.leaf 2))
      (bin_tree.node (bin_tree.leaf 3) (bin_tree.leaf 4))

    We use this notation to input long sequences without exhausting the system stack space.
    Later, we define a coercion from `bin_tree` into `list`.
-/
inductive bin_tree (α : Type u)
| empty {}       : bin_tree
| leaf (val : α) : bin_tree
| node (left right : bin_tree) : bin_tree

attribute [elab_simple] bin_tree.node bin_tree.leaf

/-- Like `by apply_instance`, but not dependent on the tactic framework. -/
@[reducible] def infer_instance {α : Type u} [i : α] : α := i
@[reducible, elab_simple] def infer_instance_as (α : Type u) [i : α] : α := i

/- Boolean operators -/

@[inline] def cond {a : Type u} : bool → a → a → a
| tt x y := x
| ff x y := y

@[inline] def bor : bool → bool → bool
| tt _  := tt
| ff tt := tt
| ff ff := ff

@[inline] def band : bool → bool → bool
| ff _  := ff
| tt ff := ff
| tt tt := tt

@[inline] def bnot : bool → bool
| tt := ff
| ff := tt

@[inline] def bxor : bool → bool → bool
| tt ff  := tt
| ff tt  := tt
| _  _   := ff

notation !x     := bnot x
notation x || y := bor x y
notation x && y := band x y

/- Logical connectives an equality -/

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

@[trans] 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 := ⟨⟩

@[inline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : ¬a) : b :=
false.rec b (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 not_false : ¬false := id

@[inline] def false.elim {C : Sort u} (h : false) : C :=
false.rec C h

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

@[simp] theorem id.def {α : Sort u} (a : α) : id a = a := rfl

@[inline] def eq.mp {α β : Sort u} (h₁ : α = β) (h₂ : α) : β :=
eq.rec_on h₁ h₂

@[inline] def eq.mpr {α β : Sort u} : (α = β) → β → α :=
λ h₁ h₂, eq.rec_on (eq.symm h₁) h₂

@[elab_as_eliminator]
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 congr_fun {α : Sort u} {β : α → Sort v} {f g : Π x, β x} (h : f = g) (a : α) : f a = g a :=
eq.subst h (eq.refl (f a))

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

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

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

theorem of_eq_true {p : Prop} (h : p = true) : p :=
h.symm ▸ trivial

theorem not_of_eq_false {p : Prop} (h : p = false) : ¬p :=
assume hp, h ▸ hp

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

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

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

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

@[simp] 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 false_of_ne : a ≠ a → false := ne.irrefl

theorem ne_false_of_self : p → p ≠ false :=
assume (hp : p) (heq : p = false), heq ▸ hp

theorem ne_true_of_not : ¬p → p ≠ true :=
assume (hnp : ¬p) (heq : p = true), (heq ▸ hnp) trivial

theorem true_ne_false : ¬true = false :=
ne_false_of_self trivial
end ne

attribute [refl] heq.refl

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

theorem heq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a == b) (h₂ : p a) : p b :=
eq.rec_on (eq_of_heq h₁) h₂

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

@[symm] theorem heq.symm (h : a == b) : b == a :=
heq.rec_on h (heq.refl a)

theorem heq_of_eq (h : a = a') : a == a' :=
eq.subst h (heq.refl a)

@[trans] theorem heq.trans (h₁ : a == b) (h₂ : b == c) : a == c :=
heq.subst h₂ h₁

@[trans] theorem heq_of_heq_of_eq (h₁ : a == b) (h₂ : b = b') : a == b' :=
heq.trans h₁ (heq_of_eq h₂)

@[trans] theorem heq_of_eq_of_heq (h₁ : a = a') (h₂ : a' == b) : a == b :=
heq.trans (heq_of_eq h₁) h₂

def type_eq_of_heq (h : a == b) : α = β :=
heq.rec_on h (eq.refl α)
end

theorem eq_rec_heq {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} (h : a = a') (p : φ a), (eq.rec_on h p : φ a') == p
| a _ rfl p := heq.refl p

theorem heq_of_eq_rec_left {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a = a') (h₂ : (eq.rec_on e p₁ : φ a') = p₂), p₁ == p₂
| a _ p₁ p₂ rfl h := eq.rec_on h (heq.refl p₁)

theorem heq_of_eq_rec_right {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a' = a) (h₂ : p₁ = eq.rec_on e p₂), p₁ == p₂
| a _ p₁ p₂ rfl h :=
  have p₁ = p₂, from h,
  this ▸ heq.refl p₁

theorem of_heq_true {a : Prop} (h : a == true) : a :=
of_eq_true (eq_of_heq h)

theorem eq_rec_compose : ∀ {α β φ : Sort u} (p₁ : β = φ) (p₂ : α = β) (a : α), (eq.rec_on p₁ (eq.rec_on p₂ a : β) : φ) = eq.rec_on (eq.trans p₂ p₁) a
| α _ _ rfl rfl a := rfl

theorem cast_heq : ∀ {α β : 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 non_contradictory_em (a : Prop) : ¬¬(a ∨ ¬a) :=
assume not_em : ¬(a ∨ ¬a),
  have neg_a : ¬a, from
    assume pos_a : a, absurd (or.inl pos_a) not_em,
  absurd (or.inr neg_a) not_em

def not_not_em := non_contradictory_em

theorem or.swap : a ∨ b → b ∨ a := or.rec or.inr or.inl

def or.symm := @or.swap

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

@[recursor 5]
theorem iff.elim : ((a → b) → (b → a) → c) → (a ↔ b) → c := iff.rec

theorem iff.elim_left : (a ↔ b) → a → b := iff.mp

theorem iff.elim_right : (a ↔ b) → b → a := iff.mpr

theorem iff_iff_implies_and_implies (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)

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

@[trans]
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))

@[symm]
theorem iff.symm (h : a ↔ b) : b ↔ a :=
iff.intro (iff.elim_right h) (iff.elim_left h)

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

theorem eq.to_iff {a b : Prop} (h : a = b) : a ↔ b :=
eq.rec_on h iff.rfl

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

theorem not_iff_not_of_iff (h₁ : a ↔ b) : ¬a ↔ ¬b :=
iff.intro
 (assume (hna : ¬ a) (hb : b), hna (iff.elim_right h₁ hb))
 (assume (hnb : ¬ b) (ha : a), hnb (iff.elim_left h₁ ha))

theorem of_iff_true (h : a ↔ true) : a :=
iff.mp (iff.symm h) trivial

theorem not_of_iff_false : (a ↔ false) → ¬a := iff.mp

theorem iff_true_intro (h : a) : a ↔ true :=
iff.intro
  (λ hl, trivial)
  (λ hr, h)

theorem iff_false_intro (h : ¬a) : a ↔ false :=
iff.intro h (false.rec a)

theorem imp_congr (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 imp_congr_ctx (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 imp_congr_right (h : a → (b ↔ c)) : (a → b) ↔ (a → c) :=
iff.intro
  (assume hab ha, iff.elim_left (h ha) (hab ha))
  (assume hab ha, iff.elim_right (h ha) (hab ha))

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

theorem not_of_not_not_not (h : ¬¬¬a) : ¬a :=
λ ha, absurd (not_not_intro ha) h

@[simp] theorem not_true : (¬ true) ↔ false :=
iff_false_intro (not_not_intro trivial)

def not_true_iff := not_true

@[simp] theorem not_false_iff : (¬ false) ↔ true :=
iff_true_intro not_false

@[congr] theorem not_congr (h : a ↔ b) : ¬a ↔ ¬b :=
iff.intro (λ h₁ h₂, h₁ (iff.mpr h h₂)) (λ h₁ h₂, h₁ (iff.mp h h₂))

@[simp] theorem ne_self_iff_false {α : Sort u} (a : α) : (not (a = a)) ↔ false :=
iff.intro false_of_ne false.elim

@[simp] theorem eq_self_iff_true {α : Sort u} (a : α) : (a = a) ↔ true :=
iff_true_intro rfl

@[simp] theorem heq_self_iff_true {α : Sort u} (a : α) : (a == a) ↔ true :=
iff_true_intro (heq.refl a)

@[simp] theorem iff_not_self (a : Prop) : (a ↔ ¬a) ↔ false :=
iff_false_intro (λ h,
   have h' : ¬a, from (λ ha, (iff.mp h ha) ha),
   h' (iff.mpr h h'))

@[simp] theorem not_iff_self (a : Prop) : (¬a ↔ a) ↔ false :=
iff_false_intro (λ h,
   have h' : ¬a, from (λ ha, (iff.mpr h ha) ha),
   h' (iff.mp h h'))

@[simp] theorem true_iff_false : (true ↔ false) ↔ false :=
iff_false_intro (λ h, iff.mp h trivial)

@[simp] theorem false_iff_true : (false ↔ true) ↔ false :=
iff_false_intro (λ h, iff.mpr h trivial)

theorem false_of_true_iff_false : (true ↔ false) → false :=
assume h, iff.mp h trivial

theorem false_of_true_eq_false : (true = false) → false :=
assume h, h ▸ trivial

theorem true_eq_false_of_false : false → (true = false) :=
false.elim

theorem eq_comm {α : 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 and_implies := @and.imp

@[congr] theorem and_congr (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 and_comm : a ∧ b ↔ b ∧ a :=
iff.intro and.swap and.swap

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

theorem and_left_comm : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) :=
iff.trans (iff.symm and_assoc) (iff.trans (and_congr and_comm (iff.refl c)) and_assoc)

@[simp] theorem and_true (a : Prop) : a ∧ true ↔ a :=
iff.intro and.left (λ ha, ⟨ha, trivial⟩)

@[simp] theorem true_and (a : Prop) : true ∧ a ↔ a :=
iff.intro and.right (λ h, ⟨trivial, h⟩)

@[simp] theorem and_false (a : Prop) : a ∧ false ↔ false :=
iff_false_intro and.right

@[simp] theorem false_and (a : Prop) : false ∧ a ↔ false :=
iff_false_intro and.left

@[simp] theorem not_and_self (a : Prop) : (¬a ∧ a) ↔ false :=
iff_false_intro (λ h, and.elim h (λ h₁ h₂, absurd h₂ h₁))

@[simp] theorem and_not_self (a : Prop) : (a ∧ ¬a) ↔ false :=
iff_false_intro (assume ⟨h₁, h₂⟩, absurd h₁ h₂)

@[simp] theorem and_self (a : Prop) : a ∧ a ↔ a :=
iff.intro and.left (assume h, ⟨h, h⟩)

/- or simp rules -/

@[congr] theorem or_congr (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 or_comm : a ∨ b ↔ b ∨ a := iff.intro or.swap or.swap

theorem or_assoc : (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 or_left_comm : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c) :=
iff.trans (iff.symm or_assoc) (iff.trans (or_congr or_comm (iff.refl c)) or_assoc)

@[simp] theorem or_true (a : Prop) : a ∨ true ↔ true :=
iff_true_intro (or.inr trivial)

@[simp] theorem true_or (a : Prop) : true ∨ a ↔ true :=
iff_true_intro (or.inl trivial)

@[simp] theorem or_false (a : Prop) : a ∨ false ↔ a :=
iff.intro (or.rec id false.elim) or.inl

@[simp] theorem false_or (a : Prop) : false ∨ a ↔ a :=
iff.trans or_comm (or_false a)

@[simp] theorem or_self (a : Prop) : a ∨ a ↔ a :=
iff.intro (or.rec id id) or.inl

theorem not_or {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 -/

def resolve_left {a b : Prop} (h : a ∨ b) (na : ¬ a) : b :=
or.elim h (λ ha, absurd ha na) id

def neg_resolve_left {a b : Prop} (h : ¬ a ∨ b) (ha : a) : b :=
or.elim h (λ na, absurd ha na) id

def resolve_right {a b : Prop} (h : a ∨ b) (nb : ¬ b) : a :=
or.elim h id (λ hb, absurd hb nb)

def neg_resolve_right {a b : Prop} (h : a ∨ ¬ b) (hb : b) : a :=
or.elim h id (λ nb, absurd hb nb)

/- iff simp rules -/

@[simp] theorem iff_true (a : Prop) : (a ↔ true) ↔ a :=
iff.intro (assume h, iff.mpr h trivial) iff_true_intro

@[simp] theorem true_iff (a : Prop) : (true ↔ a) ↔ a :=
iff.trans iff.comm (iff_true a)

@[simp] theorem iff_false (a : Prop) : (a ↔ false) ↔ ¬ a :=
iff.intro iff.mp iff_false_intro

@[simp] theorem false_iff (a : Prop) : (false ↔ a) ↔ ¬ a :=
iff.trans iff.comm (iff_false a)

@[simp] theorem iff_self (a : Prop) : (a ↔ a) ↔ true :=
iff_true_intro iff.rfl

@[congr] theorem iff_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ↔ b) ↔ (c ↔ d) :=
(iff_iff_implies_and_implies a b).trans
  ((and_congr (imp_congr h₁ h₂) (imp_congr h₂ h₁)).trans
    (iff_iff_implies_and_implies c d).symm)

/- implies simp rule -/
@[simp] theorem implies_true_iff (α : Sort u) : (α → true) ↔ true :=
iff.intro (λ h, trivial) (λ ha h, trivial)

@[simp] theorem false_implies_iff (a : Prop) : (false → a) ↔ true :=
iff.intro (λ h, trivial) (λ ha h, false.elim h)

@[simp] theorem true_implies_iff (α : 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 unique -/

theorem exists_unique.intro {α : Sort u} {p : α → Prop} (w : α) (h₁ : p w) (h₂ : ∀ y, p y → y = w) :
  ∃! x, p x :=
exists.intro w ⟨h₁, h₂⟩

attribute [recursor 4]
theorem exists_unique.elim {α : Sort u} {p : α → Prop} {b : Prop}
    (h₂ : ∃! x, p x) (h₁ : ∀ x, p x → (∀ y, p y → y = x) → b) : b :=
exists.elim h₂ (λ w hw, h₁ w (and.left hw) (and.right hw))

theorem exists_unique_of_exists_of_unique {α : Type u} {p : α → Prop}
    (hex : ∃ x, p x) (hunique : ∀ y₁ y₂, p y₁ → p y₂ → y₁ = y₂) :  ∃! x, p x :=
exists.elim hex (λ x px, exists_unique.intro x px (assume y, assume : p y, hunique y x this px))

theorem exists_of_exists_unique {α : Sort u} {p : α → Prop} (h : ∃! x, p x) : ∃ x, p x :=
exists.elim h (λ x hx, ⟨x, and.left hx⟩)

theorem unique_of_exists_unique {α : Sort u} {p : α → Prop}
    (h : ∃! x, p x) {y₁ y₂ : α} (py₁ : p y₁) (py₂ : p y₂) : y₁ = y₂ :=
exists_unique.elim h
  (assume x, assume : p x,
    assume unique : ∀ y, p y → y = x,
    show y₁ = y₂, from eq.trans (unique _ py₁) (eq.symm (unique _ py₂)))

/- exists, forall, exists unique congruences -/
@[congr] theorem forall_congr {α : 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 exists_imp_exists {α : 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⟩)

@[congr] theorem exists_congr {α : Sort u} {p q : α → Prop} (h : ∀ a, (p a ↔ q a)) : (Exists p) ↔ ∃ a, q a :=
iff.intro
  (exists_imp_exists (λ a, iff.mp (h a)))
  (exists_imp_exists (λ a, iff.mpr (h a)))

@[congr] theorem exists_unique_congr {α : Sort u} {p₁ p₂ : α → Prop} (h : ∀ x, p₁ x ↔ p₂ x) : (exists_unique p₁) ↔ (∃! x, p₂ x) := --
exists_congr (λ x, and_congr (h x) (forall_congr (λ y, imp_congr (h y) iff.rfl)))

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

/- Decidable -/

def decidable.to_bool (p : Prop) [h : decidable p] : bool :=
decidable.cases_on h (λ h₁, bool.ff) (λ h₂, bool.tt)

export decidable (is_true is_false to_bool)

@[simp] theorem to_bool_true_eq_tt (h : decidable true) : @to_bool true h = tt :=
decidable.cases_on h (λ h, false.elim (iff.mp not_true h)) (λ _, rfl)

@[simp] theorem to_bool_false_eq_ff (h : decidable false) : @to_bool false h = ff :=
decidable.cases_on h (λ h, rfl) (λ h, false.elim h)

instance : decidable true :=
is_true trivial

instance : decidable false :=
is_false not_false

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

/- if-then-else -/

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

namespace decidable
variables {p q : Prop}

def rec_on_true [h : decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : p) (h₄ : h₁ h₃)
    : (decidable.rec_on h h₂ h₁ : Sort u) :=
decidable.rec_on h (λ h, false.rec _ (h h₃)) (λ h, h₄)

def rec_on_false [h : decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : ¬p) (h₄ : h₂ h₃)
    : (decidable.rec_on h h₂ h₁ : Sort u) :=
decidable.rec_on h (λ h, h₄) (λ h, false.rec _ (h₃ h))

def by_cases {q : Sort u} [s : decidable p] (h1 : p → q) (h2 : ¬p → q) : q :=
match s with
| is_true h  := h1 h
| is_false h := h2 h
end

theorem em (p : Prop) [decidable p] : p ∨ ¬p :=
by_cases or.inl or.inr

theorem by_contradiction [decidable p] (h : ¬p → false) : p :=
by_cases id (λ np : ¬p, false.elim (h np))

theorem of_not_not [decidable p] : ¬ ¬ p → p :=
λ hnn, by_contradiction (λ hn, absurd hn hnn)

theorem not_not_iff (p) [decidable p] : (¬ ¬ p) ↔ p :=
iff.intro of_not_not not_not_intro

theorem not_and_iff_or_not (p q : Prop) [d₁ : decidable p] [d₂ : decidable q] : ¬ (p ∧ q) ↔ ¬ p ∨ ¬ q :=
iff.intro
(λ h, match d₁ with
      | is_true h₁  :=
        match d₂ with
        | is_true h₂  := absurd (and.intro h₁ h₂) h
        | is_false h₂ := or.inr h₂
        end
      | is_false h₁ := or.inl h₁
      end)
(λ h ⟨hp, hq⟩, or.elim h (λ h, h hp) (λ h, h hq))

theorem not_or_iff_and_not (p q) [d₁ : decidable p] [d₂ : decidable q] : ¬ (p ∨ q) ↔ ¬ p ∧ ¬ q :=
iff.intro
  (λ h, match d₁ with
        | is_true h₁  := false.elim $ h (or.inl h₁)
        | is_false h₁ :=
          match d₂ with
          | is_true h₂  := false.elim $ h (or.inr h₂)
          | is_false h₂ := ⟨h₁, h₂⟩
          end
        end)
  (λ ⟨np, nq⟩ h, or.elim h np nq)
end decidable

section
variables {p q : Prop}
def  decidable_of_decidable_of_iff (hp : decidable p) (h : p ↔ q) : decidable q :=
if hp : p then is_true (iff.mp h hp)
else is_false (iff.mp (not_iff_not_of_iff h) hp)

def  decidable_of_decidable_of_eq (hp : decidable p) (h : p = q) : decidable q :=
decidable_of_decidable_of_iff hp h.to_iff

protected def or.by_cases [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}

instance [decidable p] [decidable q] : decidable (p ∧ q) :=
if hp : p then
  if hq : q then is_true ⟨hp, hq⟩
  else is_false (assume h : p ∧ q, hq (and.right h))
else is_false (assume h : p ∧ q, hp (and.left h))

instance [decidable p] [decidable q] : decidable (p ∨ q) :=
if hp : p then is_true (or.inl hp) else
  if hq : q then is_true (or.inr hq) else
    is_false (or.rec hp hq)

instance [decidable p] : decidable (¬p) :=
if hp : p then is_false (absurd hp) else is_true hp

instance implies.decidable [decidable p] [decidable q] : decidable (p → q) :=
if hp : p then
  if hq : q then is_true (assume h, hq)
  else is_false (assume h : p → q, absurd (h hp) hq)
else is_true (assume h, absurd h hp)

instance [decidable p] [decidable q] : decidable (p ↔ q) :=
if hp : p then
  if hq : q then is_true ⟨λ_, hq, λ_, hp⟩
  else is_false $ λh, hq (h.1 hp)
else
  if hq : q then is_false $ λh, hp (h.2 hq)
  else is_true $ ⟨λ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 is_false (or.rec (λ ⟨_, h⟩, h hq : ¬(p ∧ ¬ q)) (λ ⟨_, h⟩, h hp : ¬(q ∧ ¬ p)))
  else is_true $ or.inl ⟨hp, hq⟩
else
  if hq : q then is_true $ or.inr ⟨hq, hp⟩
  else is_false (or.rec (λ ⟨h, _⟩, hp h : ¬(p ∧ ¬ q)) (λ ⟨h, _⟩, hq h : ¬(q ∧ ¬ p)))

instance exists_prop_decidable {p} (P : p → Prop) [decidable p] [s : ∀ h, decidable (P h)] : decidable (∃ h, P h) :=
if h : p then decidable_of_decidable_of_iff (s h)
  ⟨λ h2, ⟨h, h2⟩, λ ⟨h', h2⟩, h2⟩ else is_false (mt (λ ⟨h, _⟩, h) h)

instance forall_prop_decidable {p} (P : p → Prop)
  [Dp : decidable p] [DP : ∀ h, decidable (P h)] : decidable (∀ h, P h) :=
if h : p then decidable_of_decidable_of_iff (DP h)
  ⟨λ h2 _, h2, λal, al h⟩ else is_true (λ h2, absurd h2 h)
end

instance {α : Sort u} [decidable_eq α] (a b : α) : decidable (a ≠ b) :=
implies.decidable

theorem bool.ff_ne_tt : ff = tt → false
.

def is_dec_eq {α : Sort u} (p : α → α → bool) : Prop   := ∀ ⦃x y : α⦄, p x y = tt → x = y
def is_dec_refl {α : Sort u} (p : α → α → bool) : Prop := ∀ x, p x x = tt

instance : decidable_eq bool
| ff ff := is_true rfl
| ff tt := is_false bool.ff_ne_tt
| tt ff := is_false (ne.symm bool.ff_ne_tt)
| tt tt := is_true rfl

def decidable_eq_of_bool_pred {α : Sort u} {p : α → α → bool} (h₁ : is_dec_eq p) (h₂ : is_dec_refl p) : decidable_eq α :=
assume x y : α,
 if hp : p x y = tt then is_true (h₁ hp)
 else is_false (assume hxy : x = y, absurd (h₂ y) (@eq.rec_on _ _ (λ z, ¬p z y = tt) _ hxy hp))

theorem decidable_eq_inl_refl {α : Sort u} [h : decidable_eq α] (a : α) : h a a = is_true (eq.refl a) :=
match (h a a) with
| (is_true e)  := rfl
| (is_false n) := absurd rfl n
end

theorem decidable_eq_inr_neg {α : Sort u} [h : decidable_eq α] {a b : α} : Π n : a ≠ b, h a b = is_false n :=
assume n,
match (h a b) with
| (is_true e)   := absurd e n
| (is_false n₁) := proof_irrel n n₁ ▸ eq.refl (is_false n)
end

/- if-then-else expression theorems -/

theorem if_pos {c : Prop} [h : decidable c] (hc : c) {α : Sort u} {t e : α} : (ite c t e) = t :=
match h with
| (is_true  hc)  := rfl
| (is_false hnc) := absurd hc hnc
end

theorem if_neg {c : Prop} [h : decidable c] (hnc : ¬c) {α : Sort u} {t e : α} : (ite c t e) = e :=
match h with
| (is_true hc)   := absurd hc hnc
| (is_false hnc) := rfl
end

@[simp]
theorem if_t_t (c : Prop) [h : decidable c] {α : Sort u} (t : α) : (ite c t t) = t :=
match h with
| (is_true hc)   := rfl
| (is_false hnc) := rfl
end

theorem implies_of_if_pos {c t e : Prop} [decidable c] (h : ite c t e) : c → t :=
assume hc, eq.rec_on (if_pos hc : ite c t e = t) h

theorem implies_of_if_neg {c t e : Prop} [decidable c] (h : ite c t e) : ¬c → e :=
assume hnc, eq.rec_on (if_neg hnc : ite c t e = e) h

theorem if_ctx_congr {α : Sort u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c]
                   {x y u v : α}
                   (h_c : b ↔ c) (h_t : c → x = u) (h_e : ¬c → y = v) :
        ite b x y = ite c u v :=
match dec_b, dec_c with
| (is_false h₁), (is_false h₂) := h_e h₂
| (is_true h₁),  (is_true h₂)  := h_t h₂
| (is_false h₁), (is_true h₂)  := absurd h₂ (iff.mp (not_iff_not_of_iff h_c) h₁)
| (is_true h₁),  (is_false h₂) := absurd h₁ (iff.mpr (not_iff_not_of_iff h_c) h₂)
end

@[congr]
theorem if_congr {α : Sort u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c]
               {x y u v : α}
               (h_c : b ↔ c) (h_t : x = u) (h_e : y = v) :
        ite b x y = ite c u v :=
@if_ctx_congr α b c dec_b dec_c x y u v h_c (λ h, h_t) (λ h, h_e)

theorem if_ctx_simp_congr {α : Sort u} {b c : Prop} [dec_b : decidable b] {x y u v : α}
                        (h_c : b ↔ c) (h_t : c → x = u) (h_e : ¬c → y = v) :
        ite b x y = (@ite c (decidable_of_decidable_of_iff dec_b h_c) α u v) :=
@if_ctx_congr α b c dec_b (decidable_of_decidable_of_iff dec_b h_c) x y u v h_c h_t h_e

@[congr]
theorem if_simp_congr {α : Sort u} {b c : Prop} [dec_b : decidable b] {x y u v : α}
                    (h_c : b ↔ c) (h_t : x = u) (h_e : y = v) :
        ite b x y = (@ite c (decidable_of_decidable_of_iff dec_b h_c) α u v) :=
@if_ctx_simp_congr α b c dec_b x y u v h_c (λ h, h_t) (λ h, h_e)

@[simp]
theorem if_true {α : Sort u} {h : decidable true} (t e : α) : (@ite true h α t e) = t :=
if_pos trivial

@[simp]
theorem if_false {α : Sort u} {h : decidable false} (t e : α) : (@ite false h α t e) = e :=
if_neg not_false

theorem if_ctx_congr_prop {b c x y u v : Prop} [dec_b : decidable b] [dec_c : decidable c]
                      (h_c : b ↔ c) (h_t : c → (x ↔ u)) (h_e : ¬c → (y ↔ v)) :
        ite b x y ↔ ite c u v :=
match dec_b, dec_c with
| (is_false h₁), (is_false h₂) := h_e h₂
| (is_true h₁),  (is_true h₂)  := h_t h₂
| (is_false h₁), (is_true h₂)  := absurd h₂ (iff.mp (not_iff_not_of_iff h_c) h₁)
| (is_true h₁),  (is_false h₂) := absurd h₁ (iff.mpr (not_iff_not_of_iff h_c) h₂)
end

@[congr]
theorem if_congr_prop {b c x y u v : Prop} [dec_b : decidable b] [dec_c : decidable c]
                    (h_c : b ↔ c) (h_t : x ↔ u) (h_e : y ↔ v) :
        ite b x y ↔ ite c u v :=
if_ctx_congr_prop h_c (λ h, h_t) (λ h, h_e)

theorem if_ctx_simp_congr_prop {b c x y u v : Prop} [dec_b : decidable b]
                               (h_c : b ↔ c) (h_t : c → (x ↔ u)) (h_e : ¬c → (y ↔ v)) :
        ite b x y ↔ (@ite c (decidable_of_decidable_of_iff dec_b h_c) Prop u v) :=
@if_ctx_congr_prop b c x y u v dec_b (decidable_of_decidable_of_iff dec_b h_c) h_c h_t h_e

@[congr]
theorem if_simp_congr_prop {b c x y u v : Prop} [dec_b : decidable b]
                           (h_c : b ↔ c) (h_t : x ↔ u) (h_e : y ↔ v) :
        ite b x y ↔ (@ite c (decidable_of_decidable_of_iff dec_b h_c) Prop u v) :=
@if_ctx_simp_congr_prop b c x y u v dec_b h_c (λ h, h_t) (λ h, h_e)

@[simp] theorem dif_pos {c : Prop} [h : decidable c] (hc : c) {α : Sort u} {t : c → α} {e : ¬ c → α} : dite c t e = t hc :=
match h with
| (is_true hc)   := rfl
| (is_false hnc) := absurd hc hnc
end

@[simp] theorem dif_neg {c : Prop} [h : decidable c] (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬ c → α} : dite c t e = e hnc :=
match h with
| (is_true hc)   := absurd hc hnc
| (is_false hnc) := rfl
end

theorem dif_ctx_congr {α : Sort u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c]
                    {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
                    (h_c : b ↔ c)
                    (h_t : ∀ (h : c),    x (iff.mpr h_c h)                      = u h)
                    (h_e : ∀ (h : ¬c),   y (iff.mpr (not_iff_not_of_iff h_c) h) = v h) :
        (@dite b dec_b α x y) = (@dite c dec_c α u v) :=
match dec_b, dec_c with
| (is_false h₁), (is_false h₂) := h_e h₂
| (is_true h₁),  (is_true h₂)  := h_t h₂
| (is_false h₁), (is_true h₂)  := absurd h₂ (iff.mp (not_iff_not_of_iff h_c) h₁)
| (is_true h₁),  (is_false h₂) := absurd h₁ (iff.mpr (not_iff_not_of_iff h_c) h₂)
end

theorem dif_ctx_simp_congr {α : Sort u} {b c : Prop} [dec_b : decidable b]
                         {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
                         (h_c : b ↔ c)
                         (h_t : ∀ (h : c),    x (iff.mpr h_c h)                      = u h)
                         (h_e : ∀ (h : ¬c),   y (iff.mpr (not_iff_not_of_iff h_c) h) = v h) :
        (@dite b dec_b α x y) = (@dite c (decidable_of_decidable_of_iff dec_b h_c) α u v) :=
@dif_ctx_congr α b c dec_b (decidable_of_decidable_of_iff dec_b h_c) x u y v h_c h_t h_e

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

instance {c t e : Prop} [d_c : decidable c] [d_t : decidable t] [d_e : decidable e] : decidable (if c then t else e)  :=
match d_c with
| (is_true hc)  := d_t
| (is_false hc) := d_e
end

instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [d_c : decidable c] [d_t : ∀ h, decidable (t h)] [d_e : ∀ h, decidable (e h)] : decidable (if h : c then t h else e h)  :=
match d_c with
| (is_true hc)  := d_t hc
| (is_false hc) := d_e hc
end

def as_true (c : Prop) [decidable c] : Prop :=
if c then true else false

def as_false (c : Prop) [decidable c] : Prop :=
if c then false else true

def of_as_true {c : Prop} [h₁ : decidable c] (h₂ : as_true c) : c :=
match h₁, h₂ with
| (is_true h_c),  h₂ := h_c
| (is_false h_c), h₂ := false.elim h₂
end

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

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

theorem down_up {α : 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 up_down {α : Sort u} : ∀ (b : plift α), up (down b) = b
| (up a) := rfl

theorem down_up {α : Sort u} (a : α) : down (up a) = a := rfl
end plift

/- inhabited -/

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

def 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.rec_on h (λ b, ⟨λ a, b⟩)

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

instance : inhabited bool := ⟨ff⟩

instance : inhabited true := ⟨trivial⟩

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 nonempty_of_inhabited {α : Sort u} [inhabited α] : nonempty α :=
⟨default α⟩

theorem nonempty_of_exists {α : 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.rec (λ p, p) h

protected def subsingleton.helim {α β : Sort u} [h : subsingleton α] (h : α = β) : ∀ (a : α) (b : β), a == b :=
eq.rec_on h (λ a b : α, heq_of_eq (subsingleton.elim a b))

instance subsingleton_prop (p : Prop) : subsingleton p :=
⟨λ a b, proof_irrel a b⟩

instance (p : Prop) : subsingleton (decidable p) :=
subsingleton.intro (λ d₁,
  match d₁ with
  | (is_true t₁) := (λ d₂,
    match d₂ with
    | (is_true t₂) := eq.rec_on (proof_irrel t₁ t₂) rfl
    | (is_false f₂) := absurd t₁ f₂
    end)
  | (is_false f₁) := (λ d₂,
    match d₂ with
    | (is_true t₂) := absurd t₂ f₁
    | (is_false f₂) := eq.rec_on (proof_irrel f₁ f₂) rfl
    end)
  end)

protected theorem rec_subsingleton {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.rec_on h h₂ h₁) :=
match h with
| (is_true h)  := h₃ h
| (is_false h) := h₄ h
end

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

theorem let_value_heq {α : 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.rec_on h (heq.refl (b a₁))

theorem let_body_eq {α : 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 let_eq {α : 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.rec_on 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 mk_equivalence (rfl : reflexive r) (symm : symmetric r) (trans : transitive r) : equivalence r :=
⟨rfl, symm, trans⟩

def irreflexive := ∀ x, ¬ x ≺ x

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

def empty_relation := λ a₁ a₂ : α, false

def subrelation (q r : β → β → Prop) := ∀ ⦃x y⦄, q x y → r x y

def inv_image (f : α → β) : α → α → Prop :=
λ a₁ a₂, f a₁ ≺ f a₂

theorem inv_image.trans (f : α → β) (h : transitive r) : transitive (inv_image r f) :=
λ (a₁ a₂ a₃ : α) (h₁ : inv_image r f a₁ a₂) (h₂ : inv_image r f a₂ a₃), h h₁ h₂

theorem inv_image.irreflexive (f : α → β) (h : irreflexive r) : irreflexive (inv_image r f) :=
λ (a : α) (h₁ : inv_image 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
end relation

section binary
variables {α : Type u} {β : Type v}
variable f : α → α → α
variable inv : α → α
variable one : α
local notation a * b := f a b
local notation a ⁻¹  := inv a
variable g : α → α → α
local notation a + b := g a b

def commutative        := ∀ a b, a * b = b * a
def associative        := ∀ a b c, (a * b) * c = a * (b * c)
def left_identity      := ∀ a, one * a = a
def right_identity     := ∀ a, a * one = a
def right_inverse      := ∀ a, a * a⁻¹ = one
def left_cancelative   := ∀ a b c, a * b = a * c → b = c
def right_cancelative  := ∀ a b c, a * b = c * b → a = c
def left_distributive  := ∀ a b c, a * (b + c) = a * b + a * c
def right_distributive := ∀ a b c, (a + b) * c = a * c + b * c
def right_commutative (h : β → α → β) := ∀ b a₁ a₂, h (h b a₁) a₂ = h (h b a₂) a₁
def left_commutative  (h : α → β → β) := ∀ a₁ a₂ b, h a₁ (h a₂ b) = h a₂ (h a₁ b)

theorem left_comm : commutative f → associative f → left_commutative f :=
assume hcomm hassoc, assume a b c, calc
  a*(b*c) = (a*b)*c  : eq.symm (hassoc a b c)
    ...   = (b*a)*c  : hcomm a b ▸ rfl
    ...   = b*(a*c)  : hassoc b a c

theorem right_comm : commutative f → associative f → right_commutative f :=
assume hcomm hassoc, assume a b c, calc
  (a*b)*c = a*(b*c) : hassoc a b c
    ...   = a*(c*b) : hcomm b c ▸ rfl
    ...   = (a*c)*b : eq.symm (hassoc a c b)
end binary

/- Subtype -/

namespace subtype
def exists_of_subtype {α : Type u} {p : α → Prop} : { x // p x } → ∃ x, p x
| ⟨a, h⟩ := ⟨a, h⟩

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

theorem tag_irrelevant {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

@[simp] 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} [decidable_eq α] : decidable_eq {x : α // p x}
| ⟨a, h₁⟩ ⟨b, h₂⟩ :=
  if h : a = b then is_true (subtype.eq h)
  else is_false (λ h', subtype.no_confusion h' (λ h', absurd h' h))
end subtype

/- Sum -/

notation α ⊕ β := sum α β

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

instance sum.inhabited_left [h : inhabited α] : inhabited (α ⊕ β) :=
⟨sum.inl (default α)⟩

instance sum.inhabited_right [h : inhabited β] : inhabited (α ⊕ β) :=
⟨sum.inr (default β)⟩

instance {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] : decidable_eq (α ⊕ β)
| (sum.inl a) (sum.inl b) := if h : a = b then is_true (h ▸ rfl)
                             else is_false (λ h', sum.no_confusion h' (λ h', absurd h' h))
| (sum.inr a) (sum.inr b) := if h : a = b then is_true (h ▸ rfl)
                             else is_false (λ h', sum.no_confusion h' (λ h', absurd h' h))
| (sum.inr a) (sum.inl b) := is_false (λ h, sum.no_confusion h)
| (sum.inl a) (sum.inr b) := is_false (λ h, sum.no_confusion h)
end

/- Product -/

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

@[simp] theorem prod.mk.eta : ∀{p : α × β}, (p.1, p.2) = p
| (a, b) := rfl

instance [inhabited α] [inhabited β] : inhabited (prod α β) :=
⟨(default α, default β)⟩

instance [h₁ : decidable_eq α] [h₂ : decidable_eq β] : decidable_eq (α × β)
| (a, b) (a', b') :=
  match (h₁ a a') with
  | (is_true e₁) :=
    match (h₂ b b') with
    | (is_true e₂)  := is_true (eq.rec_on e₁ (eq.rec_on e₂ rfl))
    | (is_false n₂) := is_false (assume h, prod.no_confusion h (λ e₁' e₂', absurd e₂' n₂))
    end
  | (is_false n₁) := is_false (assume h, prod.no_confusion h (λ e₁' e₂', absurd e₁' n₁))
  end

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

instance prod_has_decidable_lt
         [has_lt α] [has_lt β]
         [decidable_eq α] [decidable_eq β]
         [decidable_rel ((<) : α → α → Prop)]
         [decidable_rel ((<) : β → β → Prop)] : Π s t : α × β, decidable (s < t) :=
λ t s, or.decidable

theorem prod.lt_def [has_lt α] [has_lt β] (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 ex_of_psig {α : 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.rec_on 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.rec_on h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂
| ⟨a, b⟩ ⟨.(a), .(b)⟩ rfl rfl := rfl
end

/- Universe polymorphic unit -/

theorem punit_eq (a b : punit) : a = b :=
punit.rec_on a (punit.rec_on b rfl)

theorem punit_eq_punit (a : punit) : a = () :=
punit_eq a ()

instance : subsingleton punit :=
subsingleton.intro punit_eq

instance : inhabited punit :=
⟨()⟩

instance : decidable_eq punit :=
λ a b, is_true (punit_eq a b)

/- Setoid -/

class setoid (α : Sort u) :=
(r : α → α → Prop) (iseqv : equivalence r)

instance setoid_has_equiv {α : Sort u} [setoid α] : has_equiv α :=
⟨setoid.r⟩

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

@[refl] theorem refl (a : α) : a ≈ a :=
match setoid.iseqv α with
| ⟨h_refl, h_symm, h_trans⟩ := h_refl a
end

@[symm] theorem symm {a b : α} (hab : a ≈ b) : b ≈ a :=
match setoid.iseqv α with
| ⟨h_refl, h_symm, h_trans⟩ := h_symm hab
end

@[trans] theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c :=
match setoid.iseqv α with
| ⟨h_refl, h_symm, h_trans⟩ := h_trans hab hbc
end
end setoid

/- Propositional extensionality -/

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

/- Additional congruence theorems. -/

theorem forall_congr_eq {a : Sort u} {p q : a → Prop} (h : ∀ x, p x = q x) : (∀ x, p x) = ∀ x, q x :=
propext (forall_congr (λ a, (h a).to_iff))

theorem imp_congr_eq {a b c d : Prop} (h₁ : a = c) (h₂ : b = d) : (a → b) = (c → d) :=
propext (imp_congr h₁.to_iff h₂.to_iff)

theorem imp_congr_ctx_eq {a b c d : Prop} (h₁ : a = c) (h₂ : c → (b = d)) : (a → b) = (c → d) :=
propext (imp_congr_ctx h₁.to_iff (λ hc, (h₂ hc).to_iff))

theorem eq_true_intro {a : Prop} (h : a) : a = true :=
propext (iff_true_intro h)

theorem eq_false_intro {a : Prop} (h : ¬a) : a = false :=
propext (iff_false_intro h)

theorem iff.to_eq {a b : Prop} (h : a ↔ b) : a = b :=
propext h

theorem iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b) :=
propext (iff.intro
  (assume h, iff.to_eq h)
  (assume h, h.to_iff))

theorem eq_false {a : Prop} : (a = false) = (¬ a) :=
have (a ↔ false) = (¬ a), from propext (iff_false a),
eq.subst (@iff_eq_eq a false) this

theorem eq_true {a : Prop} : (a = true) = a :=
have (a ↔ true) = a, from propext (iff_true a),
eq.subst (@iff_eq_eq a true) this

/- Quotients -/

-- iff can now be used to do substitutions in a calculation
@[subst] theorem iff_subst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) : p b :=
eq.subst (propext h₁) h₂

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

attribute [elab_as_eliminator] lift ind

protected theorem lift_beta {α : 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 ind_beta {α : 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, elab_as_eliminator]
protected def lift_on {α : Sort u} {β : Sort v} {r : α → α → Prop} (q : quot r) (f : α → β) (c : ∀ a b, r a b → f a = f b) : β :=
lift f c q

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

theorem exists_rep {α : Sort u} {r : α → α → Prop} (q : quot r) : ∃ a : α, (quot.mk r a) = q :=
quot.induction_on 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]
protected def indep (f : Π a, β ⟦a⟧) (a : α) : psigma β :=
⟨⟦a⟧, f a⟩

protected theorem indep_coherent (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 lift_indep_pr1
  (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.indep_coherent f h) q).1 = q  :=
quot.ind (λ (a : α), eq.refl (quot.indep f a).1) q

@[reducible, elab_as_eliminator]
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.rec_on (quot.lift_indep_pr1 f h q) ((lift (quot.indep f) (quot.indep_coherent f h) q).2)

@[reducible, elab_as_eliminator]
protected def rec_on
   (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, elab_as_eliminator]
protected def rec_on_subsingleton
   [h : ∀ a, subsingleton (β ⟦a⟧)] (q : quot r) (f : Π a, β ⟦a⟧) : β q :=
quot.rec f (λ a b h, subsingleton.elim _ (f b)) q

@[reducible, elab_as_eliminator]
protected def hrec_on
   (q : quot r) (f : Π a, β ⟦a⟧) (c : ∀ (a b : α) (p : r a b), f a == f b) : β q :=
quot.rec_on q f
  (λ a b p, eq_of_heq (calc
    (eq.rec (f a) (sound p) : β ⟦b⟧) == f a : eq_rec_heq (sound p) (f a)
                                 ... == f b : c a b p))
end
end quot

def quotient {α : Sort u} (s : setoid α) :=
@quot α setoid.r

namespace quotient

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, elab_as_eliminator]
protected def lift {α : Sort u} {β : Sort v} [s : setoid α] (f : α → β) : (∀ a b, a ≈ b → f a = f b) → quotient s → β :=
quot.lift f

@[elab_as_eliminator]
protected theorem ind {α : Sort u} [s : setoid α] {β : quotient s → Prop} : (∀ a, β ⟦a⟧) → ∀ q, β q :=
quot.ind

@[reducible, elab_as_eliminator]
protected def lift_on {α : Sort u} {β : Sort v} [s : setoid α] (q : quotient s) (f : α → β) (c : ∀ a b, a ≈ b → f a = f b) : β :=
quot.lift_on q f c

@[elab_as_eliminator]
protected theorem induction_on {α : Sort u} [s : setoid α] {β : quotient s → Prop} (q : quotient s) (h : ∀ a, β ⟦a⟧) : β q :=
quot.induction_on q h

theorem exists_rep {α : Sort u} [s : setoid α] (q : quotient s) : ∃ a : α, ⟦a⟧ = q :=
quot.exists_rep q

section
variable {α : Sort u}
variable [s : setoid α]
variable {β : quotient s → Sort v}

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, elab_as_eliminator]
protected def rec_on
   (q : quotient s) (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : a ≈ b), (eq.rec (f a) (quotient.sound p) : β ⟦b⟧) = f b) : β q :=
quot.rec_on q f h

@[reducible, elab_as_eliminator]
protected def rec_on_subsingleton
   [h : ∀ a, subsingleton (β ⟦a⟧)] (q : quotient s) (f : Π a, β ⟦a⟧) : β q :=
@quot.rec_on_subsingleton _ _ _ h q f

@[reducible, elab_as_eliminator]
protected def hrec_on
   (q : quotient s) (f : Π a, β ⟦a⟧) (c : ∀ (a b : α) (p : a ≈ b), f a == f b) : β q :=
quot.hrec_on q f c
end

section
universes u_a u_b u_c
variables {α : Sort u_a} {β : Sort u_b} {φ : Sort u_c}
variables [s₁ : setoid α] [s₂ : setoid β]
include s₁ s₂

@[reducible, elab_as_eliminator]
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₂
       (λ (a_1 : quotient s₂),
          (quotient.lift (f a) (λ (a_1 b : β), c a a_1 a b (setoid.refl a)) a_1)
          =
          (quotient.lift (f b) (λ (a b_1 : β), c b a b b_1 (setoid.refl b)) a_1))
       (λ (a' : β), c a a' b a' h (setoid.refl a'))
       q₂)
  q₁

@[reducible, elab_as_eliminator]
protected def lift_on₂
  (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₂

@[elab_as_eliminator]
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₁

@[elab_as_eliminator]
protected theorem induction_on₂
   {φ : 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₁

@[elab_as_eliminator]
protected theorem induction_on₃
   [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.lift_on₂ 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.induction_on q (λ a, setoid.refl a)

private theorem eq_imp_rel {q₁ q₂ : quotient s} : q₁ = q₂ → q₁ ~ q₂ :=
assume h, eq.rec_on h (rel.refl q₁)

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

section
universes u_a u_b u_c
variables {α : Sort u_a} {β : Sort u_b}
variables [s₁ : setoid α] [s₂ : setoid β]
include s₁ s₂

@[reducible, elab_as_eliminator]
protected def rec_on_subsingleton₂
   {φ : quotient s₁ → quotient s₂ → Sort u_c} [h : ∀ a b, subsingleton (φ ⟦a⟧ ⟦b⟧)]
   (q₁ : quotient s₁) (q₂ : quotient s₂) (f : Π a b, φ ⟦a⟧ ⟦b⟧) : φ q₁ q₂:=
@quotient.rec_on_subsingleton _ s₁ (λ q, φ q q₂) (λ a, quotient.ind (λ b, h a b) q₂) q₁
  (λ a, quotient.rec_on_subsingleton q₂ (λ b, f a b))

end
end quotient

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

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

theorem eqv_gen.is_equivalence : equivalence (@eqv_gen α r) :=
mk_equivalence _ eqv_gen.refl eqv_gen.symm eqv_gen.trans

def eqv_gen.setoid : setoid α :=
setoid.mk _ (eqv_gen.is_equivalence r)

theorem quot.exact {a b : α} (H : quot.mk r a = quot.mk r b) : eqv_gen r a b :=
@quotient.exact _ (eqv_gen.setoid r) a b (@congr_arg _ _ _ _
  (quot.lift (@quotient.mk _ (eqv_gen.setoid r)) (λx y h, quot.sound (eqv_gen.rel x y h))) H)

theorem quot.eqv_gen_sound {r : α → α → Prop} {a b : α} (H : eqv_gen r a b) : quot.mk r a = quot.mk r b :=
eqv_gen.rec_on 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)] : decidable_eq (quotient s) :=
λ q₁ q₂ : quotient s,
  quotient.rec_on_subsingleton₂ q₁ q₂
    (λ a₁ a₂,
      match (d a₁ a₂) with
      | (is_true h₁)  := is_true (quotient.sound h₁)
      | (is_false h₂) := is_false (λ h, absurd (quotient.exact h) h₂)
      end)

/- 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.is_equivalence (α : Sort u) (β : α → Sort v) : equivalence (@function.equiv α β) :=
mk_equivalence (@function.equiv α β) (@equiv.refl α β) (@equiv.symm α β) (@equiv.trans α β)
end function

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

@[instance]
private def fun_setoid (α : Sort u) (β : α → Sort v) : setoid (Π x : α, β x) :=
setoid.mk (@function.equiv α β) (function.equiv.is_equivalence α β)

private def extfun (α : Sort u) (β : α → Sort v) : Sort (imax u v) :=
quotient (fun_setoid α β)

private def fun_to_extfun (f : Π x : α, β x) : extfun α β :=
⟦f⟧
private def extfun_app (f : extfun α β) : Π x : α, β x :=
assume x,
quot.lift_on 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 extfun_app ⟦f₁⟧ = extfun_app ⟦f₂⟧, from
congr_arg extfun_app (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 theorem indefinite_description {α : Sort u} (p : α → Prop)
  (h : ∃ x, p x) : {x // p x} :=
choice $ let ⟨x, px⟩ := h in ⟨⟨x, px⟩⟩

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

theorem some_spec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (some h) :=
(indefinite_description p h).property

/- Diaconescu's theorem: using function extensionality and propositional extensionality,
   we can get excluded middle from this. -/
section diaconescu
parameter  p : Prop

private def U (x : Prop) : Prop := x = true ∨ p
private def V (x : Prop) : Prop := x = false ∨ p

private theorem exU : ∃ x, U x := ⟨true, or.inl rfl⟩
private theorem exV : ∃ x, V x := ⟨false, or.inl rfl⟩

private theorem u : Prop := some exU
private theorem v : Prop := some exV

set_option type_context.unfold_lemmas true
private theorem u_def : U u := some_spec exU
private theorem v_def : V v := some_spec exV

private theorem not_uv_or_p : u ≠ v ∨ p :=
or.elim u_def
  (assume hut : u = true,
    or.elim v_def
      (assume hvf : v = false,
        have hne : u ≠ v, from hvf.symm ▸ hut.symm ▸ true_ne_false,
        or.inl hne)
      or.inr)
  or.inr

private theorem p_implies_uv (hp : p) : u = v :=
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,
    @some _ U exU = @some _ V exV,
  from hpred ▸ λ exU exV, rfl,
show u = v, from h₀ _ _

theorem em : p ∨ ¬p :=
or.elim not_uv_or_p
  (assume hne : u ≠ v, or.inr (mt p_implies_uv hne))
  or.inl
end diaconescu

theorem exists_true_of_nonempty {α : Sort u} : nonempty α → ∃ x : α, true
| ⟨x⟩ := ⟨x, trivial⟩

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

noncomputable def inhabited_of_exists {α : Sort u} {p : α → Prop} (h : ∃ x, p x) :
  inhabited α :=
inhabited_of_nonempty (exists.elim h (λ w hw, ⟨w⟩))

/- all propositions are decidable -/
noncomputable def prop_decidable (a : Prop) : decidable a :=
choice $ or.elim (em a)
  (assume ha, ⟨is_true ha⟩)
  (assume hna, ⟨is_false hna⟩)
local attribute [instance] prop_decidable

noncomputable def decidable_inhabited (a : Prop) : inhabited (decidable a) :=
⟨prop_decidable a⟩
local attribute [instance] decidable_inhabited

noncomputable def type_decidable_eq (α : Sort u) : decidable_eq α :=
λ x y, prop_decidable (x = y)

noncomputable def type_decidable (α : Sort u) : psum α (α → false) :=
match (prop_decidable (nonempty α)) with
| (is_true hp)  := psum.inl (@inhabited.default _ (inhabited_of_nonempty hp))
| (is_false hn) := psum.inr (λ a, absurd (nonempty.intro a) hn)
end

noncomputable theorem strong_indefinite_description {α : Sort u} (p : α → Prop)
  (h : nonempty α) : {x : α // (∃ y : α, p y) → p x} :=
if hp : ∃ x : α, p x then
  let xp := indefinite_description _ 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) : α :=
(strong_indefinite_description p h).val

theorem epsilon_spec_aux {α : Sort u} (h : nonempty α) (p : α → Prop)
  : (∃ y, p y) → p (@epsilon α h p) :=
(strong_indefinite_description p h).property

theorem epsilon_spec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) :
    p (@epsilon α (nonempty_of_exists hex) p) :=
epsilon_spec_aux (nonempty_of_exists hex) p hex

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

/- the axiom of choice -/

theorem axiom_of_choice {α : Sort u} {β : α → Sort v} {r : Π x, β x → Prop} (h : ∀ x, ∃ y, r x y) :
  ∃ (f : Π x, β x), ∀ x, r x (f x) :=
⟨_, λ x, some_spec (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) :=
⟨axiom_of_choice, λ ⟨f, hw⟩ x, ⟨f x, hw x⟩⟩

theorem prop_complete (a : Prop) : a = true ∨ a = false :=
or.elim (em a)
  (λ t, or.inl (eq_true_intro t))
  (λ f, or.inr (eq_false_intro f))

def eq_true_or_eq_false := prop_complete

section aux
attribute [elab_as_eliminator]
theorem cases_true_false (p : Prop → Prop) (h1 : p true) (h2 : p false) (a : Prop) : p a :=
or.elim (prop_complete a)
  (assume ht : a = true,  ht.symm ▸ h1)
  (assume hf : a = false, hf.symm ▸ h2)

theorem cases_on (a : Prop) {p : Prop → Prop} (h1 : p true) (h2 : p false) : p a :=
cases_true_false p h1 h2 a

-- this supercedes by_cases in decidable
def by_cases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
decidable.by_cases hpq hnpq

-- this supercedes by_contradiction in decidable
theorem by_contradiction {p : Prop} (h : ¬p → false) : p :=
decidable.by_contradiction h

theorem eq_false_or_eq_true (a : Prop) : a = false ∨ a = true :=
(prop_complete a).symm
end aux

end classical