1836 lines
60 KiB
Text
1836 lines
60 KiB
Text
/-
|
||
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
|
||
|
||
universes u v w
|
||
|
||
@[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
|
||
|
||
/-- Auxiliary Declaration used to implement the named patterns `x@p` -/
|
||
@[reducible] def namedPattern {α : Sort u} (x a : α) : α := a
|
||
|
||
/-- 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} : α
|
||
|
||
set_option bootstrap.inductiveCheckResultingUniverse false in
|
||
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
|
||
|
||
inductive Eq {α : Sort u} (a : α) : α → Prop
|
||
| refl {} : Eq a a
|
||
|
||
@[elabAsEliminator, inline, reducible]
|
||
def Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : Eq a b) : motive b :=
|
||
@Eq.rec α a (fun α _ => motive α) m b h
|
||
|
||
@[elabAsEliminator, inline, reducible]
|
||
def Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} {b : α} (h : Eq a b) (m : motive a) : motive b :=
|
||
@Eq.rec α a (fun α _ => motive α) 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 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 -/
|
||
|
||
@[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₁
|
||
|
||
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
|
||
|
||
@[macroInline] def cast {α β : Sort u} (h : α = β) (a : α) : β :=
|
||
Eq.rec (motive := fun α _ => α) a h
|
||
|
||
@[matchPattern] def HEq.rfl {α : Sort u} {a : α} : a ≅ a :=
|
||
HEq.refl a
|
||
|
||
theorem eqOfHEq {α : Sort u} {a a' : α} (h : a ≅ a') : a = a' := by
|
||
have (α β : Sort u) → (a : α) → (b : β) → a ≅ b → (h : α = β) → cast h a = b by
|
||
intro α β a b h₁ h₂
|
||
induction h₁
|
||
exact rfl
|
||
show cast rfl a = a'
|
||
exact this α α a a' h rfl
|
||
|
||
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 a b
|
||
| inr (h : b) : Or a b
|
||
|
||
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 p
|
||
|
||
/- 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 p
|
||
| isTrue (h : p) : Decidable p
|
||
|
||
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 (α : Type u)
|
||
| nil : List α
|
||
| cons (head : α) (tail : List α) : List α
|
||
|
||
inductive Nat
|
||
| zero : Nat
|
||
| succ (n : Nat) : Nat
|
||
|
||
/- For numeric literals notation -/
|
||
class OfNat (α : Type u) :=
|
||
(ofNat : Nat → α)
|
||
|
||
export OfNat (ofNat)
|
||
|
||
instance : OfNat Nat := ⟨id⟩
|
||
|
||
/- 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 Add (α : Type u) := (add : α → α → α)
|
||
class Mul (α : Type u) := (mul : α → α → α)
|
||
class Neg (α : Type u) := (neg : α → α)
|
||
class Sub (α : Type u) := (sub : α → α → α)
|
||
class Div (α : Type u) := (div : α → α → α)
|
||
class Mod (α : Type u) := (mod : α → α → α)
|
||
class ModN (α : Type u) := (modn : α → Nat → α)
|
||
class LessEq (α : Type u) := (LessEq : α → α → Prop)
|
||
class Less (α : Type u) := (Less : α → α → Prop)
|
||
class BEq (α : Type u) := (beq : α → α → Bool)
|
||
class Append (α : Type u) := (append : α → α → α)
|
||
class OrElse (α : Type u) := (orElse : α → α → α)
|
||
class AndThen (α : Type u) := (andThen : α → α → α)
|
||
class Equiv (α : Sort u) := (Equiv : α → α → Prop)
|
||
class EmptyCollection (α : Type u) := (emptyCollection : α)
|
||
class Pow (α : Type u) (β : Type v) := (pow : α → β → α)
|
||
|
||
@[reducible] def GreaterEq {α : Type u} [LessEq α] (a b : α) : Prop := LessEq.LessEq b a
|
||
@[reducible] def Greater {α : Type u} [Less α] (a b : α) : Prop := Less.Less b a
|
||
|
||
/- Nat basic instances -/
|
||
|
||
set_option bootstrap.gen_matcher_code false in
|
||
@[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 Add.add Neg.neg
|
||
|
||
instance : 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.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
|
||
|
||
/- 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
|
||
|
||
/- sizeof -/
|
||
|
||
class SizeOf (α : Sort u) :=
|
||
(sizeOf : α → Nat)
|
||
|
||
export SizeOf (sizeOf)
|
||
|
||
/-
|
||
Declare sizeOf instances and theorems for types declared before SizeOf.
|
||
From now on, the inductive Compiler will automatically generate sizeOf instances and theorems.
|
||
-/
|
||
|
||
/- Every Type `α` has a default SizeOf instance that just returns 0 for every element of `α` -/
|
||
protected def default.sizeOf (α : Sort u) : α → Nat
|
||
| a => 0
|
||
|
||
instance (α : Sort u) : SizeOf α :=
|
||
⟨default.sizeOf α⟩
|
||
|
||
instance : SizeOf Nat := {
|
||
sizeOf := fun n => n
|
||
}
|
||
|
||
instance (α : Type u) (β : Type v) [SizeOf α] [SizeOf β] : SizeOf (Prod α β) := {
|
||
sizeOf := fun (a, b) => 1 + sizeOf a + sizeOf b
|
||
}
|
||
|
||
instance (α : Type u) (β : Type v) [SizeOf α] [SizeOf β] : SizeOf (Sum α β) := {
|
||
sizeOf := fun
|
||
| Sum.inl a => 1 + sizeOf a
|
||
| Sum.inr b => 1 + sizeOf b
|
||
}
|
||
|
||
instance (α : Type u) (β : Type v) [SizeOf α] [SizeOf β] : SizeOf (PSum α β) := {
|
||
sizeOf := fun
|
||
| PSum.inl a => 1 + sizeOf a
|
||
| PSum.inr b => 1 + sizeOf b
|
||
}
|
||
|
||
instance (α : Type u) (β : α → Type v) [SizeOf α] [∀ a, SizeOf (β a)] : SizeOf (Sigma β) := {
|
||
sizeOf := fun ⟨a, b⟩ => 1 + sizeOf a + sizeOf b
|
||
}
|
||
|
||
instance (α : Type u) (β : α → Type v) [SizeOf α] [(a : α) → SizeOf (β a)] : SizeOf (PSigma β) := {
|
||
sizeOf := fun ⟨a, b⟩ => 1 + sizeOf a + sizeOf b
|
||
}
|
||
|
||
instance : SizeOf PUnit := {
|
||
sizeOf := fun _ => 1
|
||
}
|
||
|
||
instance : SizeOf Bool := {
|
||
sizeOf := fun _ => 1
|
||
}
|
||
|
||
instance (α : Type u) [SizeOf α] : SizeOf (Option α) := {
|
||
sizeOf := fun
|
||
| none => 1
|
||
| some a => 1 + sizeOf a
|
||
}
|
||
|
||
instance (α : Type u) [SizeOf α] : SizeOf (List α) := {
|
||
sizeOf := fun as =>
|
||
let rec loop
|
||
| List.nil => 1
|
||
| List.cons x xs => 1 + sizeOf x + loop xs
|
||
loop as
|
||
}
|
||
|
||
instance {α : Type u} [SizeOf α] (p : α → Prop) : SizeOf (Subtype p) := {
|
||
sizeOf := fun ⟨a, _⟩ => sizeOf a
|
||
}
|
||
|
||
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
|
||
|
||
@[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} [BEq α] (a b : α) : Bool :=
|
||
!(a == b)
|
||
|
||
/- 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 : α = β) (a : α) : β :=
|
||
h ▸ a
|
||
|
||
@[macroInline] def Eq.mpr {α β : Sort u} (h : α = β) (b : β) : α :=
|
||
h ▸ b
|
||
|
||
@[elabAsEliminator]
|
||
theorem Eq.substr {α : Sort u} {p : α → Prop} {a b : α} (h₁ : b = a) (h₂ : p a) : p b :=
|
||
h₁ ▸ h₂
|
||
|
||
theorem congr {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : f₁ = f₂) (h₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=
|
||
h₁ ▸ h₂ ▸ rfl
|
||
|
||
theorem congrFun {α : Sort u} {β : α → Sort v} {f g : ∀ x, β x} (h : f = g) (a : α) : f a = g a :=
|
||
h ▸ rfl
|
||
|
||
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₁ ▸ h₂
|
||
|
||
theorem ofEqTrue {p : Prop} (h : p = True) : p :=
|
||
h ▸ trivial
|
||
|
||
theorem notOfEqFalse {p : Prop} (h : p = False) : ¬p :=
|
||
fun hp => h ▸ hp
|
||
|
||
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)
|
||
|
||
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) =>
|
||
have ¬True from h ▸ hnp
|
||
this 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 : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : a ≅ b) : motive b :=
|
||
@HEq.rec α a (fun b _ => motive b) m β b h
|
||
|
||
@[elabAsEliminator]
|
||
theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : motive a) : motive b :=
|
||
@HEq.rec α a (fun b _ => motive b) m β b h
|
||
|
||
theorem HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b :=
|
||
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 (motive := fun x => x ≅ a) 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 (motive := @fun (x : Sort u) _ => α = x) h (Eq.refl α)
|
||
|
||
end
|
||
|
||
theorem eqRecHEq {α : Sort u} {φ : α → Sort v} : {a a' : α} → (h : a = a') → (p : φ a) → (Eq.recOn (motive := fun x _ => φ x) h p) ≅ p
|
||
| a, _, rfl, p => HEq.refl p
|
||
|
||
theorem ofHEqTrue {a : Prop} (h : a ≅ True) : a :=
|
||
ofEqTrue (eqOfHEq h)
|
||
|
||
theorem heqOfEqRecEq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ : Eq.rec (motive := fun α _ => α) a h₁ = b) : a ≅ b := by
|
||
subst h₁
|
||
apply heqOfEq
|
||
exact h₂
|
||
done
|
||
|
||
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 :=
|
||
h₂ h₁.1 h₁.2
|
||
|
||
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 :=
|
||
match h₁ with
|
||
| Or.inl h => h₂ h
|
||
| Or.inr 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 :=
|
||
h₁ h₂.1 h₂.2
|
||
|
||
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 :=
|
||
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 :=
|
||
h₂ h₁.1 h₁.2
|
||
|
||
/- Decidable -/
|
||
|
||
@[inlineIfReduce, nospecialize] def Decidable.decide (p : Prop) [h : Decidable p] : Bool :=
|
||
Decidable.casesOn (motive := fun _ => Bool) h (fun _ => false) (fun _ => true)
|
||
|
||
export Decidable (isTrue isFalse decide)
|
||
|
||
instance {α : Type u} [DecidableEq α] : BEq α :=
|
||
⟨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] (t : c → α) (e : ¬ c → α) : α :=
|
||
Decidable.casesOn (motive := fun _ => α) h e t
|
||
|
||
/- if-then-else -/
|
||
|
||
@[macroInline] def ite {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α :=
|
||
Decidable.casesOn (motive := fun _ => α) h (fun _ => e) (fun _ => t)
|
||
|
||
namespace Decidable
|
||
variables {p q : Prop}
|
||
|
||
@[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 [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 from Sort to Type -/
|
||
structure PLift (α : Sort u) : Type u :=
|
||
up :: (down : α)
|
||
|
||
/- Bijection between α and PLift α -/
|
||
theorem PLift.upDown {α : Sort u} : ∀ (b : PLift α), up (down b) = b
|
||
| up a => rfl
|
||
|
||
theorem PLift.downUp {α : Sort u} (a : α) : down (up a) = a :=
|
||
rfl
|
||
|
||
/- Pointed types -/
|
||
structure PointedType :=
|
||
(type : Type u)
|
||
(val : type)
|
||
|
||
/-- Universe lifting operation -/
|
||
structure ULift.{r, s} (α : Type s) : Type (max s r) :=
|
||
up :: (down : α)
|
||
|
||
/- Bijection between α and ULift.{v} α -/
|
||
theorem ULift.upDown {α : Type u} : ∀ (b : ULift.{v} α), up (down b) = b
|
||
| up a => rfl
|
||
|
||
theorem ULift.downUp {α : Type u} (a : α) : down (up.{v} a) = a :=
|
||
rfl
|
||
|
||
/- Inhabited -/
|
||
|
||
class Inhabited (α : Sort u) :=
|
||
mk {} :: (default : α)
|
||
|
||
constant arbitrary (α : Sort u) [s : Inhabited α] : α :=
|
||
@Inhabited.default α s
|
||
|
||
instance : Inhabited Prop := {
|
||
default := True
|
||
}
|
||
|
||
instance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) := {
|
||
default := fun _ => arbitrary β
|
||
}
|
||
|
||
instance (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] : Inhabited ((a : α) → β a) := {
|
||
default := fun a => arbitrary (β a)
|
||
}
|
||
|
||
instance : Inhabited Bool := {
|
||
default := false
|
||
}
|
||
|
||
instance : Inhabited True := {
|
||
default := trivial
|
||
}
|
||
|
||
instance : Inhabited Nat := {
|
||
default := 0
|
||
}
|
||
|
||
instance : Inhabited NonScalar := {
|
||
default := ⟨arbitrary _⟩
|
||
}
|
||
|
||
instance : Inhabited PNonScalar.{u} := {
|
||
default := ⟨arbitrary _⟩
|
||
}
|
||
|
||
instance : Inhabited PointedType := {
|
||
default := {type := PUnit, val := ⟨⟩}
|
||
}
|
||
|
||
instance {α} [Inhabited α] : Inhabited (ForInStep α) := {
|
||
default:= ForInStep.done (arbitrary _)
|
||
}
|
||
|
||
class inductive Nonempty (α : Sort u) : Prop
|
||
| intro (val : α) : Nonempty α
|
||
|
||
protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p :=
|
||
h₂ h₁.1
|
||
|
||
instance {α : Sort u} [Inhabited α] : Nonempty α := {
|
||
val := 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 :=
|
||
match h with
|
||
| intro h => h
|
||
|
||
protected def Subsingleton.helim {α β : Sort u} [h₁ : Subsingleton α] (h₂ : α = β) (a : α) (b : β) : a ≅ b := by
|
||
subst h₂
|
||
apply heqOfEq
|
||
apply Subsingleton.elim
|
||
|
||
instance (p : Prop) : Subsingleton p :=
|
||
⟨fun a b => proofIrrel a b⟩
|
||
|
||
instance (p : Prop) : Subsingleton (Decidable p) :=
|
||
Subsingleton.intro fun
|
||
| (isTrue t₁) => fun
|
||
| (isTrue t₂) => proofIrrel t₁ t₂ ▸ rfl
|
||
| (isFalse f₂) => absurd t₁ f₂
|
||
| (isFalse f₁) => fun
|
||
| (isTrue t₂) => absurd t₂ f₁
|
||
| (isFalse f₂) => proofIrrel f₁ f₂ ▸ rfl
|
||
|
||
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 (motive := fun _ => Sort u) 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 := -- TODO: use structure?
|
||
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 h₁ h₂ => 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 r a b
|
||
| trans : ∀ a b c, TC r a b → TC r b c → TC r a c
|
||
|
||
@[elabAsEliminator]
|
||
theorem TC.ndrec {α : Sort u} {r : α → α → Prop} {C : α → α → Prop}
|
||
(m₁ : ∀ (a b : α), r a b → C a b)
|
||
(m₂ : ∀ (a b c : α), TC r a b → TC r b c → C a b → C b c → C a c)
|
||
{a b : α} (h : TC r a b) : C a b :=
|
||
@TC.rec α r (fun a b _ => C a b) m₁ m₂ a b h
|
||
|
||
@[elabAsEliminator]
|
||
theorem TC.ndrecOn {α : Sort u} {r : α → α → Prop} {C : α → α → Prop}
|
||
{a b : α} (h : TC r a b)
|
||
(m₁ : ∀ (a b : α), r a b → C a b)
|
||
(m₂ : ∀ (a b c : α), TC r a b → TC r b c → C a b → C b c → C a c)
|
||
: C a b :=
|
||
@TC.rec α r (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⟩, ⟨_, _⟩, rfl => rfl
|
||
|
||
theorem eta (a : {x // p x}) (h : p (val a)) : mk (val a) h = a := by
|
||
cases a
|
||
exact rfl
|
||
|
||
instance {α : Type u} {p : α → Prop} {a : α} (h : p a) : Inhabited {x // p x} := {
|
||
default := ⟨a, h⟩
|
||
}
|
||
|
||
instance {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
|
||
fun ⟨a, h₁⟩ ⟨b, h₂⟩ =>
|
||
if h : a = b then isTrue (by subst h; exact rfl)
|
||
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 α β) := {
|
||
default := Sum.inl (arbitrary α)
|
||
}
|
||
|
||
instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (Sum α β) := {
|
||
default := 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 (α × β) := {
|
||
default := (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 (e₁ ▸ 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 [BEq α] [BEq β] : BEq (α × β) := {
|
||
beq := fun ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ => a₁ == a₂ && b₁ == b₂
|
||
}
|
||
|
||
instance [Less α] [Less β] : Less (α × β) := {
|
||
Less := fun s t => s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)
|
||
}
|
||
|
||
instance prodHasDecidableLt
|
||
[Less α] [Less β] [DecidableEq α] [DecidableEq β]
|
||
[(a b : α) → Decidable (a < b)] [(a b : β) → Decidable (a < b)]
|
||
: (s t : α × β) → Decidable (s < t) :=
|
||
fun t s => inferInstanceAs (Decidable (_ ∨ _))
|
||
|
||
theorem Prod.ltDef [Less α] [Less β] (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 -/
|
||
|
||
theorem exOfPsig {α : Type u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x)
|
||
| ⟨x, hx⟩ => ⟨x, hx⟩
|
||
|
||
protected theorem PSigma.eta {α : Sort u} {β : α → Sort v} {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂}
|
||
(h₁ : a₁ = a₂) (h₂ : Eq.rec (motive := fun a _ => β a) b₁ h₁ = b₂) : PSigma.mk a₁ b₁ = PSigma.mk a₂ b₂ := by
|
||
subst h₁
|
||
subst h₂
|
||
exact rfl
|
||
|
||
/- Universe polymorphic unit -/
|
||
|
||
theorem punitEq (a b : PUnit) : a = b := by
|
||
cases a; cases b; exact rfl
|
||
|
||
theorem punitEqPUnit (a : PUnit) : a = () :=
|
||
punitEq a ()
|
||
|
||
instance : Subsingleton PUnit :=
|
||
Subsingleton.intro punitEq
|
||
|
||
instance : Inhabited PUnit := {
|
||
default := ⟨⟩
|
||
}
|
||
|
||
instance : DecidableEq PUnit :=
|
||
fun a b => isTrue (punitEq a b)
|
||
|
||
/- Setoid -/
|
||
|
||
class Setoid (α : Sort u) :=
|
||
(r : α → α → Prop)
|
||
(iseqv {} : Equivalence r)
|
||
|
||
instance {α : Sort u} [Setoid α] : Equiv α :=
|
||
⟨Setoid.r⟩
|
||
|
||
namespace Setoid
|
||
|
||
variables {α : Sort u} [Setoid α]
|
||
|
||
theorem refl (a : α) : a ≈ a :=
|
||
(Setoid.iseqv α).1 a
|
||
|
||
theorem symm {a b : α} (hab : a ≈ b) : b ≈ a :=
|
||
(Setoid.iseqv α).2.1 hab
|
||
|
||
theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c :=
|
||
(Setoid.iseqv α).2.2 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 (β := fun q => Exists (fun a => (Quot.mk r a) = q)) 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 (motive := fun x _ => β x) (f a) (sound p)) = f b)
|
||
: ∀ a b, r a b → Quot.indep f a = Quot.indep f b :=
|
||
fun a b e => PSigma.eta (sound e) (h a b e)
|
||
|
||
protected theorem liftIndepPr1
|
||
(f : ∀ a, β (Quot.mk r a))
|
||
(h : ∀ (a b : α) (p : r a b), (Eq.rec (motive := fun x _ => β x) (f a) (sound p)) = f b)
|
||
(q : Quot r) : (lift (Quot.indep f) (Quot.indepCoherent f h) q).1 = q := by
|
||
induction q using Quot.ind
|
||
exact rfl
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def rec
|
||
(f : ∀ a, β (Quot.mk r a))
|
||
(h : ∀ (a b : α) (p : r a b), (Eq.rec (motive := fun x _ => β x) (f a) (sound p)) = 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 (motive := fun x _ => β x) (f a) (sound p)) = 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 := by
|
||
induction q using Quot.rec
|
||
apply f
|
||
apply Subsingleton.elim
|
||
|
||
@[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 (motive := fun x _ => β x) (f a) (sound p)) ≅ 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 (motive := fun a _ => β a) (f a) (Quotient.sound p)) = 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 (motive := fun a _ => β a) (f a) (Quotient.sound p)) = f b) :=
|
||
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₂ := by
|
||
induction q₁ using Quotient.ind
|
||
induction q₂ using Quotient.ind
|
||
apply h
|
||
|
||
-- 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₂ := by
|
||
induction q₁ using Quotient.ind
|
||
induction q₂ using Quotient.ind
|
||
apply h
|
||
|
||
@[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₃ := by
|
||
induction q₁ using Quotient.ind
|
||
induction q₂ using Quotient.ind
|
||
induction q₃ using Quotient.ind
|
||
apply h
|
||
|
||
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 :=
|
||
Quot.inductionOn (β := fun q => rel q q) 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}
|
||
[s : ∀ a b, Subsingleton (φ (Quotient.mk a) (Quotient.mk b))]
|
||
(q₁ : Quotient s₁)
|
||
(q₂ : Quotient s₂)
|
||
(g : ∀ a b, φ (Quotient.mk a) (Quotient.mk b)) : φ q₁ q₂ := by
|
||
induction q₁ using Quot.recOnSubsingleton
|
||
induction q₂ using Quot.recOnSubsingleton
|
||
intro a; apply s
|
||
induction q₂ using Quot.recOnSubsingleton
|
||
intro a; apply s
|
||
apply g
|
||
|
||
end
|
||
end Quotient
|
||
|
||
section
|
||
variable {α : Type u}
|
||
variable (r : α → α → Prop)
|
||
|
||
instance {α : Sort u} {s : Setoid α} [d : ∀ (a b : α), Decidable (a ≈ b)] : DecidableEq (Quotient s) :=
|
||
fun (q₁ q₂ : Quotient s) =>
|
||
Quotient.recOnSubsingleton₂ (φ := fun a b => Decidable (a = b)) 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 :=
|
||
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₂ := by
|
||
show extfunApp (Quotient.mk f₁) = extfunApp (Quotient.mk f₂)
|
||
apply congrArg
|
||
apply Quotient.sound
|
||
exact h
|
||
|
||
end
|
||
|
||
instance {α : 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)
|
||
|
||
@[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} {motive : Squash α → Prop} (h : ∀ (a : α), motive (Squash.mk a)) : ∀ (q : Squash α), motive q :=
|
||
Quot.ind h
|
||
|
||
@[inline] def Squash.lift {α β} [Subsingleton β] (s : Squash α) (f : α → β) : β :=
|
||
Quot.lift f (fun a b _ => Subsingleton.elim _ _) s
|
||
|
||
instance {α} : Subsingleton (Squash α) := ⟨fun a b =>
|
||
Squash.ind (motive := fun a => a = b)
|
||
(fun a => Squash.ind (motive := fun b => Squash.mk a = b)
|
||
(fun b => show Quot.mk _ a = Quot.mk _ b by apply Quot.sound; exact trivial)
|
||
b)
|
||
a⟩
|
||
|
||
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
|