1813 lines
60 KiB
Text
1813 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
|
||
|
||
notation `Prop` := Sort 0
|
||
notation f ` $ `:1 a:0 := f a
|
||
|
||
/- Logical operations and relations -/
|
||
|
||
reserve prefix `¬`:40
|
||
reserve prefix `~`:40
|
||
reserve infixr ` ∧ `:35
|
||
reserve infixr ` /\ `:35
|
||
reserve infixr ` \/ `:30
|
||
reserve infixr ` ∨ `:30
|
||
reserve infix ` <-> `:20
|
||
reserve infix ` ↔ `:20
|
||
reserve infix ` = `:50
|
||
reserve infix ` == `:50
|
||
reserve infix ` != `:50
|
||
reserve infix ` ~= `:50
|
||
reserve infix ` ≅ `:50
|
||
reserve infix ` ≠ `:50
|
||
reserve infix ` ≈ `:50
|
||
reserve infix ` ~ `:50
|
||
reserve infix ` ≡ `:50
|
||
reserve infixl ` ⬝ `:75
|
||
reserve infixr ` ▸ `:75
|
||
reserve infixr ` ▹ `:75
|
||
|
||
/- types and Type constructors -/
|
||
|
||
reserve infixr ` ⊕ `:30
|
||
reserve infixr ` × `:35
|
||
|
||
/- arithmetic operations -/
|
||
|
||
reserve infixl ` + `:65
|
||
reserve infixl ` - `:65
|
||
reserve infixl ` * `:70
|
||
reserve infixl ` / `:70
|
||
reserve infixl ` % `:70
|
||
reserve infixl ` %ₙ `:70
|
||
reserve prefix `-`:100
|
||
reserve infixr ` ^ `:80
|
||
|
||
reserve infixr ` ∘ `:90
|
||
|
||
reserve infix ` <= `:50
|
||
reserve infix ` ≤ `:50
|
||
reserve infix ` < `:50
|
||
reserve infix ` >= `:50
|
||
reserve infix ` ≥ `:50
|
||
reserve infix ` > `:50
|
||
|
||
/- boolean operations -/
|
||
|
||
reserve prefix `!`:40
|
||
reserve infixl ` && `:35
|
||
reserve infixl ` || `:30
|
||
|
||
/- set operations -/
|
||
|
||
reserve infix ` ∈ `:50
|
||
reserve infix ` ∉ `:50
|
||
reserve infixl ` ∩ `:70
|
||
reserve infixl ` ∪ `:65
|
||
reserve infix ` ⊆ `:50
|
||
reserve infix ` ⊇ `:50
|
||
reserve infix ` ⊂ `:50
|
||
reserve infix ` ⊃ `:50
|
||
reserve infix ` \ `:70
|
||
|
||
/- other symbols -/
|
||
|
||
reserve infix ` ∣ `:50
|
||
reserve infixl ` ++ `:65
|
||
reserve infixr ` :: `:67
|
||
|
||
/- Control -/
|
||
reserve infixr ` <|> `:2
|
||
reserve infixr `; ` :3
|
||
reserve infixr ` >>= `:55
|
||
reserve infixr ` >=> `:55
|
||
reserve infixl ` <*> `:60
|
||
reserve infixl ` <* ` :60
|
||
reserve infixr ` *> ` :60
|
||
reserve infixr ` >> ` :60
|
||
reserve infixr ` <$> `:100
|
||
reserve infixr ` <$ ` :100
|
||
reserve infixr ` $> ` :100
|
||
reserve infixl ` <&> `:100
|
||
|
||
universes u v w
|
||
|
||
/-- Auxiliary unsafe constant used by the Compiler when erasing proofs from code. -/
|
||
unsafe axiom lcProof {α : Prop} : α
|
||
/-- Auxiliary unsafe constant used by the Compiler to mark unreachable code. -/
|
||
unsafe axiom lcUnreachable {α : Sort u} : α
|
||
|
||
@[inline] def id {α : Sort u} (a : α) : α := a
|
||
|
||
def inline {α : Sort u} (a : α) : α := a
|
||
|
||
@[inline] def flip {α : Sort u} {β : Sort v} {φ : Sort w} (f : α → β → φ) : β → α → φ :=
|
||
λ b a, f a b
|
||
|
||
/-
|
||
The kernel definitional equality test (t =?= s) has special support for idDelta applications.
|
||
It implements the following rules
|
||
|
||
1) (idDelta t) =?= t
|
||
2) t =?= (idDelta t)
|
||
3) (idDelta t) =?= s IF (unfoldOf t) =?= s
|
||
4) t =?= idDelta s IF t =?= (unfoldOf s)
|
||
|
||
This is mechanism for controlling the delta reduction (aka unfolding) used in the kernel.
|
||
|
||
We use idDelta applications to address performance problems when Type checking
|
||
theorems generated by the equation Compiler.
|
||
-/
|
||
@[inline] def idDelta {α : Sort u} (a : α) : α :=
|
||
a
|
||
|
||
/-- Gadget for optional parameter support. -/
|
||
@[reducible] def optParam (α : Sort u) (default : α) : Sort u :=
|
||
α
|
||
|
||
/-- Gadget for marking output parameters in type classes. -/
|
||
@[reducible] def outParam (α : Sort u) : Sort u := α
|
||
|
||
/-- Auxiliary Declaration used to implement the notation (a : α) -/
|
||
@[reducible] def typedExpr (α : Sort u) (a : α) : α := a
|
||
|
||
/- `idRhs` is an auxiliary Declaration used in the equation Compiler to address performance
|
||
issues when proving equational theorems. The equation Compiler uses it as a marker. -/
|
||
@[macroInline, reducible] def idRhs (α : Sort u) (a : α) : α := a
|
||
|
||
inductive PUnit : Sort u
|
||
| unit : PUnit
|
||
|
||
/-- An abbreviation for `PUnit.{0}`, its most common instantiation.
|
||
This Type should be preferred over `PUnit` where possible to avoid
|
||
unnecessary universe parameters. -/
|
||
abbrev Unit : Type := PUnit
|
||
|
||
@[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 cpp inline "lean::mk_thunk(#2)"] Thunk.mk
|
||
|
||
@[noinline, extern cpp inline "lean::thunk_pure(#2)"]
|
||
protected def Thunk.pure {α : Type u} (a : α) : Thunk α :=
|
||
⟨λ _, a⟩
|
||
@[noinline, extern cpp inline "lean::thunk_get_own(#2)"]
|
||
protected def Thunk.get {α : Type u} (x : @& Thunk α) : α :=
|
||
x.fn ()
|
||
@[noinline, extern cpp inline "lean::thunk_map(#3, #4)"]
|
||
protected def Thunk.map {α : Type u} {β : Type v} (f : α → β) (x : Thunk α) : Thunk β :=
|
||
⟨λ _, f x.get⟩
|
||
@[noinline, extern cpp inline "lean::thunk_bind(#3, #4)"]
|
||
protected def Thunk.bind {α : Type u} {β : Type v} (x : Thunk α) (f : α → Thunk β) : Thunk β :=
|
||
⟨λ _, (f x.get).get⟩
|
||
|
||
/- Remark: tasks have an efficient implementation in the runtime. -/
|
||
structure Task (α : Type u) : Type u :=
|
||
(fn : Unit → α)
|
||
|
||
attribute [extern cpp inline "lean::mk_task(#2)"] Task.mk
|
||
|
||
@[noinline, extern cpp inline "lean::task_pure(#2)"]
|
||
protected def Task.pure {α : Type u} (a : α) : Task α :=
|
||
⟨λ _, a⟩
|
||
@[noinline, extern cpp inline "lean::task_get(#2)"]
|
||
protected def Task.get {α : Type u} (x : @& Task α) : α :=
|
||
x.fn ()
|
||
@[noinline, extern cpp inline "lean::task_map(#3, #4)"]
|
||
protected def Task.map {α : Type u} {β : Type v} (f : α → β) (x : Task α) : Task β :=
|
||
⟨λ _, f x.get⟩
|
||
@[noinline, extern cpp inline "lean::task_bind(#3, #4)"]
|
||
protected def Task.bind {α : Type u} {β : Type v} (x : Task α) (f : α → Task β) : Task β :=
|
||
⟨λ _, (f x.get).get⟩
|
||
|
||
inductive True : Prop
|
||
| intro : True
|
||
|
||
inductive False : Prop
|
||
|
||
inductive Empty : Type
|
||
|
||
def Not (a : Prop) : Prop := a → False
|
||
prefix `¬` := Not
|
||
|
||
inductive Eq {α : Sort u} (a : α) : α → Prop
|
||
| refl : Eq a
|
||
|
||
@[elabAsEliminator, inline, reducible]
|
||
def {u1 u2} Eq.ndrec {α : Sort u2} {a : α} {C : α → Sort u1} (m : C a) {b : α} (h : Eq a b) : C b :=
|
||
@Eq.rec α a (λ α _, C α) m b h
|
||
|
||
@[elabAsEliminator, inline, reducible]
|
||
def {u1 u2} Eq.ndrecOn {α : Sort u2} {a : α} {C : α → Sort u1} {b : α} (h : Eq a b) (m : C a) : C b :=
|
||
@Eq.rec α a (λ α _, C α) m b h
|
||
|
||
/-
|
||
Initialize the Quotient Module, which effectively adds the following definitions:
|
||
|
||
constant Quot {α : Sort u} (r : α → α → Prop) : Sort u
|
||
|
||
constant Quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : Quot r
|
||
|
||
constant Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
|
||
(∀ a b : α, r a b → Eq (f a) (f b)) → Quot r → β
|
||
|
||
constant Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} :
|
||
(∀ a : α, β (Quot.mk r a)) → ∀ q : Quot r, β q
|
||
-/
|
||
initQuot
|
||
|
||
inductive Heq {α : Sort u} (a : α) : Π {β : Sort u}, β → Prop
|
||
| refl : Heq a
|
||
|
||
structure Prod (α : Type u) (β : Type v) :=
|
||
(fst : α) (snd : β)
|
||
|
||
/-- Similar to `Prod`, but α and β can be propositions.
|
||
We use this Type internally to automatically generate the brecOn recursor. -/
|
||
structure PProd (α : Sort u) (β : Sort v) :=
|
||
(fst : α) (snd : β)
|
||
|
||
structure And (a b : Prop) : Prop :=
|
||
intro :: (left : a) (right : b)
|
||
|
||
structure Iff (a b : Prop) : Prop :=
|
||
intro :: (mp : a → b) (mpr : b → a)
|
||
|
||
/- Eq basic support -/
|
||
|
||
infix = := Eq
|
||
|
||
@[matchPattern] def rfl {α : Sort u} {a : α} : a = a := Eq.refl a
|
||
|
||
@[elabAsEliminator]
|
||
theorem Eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b :=
|
||
Eq.ndrec h₂ h₁
|
||
|
||
infixr ▸ := Eq.subst
|
||
|
||
theorem Eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c :=
|
||
h₂ ▸ h₁
|
||
|
||
theorem Eq.symm {α : Sort u} {a b : α} (h : a = b) : b = a :=
|
||
h ▸ rfl
|
||
|
||
infix ~= := Heq
|
||
infix ≅ := Heq
|
||
|
||
@[matchPattern] def Heq.rfl {α : Sort u} {a : α} : a ≅ a := Heq.refl a
|
||
|
||
theorem eqOfHeq {α : Sort u} {a a' : α} (h : a ≅ a') : a = a' :=
|
||
have ∀ (α' : Sort u) (a' : α') (h₁ : @Heq α a α' a') (h₂ : α = α'), (Eq.recOn h₂ a : α') = a', from
|
||
λ (α' : Sort u) (a' : α') (h₁ : @Heq α a α' a'), Heq.recOn h₁ (λ h₂ : α = α, rfl),
|
||
show (Eq.ndrecOn (Eq.refl α) a : α) = a', from
|
||
this α a' h (Eq.refl α)
|
||
|
||
inductive Sum (α : Type u) (β : Type v)
|
||
| inl {} (val : α) : Sum
|
||
| inr {} (val : β) : Sum
|
||
|
||
inductive PSum (α : Sort u) (β : Sort v)
|
||
| inl {} (val : α) : PSum
|
||
| inr {} (val : β) : PSum
|
||
|
||
inductive Or (a b : Prop) : Prop
|
||
| inl {} (h : a) : Or
|
||
| inr {} (h : b) : Or
|
||
|
||
def Or.introLeft {a : Prop} (b : Prop) (ha : a) : Or a b :=
|
||
Or.inl ha
|
||
|
||
def Or.introRight (a : Prop) {b : Prop} (hb : b) : Or a b :=
|
||
Or.inr hb
|
||
|
||
structure Sigma {α : Type u} (β : α → Type v) :=
|
||
mk :: (fst : α) (snd : β fst)
|
||
|
||
structure PSigma {α : Sort u} (β : α → Sort v) :=
|
||
mk :: (fst : α) (snd : β fst)
|
||
|
||
inductive Bool : Type
|
||
| false : Bool
|
||
| true : Bool
|
||
|
||
/- Remark: Subtype must take a Sort instead of Type because of the axiom strongIndefiniteDescription. -/
|
||
structure Subtype {α : Sort u} (p : α → Prop) :=
|
||
(val : α) (property : p val)
|
||
|
||
inductive Exists {α : Sort u} (p : α → Prop) : Prop
|
||
| intro (w : α) (h : p w) : Exists
|
||
|
||
class inductive Decidable (p : Prop)
|
||
| isFalse (h : ¬p) : Decidable
|
||
| isTrue (h : p) : Decidable
|
||
|
||
@[reducible] def DecidablePred {α : Sort u} (r : α → Prop) :=
|
||
Π (a : α), Decidable (r a)
|
||
|
||
@[reducible] def DecidableRel {α : Sort u} (r : α → α → Prop) :=
|
||
Π (a b : α), Decidable (r a b)
|
||
|
||
class DecidableEq (α : Sort u) :=
|
||
{decEq : Π a b : α, Decidable (a = b)}
|
||
|
||
export DecidableEq (decEq)
|
||
|
||
@[inline] instance decidableOfDecidableEq {α : Sort u} (a b : α) [DecidableEq α] : Decidable (a = b) :=
|
||
decEq a b
|
||
|
||
inductive Option (α : Type u)
|
||
| none {} : Option
|
||
| some (val : α) : Option
|
||
|
||
export Option (none some)
|
||
export Bool (false true)
|
||
|
||
inductive List (T : Type u)
|
||
| nil {} : List
|
||
| cons (hd : T) (tl : List) : List
|
||
|
||
infixr :: := List.cons
|
||
|
||
inductive Nat
|
||
| zero : Nat
|
||
| succ (n : Nat) : Nat
|
||
|
||
/- Auxiliary axiom used to implement `sorry`.
|
||
TODO: add this theorem on-demand. That is,
|
||
we should only add it if after the first error. -/
|
||
unsafe axiom sorryAx (α : Sort u) (synthetic := true) : α
|
||
|
||
/- Declare builtin and reserved notation -/
|
||
|
||
class HasZero (α : Type u) := (zero : α)
|
||
class HasOne (α : Type u) := (one : α)
|
||
class HasAdd (α : Type u) := (add : α → α → α)
|
||
class HasMul (α : Type u) := (mul : α → α → α)
|
||
class HasNeg (α : Type u) := (neg : α → α)
|
||
class HasSub (α : Type u) := (sub : α → α → α)
|
||
class HasDiv (α : Type u) := (div : α → α → α)
|
||
class HasDivides (α : Type u) := (Divides : α → α → Prop)
|
||
class HasMod (α : Type u) := (mod : α → α → α)
|
||
class HasModn (α : Type u) := (modn : α → Nat → α)
|
||
class HasLessEq (α : Type u) := (LessEq : α → α → Prop)
|
||
class HasLess (α : Type u) := (Less : α → α → Prop)
|
||
class HasBeq (α : Type u) := (beq : α → α → Bool)
|
||
class HasAppend (α : Type u) := (append : α → α → α)
|
||
class HasOrelse (α : Type u) := (orelse : α → α → α)
|
||
class HasAndthen (α : Type u) := (andthen : α → α → α)
|
||
class HasUnion (α : Type u) := (union : α → α → α)
|
||
class HasInter (α : Type u) := (inter : α → α → α)
|
||
class HasSDiff (α : Type u) := (sdiff : α → α → α)
|
||
class HasEquiv (α : Sort u) := (Equiv : α → α → Prop)
|
||
class HasSubset (α : Type u) := (Subset : α → α → Prop)
|
||
class HasSSubset (α : Type u) := (SSubset : α → α → Prop)
|
||
/- Type classes HasEmptyc and HasInsert are
|
||
used to implement polymorphic notation for collections.
|
||
Example: {a, b, c}. -/
|
||
class HasEmptyc (α : Type u) := (emptyc : α)
|
||
class HasInsert (α : outParam $ Type u) (γ : Type v) := (insert : α → γ → γ)
|
||
/- Type class used to implement the notation { a ∈ c | p a } -/
|
||
class HasSep (α : outParam $ Type u) (γ : Type v) :=
|
||
(sep : (α → Prop) → γ → γ)
|
||
/- Type class for set-like membership -/
|
||
class HasMem (α : outParam $ Type u) (γ : Type v) := (mem : α → γ → Prop)
|
||
|
||
class HasPow (α : Type u) (β : Type v) :=
|
||
(pow : α → β → α)
|
||
|
||
export HasAndthen (andthen)
|
||
export HasPow (pow)
|
||
|
||
infix ∈ := HasMem.mem
|
||
notation a ` ∉ ` s := ¬ HasMem.mem a s
|
||
infix + := HasAdd.add
|
||
infix * := HasMul.mul
|
||
infix - := HasSub.sub
|
||
infix / := HasDiv.div
|
||
infix ∣ := HasDivides.Divides
|
||
infix % := HasMod.mod
|
||
infix %ₙ := HasModn.modn
|
||
prefix - := HasNeg.neg
|
||
infix <= := HasLessEq.LessEq
|
||
infix ≤ := HasLessEq.LessEq
|
||
infix < := HasLess.Less
|
||
infix == := HasBeq.beq
|
||
infix ++ := HasAppend.append
|
||
notation `∅` := HasEmptyc.emptyc _
|
||
infix ∪ := HasUnion.union
|
||
infix ∩ := HasInter.inter
|
||
infix ⊆ := HasSubset.Subset
|
||
infix ⊂ := HasSSubset.SSubset
|
||
infix \ := HasSDiff.sdiff
|
||
infix ≈ := HasEquiv.Equiv
|
||
infixr ^ := HasPow.pow
|
||
infixr /\ := And
|
||
infixr ∧ := And
|
||
infixr \/ := Or
|
||
infixr ∨ := Or
|
||
infix <-> := Iff
|
||
infix ↔ := Iff
|
||
-- notation `exists` binders `, ` r:(scoped P, Exists P) := r
|
||
-- notation `∃` binders `, ` r:(scoped P, Exists P) := r
|
||
infixr <|> := HasOrelse.orelse
|
||
infixr >> := HasAndthen.andthen
|
||
|
||
export HasAppend (append)
|
||
|
||
@[reducible] def GreaterEq {α : Type u} [HasLessEq α] (a b : α) : Prop := HasLessEq.LessEq b a
|
||
@[reducible] def Greater {α : Type u} [HasLess α] (a b : α) : Prop := HasLess.Less b a
|
||
|
||
infix >= := GreaterEq
|
||
infix ≥ := GreaterEq
|
||
infix > := Greater
|
||
|
||
@[reducible] def Superset {α : Type u} [HasSubset α] (a b : α) : Prop := HasSubset.Subset b a
|
||
@[reducible] def SSuperset {α : Type u} [HasSSubset α] (a b : α) : Prop := HasSSubset.SSubset b a
|
||
|
||
infix ⊇ := Superset
|
||
infix ⊃ := SSuperset
|
||
|
||
@[inline] def bit0 {α : Type u} [s : HasAdd α] (a : α) : α := a + a
|
||
@[inline] def bit1 {α : Type u} [s₁ : HasOne α] [s₂ : HasAdd α] (a : α) : α := (bit0 a) + 1
|
||
|
||
attribute [matchPattern] HasZero.zero HasOne.one bit0 bit1 HasAdd.add HasNeg.neg
|
||
|
||
export HasInsert (insert)
|
||
|
||
/- The Empty collection -/
|
||
@[inline] def singleton {α : Type u} {γ : Type v} [HasEmptyc γ] [HasInsert α γ] (a : α) : γ :=
|
||
HasInsert.insert a ∅
|
||
|
||
/- Nat basic instances -/
|
||
@[extern cpp "lean::nat_add"]
|
||
protected def Nat.add : (@& Nat) → (@& Nat) → Nat
|
||
| a Nat.zero := a
|
||
| a (Nat.succ b) := Nat.succ (Nat.add a b)
|
||
|
||
/- We mark the following definitions as pattern to make sure they can be used in recursive equations,
|
||
and reduced by the equation Compiler. -/
|
||
attribute [matchPattern] Nat.add Nat.add._main
|
||
|
||
instance : HasZero Nat := ⟨Nat.zero⟩
|
||
|
||
instance : HasOne Nat := ⟨Nat.succ (Nat.zero)⟩
|
||
|
||
instance : HasAdd Nat := ⟨Nat.add⟩
|
||
|
||
/- Auxiliary constant used by equation compiler. -/
|
||
constant hugeFuel : Nat := 10000
|
||
|
||
def std.priority.default : Nat := 1000
|
||
def std.priority.max : Nat := 0xFFFFFFFF
|
||
|
||
protected def Nat.prio := std.priority.default + 100
|
||
|
||
/-
|
||
Global declarations of right binding strength
|
||
|
||
If a Module reassigns these, it will be incompatible with other modules that adhere to these
|
||
conventions.
|
||
|
||
When hovering over a symbol, use "C-c C-k" to see how to input it.
|
||
-/
|
||
def std.prec.max : Nat := 1024 -- the strength of application, identifiers, (, [, etc.
|
||
def std.prec.arrow : Nat := 25
|
||
|
||
/-
|
||
The next def is "max + 10". It can be used e.g. for postfix operations that should
|
||
be stronger than application.
|
||
-/
|
||
|
||
def std.prec.maxPlus : Nat := std.prec.max + 10
|
||
|
||
infixr × := Prod
|
||
-- notation for n-ary tuples
|
||
|
||
/- Some type that is not a scalar value in our runtime.
|
||
TODO: mark opaque -/
|
||
structure NonScalar :=
|
||
(val : Nat)
|
||
|
||
/- sizeof -/
|
||
|
||
class HasSizeof (α : Sort u) :=
|
||
(sizeof : α → Nat)
|
||
|
||
export HasSizeof (sizeof)
|
||
|
||
/-
|
||
Declare sizeof instances and theorems for types declared before HasSizeof.
|
||
From now on, the inductive Compiler will automatically generate sizeof instances and theorems.
|
||
-/
|
||
|
||
/- Every Type `α` has a default HasSizeof instance that just returns 0 for every element of `α` -/
|
||
protected def default.sizeof (α : Sort u) : α → Nat
|
||
| a := 0
|
||
|
||
instance defaultHasSizeof (α : Sort u) : HasSizeof α :=
|
||
⟨default.sizeof α⟩
|
||
|
||
protected def Nat.sizeof : Nat → Nat
|
||
| n := n
|
||
|
||
instance : HasSizeof Nat :=
|
||
⟨Nat.sizeof⟩
|
||
|
||
protected def Prod.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof β] : (Prod α β) → Nat
|
||
| ⟨a, b⟩ := 1 + sizeof a + sizeof b
|
||
|
||
instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Prod α β) :=
|
||
⟨Prod.sizeof⟩
|
||
|
||
protected def Sum.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof β] : (Sum α β) → Nat
|
||
| (Sum.inl a) := 1 + sizeof a
|
||
| (Sum.inr b) := 1 + sizeof b
|
||
|
||
instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Sum α β) :=
|
||
⟨Sum.sizeof⟩
|
||
|
||
protected def PSum.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof β] : (PSum α β) → Nat
|
||
| (PSum.inl a) := 1 + sizeof a
|
||
| (PSum.inr b) := 1 + sizeof b
|
||
|
||
instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (PSum α β) :=
|
||
⟨PSum.sizeof⟩
|
||
|
||
protected def Sigma.sizeof {α : Type u} {β : α → Type v} [HasSizeof α] [∀ a, HasSizeof (β a)] : Sigma β → Nat
|
||
| ⟨a, b⟩ := 1 + sizeof a + sizeof b
|
||
|
||
instance (α : Type u) (β : α → Type v) [HasSizeof α] [∀ a, HasSizeof (β a)] : HasSizeof (Sigma β) :=
|
||
⟨Sigma.sizeof⟩
|
||
|
||
protected def PSigma.sizeof {α : Type u} {β : α → Type v} [HasSizeof α] [∀ a, HasSizeof (β a)] : PSigma β → Nat
|
||
| ⟨a, b⟩ := 1 + sizeof a + sizeof b
|
||
|
||
instance (α : Type u) (β : α → Type v) [HasSizeof α] [∀ a, HasSizeof (β a)] : HasSizeof (PSigma β) :=
|
||
⟨PSigma.sizeof⟩
|
||
|
||
protected def PUnit.sizeof : PUnit → Nat
|
||
| u := 1
|
||
|
||
instance : HasSizeof PUnit := ⟨PUnit.sizeof⟩
|
||
|
||
protected def Bool.sizeof : Bool → Nat
|
||
| b := 1
|
||
|
||
instance : HasSizeof Bool := ⟨Bool.sizeof⟩
|
||
|
||
protected def Option.sizeof {α : Type u} [HasSizeof α] : Option α → Nat
|
||
| none := 1
|
||
| (some a) := 1 + sizeof a
|
||
|
||
instance (α : Type u) [HasSizeof α] : HasSizeof (Option α) :=
|
||
⟨Option.sizeof⟩
|
||
|
||
protected def List.sizeof {α : Type u} [HasSizeof α] : List α → Nat
|
||
| List.nil := 1
|
||
| (List.cons a l) := 1 + sizeof a + List.sizeof l
|
||
|
||
instance (α : Type u) [HasSizeof α] : HasSizeof (List α) :=
|
||
⟨List.sizeof⟩
|
||
|
||
protected def Subtype.sizeof {α : Type u} [HasSizeof α] {p : α → Prop} : Subtype p → Nat
|
||
| ⟨a, _⟩ := sizeof a
|
||
|
||
instance {α : Type u} [HasSizeof α] (p : α → Prop) : HasSizeof (Subtype p) :=
|
||
⟨Subtype.sizeof⟩
|
||
|
||
theorem natAddZero (n : Nat) : n + 0 = n := rfl
|
||
|
||
theorem optParamEq (α : Sort u) (default : α) : optParam α default = α := rfl
|
||
|
||
/-- Like `by applyInstance`, but not dependent on the tactic framework. -/
|
||
@[reducible] def inferInstance {α : Type u} [i : α] : α := i
|
||
@[reducible, elabSimple] def inferInstanceAs (α : Type u) [i : α] : α := i
|
||
|
||
/- Boolean operators -/
|
||
|
||
@[macroInline] def cond {a : Type u} : Bool → a → a → a
|
||
| true x y := x
|
||
| false x y := y
|
||
|
||
@[macroInline] def or : Bool → Bool → Bool
|
||
| true _ := true
|
||
| false b := b
|
||
|
||
@[macroInline] def and : Bool → Bool → Bool
|
||
| false _ := false
|
||
| true b := b
|
||
|
||
@[macroInline] def not : Bool → Bool
|
||
| true := false
|
||
| false := true
|
||
|
||
@[macroInline] def xor : Bool → Bool → Bool
|
||
| true b := not b
|
||
| false b := b
|
||
|
||
prefix ! := not
|
||
infix || := or
|
||
infix && := and
|
||
|
||
@[extern cpp inline "#1 || #2"] def strictOr (b₁ b₂ : Bool) := b₁ || b₂
|
||
@[extern cpp inline "#1 && #2"] def strictAnd (b₁ b₂ : Bool) := b₁ && b₂
|
||
|
||
@[inline] def bne {α : Type u} [HasBeq α] (a b : α) : Bool :=
|
||
!(a == b)
|
||
|
||
infix != := bne
|
||
|
||
/- Logical connectives an equality -/
|
||
|
||
def implies (a b : Prop) := a → b
|
||
|
||
theorem implies.trans {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) : implies p r :=
|
||
assume hp, h₂ (h₁ hp)
|
||
|
||
def trivial : True := ⟨⟩
|
||
|
||
@[macroInline] def False.elim {C : Sort u} (h : False) : C :=
|
||
False.rec (λ _, C) h
|
||
|
||
@[macroInline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : ¬a) : b :=
|
||
False.elim (h₂ h₁)
|
||
|
||
theorem mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a := assume ha : a, h₂ (h₁ ha)
|
||
|
||
theorem notFalse : ¬False := id
|
||
|
||
-- proof irrelevance is built in
|
||
theorem proofIrrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ := rfl
|
||
|
||
theorem id.def {α : Sort u} (a : α) : id a = a := rfl
|
||
|
||
@[macroInline] def Eq.mp {α β : Sort u} (h₁ : α = β) (h₂ : α) : β :=
|
||
Eq.recOn h₁ h₂
|
||
|
||
@[macroInline] def Eq.mpr {α β : Sort u} : (α = β) → β → α :=
|
||
λ h₁ h₂, Eq.recOn (Eq.symm h₁) h₂
|
||
|
||
@[elabAsEliminator]
|
||
theorem Eq.substr {α : Sort u} {p : α → Prop} {a b : α} (h₁ : b = a) (h₂ : p a) : p b :=
|
||
Eq.subst (Eq.symm h₁) h₂
|
||
|
||
theorem congr {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : f₁ = f₂) (h₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=
|
||
Eq.subst h₁ (Eq.subst h₂ rfl)
|
||
|
||
theorem congrFun {α : Sort u} {β : α → Sort v} {f g : Π x, β x} (h : f = g) (a : α) : f a = g a :=
|
||
Eq.subst h (Eq.refl (f a))
|
||
|
||
theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂ :=
|
||
congr rfl h
|
||
|
||
theorem transRelLeft {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c :=
|
||
h₂ ▸ h₁
|
||
|
||
theorem transRelRight {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : a = b) (h₂ : r b c) : r a c :=
|
||
h₁.symm ▸ h₂
|
||
|
||
theorem ofEqTrue {p : Prop} (h : p = True) : p :=
|
||
h.symm ▸ trivial
|
||
|
||
theorem notOfEqFalse {p : Prop} (h : p = False) : ¬p :=
|
||
assume hp, h ▸ hp
|
||
|
||
@[macroInline] def cast {α β : Sort u} (h : α = β) (a : α) : β :=
|
||
Eq.rec a h
|
||
|
||
theorem castProofIrrel {α β : Sort u} (h₁ h₂ : α = β) (a : α) : cast h₁ a = cast h₂ a := rfl
|
||
|
||
theorem castEq {α : Sort u} (h : α = α) (a : α) : cast h a = a := rfl
|
||
|
||
@[reducible] def Ne {α : Sort u} (a b : α) := ¬(a = b)
|
||
infix ≠ := Ne
|
||
|
||
theorem Ne.def {α : Sort u} (a b : α) : a ≠ b = ¬ (a = b) := rfl
|
||
|
||
section Ne
|
||
variable {α : Sort u}
|
||
variables {a b : α} {p : Prop}
|
||
|
||
theorem Ne.intro (h : a = b → False) : a ≠ b := h
|
||
|
||
theorem Ne.elim (h : a ≠ b) : a = b → False := h
|
||
|
||
theorem Ne.irrefl (h : a ≠ a) : False := h rfl
|
||
|
||
theorem Ne.symm (h : a ≠ b) : b ≠ a :=
|
||
assume (h₁ : b = a), h (h₁.symm)
|
||
|
||
theorem falseOfNe : a ≠ a → False := Ne.irrefl
|
||
|
||
theorem neFalseOfSelf : p → p ≠ False :=
|
||
assume (hp : p) (Heq : p = False), Heq ▸ hp
|
||
|
||
theorem neTrueOfNot : ¬p → p ≠ True :=
|
||
assume (hnp : ¬p) (Heq : p = True), (Heq ▸ hnp) trivial
|
||
|
||
theorem trueNeFalse : ¬True = False :=
|
||
neFalseOfSelf trivial
|
||
end Ne
|
||
|
||
theorem eqFalseOfNeTrue : ∀ {b : Bool}, b ≠ true → b = false
|
||
| true h := False.elim (h rfl)
|
||
| false h := rfl
|
||
|
||
theorem eqTrueOfNeFalse : ∀ {b : Bool}, b ≠ false → b = true
|
||
| true h := rfl
|
||
| false h := False.elim (h rfl)
|
||
|
||
section
|
||
variables {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
|
||
|
||
@[elabAsEliminator]
|
||
theorem {u1 u2} Heq.ndrec {α : Sort u2} {a : α} {C : Π {β : Sort u2}, β → Sort u1} (m : C a) {β : Sort u2} {b : β} (h : a ≅ b) : C b :=
|
||
@Heq.rec α a (λ β b _, C b) m β b h
|
||
|
||
@[elabAsEliminator]
|
||
theorem {u1 u2} Heq.ndrecOn {α : Sort u2} {a : α} {C : Π {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : C a) : C b :=
|
||
@Heq.rec α a (λ β b _, C b) m β b h
|
||
|
||
theorem Heq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b :=
|
||
Eq.recOn (eqOfHeq h₁) h₂
|
||
|
||
theorem Heq.subst {p : ∀ T : Sort u, T → Prop} (h₁ : a ≅ b) (h₂ : p α a) : p β b :=
|
||
Heq.ndrecOn h₁ h₂
|
||
|
||
theorem Heq.symm (h : a ≅ b) : b ≅ a :=
|
||
Heq.ndrecOn h (Heq.refl a)
|
||
|
||
theorem heqOfEq (h : a = a') : a ≅ a' :=
|
||
Eq.subst h (Heq.refl a)
|
||
|
||
theorem Heq.trans (h₁ : a ≅ b) (h₂ : b ≅ c) : a ≅ c :=
|
||
Heq.subst h₂ h₁
|
||
|
||
theorem heqOfHeqOfEq (h₁ : a ≅ b) (h₂ : b = b') : a ≅ b' :=
|
||
Heq.trans h₁ (heqOfEq h₂)
|
||
|
||
theorem heqOfEqOfHeq (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b :=
|
||
Heq.trans (heqOfEq h₁) h₂
|
||
|
||
def typeEqOfHeq (h : a ≅ b) : α = β :=
|
||
Heq.ndrecOn h (Eq.refl α)
|
||
end
|
||
|
||
theorem eqRecHeq {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} (h : a = a') (p : φ a), (Eq.recOn h p : φ a') ≅ p
|
||
| a _ rfl p := Heq.refl p
|
||
|
||
theorem ofHeqTrue {a : Prop} (h : a ≅ True) : a :=
|
||
ofEqTrue (eqOfHeq h)
|
||
|
||
theorem castHeq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a
|
||
| α _ rfl a := Heq.refl a
|
||
|
||
variables {a b c d : Prop}
|
||
|
||
theorem And.elim (h₁ : a ∧ b) (h₂ : a → b → c) : c :=
|
||
And.rec h₂ h₁
|
||
|
||
theorem And.swap : a ∧ b → b ∧ a :=
|
||
assume ⟨ha, hb⟩, ⟨hb, ha⟩
|
||
|
||
def And.symm := @And.swap
|
||
|
||
theorem Or.elim (h₁ : a ∨ b) (h₂ : a → c) (h₃ : b → c) : c :=
|
||
Or.rec h₂ h₃ h₁
|
||
|
||
theorem Or.swap (h : a ∨ b) : b ∨ a :=
|
||
Or.elim h Or.inr Or.inl
|
||
|
||
def Or.symm := @Or.swap
|
||
|
||
/- xor -/
|
||
def Xor (a b : Prop) : Prop := (a ∧ ¬ b) ∨ (b ∧ ¬ a)
|
||
|
||
theorem Iff.elim (h₁ : (a → b) → (b → a) → c) (h₂ : a ↔ b) : c :=
|
||
Iff.rec h₁ h₂
|
||
|
||
theorem Iff.left : (a ↔ b) → a → b := Iff.mp
|
||
|
||
theorem Iff.right : (a ↔ b) → b → a := Iff.mpr
|
||
|
||
theorem iffIffImpliesAndImplies (a b : Prop) : (a ↔ b) ↔ (a → b) ∧ (b → a) :=
|
||
Iff.intro (λ h, And.intro h.mp h.mpr) (λ h, Iff.intro h.left h.right)
|
||
|
||
theorem Iff.refl (a : Prop) : a ↔ a :=
|
||
Iff.intro (assume h, h) (assume h, h)
|
||
|
||
theorem Iff.rfl {a : Prop} : a ↔ a :=
|
||
Iff.refl a
|
||
|
||
theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=
|
||
Iff.intro
|
||
(assume ha, Iff.mp h₂ (Iff.mp h₁ ha))
|
||
(assume hc, Iff.mpr h₁ (Iff.mpr h₂ hc))
|
||
|
||
theorem Iff.symm (h : a ↔ b) : b ↔ a :=
|
||
Iff.intro (Iff.right h) (Iff.left h)
|
||
|
||
theorem Iff.comm : (a ↔ b) ↔ (b ↔ a) :=
|
||
Iff.intro Iff.symm Iff.symm
|
||
|
||
theorem Eq.toIff {a b : Prop} (h : a = b) : a ↔ b :=
|
||
Eq.recOn h Iff.rfl
|
||
|
||
theorem neqOfNotIff {a b : Prop} : ¬(a ↔ b) → a ≠ b :=
|
||
λ h₁ h₂,
|
||
have a ↔ b, from Eq.subst h₂ (Iff.refl a),
|
||
absurd this h₁
|
||
|
||
theorem notIffNotOfIff (h₁ : a ↔ b) : ¬a ↔ ¬b :=
|
||
Iff.intro
|
||
(assume (hna : ¬ a) (hb : b), hna (Iff.right h₁ hb))
|
||
(assume (hnb : ¬ b) (ha : a), hnb (Iff.left h₁ ha))
|
||
|
||
theorem ofIffTrue (h : a ↔ True) : a :=
|
||
Iff.mp (Iff.symm h) trivial
|
||
|
||
theorem notOfIffFalse : (a ↔ False) → ¬a := Iff.mp
|
||
|
||
theorem iffTrueIntro (h : a) : a ↔ True :=
|
||
Iff.intro
|
||
(λ hl, trivial)
|
||
(λ hr, h)
|
||
|
||
theorem iffFalseIntro (h : ¬a) : a ↔ False :=
|
||
Iff.intro h (False.rec (λ _, a))
|
||
|
||
theorem notNotIntro (ha : a) : ¬¬a :=
|
||
assume hna : ¬a, hna ha
|
||
|
||
theorem notTrue : (¬ True) ↔ False :=
|
||
iffFalseIntro (notNotIntro trivial)
|
||
|
||
/- or resolution rulses -/
|
||
|
||
theorem resolveLeft {a b : Prop} (h : a ∨ b) (na : ¬ a) : b :=
|
||
Or.elim h (λ ha, absurd ha na) id
|
||
|
||
theorem negResolveLeft {a b : Prop} (h : ¬ a ∨ b) (ha : a) : b :=
|
||
Or.elim h (λ na, absurd ha na) id
|
||
|
||
theorem resolveRight {a b : Prop} (h : a ∨ b) (nb : ¬ b) : a :=
|
||
Or.elim h id (λ hb, absurd hb nb)
|
||
|
||
theorem negResolveRight {a b : Prop} (h : a ∨ ¬ b) (hb : b) : a :=
|
||
Or.elim h id (λ nb, absurd hb nb)
|
||
|
||
/- Exists -/
|
||
|
||
theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop}
|
||
(h₁ : Exists (λ x, p x)) (h₂ : ∀ (a : α), p a → b) : b :=
|
||
Exists.rec h₂ h₁
|
||
|
||
/- Decidable -/
|
||
|
||
@[inlineIfReduce, nospecialize] def Decidable.decide (p : Prop) [h : Decidable p] : Bool :=
|
||
Decidable.casesOn h (λ h₁, false) (λ h₂, true)
|
||
|
||
export Decidable (isTrue isFalse decide)
|
||
|
||
instance beqOfEq {α : Type u} [DecidableEq α] : HasBeq α :=
|
||
⟨λ a b, decide (a = b)⟩
|
||
|
||
theorem decideTrueEqTrue (h : Decidable True) : @decide True h = true :=
|
||
Decidable.casesOn h (λ h, False.elim (Iff.mp notTrue h)) (λ _, rfl)
|
||
|
||
theorem decideFalseEqFalse (h : Decidable False) : @decide False h = false :=
|
||
Decidable.casesOn h (λ h, rfl) (λ h, False.elim h)
|
||
|
||
instance : Decidable True :=
|
||
isTrue trivial
|
||
|
||
instance : Decidable False :=
|
||
isFalse notFalse
|
||
|
||
-- We use "dependent" if-then-else to be able to communicate the if-then-else condition
|
||
-- to the branches
|
||
@[macroInline] def dite (c : Prop) [h : Decidable c] {α : Sort u} : (c → α) → (¬ c → α) → α :=
|
||
λ t e, Decidable.casesOn h e t
|
||
|
||
/- if-then-else -/
|
||
|
||
@[macroInline] def ite (c : Prop) [h : Decidable c] {α : Sort u} (t e : α) : α :=
|
||
Decidable.casesOn h (λ hnc, e) (λ hc, t)
|
||
|
||
namespace Decidable
|
||
variables {p q : Prop}
|
||
|
||
def recOnTrue [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : p) (h₄ : h₁ h₃)
|
||
: (Decidable.recOn h h₂ h₁ : Sort u) :=
|
||
Decidable.casesOn h (λ h, False.rec _ (h h₃)) (λ h, h₄)
|
||
|
||
def recOnFalse [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : ¬p) (h₄ : h₂ h₃)
|
||
: (Decidable.recOn h h₂ h₁ : Sort u) :=
|
||
Decidable.casesOn h (λ h, h₄) (λ h, False.rec _ (h₃ h))
|
||
|
||
@[macroInline] def byCases {q : Sort u} [s : Decidable p] (h1 : p → q) (h2 : ¬p → q) : q :=
|
||
match s with
|
||
| isTrue h := h1 h
|
||
| isFalse h := h2 h
|
||
|
||
theorem em (p : Prop) [Decidable p] : p ∨ ¬p :=
|
||
byCases Or.inl Or.inr
|
||
|
||
theorem byContradiction [Decidable p] (h : ¬p → False) : p :=
|
||
byCases id (λ np : ¬p, False.elim (h np))
|
||
|
||
theorem ofNotNot [Decidable p] : ¬ ¬ p → p :=
|
||
λ hnn, byContradiction (λ hn, absurd hn hnn)
|
||
|
||
theorem notNotIff (p) [Decidable p] : (¬ ¬ p) ↔ p :=
|
||
Iff.intro ofNotNot notNotIntro
|
||
|
||
theorem notAndIffOrNot (p q : Prop) [d₁ : Decidable p] [d₂ : Decidable q] : ¬ (p ∧ q) ↔ ¬ p ∨ ¬ q :=
|
||
Iff.intro
|
||
(λ h, match d₁, d₂ with
|
||
| isTrue h₁, isTrue h₂ := absurd (And.intro h₁ h₂) h
|
||
| _, isFalse h₂ := Or.inr h₂
|
||
| isFalse h₁, _ := Or.inl h₁)
|
||
(λ h ⟨hp, hq⟩, Or.elim h (λ h, h hp) (λ h, h hq))
|
||
|
||
end Decidable
|
||
|
||
section
|
||
variables {p q : Prop}
|
||
@[inline] def decidableOfDecidableOfIff (hp : Decidable p) (h : p ↔ q) : Decidable q :=
|
||
if hp : p then isTrue (Iff.mp h hp)
|
||
else isFalse (Iff.mp (notIffNotOfIff h) hp)
|
||
|
||
@[inline] def decidableOfDecidableOfEq (hp : Decidable p) (h : p = q) : Decidable q :=
|
||
decidableOfDecidableOfIff hp h.toIff
|
||
end
|
||
|
||
section
|
||
variables {p q : Prop}
|
||
|
||
@[macroInline] instance [Decidable p] [Decidable q] : Decidable (p ∧ q) :=
|
||
if hp : p then
|
||
if hq : q then isTrue ⟨hp, hq⟩
|
||
else isFalse (assume h : p ∧ q, hq (And.right h))
|
||
else isFalse (assume h : p ∧ q, hp (And.left h))
|
||
|
||
@[macroInline] instance [Decidable p] [Decidable q] : Decidable (p ∨ q) :=
|
||
if hp : p then isTrue (Or.inl hp) else
|
||
if hq : q then isTrue (Or.inr hq) else
|
||
isFalse (λ h, Or.elim h hp hq)
|
||
|
||
instance [Decidable p] : Decidable (¬p) :=
|
||
if hp : p then isFalse (absurd hp) else isTrue hp
|
||
|
||
@[macroInline] instance implies.Decidable [Decidable p] [Decidable q] : Decidable (p → q) :=
|
||
if hp : p then
|
||
if hq : q then isTrue (assume h, hq)
|
||
else isFalse (assume h : p → q, absurd (h hp) hq)
|
||
else isTrue (assume h, absurd h hp)
|
||
|
||
instance [Decidable p] [Decidable q] : Decidable (p ↔ q) :=
|
||
if hp : p then
|
||
if hq : q then isTrue ⟨λ_, hq, λ_, hp⟩
|
||
else isFalse $ λh, hq (h.1 hp)
|
||
else
|
||
if hq : q then isFalse $ λh, hp (h.2 hq)
|
||
else isTrue $ ⟨λh, absurd h hp, λh, absurd h hq⟩
|
||
|
||
instance [Decidable p] [Decidable q] : Decidable (Xor p q) :=
|
||
if hp : p then
|
||
if hq : q then isFalse (λ h, Or.elim h (λ ⟨_, h⟩, h hq : ¬(p ∧ ¬ q)) (λ ⟨_, h⟩, h hp : ¬(q ∧ ¬ p)))
|
||
else isTrue $ Or.inl ⟨hp, hq⟩
|
||
else
|
||
if hq : q then isTrue $ Or.inr ⟨hq, hp⟩
|
||
else isFalse (λ h, Or.elim h (λ ⟨h, _⟩, hp h : ¬(p ∧ ¬ q)) (λ ⟨h, _⟩, hq h : ¬(q ∧ ¬ p)))
|
||
|
||
end
|
||
|
||
@[inline] instance {α : Sort u} [DecidableEq α] (a b : α) : Decidable (a ≠ b) :=
|
||
match decEq a b with
|
||
| isTrue h := isFalse $ λ h', absurd h h'
|
||
| isFalse h := isTrue h
|
||
|
||
theorem Bool.falseNeTrue (h : false = true) : False :=
|
||
Bool.noConfusion h
|
||
|
||
instance : DecidableEq Bool :=
|
||
{decEq := λ a b, match a, b with
|
||
| false, false := isTrue rfl
|
||
| false, true := isFalse Bool.falseNeTrue
|
||
| true, false := isFalse (Ne.symm Bool.falseNeTrue)
|
||
| true, true := isTrue rfl}
|
||
|
||
/- if-then-else expression theorems -/
|
||
|
||
theorem ifPos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t e : α} : (ite c t e) = t :=
|
||
match h with
|
||
| (isTrue hc) := rfl
|
||
| (isFalse hnc) := absurd hc hnc
|
||
|
||
theorem ifNeg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t e : α} : (ite c t e) = e :=
|
||
match h with
|
||
| (isTrue hc) := absurd hc hnc
|
||
| (isFalse hnc) := rfl
|
||
|
||
-- Remark: dite and ite are "defally equal" when we ignore the proofs.
|
||
theorem difEqIf (c : Prop) [h : Decidable c] {α : Sort u} (t : α) (e : α) : dite c (λ h, t) (λ h, e) = ite c t e :=
|
||
match h with
|
||
| (isTrue hc) := rfl
|
||
| (isFalse hnc) := rfl
|
||
|
||
instance {c t e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] : Decidable (if c then t else e) :=
|
||
match dC with
|
||
| (isTrue hc) := dT
|
||
| (isFalse hc) := dE
|
||
|
||
instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : ∀ h, Decidable (t h)] [dE : ∀ h, Decidable (e h)] : Decidable (if h : c then t h else e h) :=
|
||
match dC with
|
||
| (isTrue hc) := dT hc
|
||
| (isFalse hc) := dE hc
|
||
|
||
/-- Universe lifting operation -/
|
||
structure {r s} ULift (α : Type s) : Type (max s r) :=
|
||
up :: (down : α)
|
||
|
||
namespace ULift
|
||
/- Bijection between α and ULift.{v} α -/
|
||
theorem upDown {α : Type u} : ∀ (b : ULift.{v} α), up (down b) = b
|
||
| (up a) := rfl
|
||
|
||
theorem downUp {α : Type u} (a : α) : down (up.{v} a) = a := rfl
|
||
end ULift
|
||
|
||
/-- Universe lifting operation from Sort to Type -/
|
||
structure PLift (α : Sort u) : Type u :=
|
||
up :: (down : α)
|
||
|
||
namespace PLift
|
||
/- Bijection between α and PLift α -/
|
||
theorem upDown {α : Sort u} : ∀ (b : PLift α), up (down b) = b
|
||
| (up a) := rfl
|
||
|
||
theorem downUp {α : Sort u} (a : α) : down (up a) = a := rfl
|
||
end PLift
|
||
|
||
/- pointed types -/
|
||
structure PointedType :=
|
||
(type : Type u) (val : type)
|
||
|
||
/- Inhabited -/
|
||
|
||
class Inhabited (α : Sort u) :=
|
||
(default : α)
|
||
|
||
constant default (α : Sort u) [Inhabited α] : α :=
|
||
Inhabited.default α
|
||
|
||
@[inline, irreducible] def arbitrary (α : Sort u) [Inhabited α] : α :=
|
||
default α
|
||
|
||
instance Prop.Inhabited : Inhabited Prop :=
|
||
⟨True⟩
|
||
|
||
instance Fun.Inhabited (α : Sort u) {β : Sort v} [h : Inhabited β] : Inhabited (α → β) :=
|
||
Inhabited.casesOn h (λ b, ⟨λ a, b⟩)
|
||
|
||
instance Pi.Inhabited (α : Sort u) {β : α → Sort v} [Π x, Inhabited (β x)] : Inhabited (Π x, β x) :=
|
||
⟨λ a, default (β a)⟩
|
||
|
||
instance : Inhabited Bool := ⟨false⟩
|
||
|
||
instance : Inhabited True := ⟨trivial⟩
|
||
|
||
instance : Inhabited Nat := ⟨0⟩
|
||
|
||
instance : Inhabited NonScalar := ⟨⟨default _⟩⟩
|
||
|
||
instance : Inhabited PointedType := ⟨{type := PUnit, val := ⟨⟩}⟩
|
||
|
||
class inductive Nonempty (α : Sort u) : Prop
|
||
| intro (val : α) : Nonempty
|
||
|
||
protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p :=
|
||
Nonempty.rec h₂ h₁
|
||
|
||
instance nonemptyOfInhabited {α : Sort u} [Inhabited α] : Nonempty α :=
|
||
⟨default α⟩
|
||
|
||
theorem nonemptyOfExists {α : Sort u} {p : α → Prop} : Exists (λ x, p x) → Nonempty α
|
||
| ⟨w, h⟩ := ⟨w⟩
|
||
|
||
/- Subsingleton -/
|
||
|
||
class inductive Subsingleton (α : Sort u) : Prop
|
||
| intro (h : ∀ a b : α, a = b) : Subsingleton
|
||
|
||
protected def Subsingleton.elim {α : Sort u} [h : Subsingleton α] : ∀ (a b : α), a = b :=
|
||
Subsingleton.casesOn h (λ p, p)
|
||
|
||
protected def Subsingleton.helim {α β : Sort u} [h : Subsingleton α] (h : α = β) : ∀ (a : α) (b : β), a ≅ b :=
|
||
Eq.recOn h (λ a b : α, heqOfEq (Subsingleton.elim a b))
|
||
|
||
instance subsingletonProp (p : Prop) : Subsingleton p :=
|
||
⟨λ a b, proofIrrel a b⟩
|
||
|
||
instance (p : Prop) : Subsingleton (Decidable p) :=
|
||
Subsingleton.intro (λ d₁,
|
||
match d₁ with
|
||
| (isTrue t₁) := (λ d₂,
|
||
match d₂ with
|
||
| (isTrue t₂) := Eq.recOn (proofIrrel t₁ t₂) rfl
|
||
| (isFalse f₂) := absurd t₁ f₂)
|
||
| (isFalse f₁) := (λ d₂,
|
||
match d₂ with
|
||
| (isTrue t₂) := absurd t₂ f₁
|
||
| (isFalse f₂) := Eq.recOn (proofIrrel f₁ f₂) rfl))
|
||
|
||
protected theorem recSubsingleton {p : Prop} [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u}
|
||
[h₃ : Π (h : p), Subsingleton (h₁ h)] [h₄ : Π (h : ¬p), Subsingleton (h₂ h)]
|
||
: Subsingleton (Decidable.casesOn h h₂ h₁) :=
|
||
match h with
|
||
| (isTrue h) := h₃ h
|
||
| (isFalse h) := h₄ h
|
||
|
||
section relation
|
||
variables {α : Sort u} {β : Sort v} (r : β → β → Prop)
|
||
|
||
def Reflexive := ∀ x, r x x
|
||
|
||
def Symmetric := ∀ {x y}, r x y → r y x
|
||
|
||
def Transitive := ∀ {x y z}, r x y → r y z → r x z
|
||
|
||
def Equivalence := Reflexive r ∧ Symmetric r ∧ Transitive r
|
||
|
||
def Total := ∀ x y, r x y ∨ r y x
|
||
|
||
def mkEquivalence (rfl : Reflexive r) (symm : Symmetric r) (trans : Transitive r) : Equivalence r :=
|
||
⟨rfl, @symm, @trans⟩
|
||
|
||
def Irreflexive := ∀ x, ¬ r x x
|
||
|
||
def AntiSymmetric := ∀ {x y}, r x y → r y x → x = y
|
||
|
||
def emptyRelation := λ a₁ a₂ : α, False
|
||
|
||
def Subrelation (q r : β → β → Prop) := ∀ {x y}, q x y → r x y
|
||
|
||
def InvImage (f : α → β) : α → α → Prop :=
|
||
λ a₁ a₂, r (f a₁) (f a₂)
|
||
|
||
theorem InvImage.Transitive (f : α → β) (h : Transitive r) : Transitive (InvImage r f) :=
|
||
λ (a₁ a₂ a₃ : α) (h₁ : InvImage r f a₁ a₂) (h₂ : InvImage r f a₂ a₃), h h₁ h₂
|
||
|
||
theorem InvImage.Irreflexive (f : α → β) (h : Irreflexive r) : Irreflexive (InvImage r f) :=
|
||
λ (a : α) (h₁ : InvImage r f a a), h (f a) h₁
|
||
|
||
inductive TC {α : Sort u} (r : α → α → Prop) : α → α → Prop
|
||
| base : ∀ a b, r a b → TC a b
|
||
| trans : ∀ a b c, TC a b → TC b c → TC a c
|
||
|
||
@[elabAsEliminator]
|
||
theorem {u1 u2} TC.ndrec {α : Sort u} {r : α → α → Prop} {C : α → α → Prop}
|
||
(m₁ : ∀ (a b : α), r a b → C a b)
|
||
(m₂ : ∀ (a b c : α), TC r a b → TC r b c → C a b → C b c → C a c)
|
||
{a b : α} (h : TC r a b) : C a b :=
|
||
@TC.rec α r (λ a b _, C a b) m₁ m₂ a b h
|
||
|
||
@[elabAsEliminator]
|
||
theorem {u1 u2} TC.ndrecOn {α : Sort u} {r : α → α → Prop} {C : α → α → Prop}
|
||
{a b : α} (h : TC r a b)
|
||
(m₁ : ∀ (a b : α), r a b → C a b)
|
||
(m₂ : ∀ (a b c : α), TC r a b → TC r b c → C a b → C b c → C a c)
|
||
: C a b :=
|
||
@TC.rec α r (λ a b _, C a b) m₁ m₂ a b h
|
||
|
||
end relation
|
||
|
||
section Binary
|
||
variables {α : Type u} {β : Type v}
|
||
variable f : α → α → α
|
||
|
||
def Commutative := ∀ a b, f a b = f b a
|
||
def Associative := ∀ a b c, f (f a b) c = f a (f b c)
|
||
def RightCommutative (h : β → α → β) := ∀ b a₁ a₂, h (h b a₁) a₂ = h (h b a₂) a₁
|
||
def LeftCommutative (h : α → β → β) := ∀ a₁ a₂ b, h a₁ (h a₂ b) = h a₂ (h a₁ b)
|
||
|
||
theorem leftComm : Commutative f → Associative f → LeftCommutative f :=
|
||
assume hcomm hassoc, assume a b c,
|
||
((Eq.symm (hassoc a b c)).trans (hcomm a b ▸ rfl : f (f a b) c = f (f b a) c)).trans (hassoc b a c)
|
||
|
||
theorem rightComm : Commutative f → Associative f → RightCommutative f :=
|
||
assume hcomm hassoc, assume a b c,
|
||
((hassoc a b c).trans (hcomm b c ▸ rfl : f a (f b c) = f a (f c b))).trans (Eq.symm (hassoc a c b))
|
||
|
||
end Binary
|
||
|
||
/- Subtype -/
|
||
|
||
namespace Subtype
|
||
def existsOfSubtype {α : Type u} {p : α → Prop} : { x // p x } → Exists (λ x, p x)
|
||
| ⟨a, h⟩ := ⟨a, h⟩
|
||
|
||
variables {α : Type u} {p : α → Prop}
|
||
|
||
theorem tagIrrelevant {a : α} (h1 h2 : p a) : mk a h1 = mk a h2 :=
|
||
rfl
|
||
|
||
protected theorem eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
|
||
| ⟨x, h1⟩ ⟨.(x), h2⟩ rfl := rfl
|
||
|
||
theorem eta (a : {x // p x}) (h : p (val a)) : mk (val a) h = a :=
|
||
Subtype.eq rfl
|
||
|
||
instance {α : Type u} {p : α → Prop} {a : α} (h : p a) : Inhabited {x // p x} :=
|
||
⟨⟨a, h⟩⟩
|
||
|
||
instance {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
|
||
{decEq := λ ⟨a, h₁⟩ ⟨b, h₂⟩,
|
||
if h : a = b then isTrue (Subtype.eq h)
|
||
else isFalse (λ h', Subtype.noConfusion h' (λ h', absurd h' h))}
|
||
end Subtype
|
||
|
||
/- Sum -/
|
||
|
||
infixr ⊕ := Sum
|
||
|
||
section
|
||
variables {α : Type u} {β : Type v}
|
||
|
||
instance Sum.inhabitedLeft [h : Inhabited α] : Inhabited (α ⊕ β) :=
|
||
⟨Sum.inl (default α)⟩
|
||
|
||
instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (α ⊕ β) :=
|
||
⟨Sum.inr (default β)⟩
|
||
|
||
instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (α ⊕ β) :=
|
||
{decEq := λ a b,
|
||
match a, b with
|
||
| (Sum.inl a), (Sum.inl b) := if h : a = b then isTrue (h ▸ rfl)
|
||
else isFalse (λ h', Sum.noConfusion h' (λ h', absurd h' h))
|
||
| (Sum.inr a), (Sum.inr b) := if h : a = b then isTrue (h ▸ rfl)
|
||
else isFalse (λ h', Sum.noConfusion h' (λ h', absurd h' h))
|
||
| (Sum.inr a), (Sum.inl b) := isFalse (λ h, Sum.noConfusion h)
|
||
| (Sum.inl a), (Sum.inr b) := isFalse (λ h, Sum.noConfusion h)}
|
||
end
|
||
|
||
/- Product -/
|
||
|
||
section
|
||
variables {α : Type u} {β : Type v}
|
||
|
||
instance [Inhabited α] [Inhabited β] : Inhabited (Prod α β) :=
|
||
⟨(default α, default β)⟩
|
||
|
||
instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
|
||
{decEq := λ ⟨a, b⟩ ⟨a', b'⟩,
|
||
match (decEq a a') with
|
||
| (isTrue e₁) :=
|
||
(match (decEq b b') with
|
||
| (isTrue e₂) := isTrue (Eq.recOn e₁ (Eq.recOn e₂ rfl))
|
||
| (isFalse n₂) := isFalse (assume h, Prod.noConfusion h (λ e₁' e₂', absurd e₂' n₂)))
|
||
| (isFalse n₁) := isFalse (assume h, Prod.noConfusion h (λ e₁' e₂', absurd e₁' n₁))}
|
||
|
||
instance [HasLess α] [HasLess β] : HasLess (α × β) :=
|
||
⟨λ s t, s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)⟩
|
||
|
||
instance prodHasDecidableLt
|
||
[HasLess α] [HasLess β] [DecidableEq α] [DecidableEq β]
|
||
[Π a b : α, Decidable (a < b)] [Π a b : β, Decidable (a < b)]
|
||
: Π s t : α × β, Decidable (s < t) :=
|
||
λ t s, Or.Decidable
|
||
|
||
theorem Prod.ltDef [HasLess α] [HasLess β] (s t : α × β) : (s < t) = (s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)) :=
|
||
rfl
|
||
end
|
||
|
||
def {u₁ u₂ v₁ v₂} Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂}
|
||
(f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
|
||
| (a, b) := (f a, g b)
|
||
|
||
/- Dependent products -/
|
||
|
||
-- notation `Σ` binders `, ` r:(scoped p, Sigma p) := r
|
||
-- notation `Σ'` binders `, ` r:(scoped p, PSigma p) := r
|
||
|
||
theorem exOfPsig {α : Type u} {p : α → Prop} : (PSigma (λ x, p x)) → Exists (λ x, p x)
|
||
| ⟨x, hx⟩ := ⟨x, hx⟩
|
||
|
||
section
|
||
variables {α : Type u} {β : α → Type v}
|
||
|
||
protected theorem Sigma.eq : ∀ {p₁ p₂ : Sigma (λ a : α, β a)} (h₁ : p₁.1 = p₂.1), (Eq.recOn h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂
|
||
| ⟨a, b⟩ ⟨.(a), .(b)⟩ rfl rfl := rfl
|
||
end
|
||
|
||
section
|
||
variables {α : Sort u} {β : α → Sort v}
|
||
|
||
protected theorem PSigma.eq : ∀ {p₁ p₂ : PSigma β} (h₁ : p₁.1 = p₂.1), (Eq.recOn h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂
|
||
| ⟨a, b⟩ ⟨.(a), .(b)⟩ rfl rfl := rfl
|
||
end
|
||
|
||
/- Universe polymorphic unit -/
|
||
|
||
theorem punitEq (a b : PUnit) : a = b :=
|
||
PUnit.recOn a (PUnit.recOn b rfl)
|
||
|
||
theorem punitEqPUnit (a : PUnit) : a = () :=
|
||
punitEq a ()
|
||
|
||
instance : Subsingleton PUnit :=
|
||
Subsingleton.intro punitEq
|
||
|
||
instance : Inhabited PUnit :=
|
||
⟨⟨⟩⟩
|
||
|
||
instance : DecidableEq PUnit :=
|
||
{decEq := λ a b, isTrue (punitEq a b)}
|
||
|
||
/- Setoid -/
|
||
|
||
class Setoid (α : Sort u) :=
|
||
(r : α → α → Prop) (iseqv : Equivalence r)
|
||
|
||
instance setoidHasEquiv {α : Sort u} [Setoid α] : HasEquiv α :=
|
||
⟨Setoid.r⟩
|
||
|
||
namespace Setoid
|
||
variables {α : Sort u} [Setoid α]
|
||
|
||
theorem refl (a : α) : a ≈ a :=
|
||
match Setoid.iseqv α with
|
||
| ⟨hRefl, hSymm, hTrans⟩ := hRefl a
|
||
|
||
theorem symm {a b : α} (hab : a ≈ b) : b ≈ a :=
|
||
match Setoid.iseqv α with
|
||
| ⟨hRefl, hSymm, hTrans⟩ := hSymm hab
|
||
|
||
theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c :=
|
||
match Setoid.iseqv α with
|
||
| ⟨hRefl, hSymm, hTrans⟩ := hTrans hab hbc
|
||
end Setoid
|
||
|
||
/- Propositional extensionality -/
|
||
|
||
axiom propext {a b : Prop} : (a ↔ b) → a = b
|
||
|
||
theorem eqTrueIntro {a : Prop} (h : a) : a = True :=
|
||
propext (iffTrueIntro h)
|
||
|
||
theorem eqFalseIntro {a : Prop} (h : ¬a) : a = False :=
|
||
propext (iffFalseIntro h)
|
||
|
||
/- Quotients -/
|
||
|
||
-- Iff can now be used to do substitutions in a calculation
|
||
theorem iffSubst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) : p b :=
|
||
Eq.subst (propext h₁) h₂
|
||
|
||
namespace Quot
|
||
axiom sound : Π {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r b
|
||
|
||
attribute [elabAsEliminator] lift ind
|
||
|
||
protected theorem liftBeta {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) (c : ∀ a b, r a b → f a = f b) (a : α) : lift f c (Quot.mk r a) = f a :=
|
||
rfl
|
||
|
||
protected theorem indBeta {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} (p : ∀ a, β (Quot.mk r a)) (a : α) : (ind p (Quot.mk r a) : β (Quot.mk r a)) = p a :=
|
||
rfl
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def liftOn {α : Sort u} {β : Sort v} {r : α → α → Prop} (q : Quot r) (f : α → β) (c : ∀ a b, r a b → f a = f b) : β :=
|
||
lift f c q
|
||
|
||
@[elabAsEliminator]
|
||
protected theorem inductionOn {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} (q : Quot r) (h : ∀ a, β (Quot.mk r a)) : β q :=
|
||
ind h q
|
||
|
||
theorem existsRep {α : Sort u} {r : α → α → Prop} (q : Quot r) : Exists (λ a : α, (Quot.mk r a) = q) :=
|
||
Quot.inductionOn q (λ a, ⟨a, rfl⟩)
|
||
|
||
section
|
||
variable {α : Sort u}
|
||
variable {r : α → α → Prop}
|
||
variable {β : Quot r → Sort v}
|
||
|
||
@[reducible, macroInline]
|
||
protected def indep (f : Π a, β (Quot.mk r a)) (a : α) : PSigma β :=
|
||
⟨Quot.mk r a, f a⟩
|
||
|
||
protected theorem indepCoherent (f : Π a, β (Quot.mk r a))
|
||
(h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β (Quot.mk r b)) = f b)
|
||
: ∀ a b, r a b → Quot.indep f a = Quot.indep f b :=
|
||
λ a b e, PSigma.eq (sound e) (h a b e)
|
||
|
||
protected theorem liftIndepPr1
|
||
(f : Π a, β (Quot.mk r a)) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β (Quot.mk r b)) = f b)
|
||
(q : Quot r) : (lift (Quot.indep f) (Quot.indepCoherent f h) q).1 = q :=
|
||
Quot.ind (λ (a : α), Eq.refl (Quot.indep f a).1) q
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def rec
|
||
(f : Π a, β (Quot.mk r a)) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β (Quot.mk r b)) = f b)
|
||
(q : Quot r) : β q :=
|
||
Eq.ndrecOn (Quot.liftIndepPr1 f h q) ((lift (Quot.indep f) (Quot.indepCoherent f h) q).2)
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def recOn
|
||
(q : Quot r) (f : Π a, β (Quot.mk r a)) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β (Quot.mk r b)) = f b) : β q :=
|
||
Quot.rec f h q
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def recOnSubsingleton
|
||
[h : ∀ a, Subsingleton (β (Quot.mk r a))] (q : Quot r) (f : Π a, β (Quot.mk r a)) : β q :=
|
||
Quot.rec f (λ a b h, Subsingleton.elim _ (f b)) q
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def hrecOn
|
||
(q : Quot r) (f : Π a, β (Quot.mk r a)) (c : ∀ (a b : α) (p : r a b), f a ≅ f b) : β q :=
|
||
Quot.recOn q f $
|
||
λ a b p, eqOfHeq $
|
||
have p₁ : (Eq.rec (f a) (sound p) : β (Quot.mk r b)) ≅ f a, from eqRecHeq (sound p) (f a),
|
||
Heq.trans p₁ (c a b p)
|
||
|
||
end
|
||
end Quot
|
||
|
||
def Quotient {α : Sort u} (s : Setoid α) :=
|
||
@Quot α Setoid.r
|
||
|
||
namespace Quotient
|
||
|
||
@[inline]
|
||
protected def mk {α : Sort u} [s : Setoid α] (a : α) : Quotient s :=
|
||
Quot.mk Setoid.r a
|
||
|
||
notation `⟦`:max a `⟧`:0 := Quotient.mk a
|
||
|
||
def sound {α : Sort u} [s : Setoid α] {a b : α} : a ≈ b → ⟦a⟧ = ⟦b⟧ :=
|
||
Quot.sound
|
||
|
||
@[reducible, elabAsEliminator]
|
||
protected def lift {α : Sort u} {β : Sort v} [s : Setoid α] (f : α → β) : (∀ a b, a ≈ b → f a = f b) → Quotient s → β :=
|
||
Quot.lift f
|
||
|
||
@[elabAsEliminator]
|
||
protected theorem ind {α : Sort u} [s : Setoid α] {β : Quotient s → Prop} : (∀ a, β ⟦a⟧) → ∀ q, β q :=
|
||
Quot.ind
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def liftOn {α : Sort u} {β : Sort v} [s : Setoid α] (q : Quotient s) (f : α → β) (c : ∀ a b, a ≈ b → f a = f b) : β :=
|
||
Quot.liftOn q f c
|
||
|
||
@[elabAsEliminator]
|
||
protected theorem inductionOn {α : Sort u} [s : Setoid α] {β : Quotient s → Prop} (q : Quotient s) (h : ∀ a, β ⟦a⟧) : β q :=
|
||
Quot.inductionOn q h
|
||
|
||
theorem existsRep {α : Sort u} [s : Setoid α] (q : Quotient s) : Exists (λ a : α, ⟦a⟧ = q) :=
|
||
Quot.existsRep q
|
||
|
||
section
|
||
variable {α : Sort u}
|
||
variable [s : Setoid α]
|
||
variable {β : Quotient s → Sort v}
|
||
|
||
@[inline]
|
||
protected def rec
|
||
(f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : a ≈ b), (Eq.rec (f a) (Quotient.sound p) : β ⟦b⟧) = f b)
|
||
(q : Quotient s) : β q :=
|
||
Quot.rec f h q
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def recOn
|
||
(q : Quotient s) (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : a ≈ b), (Eq.rec (f a) (Quotient.sound p) : β ⟦b⟧) = f b) : β q :=
|
||
Quot.recOn q f h
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def recOnSubsingleton
|
||
[h : ∀ a, Subsingleton (β ⟦a⟧)] (q : Quotient s) (f : Π a, β ⟦a⟧) : β q :=
|
||
@Quot.recOnSubsingleton _ _ _ h q f
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def hrecOn
|
||
(q : Quotient s) (f : Π a, β ⟦a⟧) (c : ∀ (a b : α) (p : a ≈ b), f a ≅ f b) : β q :=
|
||
Quot.hrecOn q f c
|
||
end
|
||
|
||
section
|
||
universes uA uB uC
|
||
variables {α : Sort uA} {β : Sort uB} {φ : Sort uC}
|
||
variables [s₁ : Setoid α] [s₂ : Setoid β]
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def lift₂
|
||
(f : α → β → φ)(c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂)
|
||
(q₁ : Quotient s₁) (q₂ : Quotient s₂) : φ :=
|
||
Quotient.lift
|
||
(λ (a₁ : α), Quotient.lift (f a₁) (λ (a b : β), c a₁ a a₁ b (Setoid.refl a₁)) q₂)
|
||
(λ (a b : α) (h : a ≈ b),
|
||
@Quotient.ind β s₂
|
||
(λ (a1 : Quotient s₂),
|
||
(Quotient.lift (f a) (λ (a1 b : β), c a a1 a b (Setoid.refl a)) a1)
|
||
=
|
||
(Quotient.lift (f b) (λ (a b1 : β), c b a b b1 (Setoid.refl b)) a1))
|
||
(λ (a' : β), c a a' b a' h (Setoid.refl a'))
|
||
q₂)
|
||
q₁
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def liftOn₂
|
||
(q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : α → β → φ) (c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) : φ :=
|
||
Quotient.lift₂ f c q₁ q₂
|
||
|
||
@[elabAsEliminator]
|
||
protected theorem ind₂ {φ : Quotient s₁ → Quotient s₂ → Prop} (h : ∀ a b, φ ⟦a⟧ ⟦b⟧) (q₁ : Quotient s₁) (q₂ : Quotient s₂) : φ q₁ q₂ :=
|
||
Quotient.ind (λ a₁, Quotient.ind (λ a₂, h a₁ a₂) q₂) q₁
|
||
|
||
@[elabAsEliminator]
|
||
protected theorem inductionOn₂
|
||
{φ : Quotient s₁ → Quotient s₂ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (h : ∀ a b, φ ⟦a⟧ ⟦b⟧) : φ q₁ q₂ :=
|
||
Quotient.ind (λ a₁, Quotient.ind (λ a₂, h a₁ a₂) q₂) q₁
|
||
|
||
@[elabAsEliminator]
|
||
protected theorem inductionOn₃
|
||
[s₃ : Setoid φ]
|
||
{δ : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (q₃ : Quotient s₃) (h : ∀ a b c, δ ⟦a⟧ ⟦b⟧ ⟦c⟧)
|
||
: δ q₁ q₂ q₃ :=
|
||
Quotient.ind (λ a₁, Quotient.ind (λ a₂, Quotient.ind (λ a₃, h a₁ a₂ a₃) q₃) q₂) q₁
|
||
end
|
||
|
||
section Exact
|
||
variable {α : Sort u}
|
||
|
||
private def rel [s : Setoid α] (q₁ q₂ : Quotient s) : Prop :=
|
||
Quotient.liftOn₂ q₁ q₂
|
||
(λ a₁ a₂, a₁ ≈ a₂)
|
||
(λ a₁ a₂ b₁ b₂ a₁b₁ a₂b₂,
|
||
propext (Iff.intro
|
||
(λ a₁a₂, Setoid.trans (Setoid.symm a₁b₁) (Setoid.trans a₁a₂ a₂b₂))
|
||
(λ b₁b₂, Setoid.trans a₁b₁ (Setoid.trans b₁b₂ (Setoid.symm a₂b₂)))))
|
||
|
||
private theorem rel.refl [s : Setoid α] : ∀ q : Quotient s, rel q q :=
|
||
λ q, Quot.inductionOn q (λ a, Setoid.refl a)
|
||
|
||
private theorem eqImpRel [s : Setoid α] {q₁ q₂ : Quotient s} : q₁ = q₂ → rel q₁ q₂ :=
|
||
assume h, Eq.ndrecOn h (rel.refl q₁)
|
||
|
||
theorem exact [s : Setoid α] {a b : α} : ⟦a⟧ = ⟦b⟧ → a ≈ b :=
|
||
assume h, eqImpRel h
|
||
end Exact
|
||
|
||
section
|
||
universes uA uB uC
|
||
variables {α : Sort uA} {β : Sort uB}
|
||
variables [s₁ : Setoid α] [s₂ : Setoid β]
|
||
|
||
@[reducible, elabAsEliminator]
|
||
protected def recOnSubsingleton₂
|
||
{φ : Quotient s₁ → Quotient s₂ → Sort uC} [h : ∀ a b, Subsingleton (φ ⟦a⟧ ⟦b⟧)]
|
||
(q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : Π a b, φ ⟦a⟧ ⟦b⟧) : φ q₁ q₂:=
|
||
@Quotient.recOnSubsingleton _ s₁ (λ q, φ q q₂) (λ a, Quotient.ind (λ b, h a b) q₂) q₁
|
||
(λ a, Quotient.recOnSubsingleton q₂ (λ b, f a b))
|
||
|
||
end
|
||
end Quotient
|
||
|
||
section
|
||
variable {α : Type u}
|
||
variable (r : α → α → Prop)
|
||
|
||
inductive EqvGen : α → α → Prop
|
||
| rel {} : Π x y, r x y → EqvGen x y
|
||
| refl {} : Π x, EqvGen x x
|
||
| symm {} : Π x y, EqvGen x y → EqvGen y x
|
||
| trans {} : Π x y z, EqvGen x y → EqvGen y z → EqvGen x z
|
||
|
||
theorem EqvGen.isEquivalence : Equivalence (@EqvGen α r) :=
|
||
mkEquivalence _ EqvGen.refl EqvGen.symm EqvGen.trans
|
||
|
||
def EqvGen.Setoid : Setoid α :=
|
||
Setoid.mk _ (EqvGen.isEquivalence r)
|
||
|
||
theorem Quot.exact {a b : α} (H : Quot.mk r a = Quot.mk r b) : EqvGen r a b :=
|
||
@Quotient.exact _ (EqvGen.Setoid r) a b (@congrArg _ _ _ _
|
||
(Quot.lift (@Quotient.mk _ (EqvGen.Setoid r)) (λx y h, Quot.sound (EqvGen.rel x y h))) H)
|
||
|
||
theorem Quot.eqvGenSound {r : α → α → Prop} {a b : α} (H : EqvGen r a b) : Quot.mk r a = Quot.mk r b :=
|
||
EqvGen.recOn H
|
||
(λ x y h, Quot.sound h)
|
||
(λ x, rfl)
|
||
(λ x y _ IH, Eq.symm IH)
|
||
(λ x y z _ _ IH₁ IH₂, Eq.trans IH₁ IH₂)
|
||
end
|
||
|
||
instance {α : Sort u} {s : Setoid α} [d : ∀ a b : α, Decidable (a ≈ b)] : DecidableEq (Quotient s) :=
|
||
{decEq := λ q₁ q₂ : Quotient s,
|
||
Quotient.recOnSubsingleton₂ q₁ q₂
|
||
(λ a₁ a₂,
|
||
match (d a₁ a₂) with
|
||
| (isTrue h₁) := isTrue (Quotient.sound h₁)
|
||
| (isFalse h₂) := isFalse (λ h, absurd (Quotient.exact h) h₂))}
|
||
|
||
/- Function extensionality -/
|
||
|
||
namespace Function
|
||
variables {α : Sort u} {β : α → Sort v}
|
||
|
||
def Equiv (f₁ f₂ : Π x : α, β x) : Prop := ∀ x, f₁ x = f₂ x
|
||
|
||
protected theorem Equiv.refl (f : Π x : α, β x) : Equiv f f := assume x, rfl
|
||
|
||
protected theorem Equiv.symm {f₁ f₂ : Π x: α, β x} : Equiv f₁ f₂ → Equiv f₂ f₁ :=
|
||
λ h x, Eq.symm (h x)
|
||
|
||
protected theorem Equiv.trans {f₁ f₂ f₃ : Π x: α, β x} : Equiv f₁ f₂ → Equiv f₂ f₃ → Equiv f₁ f₃ :=
|
||
λ h₁ h₂ x, Eq.trans (h₁ x) (h₂ x)
|
||
|
||
protected theorem Equiv.isEquivalence (α : Sort u) (β : α → Sort v) : Equivalence (@Function.Equiv α β) :=
|
||
mkEquivalence (@Function.Equiv α β) (@Equiv.refl α β) (@Equiv.symm α β) (@Equiv.trans α β)
|
||
end Function
|
||
|
||
section
|
||
open Quotient
|
||
variables {α : Sort u} {β : α → Sort v}
|
||
|
||
@[instance]
|
||
private def funSetoid (α : Sort u) (β : α → Sort v) : Setoid (Π x : α, β x) :=
|
||
Setoid.mk (@Function.Equiv α β) (Function.Equiv.isEquivalence α β)
|
||
|
||
private def extfunApp (f : Quotient $ funSetoid α β) : Π x : α, β x :=
|
||
assume x,
|
||
Quot.liftOn f
|
||
(λ f : Π x : α, β x, f x)
|
||
(λ f₁ f₂ h, h x)
|
||
|
||
theorem funext {f₁ f₂ : Π x : α, β x} (h : ∀ x, f₁ x = f₂ x) : f₁ = f₂ :=
|
||
show extfunApp ⟦f₁⟧ = extfunApp ⟦f₂⟧, from
|
||
congrArg extfunApp (sound h)
|
||
end
|
||
|
||
instance Pi.Subsingleton {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] : Subsingleton (Π a, β a) :=
|
||
⟨λ f₁ f₂, funext (λ a, Subsingleton.elim (f₁ a) (f₂ a))⟩
|
||
|
||
/- General operations on functions -/
|
||
namespace Function
|
||
universes u₁ u₂ u₃ u₄
|
||
variables {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} {ζ : Sort u₁}
|
||
|
||
@[inline, reducible] def comp (f : β → φ) (g : α → β) : α → φ :=
|
||
λ x, f (g x)
|
||
|
||
infixr ` ∘ ` := Function.comp
|
||
|
||
@[inline, reducible] def onFun (f : β → β → φ) (g : α → β) : α → α → φ :=
|
||
λ x y, f (g x) (g y)
|
||
|
||
@[inline, reducible] def combine (f : α → β → φ) (op : φ → δ → ζ) (g : α → β → δ)
|
||
: α → β → ζ :=
|
||
λ x y, op (f x y) (g x y)
|
||
|
||
@[inline, reducible] def const (β : Sort u₂) (a : α) : β → α :=
|
||
λ x, a
|
||
|
||
@[inline, reducible] def swap {φ : α → β → Sort u₃} (f : Π x y, φ x y) : Π y x, φ x y :=
|
||
λ y x, f x y
|
||
|
||
end Function
|
||
|
||
/- Classical reasoning support -/
|
||
|
||
namespace Classical
|
||
|
||
axiom choice {α : Sort u} : Nonempty α → α
|
||
|
||
noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop)
|
||
(h : Exists (λ x, p x)) : {x // p x} :=
|
||
choice $ let ⟨x, px⟩ := h; ⟨⟨x, px⟩⟩
|
||
|
||
noncomputable def choose {α : Sort u} {p : α → Prop} (h : Exists (λ x, p x)) : α :=
|
||
(indefiniteDescription p h).val
|
||
|
||
theorem chooseSpec {α : Sort u} {p : α → Prop} (h : Exists (λ x, p x)) : p (choose h) :=
|
||
(indefiniteDescription p h).property
|
||
|
||
/- Diaconescu's theorem: excluded middle from choice, Function extensionality and propositional extensionality. -/
|
||
theorem em (p : Prop) : p ∨ ¬p :=
|
||
let U (x : Prop) : Prop := x = True ∨ p;
|
||
let V (x : Prop) : Prop := x = False ∨ p;
|
||
have exU : Exists (λ x, U x), from ⟨True, Or.inl rfl⟩,
|
||
have exV : Exists (λ x, V x), from ⟨False, Or.inl rfl⟩,
|
||
let u : Prop := choose exU;
|
||
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
|
||
(assume hut : u = True,
|
||
Or.elim vDef
|
||
(assume hvf : v = False,
|
||
have hne : u ≠ v, from hvf.symm ▸ hut.symm ▸ trueNeFalse,
|
||
Or.inl hne)
|
||
Or.inr)
|
||
Or.inr,
|
||
have pImpliesUv : p → u = v, from
|
||
assume hp : p,
|
||
have hpred : U = V, from
|
||
funext $ assume x : Prop,
|
||
have hl : (x = True ∨ p) → (x = False ∨ p), from
|
||
assume a, Or.inr hp,
|
||
have hr : (x = False ∨ p) → (x = True ∨ p), from
|
||
assume a, Or.inr hp,
|
||
show (x = True ∨ p) = (x = False ∨ p), from
|
||
propext (Iff.intro hl hr),
|
||
have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV, from
|
||
hpred ▸ λ exU exV, rfl,
|
||
show u = v, from h₀ _ _,
|
||
Or.elim notUvOrP
|
||
(assume hne : u ≠ v, Or.inr (mt pImpliesUv hne))
|
||
Or.inl
|
||
|
||
theorem existsTrueOfNonempty {α : Sort u} : Nonempty α → Exists (λ x : α, True)
|
||
| ⟨x⟩ := ⟨x, trivial⟩
|
||
|
||
noncomputable def inhabitedOfNonempty {α : Sort u} (h : Nonempty α) : Inhabited α :=
|
||
⟨choice h⟩
|
||
|
||
noncomputable def inhabitedOfExists {α : Sort u} {p : α → Prop} (h : Exists (λ x, p x)) :
|
||
Inhabited α :=
|
||
inhabitedOfNonempty (Exists.elim h (λ w hw, ⟨w⟩))
|
||
|
||
/- all propositions are Decidable -/
|
||
noncomputable def propDecidable (a : Prop) : Decidable a :=
|
||
choice $ Or.elim (em a)
|
||
(assume ha, ⟨isTrue ha⟩)
|
||
(assume hna, ⟨isFalse hna⟩)
|
||
|
||
noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) :=
|
||
⟨propDecidable a⟩
|
||
|
||
noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
|
||
{decEq := λ x y, propDecidable (x = y)}
|
||
|
||
noncomputable def typeDecidable (α : Sort u) : PSum α (α → False) :=
|
||
match (propDecidable (Nonempty α)) with
|
||
| (isTrue hp) := PSum.inl (@Inhabited.default _ (inhabitedOfNonempty hp))
|
||
| (isFalse hn) := PSum.inr (λ a, absurd (Nonempty.intro a) hn)
|
||
|
||
noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop)
|
||
(h : Nonempty α) : {x : α // Exists (λ y : α, p y) → p x} :=
|
||
@dite (Exists (λ x : α, p x)) (propDecidable _) _
|
||
(λ hp : Exists (λ x : α, p x),
|
||
show {x : α // Exists (λ y : α, p y) → p x}, from
|
||
let xp := indefiniteDescription _ hp;
|
||
⟨xp.val, λ h', xp.property⟩)
|
||
(λ hp, ⟨choice h, λ h, absurd h hp⟩)
|
||
|
||
/- the Hilbert epsilon Function -/
|
||
|
||
noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α :=
|
||
(strongIndefiniteDescription p h).val
|
||
|
||
theorem epsilonSpecAux {α : Sort u} (h : Nonempty α) (p : α → Prop)
|
||
: Exists (λ y, p y) → p (@epsilon α h p) :=
|
||
(strongIndefiniteDescription p h).property
|
||
|
||
theorem epsilonSpec {α : Sort u} {p : α → Prop} (hex : Exists (λ y, p y)) :
|
||
p (@epsilon α (nonemptyOfExists hex) p) :=
|
||
epsilonSpecAux (nonemptyOfExists hex) p hex
|
||
|
||
theorem epsilonSingleton {α : Sort u} (x : α) : @epsilon α ⟨x⟩ (λ y, y = x) = x :=
|
||
@epsilonSpec α (λ y, y = x) ⟨x, rfl⟩
|
||
|
||
/- the axiom of choice -/
|
||
|
||
theorem axiomOfChoice {α : Sort u} {β : α → Sort v} {r : Π x, β x → Prop} (h : ∀ x, Exists (λ y, r x y)) :
|
||
Exists (λ (f : Π x, β x), ∀ x, r x (f x)) :=
|
||
⟨_, λ x, chooseSpec (h x)⟩
|
||
|
||
theorem skolem {α : Sort u} {b : α → Sort v} {p : Π x, b x → Prop} :
|
||
(∀ x, Exists (λ y, p x y)) ↔ Exists (λ (f : Π x, b x), ∀ x, p x (f x)) :=
|
||
⟨axiomOfChoice, λ ⟨f, hw⟩ x, ⟨f x, hw x⟩⟩
|
||
|
||
theorem propComplete (a : Prop) : a = True ∨ a = False :=
|
||
Or.elim (em a)
|
||
(λ t, Or.inl (eqTrueIntro t))
|
||
(λ f, Or.inr (eqFalseIntro f))
|
||
|
||
-- this supercedes byCases in Decidable
|
||
theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
|
||
@Decidable.byCases _ _ (propDecidable _) hpq hnpq
|
||
|
||
-- this supercedes byContradiction in Decidable
|
||
theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
|
||
@Decidable.byContradiction _ (propDecidable _) h
|
||
|
||
end Classical
|