2201 lines
74 KiB
Text
2201 lines
74 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 infixl ` ⬝ `:75
|
||
reserve infixr ` ▸ `:75
|
||
reserve infixr ` ▹ `:75
|
||
|
||
/- types and Type constructors -/
|
||
|
||
reserve infixr ` ⊕ `:30
|
||
reserve infixr ` × `:35
|
||
|
||
/- arithmetic operations -/
|
||
|
||
reserve infixl ` + `:65
|
||
reserve infixl ` - `:65
|
||
reserve infixl ` * `:70
|
||
reserve infixl ` / `:70
|
||
reserve infixl ` % `:70
|
||
reserve infixl ` %ₙ `:70
|
||
reserve prefix `-`:100
|
||
reserve infixr ` ^ `:80
|
||
|
||
reserve infixr ` ∘ `:90
|
||
|
||
reserve infix ` <= `:50
|
||
reserve infix ` ≤ `:50
|
||
reserve infix ` < `:50
|
||
reserve infix ` >= `:50
|
||
reserve infix ` ≥ `:50
|
||
reserve infix ` > `:50
|
||
|
||
/- boolean operations -/
|
||
|
||
reserve prefix `!`:40
|
||
reserve infixl ` && `:35
|
||
reserve infixl ` || `:30
|
||
|
||
/- set operations -/
|
||
|
||
reserve infix ` ∈ `:50
|
||
reserve infix ` ∉ `:50
|
||
reserve infixl ` ∩ `:70
|
||
reserve infixl ` ∪ `:65
|
||
reserve infix ` ⊆ `:50
|
||
reserve infix ` ⊇ `:50
|
||
reserve infix ` ⊂ `:50
|
||
reserve infix ` ⊃ `:50
|
||
reserve infix ` \ `:70
|
||
|
||
/- other symbols -/
|
||
|
||
reserve infix ` ∣ `:50
|
||
reserve infixl ` ++ `:65
|
||
reserve infixr ` :: `:67
|
||
reserve infixl `; `:1
|
||
|
||
universes u v w
|
||
|
||
/-- Auxiliary unsafe constant used by the Compiler when erasing proofs from code. -/
|
||
unsafe axiom lcProof {α : Prop} : α
|
||
/-- Auxiliary unsafe constant used by the Compiler to mark unreachable code. -/
|
||
unsafe axiom lcUnreachable {α : Sort u} : α
|
||
|
||
@[inline] def id {α : Sort u} (a : α) : α := a
|
||
|
||
def inline {α : Sort u} (a : α) : α := a
|
||
|
||
@[inline] def flip {α : Sort u} {β : Sort v} {φ : Sort w} (f : α → β → φ) : β → α → φ :=
|
||
λ b a, f a b
|
||
|
||
/-
|
||
The kernel definitional equality test (t =?= s) has special support for idDelta applications.
|
||
It implements the following rules
|
||
|
||
1) (idDelta t) =?= t
|
||
2) t =?= (idDelta t)
|
||
3) (idDelta t) =?= s IF (unfoldOf t) =?= s
|
||
4) t =?= idDelta s IF t =?= (unfoldOf s)
|
||
|
||
This is mechanism for controlling the delta reduction (aka unfolding) used in the kernel.
|
||
|
||
We use idDelta applications to address performance problems when Type checking
|
||
lemmas generated by the equation Compiler.
|
||
-/
|
||
@[inline] def idDelta {α : Sort u} (a : α) : α :=
|
||
a
|
||
|
||
/-- Gadget for optional parameter support. -/
|
||
@[reducible] def optParam (α : Sort u) (default : α) : Sort u :=
|
||
α
|
||
|
||
/-- Gadget for marking output parameters in type classes. -/
|
||
@[reducible] def outParam (α : Sort u) : Sort u := α
|
||
|
||
/-- Auxiliary Declaration used to implement the notation (a : α) -/
|
||
@[reducible] def typedExpr (α : Sort u) (a : α) : α := a
|
||
|
||
/- `idRhs` is an auxiliary Declaration used in the equation Compiler to address performance
|
||
issues when proving equational lemmas. The equation Compiler uses it as a marker. -/
|
||
@[macroInline] abbrev idRhs (α : Sort u) (a : α) : α := a
|
||
|
||
inductive PUnit : Sort u
|
||
| star : PUnit
|
||
|
||
/-- An abbreviation for `PUnit.{0}`, its most common instantiation.
|
||
This Type should be preferred over `PUnit` where possible to avoid
|
||
unnecessary universe parameters. -/
|
||
abbrev Unit : Type := PUnit
|
||
|
||
@[pattern] abbrev Unit.star : Unit := PUnit.star
|
||
|
||
/- Remark: thunks have an efficient implementation in the runtime. -/
|
||
structure Thunk (α : Type u) : Type u :=
|
||
(fn : Unit → α)
|
||
|
||
attribute [extern cpp inline "lean::mk_thunk(#2)"] Thunk.mk
|
||
|
||
@[noinline, extern cpp inline "lean::thunk_pure(#2)"]
|
||
protected def Thunk.pure {α : Type u} (a : α) : Thunk α :=
|
||
⟨λ _, a⟩
|
||
@[noinline, extern cpp inline "lean::thunk_get(#2)"]
|
||
protected def Thunk.get {α : Type u} (x : @& Thunk α) : α :=
|
||
x.fn ()
|
||
@[noinline, extern cpp inline "lean::thunk_map(#3, #4)"]
|
||
protected def Thunk.map {α : Type u} {β : Type v} (f : α → β) (x : Thunk α) : Thunk β :=
|
||
⟨λ _, f x.get⟩
|
||
@[noinline, extern cpp inline "lean::thunk_bind(#3, #4)"]
|
||
protected def Thunk.bind {α : Type u} {β : Type v} (x : Thunk α) (f : α → Thunk β) : Thunk β :=
|
||
⟨λ _, (f x.get).get⟩
|
||
|
||
/- Remark: tasks have an efficient implementation in the runtime. -/
|
||
structure Task (α : Type u) : Type u :=
|
||
(fn : Unit → α)
|
||
|
||
attribute [extern cpp inline "lean::mk_task(#2)"] Task.mk
|
||
|
||
@[noinline, extern cpp inline "lean::task_pure(#2)"]
|
||
protected def Task.pure {α : Type u} (a : α) : Task α :=
|
||
⟨λ _, a⟩
|
||
@[noinline, extern cpp inline "lean::task_get(#2)"]
|
||
protected def Task.get {α : Type u} (x : @& Task α) : α :=
|
||
x.fn ()
|
||
@[noinline, extern cpp inline "lean::task_map(#3, #4)"]
|
||
protected def Task.map {α : Type u} {β : Type v} (f : α → β) (x : Task α) : Task β :=
|
||
⟨λ _, f x.get⟩
|
||
@[noinline, extern cpp inline "lean::task_bind(#3, #4)"]
|
||
protected def Task.bind {α : Type u} {β : Type v} (x : Task α) (f : α → Task β) : Task β :=
|
||
⟨λ _, (f x.get).get⟩
|
||
|
||
inductive True : Prop
|
||
| intro : True
|
||
|
||
inductive False : Prop
|
||
|
||
inductive Empty : Type
|
||
|
||
def Not (a : Prop) : Prop := a → False
|
||
prefix `¬` := Not
|
||
|
||
inductive Eq {α : Sort u} (a : α) : α → Prop
|
||
| refl : Eq a
|
||
|
||
@[elabAsEliminator, inline, reducible]
|
||
def {u1 u2} Eq.ndrec {α : Sort u2} {a : α} {C : α → Sort u1} (m : C a) {b : α} (h : Eq a b) : C b :=
|
||
@Eq.rec α a (λ α _, C α) m b h
|
||
|
||
@[elabAsEliminator, inline, reducible]
|
||
def {u1 u2} Eq.ndrecOn {α : Sort u2} {a : α} {C : α → Sort u1} {b : α} (h : Eq a b) (m : C a) : C b :=
|
||
@Eq.rec α a (λ α _, C α) m b h
|
||
|
||
/-
|
||
Initialize the Quotient Module, which effectively adds the following definitions:
|
||
|
||
constant Quot {α : Sort u} (r : α → α → Prop) : Sort u
|
||
|
||
constant Quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : Quot r
|
||
|
||
constant Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
|
||
(∀ a b : α, r a b → Eq (f a) (f b)) → Quot r → β
|
||
|
||
constant Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} :
|
||
(∀ a : α, β (Quot.mk r a)) → ∀ q : Quot r, β q
|
||
-/
|
||
initQuot
|
||
|
||
inductive Heq {α : Sort u} (a : α) : Π {β : Sort u}, β → Prop
|
||
| refl : Heq a
|
||
|
||
structure Prod (α : Type u) (β : Type v) :=
|
||
(fst : α) (snd : β)
|
||
|
||
/-- Similar to `Prod`, but α and β can be propositions.
|
||
We use this Type internally to automatically generate the brecOn recursor. -/
|
||
structure PProd (α : Sort u) (β : Sort v) :=
|
||
(fst : α) (snd : β)
|
||
|
||
structure And (a b : Prop) : Prop :=
|
||
intro :: (left : a) (right : b)
|
||
|
||
def And.elimLeft {a b : Prop} (h : And a b) : a := h.1
|
||
|
||
def And.elimRight {a b : Prop} (h : And a b) : b := h.2
|
||
|
||
structure Iff (a b : Prop) : Prop :=
|
||
intro :: (mp : a → b) (mpr : b → a)
|
||
|
||
/- Eq basic support -/
|
||
|
||
infix = := Eq
|
||
|
||
@[pattern] def rfl {α : Sort u} {a : α} : a = a := Eq.refl a
|
||
|
||
@[elabAsEliminator]
|
||
theorem Eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b :=
|
||
Eq.ndrec h₂ h₁
|
||
|
||
infixr ▸ := Eq.subst
|
||
|
||
theorem Eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c :=
|
||
h₂ ▸ h₁
|
||
|
||
theorem Eq.symm {α : Sort u} {a b : α} (h : a = b) : b = a :=
|
||
h ▸ rfl
|
||
|
||
infix ~= := Heq
|
||
infix ≅ := Heq
|
||
|
||
@[pattern] def Heq.rfl {α : Sort u} {a : α} : a ≅ a := Heq.refl a
|
||
|
||
theorem eqOfHeq {α : Sort u} {a a' : α} (h : a ≅ a') : a = a' :=
|
||
have ∀ (α' : Sort u) (a' : α') (h₁ : @Heq α a α' a') (h₂ : α = α'), (Eq.recOn h₂ a : α') = a', from
|
||
λ (α' : Sort u) (a' : α') (h₁ : @Heq α a α' a'), Heq.recOn h₁ (λ h₂ : α = α, rfl),
|
||
show (Eq.ndrecOn (Eq.refl α) a : α) = a', from
|
||
this α a' h (Eq.refl α)
|
||
|
||
inductive Sum (α : Type u) (β : Type v)
|
||
| inl {} (val : α) : Sum
|
||
| inr {} (val : β) : Sum
|
||
|
||
inductive PSum (α : Sort u) (β : Sort v)
|
||
| inl {} (val : α) : PSum
|
||
| inr {} (val : β) : PSum
|
||
|
||
inductive Or (a b : Prop) : Prop
|
||
| inl {} (h : a) : Or
|
||
| inr {} (h : b) : Or
|
||
|
||
def Or.introLeft {a : Prop} (b : Prop) (ha : a) : Or a b :=
|
||
Or.inl ha
|
||
|
||
def Or.introRight (a : Prop) {b : Prop} (hb : b) : Or a b :=
|
||
Or.inr hb
|
||
|
||
structure Sigma {α : Type u} (β : α → Type v) :=
|
||
mk :: (fst : α) (snd : β fst)
|
||
|
||
structure PSigma {α : Sort u} (β : α → Sort v) :=
|
||
mk :: (fst : α) (snd : β fst)
|
||
|
||
inductive Bool : Type
|
||
| false : Bool
|
||
| true : Bool
|
||
|
||
/- Remark: Subtype must take a Sort instead of Type because of the axiom strongIndefiniteDescription. -/
|
||
structure Subtype {α : Sort u} (p : α → Prop) :=
|
||
(val : α) (property : p val)
|
||
|
||
inductive Exists {α : Sort u} (p : α → Prop) : Prop
|
||
| intro (w : α) (h : p w) : Exists
|
||
|
||
attribute [ppAnonymousCtor] Sigma PSigma Subtype PProd And
|
||
|
||
class inductive Decidable (p : Prop)
|
||
| isFalse (h : ¬p) : Decidable
|
||
| isTrue (h : p) : Decidable
|
||
|
||
@[reducible] def DecidablePred {α : Sort u} (r : α → Prop) :=
|
||
Π (a : α), Decidable (r a)
|
||
|
||
@[reducible] def DecidableRel {α : Sort u} (r : α → α → Prop) :=
|
||
Π (a b : α), Decidable (r a b)
|
||
|
||
class DecidableEq (α : Sort u) :=
|
||
{decEq : Π a b : α, Decidable (a = b)}
|
||
|
||
export DecidableEq (decEq)
|
||
|
||
@[inline] instance decidableOfDecidableEq {α : Sort u} (a b : α) [DecidableEq α] : Decidable (a = b) :=
|
||
decEq a b
|
||
|
||
inductive Option (α : Type u)
|
||
| none {} : Option
|
||
| some (val : α) : Option
|
||
|
||
export Option (none some)
|
||
export Bool (false true)
|
||
|
||
inductive List (T : Type u)
|
||
| nil {} : List
|
||
| cons (hd : T) (tl : List) : List
|
||
|
||
infixr :: := List.cons
|
||
notation `[` l:(foldr `, ` (h t, List.cons h t) List.nil `]`) := l
|
||
|
||
inductive Nat
|
||
| zero : Nat
|
||
| succ (n : Nat) : Nat
|
||
|
||
/- Auxiliary axiom used to implement `sorry`.
|
||
TODO: add this theorem on-demand. That is,
|
||
we should only add it if after the first error. -/
|
||
unsafe axiom sorryAx (α : Sort u) (synthetic := true) : α
|
||
|
||
/- Declare builtin and reserved notation -/
|
||
|
||
class HasZero (α : Type u) := (zero : α)
|
||
class HasOne (α : Type u) := (one : α)
|
||
class HasAdd (α : Type u) := (add : α → α → α)
|
||
class HasMul (α : Type u) := (mul : α → α → α)
|
||
class HasNeg (α : Type u) := (neg : α → α)
|
||
class HasSub (α : Type u) := (sub : α → α → α)
|
||
class HasDiv (α : Type u) := (div : α → α → α)
|
||
class HasDvd (α : Type u) := (dvd : α → α → Prop)
|
||
class HasMod (α : Type u) := (mod : α → α → α)
|
||
class HasModn (α : Type u) := (modn : α → Nat → α)
|
||
class HasLe (α : Type u) := (le : α → α → Prop)
|
||
class HasLt (α : Type u) := (lt : α → α → Prop)
|
||
class HasBeq (α : Type u) := (beq : α → α → Bool)
|
||
class HasAppend (α : Type u) := (append : α → α → α)
|
||
class HasAndthen (α : Type u) (β : Type v) (σ : outParam $ Type w) := (andthen : α → β → σ)
|
||
class HasUnion (α : Type u) := (union : α → α → α)
|
||
class HasInter (α : Type u) := (inter : α → α → α)
|
||
class HasSDiff (α : Type u) := (sdiff : α → α → α)
|
||
class HasEquiv (α : Sort u) := (equiv : α → α → Prop)
|
||
class HasSubset (α : Type u) := (subset : α → α → Prop)
|
||
class HasSSubset (α : Type u) := (ssubset : α → α → Prop)
|
||
/- Type classes HasEmptyc and HasInsert are
|
||
used to implement polymorphic notation for collections.
|
||
Example: {a, b, c}. -/
|
||
class HasEmptyc (α : Type u) := (emptyc : α)
|
||
class HasInsert (α : outParam $ Type u) (γ : Type v) := (insert : α → γ → γ)
|
||
/- Type class used to implement the notation { a ∈ c | p a } -/
|
||
class HasSep (α : outParam $ Type u) (γ : Type v) :=
|
||
(sep : (α → Prop) → γ → γ)
|
||
/- Type class for set-like membership -/
|
||
class HasMem (α : outParam $ Type u) (γ : Type v) := (mem : α → γ → Prop)
|
||
|
||
class HasPow (α : Type u) (β : Type v) :=
|
||
(pow : α → β → α)
|
||
|
||
export HasAndthen (andthen)
|
||
export HasPow (pow)
|
||
|
||
infix ∈ := HasMem.mem
|
||
notation a ` ∉ ` s := ¬ HasMem.mem a s
|
||
infix + := HasAdd.add
|
||
infix * := HasMul.mul
|
||
infix - := HasSub.sub
|
||
infix / := HasDiv.div
|
||
infix ∣ := HasDvd.dvd
|
||
infix % := HasMod.mod
|
||
infix %ₙ := HasModn.modn
|
||
prefix - := HasNeg.neg
|
||
infix <= := HasLe.le
|
||
infix ≤ := HasLe.le
|
||
infix < := HasLt.lt
|
||
infix == := HasBeq.beq
|
||
infix ++ := HasAppend.append
|
||
infix ; := andthen
|
||
notation `∅` := HasEmptyc.emptyc _
|
||
infix ∪ := HasUnion.union
|
||
infix ∩ := HasInter.inter
|
||
infix ⊆ := HasSubset.subset
|
||
infix ⊂ := HasSSubset.ssubset
|
||
infix \ := HasSDiff.sdiff
|
||
infix ≈ := HasEquiv.equiv
|
||
infixr ^ := HasPow.pow
|
||
infixr /\ := And
|
||
infixr ∧ := And
|
||
infixr \/ := Or
|
||
infixr ∨ := Or
|
||
infix <-> := Iff
|
||
infix ↔ := Iff
|
||
notation `exists` binders `, ` r:(scoped P, Exists P) := r
|
||
notation `∃` binders `, ` r:(scoped P, Exists P) := r
|
||
|
||
export HasAppend (append)
|
||
|
||
@[reducible] def ge {α : Type u} [HasLe α] (a b : α) : Prop := HasLe.le b a
|
||
@[reducible] def gt {α : Type u} [HasLt α] (a b : α) : Prop := HasLt.lt b a
|
||
|
||
infix >= := ge
|
||
infix ≥ := ge
|
||
infix > := gt
|
||
|
||
@[reducible] def superset {α : Type u} [HasSubset α] (a b : α) : Prop := HasSubset.subset b a
|
||
@[reducible] def ssuperset {α : Type u} [HasSSubset α] (a b : α) : Prop := HasSSubset.ssubset b a
|
||
|
||
infix ⊇ := superset
|
||
infix ⊃ := ssuperset
|
||
|
||
@[inline] def bit0 {α : Type u} [s : HasAdd α] (a : α) : α := a + a
|
||
@[inline] def bit1 {α : Type u} [s₁ : HasOne α] [s₂ : HasAdd α] (a : α) : α := (bit0 a) + 1
|
||
|
||
attribute [pattern] HasZero.zero HasOne.one bit0 bit1 HasAdd.add HasNeg.neg
|
||
|
||
export HasInsert (insert)
|
||
|
||
/- The Empty collection -/
|
||
@[inline] def singleton {α : Type u} {γ : Type v} [HasEmptyc γ] [HasInsert α γ] (a : α) : γ :=
|
||
HasInsert.insert a ∅
|
||
|
||
/- Nat basic instances -/
|
||
@[extern cpp "lean::nat_add"]
|
||
protected def Nat.add : (@& Nat) → (@& Nat) → Nat
|
||
| a Nat.zero := a
|
||
| a (Nat.succ b) := Nat.succ (Nat.add a b)
|
||
|
||
/- We mark the following definitions as pattern to make sure they can be used in recursive equations,
|
||
and reduced by the equation Compiler. -/
|
||
attribute [pattern] Nat.add Nat.add._main
|
||
|
||
instance : HasZero Nat := ⟨Nat.zero⟩
|
||
|
||
instance : HasOne Nat := ⟨Nat.succ (Nat.zero)⟩
|
||
|
||
instance : HasAdd Nat := ⟨Nat.add⟩
|
||
|
||
def std.priority.default : Nat := 1000
|
||
def std.priority.max : Nat := 0xFFFFFFFF
|
||
|
||
protected def Nat.prio := std.priority.default + 100
|
||
|
||
/-
|
||
Global declarations of right binding strength
|
||
|
||
If a Module reassigns these, it will be incompatible with other modules that adhere to these
|
||
conventions.
|
||
|
||
When hovering over a symbol, use "C-c C-k" to see how to input it.
|
||
-/
|
||
def std.prec.max : Nat := 1024 -- the strength of application, identifiers, (, [, etc.
|
||
def std.prec.arrow : Nat := 25
|
||
|
||
/-
|
||
The next def is "max + 10". It can be used e.g. for postfix operations that should
|
||
be stronger than application.
|
||
-/
|
||
|
||
def std.prec.maxPlus : Nat := std.prec.max + 10
|
||
|
||
infixr × := Prod
|
||
-- notation for n-ary tuples
|
||
|
||
/- sizeof -/
|
||
|
||
class HasSizeof (α : Sort u) :=
|
||
(sizeof : α → Nat)
|
||
|
||
export HasSizeof (sizeof)
|
||
|
||
/-
|
||
Declare sizeof instances and lemmas for types declared before HasSizeof.
|
||
From now on, the inductive Compiler will automatically generate sizeof instances and lemmas.
|
||
-/
|
||
|
||
/- Every Type `α` has a default HasSizeof instance that just returns 0 for every element of `α` -/
|
||
protected def default.sizeof (α : Sort u) : α → Nat
|
||
| a := 0
|
||
|
||
instance defaultHasSizeof (α : Sort u) : HasSizeof α :=
|
||
⟨default.sizeof α⟩
|
||
|
||
protected def Nat.sizeof : Nat → Nat
|
||
| n := n
|
||
|
||
instance : HasSizeof Nat :=
|
||
⟨Nat.sizeof⟩
|
||
|
||
protected def Prod.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof β] : (Prod α β) → Nat
|
||
| ⟨a, b⟩ := 1 + sizeof a + sizeof b
|
||
|
||
instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Prod α β) :=
|
||
⟨Prod.sizeof⟩
|
||
|
||
protected def Sum.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof β] : (Sum α β) → Nat
|
||
| (Sum.inl a) := 1 + sizeof a
|
||
| (Sum.inr b) := 1 + sizeof b
|
||
|
||
instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Sum α β) :=
|
||
⟨Sum.sizeof⟩
|
||
|
||
protected def PSum.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof β] : (PSum α β) → Nat
|
||
| (PSum.inl a) := 1 + sizeof a
|
||
| (PSum.inr b) := 1 + sizeof b
|
||
|
||
instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (PSum α β) :=
|
||
⟨PSum.sizeof⟩
|
||
|
||
protected def Sigma.sizeof {α : Type u} {β : α → Type v} [HasSizeof α] [∀ a, HasSizeof (β a)] : Sigma β → Nat
|
||
| ⟨a, b⟩ := 1 + sizeof a + sizeof b
|
||
|
||
instance (α : Type u) (β : α → Type v) [HasSizeof α] [∀ a, HasSizeof (β a)] : HasSizeof (Sigma β) :=
|
||
⟨Sigma.sizeof⟩
|
||
|
||
protected def PSigma.sizeof {α : Type u} {β : α → Type v} [HasSizeof α] [∀ a, HasSizeof (β a)] : PSigma β → Nat
|
||
| ⟨a, b⟩ := 1 + sizeof a + sizeof b
|
||
|
||
instance (α : Type u) (β : α → Type v) [HasSizeof α] [∀ a, HasSizeof (β a)] : HasSizeof (PSigma β) :=
|
||
⟨PSigma.sizeof⟩
|
||
|
||
protected def PUnit.sizeof : PUnit → Nat
|
||
| u := 1
|
||
|
||
instance : HasSizeof PUnit := ⟨PUnit.sizeof⟩
|
||
|
||
protected def Bool.sizeof : Bool → Nat
|
||
| b := 1
|
||
|
||
instance : HasSizeof Bool := ⟨Bool.sizeof⟩
|
||
|
||
protected def Option.sizeof {α : Type u} [HasSizeof α] : Option α → Nat
|
||
| none := 1
|
||
| (some a) := 1 + sizeof a
|
||
|
||
instance (α : Type u) [HasSizeof α] : HasSizeof (Option α) :=
|
||
⟨Option.sizeof⟩
|
||
|
||
protected def List.sizeof {α : Type u} [HasSizeof α] : List α → Nat
|
||
| List.nil := 1
|
||
| (List.cons a l) := 1 + sizeof a + List.sizeof l
|
||
|
||
instance (α : Type u) [HasSizeof α] : HasSizeof (List α) :=
|
||
⟨List.sizeof⟩
|
||
|
||
protected def Subtype.sizeof {α : Type u} [HasSizeof α] {p : α → Prop} : Subtype p → Nat
|
||
| ⟨a, _⟩ := sizeof a
|
||
|
||
instance {α : Type u} [HasSizeof α] (p : α → Prop) : HasSizeof (Subtype p) :=
|
||
⟨Subtype.sizeof⟩
|
||
|
||
theorem natAddZero (n : Nat) : n + 0 = n := rfl
|
||
|
||
/- Combinator calculus -/
|
||
namespace Combinator
|
||
universes u₁ u₂ u₃
|
||
def I {α : Type u₁} (a : α) := a
|
||
def K {α : Type u₁} {β : Type u₂} (a : α) (b : β) := a
|
||
def S {α : Type u₁} {β : Type u₂} {γ : Type u₃} (x : α → β → γ) (y : α → β) (z : α) := x z (y z)
|
||
end Combinator
|
||
|
||
theorem optParamEq (α : Sort u) (default : α) : optParam α default = α := rfl
|
||
|
||
/-- Auxiliary datatype for #[ ... ] notation.
|
||
#[1, 2, 3, 4] is notation for
|
||
|
||
BinTree.Node
|
||
(BinTree.Node (BinTree.leaf 1) (BinTree.leaf 2))
|
||
(BinTree.Node (BinTree.leaf 3) (BinTree.leaf 4))
|
||
|
||
We use this notation to input long sequences without exhausting the System stack space.
|
||
Later, we define a coercion from `BinTree` into `List`.
|
||
-/
|
||
inductive BinTree (α : Type u)
|
||
| Empty {} : BinTree
|
||
| leaf (val : α) : BinTree
|
||
| Node (left right : BinTree) : BinTree
|
||
|
||
attribute [elabSimple] BinTree.Node BinTree.leaf
|
||
|
||
/-- Like `by applyInstance`, but not dependent on the tactic framework. -/
|
||
@[reducible] def inferInstance {α : Type u} [i : α] : α := i
|
||
@[reducible, elabSimple] def inferInstanceAs (α : Type u) [i : α] : α := i
|
||
|
||
/- Boolean operators -/
|
||
|
||
@[macroInline] def cond {a : Type u} : Bool → a → a → a
|
||
| true x y := x
|
||
| false x y := y
|
||
|
||
@[macroInline] def bor : Bool → Bool → Bool
|
||
| true _ := true
|
||
| false b := b
|
||
|
||
@[macroInline] def band : Bool → Bool → Bool
|
||
| false _ := false
|
||
| true b := b
|
||
|
||
@[macroInline] def bnot : Bool → Bool
|
||
| true := false
|
||
| false := true
|
||
|
||
@[macroInline] def bxor : Bool → Bool → Bool
|
||
| true false := true
|
||
| false true := true
|
||
| _ _ := false
|
||
|
||
prefix ! := bnot
|
||
infix || := bor
|
||
infix && := band
|
||
|
||
/- Logical connectives an equality -/
|
||
|
||
def implies (a b : Prop) := a → b
|
||
|
||
theorem implies.trans {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) : implies p r :=
|
||
assume hp, h₂ (h₁ hp)
|
||
|
||
def trivial : True := ⟨⟩
|
||
|
||
@[macroInline] def False.elim {C : Sort u} (h : False) : C :=
|
||
False.rec (λ _, C) h
|
||
|
||
@[macroInline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : ¬a) : b :=
|
||
False.elim (h₂ h₁)
|
||
|
||
theorem mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a := assume ha : a, h₂ (h₁ ha)
|
||
|
||
theorem not.intro {a : Prop} (h : a → False) : ¬ a := h
|
||
|
||
theorem notFalse : ¬False := id
|
||
|
||
-- proof irrelevance is built in
|
||
theorem proofIrrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ := rfl
|
||
|
||
theorem id.def {α : Sort u} (a : α) : id a = a := rfl
|
||
|
||
@[macroInline] def Eq.mp {α β : Sort u} (h₁ : α = β) (h₂ : α) : β :=
|
||
Eq.recOn h₁ h₂
|
||
|
||
@[macroInline] def Eq.mpr {α β : Sort u} : (α = β) → β → α :=
|
||
λ h₁ h₂, Eq.recOn (Eq.symm h₁) h₂
|
||
|
||
@[elabAsEliminator]
|
||
theorem Eq.substr {α : Sort u} {p : α → Prop} {a b : α} (h₁ : b = a) (h₂ : p a) : p b :=
|
||
Eq.subst (Eq.symm h₁) h₂
|
||
|
||
theorem congr {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : f₁ = f₂) (h₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=
|
||
Eq.subst h₁ (Eq.subst h₂ rfl)
|
||
|
||
theorem congrFun {α : Sort u} {β : α → Sort v} {f g : Π x, β x} (h : f = g) (a : α) : f a = g a :=
|
||
Eq.subst h (Eq.refl (f a))
|
||
|
||
theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂ :=
|
||
congr rfl h
|
||
|
||
theorem transRelLeft {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c :=
|
||
h₂ ▸ h₁
|
||
|
||
theorem transRelRight {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : a = b) (h₂ : r b c) : r a c :=
|
||
h₁.symm ▸ h₂
|
||
|
||
theorem ofEqTrue {p : Prop} (h : p = True) : p :=
|
||
h.symm ▸ trivial
|
||
|
||
theorem notOfEqFalse {p : Prop} (h : p = False) : ¬p :=
|
||
assume hp, h ▸ hp
|
||
|
||
@[macroInline] def cast {α β : Sort u} (h : α = β) (a : α) : β :=
|
||
Eq.rec a h
|
||
|
||
theorem castProofIrrel {α β : Sort u} (h₁ h₂ : α = β) (a : α) : cast h₁ a = cast h₂ a := rfl
|
||
|
||
theorem castEq {α : Sort u} (h : α = α) (a : α) : cast h a = a := rfl
|
||
|
||
@[reducible] def Ne {α : Sort u} (a b : α) := ¬(a = b)
|
||
infix ≠ := Ne
|
||
|
||
theorem Ne.def {α : Sort u} (a b : α) : a ≠ b = ¬ (a = b) := rfl
|
||
|
||
section Ne
|
||
variable {α : Sort u}
|
||
variables {a b : α} {p : Prop}
|
||
|
||
theorem Ne.intro (h : a = b → False) : a ≠ b := h
|
||
|
||
theorem Ne.elim (h : a ≠ b) : a = b → False := h
|
||
|
||
theorem Ne.irrefl (h : a ≠ a) : False := h rfl
|
||
|
||
theorem Ne.symm (h : a ≠ b) : b ≠ a :=
|
||
assume (h₁ : b = a), h (h₁.symm)
|
||
|
||
theorem falseOfNe : a ≠ a → False := Ne.irrefl
|
||
|
||
theorem neFalseOfSelf : p → p ≠ False :=
|
||
assume (hp : p) (Heq : p = False), Heq ▸ hp
|
||
|
||
theorem neTrueOfNot : ¬p → p ≠ True :=
|
||
assume (hnp : ¬p) (Heq : p = True), (Heq ▸ hnp) trivial
|
||
|
||
theorem trueNeFalse : ¬True = False :=
|
||
neFalseOfSelf trivial
|
||
end Ne
|
||
|
||
theorem eqFfOfNeTt : ∀ {b : Bool}, b ≠ true → b = false
|
||
| true h := False.elim (h rfl)
|
||
| false h := rfl
|
||
|
||
theorem eqTtOfNeFf : ∀ {b : Bool}, b ≠ false → b = true
|
||
| true h := rfl
|
||
| false h := False.elim (h rfl)
|
||
|
||
section
|
||
variables {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
|
||
|
||
@[elabAsEliminator]
|
||
theorem {u1 u2} Heq.ndrec {α : Sort u2} {a : α} {C : Π {β : Sort u2}, β → Sort u1} (m : C a) {β : Sort u2} {b : β} (h : a ≅ b) : C b :=
|
||
@Heq.rec α a (λ β b _, C b) m β b h
|
||
|
||
@[elabAsEliminator]
|
||
theorem {u1 u2} Heq.ndrecOn {α : Sort u2} {a : α} {C : Π {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : C a) : C b :=
|
||
@Heq.rec α a (λ β b _, C b) m β b h
|
||
|
||
theorem Heq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b :=
|
||
Eq.recOn (eqOfHeq h₁) h₂
|
||
|
||
theorem Heq.subst {p : ∀ T : Sort u, T → Prop} (h₁ : a ≅ b) (h₂ : p α a) : p β b :=
|
||
Heq.ndrecOn h₁ h₂
|
||
|
||
theorem Heq.symm (h : a ≅ b) : b ≅ a :=
|
||
Heq.ndrecOn h (Heq.refl a)
|
||
|
||
theorem heqOfEq (h : a = a') : a ≅ a' :=
|
||
Eq.subst h (Heq.refl a)
|
||
|
||
theorem Heq.trans (h₁ : a ≅ b) (h₂ : b ≅ c) : a ≅ c :=
|
||
Heq.subst h₂ h₁
|
||
|
||
theorem heqOfHeqOfEq (h₁ : a ≅ b) (h₂ : b = b') : a ≅ b' :=
|
||
Heq.trans h₁ (heqOfEq h₂)
|
||
|
||
theorem heqOfEqOfHeq (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b :=
|
||
Heq.trans (heqOfEq h₁) h₂
|
||
|
||
def typeEqOfHeq (h : a ≅ b) : α = β :=
|
||
Heq.ndrecOn h (Eq.refl α)
|
||
end
|
||
|
||
theorem eqRecHeq {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} (h : a = a') (p : φ a), (Eq.recOn h p : φ a') ≅ p
|
||
| a _ rfl p := Heq.refl p
|
||
|
||
theorem heqOfEqRecLeft {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a = a') (h₂ : (Eq.recOn e p₁ : φ a') = p₂), p₁ ≅ p₂
|
||
| a _ p₁ p₂ rfl h := Eq.recOn h (Heq.refl p₁)
|
||
|
||
theorem heqOfEqRecRight {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a' = a) (h₂ : p₁ = Eq.recOn e p₂), p₁ ≅ p₂
|
||
| a _ p₁ p₂ rfl h :=
|
||
have p₁ = p₂, from h,
|
||
this ▸ Heq.refl p₁
|
||
|
||
theorem ofHeqTrue {a : Prop} (h : a ≅ True) : a :=
|
||
ofEqTrue (eqOfHeq h)
|
||
|
||
theorem castHeq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a
|
||
| α _ rfl a := Heq.refl a
|
||
|
||
variables {a b c d : Prop}
|
||
|
||
theorem and.elim (h₁ : a ∧ b) (h₂ : a → b → c) : c :=
|
||
And.rec h₂ h₁
|
||
|
||
theorem and.swap : a ∧ b → b ∧ a :=
|
||
assume ⟨ha, hb⟩, ⟨hb, ha⟩
|
||
|
||
def and.symm := @and.swap
|
||
|
||
theorem Or.elim (h₁ : a ∨ b) (h₂ : a → c) (h₃ : b → c) : c :=
|
||
Or.rec h₂ h₃ h₁
|
||
|
||
theorem nonContradictoryEm (a : Prop) : ¬¬(a ∨ ¬a) :=
|
||
assume notEm : ¬(a ∨ ¬a),
|
||
have negA : ¬a, from
|
||
assume posA : a, absurd (Or.inl posA) notEm,
|
||
absurd (Or.inr negA) notEm
|
||
|
||
def notNotEm := nonContradictoryEm
|
||
|
||
theorem Or.swap (h : a ∨ b) : b ∨ a :=
|
||
Or.elim h Or.inr Or.inl
|
||
|
||
def Or.symm := @Or.swap
|
||
|
||
/- xor -/
|
||
def xor (a b : Prop) := (a ∧ ¬ b) ∨ (b ∧ ¬ a)
|
||
|
||
@[recursor 5]
|
||
theorem Iff.elim (h₁ : (a → b) → (b → a) → c) (h₂ : a ↔ b) : c :=
|
||
Iff.rec h₁ h₂
|
||
|
||
theorem Iff.elimLeft : (a ↔ b) → a → b := Iff.mp
|
||
|
||
theorem Iff.elimRight : (a ↔ b) → b → a := Iff.mpr
|
||
|
||
theorem iffIffImpliesAndImplies (a b : Prop) : (a ↔ b) ↔ (a → b) ∧ (b → a) :=
|
||
Iff.intro (λ h, And.intro h.mp h.mpr) (λ h, Iff.intro h.left h.right)
|
||
|
||
theorem Iff.refl (a : Prop) : a ↔ a :=
|
||
Iff.intro (assume h, h) (assume h, h)
|
||
|
||
theorem Iff.rfl {a : Prop} : a ↔ a :=
|
||
Iff.refl a
|
||
|
||
theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=
|
||
Iff.intro
|
||
(assume ha, Iff.mp h₂ (Iff.mp h₁ ha))
|
||
(assume hc, Iff.mpr h₁ (Iff.mpr h₂ hc))
|
||
|
||
theorem Iff.symm (h : a ↔ b) : b ↔ a :=
|
||
Iff.intro (Iff.elimRight h) (Iff.elimLeft h)
|
||
|
||
theorem Iff.comm : (a ↔ b) ↔ (b ↔ a) :=
|
||
Iff.intro Iff.symm Iff.symm
|
||
|
||
theorem Eq.toIff {a b : Prop} (h : a = b) : a ↔ b :=
|
||
Eq.recOn h Iff.rfl
|
||
|
||
theorem neqOfNotIff {a b : Prop} : ¬(a ↔ b) → a ≠ b :=
|
||
λ h₁ h₂,
|
||
have a ↔ b, from Eq.subst h₂ (Iff.refl a),
|
||
absurd this h₁
|
||
|
||
theorem notIffNotOfIff (h₁ : a ↔ b) : ¬a ↔ ¬b :=
|
||
Iff.intro
|
||
(assume (hna : ¬ a) (hb : b), hna (Iff.elimRight h₁ hb))
|
||
(assume (hnb : ¬ b) (ha : a), hnb (Iff.elimLeft h₁ ha))
|
||
|
||
theorem ofIffTrue (h : a ↔ True) : a :=
|
||
Iff.mp (Iff.symm h) trivial
|
||
|
||
theorem notOfIffFalse : (a ↔ False) → ¬a := Iff.mp
|
||
|
||
theorem iffTrueIntro (h : a) : a ↔ True :=
|
||
Iff.intro
|
||
(λ hl, trivial)
|
||
(λ hr, h)
|
||
|
||
theorem iffFalseIntro (h : ¬a) : a ↔ False :=
|
||
Iff.intro h (False.rec (λ _, a))
|
||
|
||
theorem impCongr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a → b) ↔ (c → d) :=
|
||
Iff.intro
|
||
(λ hab hc, Iff.mp h₂ (hab (Iff.mpr h₁ hc)))
|
||
(λ hcd ha, Iff.mpr h₂ (hcd (Iff.mp h₁ ha)))
|
||
|
||
theorem impCongrCtx (h₁ : a ↔ c) (h₂ : c → (b ↔ d)) : (a → b) ↔ (c → d) :=
|
||
Iff.intro
|
||
(λ hab hc, have ha : a, from Iff.mpr h₁ hc,
|
||
have hb : b, from hab ha,
|
||
Iff.mp (h₂ hc) hb)
|
||
(λ hcd ha, have hc : c, from Iff.mp h₁ ha,
|
||
have hd : d, from hcd hc,
|
||
Iff.mpr (h₂ hc) hd)
|
||
|
||
theorem impCongrRight (h : a → (b ↔ c)) : (a → b) ↔ (a → c) :=
|
||
Iff.intro
|
||
(assume hab ha, Iff.elimLeft (h ha) (hab ha))
|
||
(assume hab ha, Iff.elimRight (h ha) (hab ha))
|
||
|
||
theorem notNotIntro (ha : a) : ¬¬a :=
|
||
assume hna : ¬a, hna ha
|
||
|
||
theorem notOfNotNotNot (h : ¬¬¬a) : ¬a :=
|
||
λ ha, absurd (notNotIntro ha) h
|
||
|
||
theorem notTrue : (¬ True) ↔ False :=
|
||
iffFalseIntro (notNotIntro trivial)
|
||
|
||
def notTrueIff := notTrue
|
||
|
||
theorem notFalseIff : (¬ False) ↔ True :=
|
||
iffTrueIntro notFalse
|
||
|
||
theorem notCongr (h : a ↔ b) : ¬a ↔ ¬b :=
|
||
Iff.intro (λ h₁ h₂, h₁ (Iff.mpr h h₂)) (λ h₁ h₂, h₁ (Iff.mp h h₂))
|
||
|
||
theorem neSelfIffFalse {α : Sort u} (a : α) : (Not (a = a)) ↔ False :=
|
||
Iff.intro falseOfNe False.elim
|
||
|
||
theorem eqSelfIffTrue {α : Sort u} (a : α) : (a = a) ↔ True :=
|
||
iffTrueIntro rfl
|
||
|
||
theorem heqSelfIffTrue {α : Sort u} (a : α) : (a ≅ a) ↔ True :=
|
||
iffTrueIntro (Heq.refl a)
|
||
|
||
theorem iffNotSelf (a : Prop) : (a ↔ ¬a) ↔ False :=
|
||
iffFalseIntro (λ h,
|
||
have h' : ¬a, from (λ ha, (Iff.mp h ha) ha),
|
||
h' (Iff.mpr h h'))
|
||
|
||
theorem notIffSelf (a : Prop) : (¬a ↔ a) ↔ False :=
|
||
iffFalseIntro (λ h,
|
||
have h' : ¬a, from (λ ha, (Iff.mpr h ha) ha),
|
||
h' (Iff.mp h h'))
|
||
|
||
theorem trueIffFalse : (True ↔ False) ↔ False :=
|
||
iffFalseIntro (λ h, Iff.mp h trivial)
|
||
|
||
theorem falseIffTrue : (False ↔ True) ↔ False :=
|
||
iffFalseIntro (λ h, Iff.mpr h trivial)
|
||
|
||
theorem falseOfTrueIffFalse : (True ↔ False) → False :=
|
||
assume h, Iff.mp h trivial
|
||
|
||
theorem falseOfTrueEqFalse : (True = False) → False :=
|
||
assume h, h ▸ trivial
|
||
|
||
theorem trueEqFalseOfFalse : False → (True = False) :=
|
||
False.elim
|
||
|
||
theorem eqComm {α : Sort u} {a b : α} : a = b ↔ b = a :=
|
||
⟨Eq.symm, Eq.symm⟩
|
||
|
||
/- and simp rules -/
|
||
theorem and.imp (hac : a → c) (hbd : b → d) : a ∧ b → c ∧ d :=
|
||
assume ⟨ha, hb⟩, ⟨hac ha, hbd hb⟩
|
||
|
||
def andImplies := @and.imp
|
||
|
||
theorem andCongr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ∧ b) ↔ (c ∧ d) :=
|
||
Iff.intro (and.imp (Iff.mp h₁) (Iff.mp h₂)) (and.imp (Iff.mpr h₁) (Iff.mpr h₂))
|
||
|
||
theorem andComm : a ∧ b ↔ b ∧ a :=
|
||
Iff.intro and.swap and.swap
|
||
|
||
theorem andAssoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
|
||
Iff.intro
|
||
(assume ⟨⟨ha, hb⟩, hc⟩, ⟨ha, ⟨hb, hc⟩⟩)
|
||
(assume ⟨ha, ⟨hb, hc⟩⟩, ⟨⟨ha, hb⟩, hc⟩)
|
||
|
||
theorem andLeftComm : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) :=
|
||
Iff.trans (Iff.symm andAssoc) (Iff.trans (andCongr andComm (Iff.refl c)) andAssoc)
|
||
|
||
theorem andTrue (a : Prop) : a ∧ True ↔ a :=
|
||
Iff.intro And.left (λ ha, ⟨ha, trivial⟩)
|
||
|
||
theorem trueAnd (a : Prop) : True ∧ a ↔ a :=
|
||
Iff.intro And.right (λ h, ⟨trivial, h⟩)
|
||
|
||
theorem andFalse (a : Prop) : a ∧ False ↔ False :=
|
||
iffFalseIntro And.right
|
||
|
||
theorem falseAnd (a : Prop) : False ∧ a ↔ False :=
|
||
iffFalseIntro And.left
|
||
|
||
theorem notAndSelf (a : Prop) : (¬a ∧ a) ↔ False :=
|
||
iffFalseIntro (λ h, and.elim h (λ h₁ h₂, absurd h₂ h₁))
|
||
|
||
theorem andNotSelf (a : Prop) : (a ∧ ¬a) ↔ False :=
|
||
iffFalseIntro (assume ⟨h₁, h₂⟩, absurd h₁ h₂)
|
||
|
||
theorem andSelf (a : Prop) : a ∧ a ↔ a :=
|
||
Iff.intro And.left (assume h, ⟨h, h⟩)
|
||
|
||
/- or simp rules -/
|
||
|
||
theorem orCongr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ∨ b) ↔ (c ∨ d) :=
|
||
Iff.intro (λ h, Or.elim h (λ h, Or.inl (Iff.mp h₁ h)) (λ h, Or.inr (Iff.mp h₂ h)))
|
||
(λ h, Or.elim h (λ h, Or.inl (Iff.mpr h₁ h)) (λ h, Or.inr (Iff.mpr h₂ h)))
|
||
|
||
theorem orComm : a ∨ b ↔ b ∨ a := Iff.intro Or.swap Or.swap
|
||
|
||
theorem orAssoc : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) :=
|
||
Iff.intro (λ h, Or.elim h (λ h, Or.elim h Or.inl (λ h, Or.inr (Or.inl h))) (λ h, Or.inr (Or.inr h)))
|
||
(λ h, Or.elim h (λ h, Or.inl (Or.inl h)) (λ h, Or.elim h (λ h, Or.inl (Or.inr h)) Or.inr))
|
||
|
||
theorem orLeftComm : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c) :=
|
||
Iff.trans (Iff.symm orAssoc) (Iff.trans (orCongr orComm (Iff.refl c)) orAssoc)
|
||
|
||
theorem orTrue (a : Prop) : a ∨ True ↔ True :=
|
||
iffTrueIntro (Or.inr trivial)
|
||
|
||
theorem trueOr (a : Prop) : True ∨ a ↔ True :=
|
||
iffTrueIntro (Or.inl trivial)
|
||
|
||
theorem orFalse (a : Prop) : a ∨ False ↔ a :=
|
||
Iff.intro (λ h, Or.elim h id False.elim) Or.inl
|
||
|
||
theorem falseOr (a : Prop) : False ∨ a ↔ a :=
|
||
Iff.trans orComm (orFalse a)
|
||
|
||
theorem orSelf (a : Prop) : a ∨ a ↔ a :=
|
||
Iff.intro (λ h, Or.elim h id id) Or.inl
|
||
|
||
theorem notOr {a b : Prop} : ¬ a → ¬ b → ¬ (a ∨ b)
|
||
| hna hnb (Or.inl ha) := absurd ha hna
|
||
| hna hnb (Or.inr hb) := absurd hb hnb
|
||
|
||
/- or resolution rulses -/
|
||
|
||
theorem resolveLeft {a b : Prop} (h : a ∨ b) (na : ¬ a) : b :=
|
||
Or.elim h (λ ha, absurd ha na) id
|
||
|
||
theorem negResolveLeft {a b : Prop} (h : ¬ a ∨ b) (ha : a) : b :=
|
||
Or.elim h (λ na, absurd ha na) id
|
||
|
||
theorem resolveRight {a b : Prop} (h : a ∨ b) (nb : ¬ b) : a :=
|
||
Or.elim h id (λ hb, absurd hb nb)
|
||
|
||
theorem negResolveRight {a b : Prop} (h : a ∨ ¬ b) (hb : b) : a :=
|
||
Or.elim h id (λ nb, absurd hb nb)
|
||
|
||
/- Iff simp rules -/
|
||
|
||
theorem iffTrue (a : Prop) : (a ↔ True) ↔ a :=
|
||
Iff.intro (assume h, Iff.mpr h trivial) iffTrueIntro
|
||
|
||
theorem trueIff (a : Prop) : (True ↔ a) ↔ a :=
|
||
Iff.trans Iff.comm (iffTrue a)
|
||
|
||
theorem iffFalse (a : Prop) : (a ↔ False) ↔ ¬ a :=
|
||
Iff.intro Iff.mp iffFalseIntro
|
||
|
||
theorem falseIff (a : Prop) : (False ↔ a) ↔ ¬ a :=
|
||
Iff.trans Iff.comm (iffFalse a)
|
||
|
||
theorem iffSelf (a : Prop) : (a ↔ a) ↔ True :=
|
||
iffTrueIntro Iff.rfl
|
||
|
||
theorem iffCongr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ↔ b) ↔ (c ↔ d) :=
|
||
(iffIffImpliesAndImplies a b).trans
|
||
((andCongr (impCongr h₁ h₂) (impCongr h₂ h₁)).trans
|
||
(iffIffImpliesAndImplies c d).symm)
|
||
|
||
/- implies simp rule -/
|
||
theorem impliesTrueIff (α : Sort u) : (α → True) ↔ True :=
|
||
Iff.intro (λ h, trivial) (λ ha h, trivial)
|
||
|
||
theorem falseImpliesIff (a : Prop) : (False → a) ↔ True :=
|
||
Iff.intro (λ h, trivial) (λ ha h, False.elim h)
|
||
|
||
theorem trueImpliesIff (α : Prop) : (True → α) ↔ α :=
|
||
Iff.intro (λ h, h trivial) (λ h h', h)
|
||
|
||
/- exists -/
|
||
|
||
@[pattern]
|
||
def exists.intro := @Exists.intro
|
||
|
||
theorem exists.elim {α : Sort u} {p : α → Prop} {b : Prop}
|
||
(h₁ : ∃ x, p x) (h₂ : ∀ (a : α), p a → b) : b :=
|
||
Exists.rec h₂ h₁
|
||
|
||
/- exists and forall congruences -/
|
||
theorem forallCongr {α : Sort u} {p q : α → Prop} (h : ∀ a, (p a ↔ q a)) : (∀ a, p a) ↔ ∀ a, q a :=
|
||
Iff.intro (λ p a, Iff.mp (h a) (p a)) (λ q a, Iff.mpr (h a) (q a))
|
||
|
||
theorem existsImpExists {α : Sort u} {p q : α → Prop} (h : ∀ a, (p a → q a)) (p : ∃ a, p a) : ∃ a, q a :=
|
||
exists.elim p (λ a hp, ⟨a, h a hp⟩)
|
||
|
||
theorem existsCongr {α : Sort u} {p q : α → Prop} (h : ∀ a, (p a ↔ q a)) : (Exists p) ↔ ∃ a, q a :=
|
||
Iff.intro
|
||
(existsImpExists (λ a, Iff.mp (h a)))
|
||
(existsImpExists (λ a, Iff.mpr (h a)))
|
||
|
||
theorem forallNotOfNotExists {α : Sort u} {p : α → Prop} : ¬(∃ x, p x) → (∀ x, ¬p x) :=
|
||
λ hne x hp, hne ⟨x, hp⟩
|
||
|
||
/- Decidable -/
|
||
|
||
@[macroInline] def Decidable.toBool (p : Prop) [h : Decidable p] : Bool :=
|
||
Decidable.casesOn h (λ h₁, false) (λ h₂, true)
|
||
|
||
export Decidable (isTrue isFalse toBool)
|
||
|
||
theorem toBoolTrueEqTt (h : Decidable True) : @toBool True h = true :=
|
||
Decidable.casesOn h (λ h, False.elim (Iff.mp notTrue h)) (λ _, rfl)
|
||
|
||
theorem toBoolFalseEqFf (h : Decidable False) : @toBool False h = false :=
|
||
Decidable.casesOn h (λ h, rfl) (λ h, False.elim h)
|
||
|
||
instance : Decidable True :=
|
||
isTrue trivial
|
||
|
||
instance : Decidable False :=
|
||
isFalse notFalse
|
||
|
||
-- We use "dependent" if-then-else to be able to communicate the if-then-else condition
|
||
-- to the branches
|
||
@[macroInline] def dite (c : Prop) [h : Decidable c] {α : Sort u} : (c → α) → (¬ c → α) → α :=
|
||
λ t e, Decidable.casesOn h e t
|
||
|
||
/- if-then-else -/
|
||
|
||
@[macroInline] def ite (c : Prop) [h : Decidable c] {α : Sort u} (t e : α) : α :=
|
||
Decidable.casesOn h (λ hnc, e) (λ hc, t)
|
||
|
||
namespace Decidable
|
||
variables {p q : Prop}
|
||
|
||
def recOnTrue [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : p) (h₄ : h₁ h₃)
|
||
: (Decidable.recOn h h₂ h₁ : Sort u) :=
|
||
Decidable.casesOn h (λ h, False.rec _ (h h₃)) (λ h, h₄)
|
||
|
||
def recOnFalse [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : ¬p) (h₄ : h₂ h₃)
|
||
: (Decidable.recOn h h₂ h₁ : Sort u) :=
|
||
Decidable.casesOn h (λ h, h₄) (λ h, False.rec _ (h₃ h))
|
||
|
||
@[macroInline] def byCases {q : Sort u} [s : Decidable p] (h1 : p → q) (h2 : ¬p → q) : q :=
|
||
match s with
|
||
| isTrue h := h1 h
|
||
| isFalse h := h2 h
|
||
|
||
theorem em (p : Prop) [Decidable p] : p ∨ ¬p :=
|
||
byCases Or.inl Or.inr
|
||
|
||
theorem byContradiction [Decidable p] (h : ¬p → False) : p :=
|
||
byCases id (λ np : ¬p, False.elim (h np))
|
||
|
||
theorem ofNotNot [Decidable p] : ¬ ¬ p → p :=
|
||
λ hnn, byContradiction (λ hn, absurd hn hnn)
|
||
|
||
theorem notNotIff (p) [Decidable p] : (¬ ¬ p) ↔ p :=
|
||
Iff.intro ofNotNot notNotIntro
|
||
|
||
theorem notAndIffOrNot (p q : Prop) [d₁ : Decidable p] [d₂ : Decidable q] : ¬ (p ∧ q) ↔ ¬ p ∨ ¬ q :=
|
||
Iff.intro
|
||
(λ h, match d₁, d₂ with
|
||
| isTrue h₁, isTrue h₂ := absurd (And.intro h₁ h₂) h
|
||
| _, isFalse h₂ := Or.inr h₂
|
||
| isFalse h₁, _ := Or.inl h₁)
|
||
(λ h ⟨hp, hq⟩, Or.elim h (λ h, h hp) (λ h, h hq))
|
||
|
||
theorem notOrIffAndNot (p q) [d₁ : Decidable p] [d₂ : Decidable q] : ¬ (p ∨ q) ↔ ¬ p ∧ ¬ q :=
|
||
Iff.intro
|
||
(λ h, match d₁ with
|
||
| isTrue h₁ := False.elim $ h (Or.inl h₁)
|
||
| isFalse h₁ :=
|
||
match d₂ with
|
||
| isTrue h₂ := False.elim $ h (Or.inr h₂)
|
||
| isFalse h₂ := ⟨h₁, h₂⟩)
|
||
(λ ⟨np, nq⟩ h, Or.elim h np nq)
|
||
end Decidable
|
||
|
||
section
|
||
variables {p q : Prop}
|
||
@[inline] def decidableOfDecidableOfIff (hp : Decidable p) (h : p ↔ q) : Decidable q :=
|
||
if hp : p then isTrue (Iff.mp h hp)
|
||
else isFalse (Iff.mp (notIffNotOfIff h) hp)
|
||
|
||
@[inline] def decidableOfDecidableOfEq (hp : Decidable p) (h : p = q) : Decidable q :=
|
||
decidableOfDecidableOfIff hp h.toIff
|
||
|
||
@[macroInline]
|
||
protected def or.byCases [Decidable p] [Decidable q] {α : Sort u}
|
||
(h : p ∨ q) (h₁ : p → α) (h₂ : q → α) : α :=
|
||
if hp : p then h₁ hp else
|
||
if hq : q then h₂ hq else
|
||
False.rec _ (Or.elim h hp hq)
|
||
end
|
||
|
||
section
|
||
variables {p q : Prop}
|
||
|
||
@[macroInline] instance [Decidable p] [Decidable q] : Decidable (p ∧ q) :=
|
||
if hp : p then
|
||
if hq : q then isTrue ⟨hp, hq⟩
|
||
else isFalse (assume h : p ∧ q, hq (And.right h))
|
||
else isFalse (assume h : p ∧ q, hp (And.left h))
|
||
|
||
@[macroInline] instance [Decidable p] [Decidable q] : Decidable (p ∨ q) :=
|
||
if hp : p then isTrue (Or.inl hp) else
|
||
if hq : q then isTrue (Or.inr hq) else
|
||
isFalse (λ h, Or.elim h hp hq)
|
||
|
||
instance [Decidable p] : Decidable (¬p) :=
|
||
if hp : p then isFalse (absurd hp) else isTrue hp
|
||
|
||
@[macroInline] instance implies.Decidable [Decidable p] [Decidable q] : Decidable (p → q) :=
|
||
if hp : p then
|
||
if hq : q then isTrue (assume h, hq)
|
||
else isFalse (assume h : p → q, absurd (h hp) hq)
|
||
else isTrue (assume h, absurd h hp)
|
||
|
||
instance [Decidable p] [Decidable q] : Decidable (p ↔ q) :=
|
||
if hp : p then
|
||
if hq : q then isTrue ⟨λ_, hq, λ_, hp⟩
|
||
else isFalse $ λh, hq (h.1 hp)
|
||
else
|
||
if hq : q then isFalse $ λh, hp (h.2 hq)
|
||
else isTrue $ ⟨λh, absurd h hp, λh, absurd h hq⟩
|
||
|
||
instance [Decidable p] [Decidable q] : Decidable (xor p q) :=
|
||
if hp : p then
|
||
if hq : q then isFalse (λ h, Or.elim h (λ ⟨_, h⟩, h hq : ¬(p ∧ ¬ q)) (λ ⟨_, h⟩, h hp : ¬(q ∧ ¬ p)))
|
||
else isTrue $ Or.inl ⟨hp, hq⟩
|
||
else
|
||
if hq : q then isTrue $ Or.inr ⟨hq, hp⟩
|
||
else isFalse (λ h, Or.elim h (λ ⟨h, _⟩, hp h : ¬(p ∧ ¬ q)) (λ ⟨h, _⟩, hq h : ¬(q ∧ ¬ p)))
|
||
|
||
instance existsPropDecidable {p} (P : p → Prop) [Decidable p] [s : ∀ h, Decidable (P h)] : Decidable (∃ h, P h) :=
|
||
if h : p then decidableOfDecidableOfIff (s h)
|
||
⟨λ h2, ⟨h, h2⟩, λ ⟨h', h2⟩, h2⟩ else isFalse (mt (λ ⟨h, _⟩, h) h)
|
||
|
||
instance forallPropDecidable {p} (P : p → Prop)
|
||
[Dp : Decidable p] [DP : ∀ h, Decidable (P h)] : Decidable (∀ h, P h) :=
|
||
if h : p then decidableOfDecidableOfIff (DP h)
|
||
⟨λ h2 _, h2, λal, al h⟩ else isTrue (λ h2, absurd h2 h)
|
||
end
|
||
|
||
@[inline] instance {α : Sort u} [DecidableEq α] (a b : α) : Decidable (a ≠ b) :=
|
||
match decEq a b with
|
||
| isTrue h := isFalse $ λ h', absurd h h'
|
||
| isFalse h := isTrue h
|
||
|
||
theorem Bool.falseNeTrue (h : false = true) : False :=
|
||
Bool.noConfusion h
|
||
|
||
def isDecEq {α : Sort u} (p : α → α → Bool) : Prop := ∀ ⦃x y : α⦄, p x y = true → x = y
|
||
def isDecRefl {α : Sort u} (p : α → α → Bool) : Prop := ∀ x, p x x = true
|
||
|
||
instance : DecidableEq Bool :=
|
||
{decEq := λ a b, match a, b with
|
||
| false, false := isTrue rfl
|
||
| false, true := isFalse Bool.falseNeTrue
|
||
| true, false := isFalse (Ne.symm Bool.falseNeTrue)
|
||
| true, true := isTrue rfl}
|
||
|
||
@[inline]
|
||
def decidableEqOfBoolPred {α : Sort u} {p : α → α → Bool} (h₁ : isDecEq p) (h₂ : isDecRefl p) : DecidableEq α :=
|
||
{decEq := λ x y : α,
|
||
if hp : p x y = true then isTrue (h₁ hp)
|
||
else isFalse (assume hxy : x = y, absurd (h₂ y) (@Eq.recOn _ _ (λ z _, ¬p z y = true) _ hxy hp))}
|
||
|
||
theorem decidableEqInlRefl {α : Sort u} [DecidableEq α] (a : α) : decEq a a = isTrue (Eq.refl a) :=
|
||
match (decEq a a) with
|
||
| (isTrue e) := rfl
|
||
| (isFalse n) := absurd rfl n
|
||
|
||
theorem decidableEqInrNeg {α : Sort u} [DecidableEq α] {a b : α} : Π n : a ≠ b, decEq a b = isFalse n :=
|
||
assume n,
|
||
match decEq a b with
|
||
| isTrue e := absurd e n
|
||
| isFalse n₁ := proofIrrel n n₁ ▸ Eq.refl (isFalse n)
|
||
|
||
/- if-then-else expression theorems -/
|
||
|
||
theorem ifPos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t e : α} : (ite c t e) = t :=
|
||
match h with
|
||
| (isTrue hc) := rfl
|
||
| (isFalse hnc) := absurd hc hnc
|
||
|
||
theorem ifNeg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t e : α} : (ite c t e) = e :=
|
||
match h with
|
||
| (isTrue hc) := absurd hc hnc
|
||
| (isFalse hnc) := rfl
|
||
|
||
theorem ifTT (c : Prop) [h : Decidable c] {α : Sort u} (t : α) : (ite c t t) = t :=
|
||
match h with
|
||
| (isTrue hc) := rfl
|
||
| (isFalse hnc) := rfl
|
||
|
||
theorem ifCtxCongr {α : Sort u} {b c : Prop} [decB : Decidable b] [decC : Decidable c]
|
||
{x y u v : α}
|
||
(hC : b ↔ c) (hT : c → x = u) (hE : ¬c → y = v) :
|
||
ite b x y = ite c u v :=
|
||
match decB, decC with
|
||
| (isFalse h₁), (isFalse h₂) := hE h₂
|
||
| (isTrue h₁), (isTrue h₂) := hT h₂
|
||
| (isFalse h₁), (isTrue h₂) := absurd h₂ (Iff.mp (notIffNotOfIff hC) h₁)
|
||
| (isTrue h₁), (isFalse h₂) := absurd h₁ (Iff.mpr (notIffNotOfIff hC) h₂)
|
||
|
||
theorem ifCongr {α : Sort u} {b c : Prop} [decB : Decidable b] [decC : Decidable c]
|
||
{x y u v : α}
|
||
(hC : b ↔ c) (hT : x = u) (hE : y = v) :
|
||
ite b x y = ite c u v :=
|
||
@ifCtxCongr α b c decB decC x y u v hC (λ h, hT) (λ h, hE)
|
||
|
||
theorem ifCtxSimpCongr {α : Sort u} {b c : Prop} [decB : Decidable b] {x y u v : α}
|
||
(hC : b ↔ c) (hT : c → x = u) (hE : ¬c → y = v) :
|
||
ite b x y = (@ite c (decidableOfDecidableOfIff decB hC) α u v) :=
|
||
@ifCtxCongr α b c decB (decidableOfDecidableOfIff decB hC) x y u v hC hT hE
|
||
|
||
theorem ifSimpCongr {α : Sort u} {b c : Prop} [decB : Decidable b] {x y u v : α}
|
||
(hC : b ↔ c) (hT : x = u) (hE : y = v) :
|
||
ite b x y = (@ite c (decidableOfDecidableOfIff decB hC) α u v) :=
|
||
@ifCtxSimpCongr α b c decB x y u v hC (λ h, hT) (λ h, hE)
|
||
|
||
theorem ifTrue {α : Sort u} {h : Decidable True} (t e : α) : (@ite True h α t e) = t :=
|
||
ifPos trivial
|
||
|
||
theorem ifFalse {α : Sort u} {h : Decidable False} (t e : α) : (@ite False h α t e) = e :=
|
||
ifNeg notFalse
|
||
|
||
theorem difPos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t : c → α} {e : ¬ c → α} : dite c t e = t hc :=
|
||
match h with
|
||
| (isTrue hc) := rfl
|
||
| (isFalse hnc) := absurd hc hnc
|
||
|
||
theorem difNeg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬ c → α} : dite c t e = e hnc :=
|
||
match h with
|
||
| (isTrue hc) := absurd hc hnc
|
||
| (isFalse hnc) := rfl
|
||
|
||
theorem difCtxCongr {α : Sort u} {b c : Prop} [decB : Decidable b] [decC : Decidable c]
|
||
{x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
|
||
(hC : b ↔ c)
|
||
(hT : ∀ (h : c), x (Iff.mpr hC h) = u h)
|
||
(hE : ∀ (h : ¬c), y (Iff.mpr (notIffNotOfIff hC) h) = v h) :
|
||
(@dite b decB α x y) = (@dite c decC α u v) :=
|
||
match decB, decC with
|
||
| (isFalse h₁), (isFalse h₂) := hE h₂
|
||
| (isTrue h₁), (isTrue h₂) := hT h₂
|
||
| (isFalse h₁), (isTrue h₂) := absurd h₂ (Iff.mp (notIffNotOfIff hC) h₁)
|
||
| (isTrue h₁), (isFalse h₂) := absurd h₁ (Iff.mpr (notIffNotOfIff hC) h₂)
|
||
|
||
theorem difCtxSimpCongr {α : Sort u} {b c : Prop} [decB : Decidable b]
|
||
{x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
|
||
(hC : b ↔ c)
|
||
(hT : ∀ (h : c), x (Iff.mpr hC h) = u h)
|
||
(hE : ∀ (h : ¬c), y (Iff.mpr (notIffNotOfIff hC) h) = v h) :
|
||
(@dite b decB α x y) = (@dite c (decidableOfDecidableOfIff decB hC) α u v) :=
|
||
@difCtxCongr α b c decB (decidableOfDecidableOfIff decB hC) x u y v hC hT hE
|
||
|
||
-- Remark: dite and ite are "defally equal" when we ignore the proofs.
|
||
theorem difEqIf (c : Prop) [h : Decidable c] {α : Sort u} (t : α) (e : α) : dite c (λ h, t) (λ h, e) = ite c t e :=
|
||
match h with
|
||
| (isTrue hc) := rfl
|
||
| (isFalse hnc) := rfl
|
||
|
||
instance {c t e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] : Decidable (if c then t else e) :=
|
||
match dC with
|
||
| (isTrue hc) := dT
|
||
| (isFalse hc) := dE
|
||
|
||
instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : ∀ h, Decidable (t h)] [dE : ∀ h, Decidable (e h)] : Decidable (if h : c then t h else e h) :=
|
||
match dC with
|
||
| (isTrue hc) := dT hc
|
||
| (isFalse hc) := dE hc
|
||
|
||
def asTrue (c : Prop) [Decidable c] : Prop :=
|
||
if c then True else False
|
||
|
||
def asFalse (c : Prop) [Decidable c] : Prop :=
|
||
if c then False else True
|
||
|
||
def ofAsTrue {c : Prop} [h₁ : Decidable c] (h₂ : asTrue c) : c :=
|
||
match h₁, h₂ with
|
||
| (isTrue hC), h₂ := hC
|
||
| (isFalse hC), h₂ := False.elim h₂
|
||
|
||
/-- Universe lifting operation -/
|
||
structure {r s} Ulift (α : Type s) : Type (max s r) :=
|
||
up :: (down : α)
|
||
|
||
namespace Ulift
|
||
/- Bijection between α and Ulift.{v} α -/
|
||
theorem upDown {α : Type u} : ∀ (b : Ulift.{v} α), up (down b) = b
|
||
| (up a) := rfl
|
||
|
||
theorem downUp {α : Type u} (a : α) : down (up.{v} a) = a := rfl
|
||
end Ulift
|
||
|
||
/-- Universe lifting operation from Sort to Type -/
|
||
structure Plift (α : Sort u) : Type u :=
|
||
up :: (down : α)
|
||
|
||
namespace Plift
|
||
/- Bijection between α and Plift α -/
|
||
theorem upDown {α : Sort u} : ∀ (b : Plift α), up (down b) = b
|
||
| (up a) := rfl
|
||
|
||
theorem downUp {α : Sort u} (a : α) : down (up a) = a := rfl
|
||
end Plift
|
||
|
||
/- pointed types -/
|
||
structure PointedType :=
|
||
(type : Type u) (val : type)
|
||
|
||
/- Inhabited -/
|
||
|
||
class Inhabited (α : Sort u) :=
|
||
(default : α)
|
||
|
||
constant default (α : Sort u) [Inhabited α] : α :=
|
||
Inhabited.default α
|
||
|
||
@[inline, irreducible] def arbitrary (α : Sort u) [Inhabited α] : α :=
|
||
default α
|
||
|
||
instance prop.Inhabited : Inhabited Prop :=
|
||
⟨True⟩
|
||
|
||
instance fun.Inhabited (α : Sort u) {β : Sort v} [h : Inhabited β] : Inhabited (α → β) :=
|
||
Inhabited.casesOn h (λ b, ⟨λ a, b⟩)
|
||
|
||
instance pi.Inhabited (α : Sort u) {β : α → Sort v} [Π x, Inhabited (β x)] : Inhabited (Π x, β x) :=
|
||
⟨λ a, default (β a)⟩
|
||
|
||
instance : Inhabited Bool := ⟨false⟩
|
||
|
||
instance : Inhabited True := ⟨trivial⟩
|
||
|
||
instance : Inhabited Nat := ⟨0⟩
|
||
|
||
instance : Inhabited PointedType := ⟨{type := PUnit, val := ⟨⟩}⟩
|
||
|
||
class inductive nonempty (α : Sort u) : Prop
|
||
| intro (val : α) : nonempty
|
||
|
||
protected def nonempty.elim {α : Sort u} {p : Prop} (h₁ : nonempty α) (h₂ : α → p) : p :=
|
||
nonempty.rec h₂ h₁
|
||
|
||
instance nonemptyOfInhabited {α : Sort u} [Inhabited α] : nonempty α :=
|
||
⟨default α⟩
|
||
|
||
theorem nonemptyOfExists {α : Sort u} {p : α → Prop} : (∃ x, p x) → nonempty α
|
||
| ⟨w, h⟩ := ⟨w⟩
|
||
|
||
/- subsingleton -/
|
||
|
||
class inductive subsingleton (α : Sort u) : Prop
|
||
| intro (h : ∀ a b : α, a = b) : subsingleton
|
||
|
||
protected def subsingleton.elim {α : Sort u} [h : subsingleton α] : ∀ (a b : α), a = b :=
|
||
subsingleton.casesOn h (λ p, p)
|
||
|
||
protected def subsingleton.helim {α β : Sort u} [h : subsingleton α] (h : α = β) : ∀ (a : α) (b : β), a ≅ b :=
|
||
Eq.recOn h (λ a b : α, heqOfEq (subsingleton.elim a b))
|
||
|
||
instance subsingletonProp (p : Prop) : subsingleton p :=
|
||
⟨λ a b, proofIrrel a b⟩
|
||
|
||
instance (p : Prop) : subsingleton (Decidable p) :=
|
||
subsingleton.intro (λ d₁,
|
||
match d₁ with
|
||
| (isTrue t₁) := (λ d₂,
|
||
match d₂ with
|
||
| (isTrue t₂) := Eq.recOn (proofIrrel t₁ t₂) rfl
|
||
| (isFalse f₂) := absurd t₁ f₂)
|
||
| (isFalse f₁) := (λ d₂,
|
||
match d₂ with
|
||
| (isTrue t₂) := absurd t₂ f₁
|
||
| (isFalse f₂) := Eq.recOn (proofIrrel f₁ f₂) rfl))
|
||
|
||
protected theorem recSubsingleton {p : Prop} [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u}
|
||
[h₃ : Π (h : p), subsingleton (h₁ h)] [h₄ : Π (h : ¬p), subsingleton (h₂ h)]
|
||
: subsingleton (Decidable.casesOn h h₂ h₁) :=
|
||
match h with
|
||
| (isTrue h) := h₃ h
|
||
| (isFalse h) := h₄ h
|
||
|
||
/- Equalities for rewriting let-expressions -/
|
||
theorem letValueEq {α : Sort u} {β : Sort v} {a₁ a₂ : α} (b : α → β) :
|
||
a₁ = a₂ → (let x : α := a₁ in b x) = (let x : α := a₂ in b x) :=
|
||
λ h, Eq.ndrecOn h rfl
|
||
|
||
theorem letValueHeq {α : Sort v} {β : α → Sort u} {a₁ a₂ : α} (b : Π x : α, β x) :
|
||
a₁ = a₂ → (let x : α := a₁ in b x) ≅ (let x : α := a₂ in b x) :=
|
||
λ h, Eq.ndrecOn h (Heq.refl (b a₁))
|
||
|
||
theorem letBodyEq {α : Sort v} {β : α → Sort u} (a : α) {b₁ b₂ : Π x : α, β x} :
|
||
(∀ x, b₁ x = b₂ x) → (let x : α := a in b₁ x) = (let x : α := a in b₂ x) :=
|
||
λ h, h a
|
||
|
||
theorem letEq {α : Sort v} {β : Sort u} {a₁ a₂ : α} {b₁ b₂ : α → β} :
|
||
a₁ = a₂ → (∀ x, b₁ x = b₂ x) → (let x : α := a₁ in b₁ x) = (let x : α := a₂ in b₂ x) :=
|
||
λ h₁ h₂, Eq.ndrecOn h₁ (h₂ a₁)
|
||
|
||
section relation
|
||
variables {α : Sort u} {β : Sort v} (r : β → β → Prop)
|
||
local infix `≺`:50 := r
|
||
|
||
def reflexive := ∀ x, x ≺ x
|
||
|
||
def symmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x
|
||
|
||
def transitive := ∀ ⦃x y z⦄, x ≺ y → y ≺ z → x ≺ z
|
||
|
||
def equivalence := reflexive r ∧ symmetric r ∧ transitive r
|
||
|
||
def total := ∀ x y, x ≺ y ∨ y ≺ x
|
||
|
||
def mkEquivalence (rfl : reflexive r) (symm : symmetric r) (trans : transitive r) : equivalence r :=
|
||
⟨rfl, symm, trans⟩
|
||
|
||
def irreflexive := ∀ x, ¬ x ≺ x
|
||
|
||
def antiSymmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x → x = y
|
||
|
||
def emptyRelation := λ a₁ a₂ : α, False
|
||
|
||
def Subrelation (q r : β → β → Prop) := ∀ ⦃x y⦄, q x y → r x y
|
||
|
||
def InvImage (f : α → β) : α → α → Prop :=
|
||
λ a₁ a₂, f a₁ ≺ f a₂
|
||
|
||
theorem InvImage.trans (f : α → β) (h : transitive r) : transitive (InvImage r f) :=
|
||
λ (a₁ a₂ a₃ : α) (h₁ : InvImage r f a₁ a₂) (h₂ : InvImage r f a₂ a₃), h h₁ h₂
|
||
|
||
theorem InvImage.irreflexive (f : α → β) (h : irreflexive r) : irreflexive (InvImage r f) :=
|
||
λ (a : α) (h₁ : InvImage r f a a), h (f a) h₁
|
||
|
||
inductive Tc {α : Sort u} (r : α → α → Prop) : α → α → Prop
|
||
| base : ∀ a b, r a b → Tc a b
|
||
| trans : ∀ a b c, Tc a b → Tc b c → Tc a c
|
||
|
||
@[elabAsEliminator]
|
||
theorem {u1 u2} Tc.ndrec {α : Sort u} {r : α → α → Prop} {C : α → α → Prop}
|
||
(m₁ : ∀ (a b : α), r a b → C a b)
|
||
(m₂ : ∀ (a b c : α), Tc r a b → Tc r b c → C a b → C b c → C a c)
|
||
{a b : α} (h : Tc r a b) : C a b :=
|
||
@Tc.rec α r (λ a b _, C a b) m₁ m₂ a b h
|
||
|
||
@[elabAsEliminator]
|
||
theorem {u1 u2} Tc.ndrecOn {α : Sort u} {r : α → α → Prop} {C : α → α → Prop}
|
||
{a b : α} (h : Tc r a b)
|
||
(m₁ : ∀ (a b : α), r a b → C a b)
|
||
(m₂ : ∀ (a b c : α), Tc r a b → Tc r b c → C a b → C b c → C a c)
|
||
: C a b :=
|
||
@Tc.rec α r (λ a b _, C a b) m₁ m₂ a b h
|
||
|
||
end relation
|
||
|
||
section binary
|
||
variables {α : Type u} {β : Type v}
|
||
variable f : α → α → α
|
||
variable inv : α → α
|
||
variable one : α
|
||
local infix * := f
|
||
local postfix `⁻¹`:max := inv
|
||
variable g : α → α → α
|
||
local infix + := g
|
||
|
||
def commutative := ∀ a b, a * b = b * a
|
||
def associative := ∀ a b c, (a * b) * c = a * (b * c)
|
||
def leftIdentity := ∀ a, one * a = a
|
||
def rightIdentity := ∀ a, a * one = a
|
||
def rightInverse := ∀ a, a * a⁻¹ = one
|
||
def leftCancelative := ∀ a b c, a * b = a * c → b = c
|
||
def rightCancelative := ∀ a b c, a * b = c * b → a = c
|
||
def leftDistributive := ∀ a b c, a * (b + c) = a * b + a * c
|
||
def rightDistributive := ∀ a b c, (a + b) * c = a * c + b * c
|
||
def rightCommutative (h : β → α → β) := ∀ b a₁ a₂, h (h b a₁) a₂ = h (h b a₂) a₁
|
||
def leftCommutative (h : α → β → β) := ∀ a₁ a₂ b, h a₁ (h a₂ b) = h a₂ (h a₁ b)
|
||
|
||
local infix `◾`:50 := Eq.trans
|
||
|
||
theorem leftComm : commutative f → associative f → leftCommutative f :=
|
||
assume hcomm hassoc, assume a b c,
|
||
Eq.symm (hassoc a b c)
|
||
◾ (hcomm a b ▸ rfl : (a*b)*c = (b*a)*c)
|
||
◾ hassoc b a c
|
||
|
||
theorem rightComm : commutative f → associative f → rightCommutative f :=
|
||
assume hcomm hassoc, assume a b c,
|
||
hassoc a b c
|
||
◾ (hcomm b c ▸ rfl : a*(b*c) = a*(c*b))
|
||
◾ Eq.symm (hassoc a c b)
|
||
|
||
end binary
|
||
|
||
/- Subtype -/
|
||
|
||
namespace Subtype
|
||
def existsOfSubtype {α : Type u} {p : α → Prop} : { x // p x } → ∃ x, p x
|
||
| ⟨a, h⟩ := ⟨a, h⟩
|
||
|
||
variables {α : Type u} {p : α → Prop}
|
||
|
||
theorem tagIrrelevant {a : α} (h1 h2 : p a) : mk a h1 = mk a h2 :=
|
||
rfl
|
||
|
||
protected theorem Eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
|
||
| ⟨x, h1⟩ ⟨.(x), h2⟩ rfl := rfl
|
||
|
||
theorem eta (a : {x // p x}) (h : p (val a)) : mk (val a) h = a :=
|
||
Subtype.Eq rfl
|
||
|
||
instance {α : Type u} {p : α → Prop} {a : α} (h : p a) : Inhabited {x // p x} :=
|
||
⟨⟨a, h⟩⟩
|
||
|
||
instance {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
|
||
{decEq := λ ⟨a, h₁⟩ ⟨b, h₂⟩,
|
||
if h : a = b then isTrue (Subtype.Eq h)
|
||
else isFalse (λ h', Subtype.noConfusion h' (λ h', absurd h' h))}
|
||
end Subtype
|
||
|
||
/- Sum -/
|
||
|
||
infixr ⊕ := Sum
|
||
|
||
section
|
||
variables {α : Type u} {β : Type v}
|
||
|
||
instance Sum.inhabitedLeft [h : Inhabited α] : Inhabited (α ⊕ β) :=
|
||
⟨Sum.inl (default α)⟩
|
||
|
||
instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (α ⊕ β) :=
|
||
⟨Sum.inr (default β)⟩
|
||
|
||
instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (α ⊕ β) :=
|
||
{decEq := λ a b,
|
||
match a, b with
|
||
| (Sum.inl a), (Sum.inl b) := if h : a = b then isTrue (h ▸ rfl)
|
||
else isFalse (λ h', Sum.noConfusion h' (λ h', absurd h' h))
|
||
| (Sum.inr a), (Sum.inr b) := if h : a = b then isTrue (h ▸ rfl)
|
||
else isFalse (λ h', Sum.noConfusion h' (λ h', absurd h' h))
|
||
| (Sum.inr a), (Sum.inl b) := isFalse (λ h, Sum.noConfusion h)
|
||
| (Sum.inl a), (Sum.inr b) := isFalse (λ h, Sum.noConfusion h)}
|
||
end
|
||
|
||
/- Product -/
|
||
|
||
section
|
||
variables {α : Type u} {β : Type v}
|
||
|
||
theorem Prod.mk.eta : ∀{p : α × β}, (p.1, p.2) = p
|
||
| (a, b) := rfl
|
||
|
||
instance [Inhabited α] [Inhabited β] : Inhabited (Prod α β) :=
|
||
⟨(default α, default β)⟩
|
||
|
||
instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
|
||
{decEq := λ ⟨a, b⟩ ⟨a', b'⟩,
|
||
match (decEq a a') with
|
||
| (isTrue e₁) :=
|
||
(match (decEq b b') with
|
||
| (isTrue e₂) := isTrue (Eq.recOn e₁ (Eq.recOn e₂ rfl))
|
||
| (isFalse n₂) := isFalse (assume h, Prod.noConfusion h (λ e₁' e₂', absurd e₂' n₂)))
|
||
| (isFalse n₁) := isFalse (assume h, Prod.noConfusion h (λ e₁' e₂', absurd e₁' n₁))}
|
||
|
||
instance [HasLt α] [HasLt β] : HasLt (α × β) :=
|
||
⟨λ s t, s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)⟩
|
||
|
||
instance prodHasDecidableLt
|
||
[HasLt α] [HasLt β] [DecidableEq α] [DecidableEq β]
|
||
[Π a b : α, Decidable (a < b)] [Π a b : β, Decidable (a < b)]
|
||
: Π s t : α × β, Decidable (s < t) :=
|
||
λ t s, Or.Decidable
|
||
|
||
theorem Prod.ltDef [HasLt α] [HasLt β] (s t : α × β) : (s < t) = (s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)) :=
|
||
rfl
|
||
end
|
||
|
||
def {u₁ u₂ v₁ v₂} Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂}
|
||
(f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
|
||
| (a, b) := (f a, g b)
|
||
|
||
/- Dependent products -/
|
||
|
||
notation `Σ` binders `, ` r:(scoped p, Sigma p) := r
|
||
notation `Σ'` binders `, ` r:(scoped p, PSigma p) := r
|
||
|
||
theorem exOfPsig {α : Type u} {p : α → Prop} : (Σ' x, p x) → ∃ x, p x
|
||
| ⟨x, hx⟩ := ⟨x, hx⟩
|
||
|
||
section
|
||
variables {α : Type u} {β : α → Type v}
|
||
|
||
protected theorem Sigma.Eq : ∀ {p₁ p₂ : Σ a : α, β a} (h₁ : p₁.1 = p₂.1), (Eq.recOn h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂
|
||
| ⟨a, b⟩ ⟨.(a), .(b)⟩ rfl rfl := rfl
|
||
end
|
||
|
||
section
|
||
variables {α : Sort u} {β : α → Sort v}
|
||
|
||
protected theorem PSigma.Eq : ∀ {p₁ p₂ : PSigma β} (h₁ : p₁.1 = p₂.1), (Eq.recOn h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂
|
||
| ⟨a, b⟩ ⟨.(a), .(b)⟩ rfl rfl := rfl
|
||
end
|
||
|
||
/- Universe polymorphic unit -/
|
||
|
||
theorem punitEq (a b : PUnit) : a = b :=
|
||
PUnit.recOn a (PUnit.recOn b rfl)
|
||
|
||
theorem punitEqPUnit (a : PUnit) : a = () :=
|
||
punitEq a ()
|
||
|
||
instance : subsingleton PUnit :=
|
||
subsingleton.intro punitEq
|
||
|
||
instance : Inhabited PUnit :=
|
||
⟨()⟩
|
||
|
||
instance : DecidableEq PUnit :=
|
||
{decEq := λ a b, isTrue (punitEq a b)}
|
||
|
||
/- Setoid -/
|
||
|
||
class Setoid (α : Sort u) :=
|
||
(r : α → α → Prop) (iseqv : equivalence r)
|
||
|
||
instance setoidHasEquiv {α : Sort u} [Setoid α] : HasEquiv α :=
|
||
⟨Setoid.r⟩
|
||
|
||
namespace Setoid
|
||
variables {α : Sort u} [Setoid α]
|
||
|
||
theorem refl (a : α) : a ≈ a :=
|
||
match Setoid.iseqv α with
|
||
| ⟨hRefl, hSymm, hTrans⟩ := hRefl a
|
||
|
||
theorem symm {a b : α} (hab : a ≈ b) : b ≈ a :=
|
||
match Setoid.iseqv α with
|
||
| ⟨hRefl, hSymm, hTrans⟩ := hSymm hab
|
||
|
||
theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c :=
|
||
(match Setoid.iseqv α with
|
||
| ⟨hRefl, hSymm, hTrans⟩ := hTrans hab hbc)
|
||
end Setoid
|
||
|
||
/- Propositional extensionality -/
|
||
|
||
axiom propext {a b : Prop} : (a ↔ b) → a = b
|
||
|
||
/- Additional congruence theorems. -/
|
||
|
||
theorem forallCongrEq {a : Sort u} {p q : a → Prop} (h : ∀ x, p x = q x) : (∀ x, p x) = ∀ x, q x :=
|
||
propext (forallCongr (λ a, (h a).toIff))
|
||
|
||
theorem impCongrEq {a b c d : Prop} (h₁ : a = c) (h₂ : b = d) : (a → b) = (c → d) :=
|
||
propext (impCongr h₁.toIff h₂.toIff)
|
||
|
||
theorem impCongrCtxEq {a b c d : Prop} (h₁ : a = c) (h₂ : c → (b = d)) : (a → b) = (c → d) :=
|
||
propext (impCongrCtx h₁.toIff (λ hc, (h₂ hc).toIff))
|
||
|
||
theorem eqTrueIntro {a : Prop} (h : a) : a = True :=
|
||
propext (iffTrueIntro h)
|
||
|
||
theorem eqFalseIntro {a : Prop} (h : ¬a) : a = False :=
|
||
propext (iffFalseIntro h)
|
||
|
||
theorem Iff.toEq {a b : Prop} (h : a ↔ b) : a = b :=
|
||
propext h
|
||
|
||
theorem iffEqEq {a b : Prop} : (a ↔ b) = (a = b) :=
|
||
propext (Iff.intro
|
||
(assume h, Iff.toEq h)
|
||
(assume h, h.toIff))
|
||
|
||
theorem eqFalse {a : Prop} : (a = False) = (¬ a) :=
|
||
have (a ↔ False) = (¬ a), from propext (iffFalse a),
|
||
Eq.subst (@iffEqEq a False) this
|
||
|
||
theorem eqTrue {a : Prop} : (a = True) = a :=
|
||
have (a ↔ True) = a, from propext (iffTrue a),
|
||
Eq.subst (@iffEqEq a True) this
|
||
|
||
/- Quotients -/
|
||
|
||
-- Iff can now be used to do substitutions in a calculation
|
||
theorem iffSubst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) : p b :=
|
||
Eq.subst (propext h₁) h₂
|
||
|
||
namespace Quot
|
||
axiom sound : Π {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r b
|
||
|
||
attribute [elabAsEliminator] lift ind
|
||
|
||
protected theorem liftBeta {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) (c : ∀ a b, r a b → f a = f b) (a : α) : lift f c (Quot.mk r a) = f a :=
|
||
rfl
|
||
|
||
protected theorem indBeta {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} (p : ∀ a, β (Quot.mk r a)) (a : α) : (ind p (Quot.mk r a) : β (Quot.mk r a)) = p a :=
|
||
rfl
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def liftOn {α : Sort u} {β : Sort v} {r : α → α → Prop} (q : Quot r) (f : α → β) (c : ∀ a b, r a b → f a = f b) : β :=
|
||
lift f c q
|
||
|
||
@[elabAsEliminator]
|
||
protected theorem inductionOn {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} (q : Quot r) (h : ∀ a, β (Quot.mk r a)) : β q :=
|
||
ind h q
|
||
|
||
theorem existsRep {α : Sort u} {r : α → α → Prop} (q : Quot r) : ∃ a : α, (Quot.mk r a) = q :=
|
||
Quot.inductionOn q (λ a, ⟨a, rfl⟩)
|
||
|
||
section
|
||
variable {α : Sort u}
|
||
variable {r : α → α → Prop}
|
||
variable {β : Quot r → Sort v}
|
||
|
||
local notation `⟦`:max a `⟧` := Quot.mk r a
|
||
|
||
@[reducible, macroInline]
|
||
protected def indep (f : Π a, β ⟦a⟧) (a : α) : PSigma β :=
|
||
⟨⟦a⟧, f a⟩
|
||
|
||
protected theorem indepCoherent (f : Π a, β ⟦a⟧)
|
||
(h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β ⟦b⟧) = f b)
|
||
: ∀ a b, r a b → Quot.indep f a = Quot.indep f b :=
|
||
λ a b e, PSigma.Eq (sound e) (h a b e)
|
||
|
||
protected theorem liftIndepPr1
|
||
(f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β ⟦b⟧) = f b)
|
||
(q : Quot r) : (lift (Quot.indep f) (Quot.indepCoherent f h) q).1 = q :=
|
||
Quot.ind (λ (a : α), Eq.refl (Quot.indep f a).1) q
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def rec
|
||
(f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β ⟦b⟧) = f b)
|
||
(q : Quot r) : β q :=
|
||
Eq.ndrecOn (Quot.liftIndepPr1 f h q) ((lift (Quot.indep f) (Quot.indepCoherent f h) q).2)
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def recOn
|
||
(q : Quot r) (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β ⟦b⟧) = f b) : β q :=
|
||
Quot.rec f h q
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def recOnSubsingleton
|
||
[h : ∀ a, subsingleton (β ⟦a⟧)] (q : Quot r) (f : Π a, β ⟦a⟧) : β q :=
|
||
Quot.rec f (λ a b h, subsingleton.elim _ (f b)) q
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def hrecOn
|
||
(q : Quot r) (f : Π a, β ⟦a⟧) (c : ∀ (a b : α) (p : r a b), f a ≅ f b) : β q :=
|
||
Quot.recOn q f $
|
||
λ a b p, eqOfHeq $
|
||
have p₁ : (Eq.rec (f a) (sound p) : β ⟦b⟧) ≅ f a, from eqRecHeq (sound p) (f a),
|
||
Heq.trans p₁ (c a b p)
|
||
|
||
end
|
||
end Quot
|
||
|
||
def Quotient {α : Sort u} (s : Setoid α) :=
|
||
@Quot α Setoid.r
|
||
|
||
namespace Quotient
|
||
|
||
@[inline]
|
||
protected def mk {α : Sort u} [s : Setoid α] (a : α) : Quotient s :=
|
||
Quot.mk Setoid.r a
|
||
|
||
notation `⟦`:max a `⟧`:0 := Quotient.mk a
|
||
|
||
def sound {α : Sort u} [s : Setoid α] {a b : α} : a ≈ b → ⟦a⟧ = ⟦b⟧ :=
|
||
Quot.sound
|
||
|
||
@[reducible, elabAsEliminator]
|
||
protected def lift {α : Sort u} {β : Sort v} [s : Setoid α] (f : α → β) : (∀ a b, a ≈ b → f a = f b) → Quotient s → β :=
|
||
Quot.lift f
|
||
|
||
@[elabAsEliminator]
|
||
protected theorem ind {α : Sort u} [s : Setoid α] {β : Quotient s → Prop} : (∀ a, β ⟦a⟧) → ∀ q, β q :=
|
||
Quot.ind
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def liftOn {α : Sort u} {β : Sort v} [s : Setoid α] (q : Quotient s) (f : α → β) (c : ∀ a b, a ≈ b → f a = f b) : β :=
|
||
Quot.liftOn q f c
|
||
|
||
@[elabAsEliminator]
|
||
protected theorem inductionOn {α : Sort u} [s : Setoid α] {β : Quotient s → Prop} (q : Quotient s) (h : ∀ a, β ⟦a⟧) : β q :=
|
||
Quot.inductionOn q h
|
||
|
||
theorem existsRep {α : Sort u} [s : Setoid α] (q : Quotient s) : ∃ a : α, ⟦a⟧ = q :=
|
||
Quot.existsRep q
|
||
|
||
section
|
||
variable {α : Sort u}
|
||
variable [s : Setoid α]
|
||
variable {β : Quotient s → Sort v}
|
||
|
||
@[inline]
|
||
protected def rec
|
||
(f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : a ≈ b), (Eq.rec (f a) (Quotient.sound p) : β ⟦b⟧) = f b)
|
||
(q : Quotient s) : β q :=
|
||
Quot.rec f h q
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def recOn
|
||
(q : Quotient s) (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : a ≈ b), (Eq.rec (f a) (Quotient.sound p) : β ⟦b⟧) = f b) : β q :=
|
||
Quot.recOn q f h
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def recOnSubsingleton
|
||
[h : ∀ a, subsingleton (β ⟦a⟧)] (q : Quotient s) (f : Π a, β ⟦a⟧) : β q :=
|
||
@Quot.recOnSubsingleton _ _ _ h q f
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def hrecOn
|
||
(q : Quotient s) (f : Π a, β ⟦a⟧) (c : ∀ (a b : α) (p : a ≈ b), f a ≅ f b) : β q :=
|
||
Quot.hrecOn q f c
|
||
end
|
||
|
||
section
|
||
universes uA uB uC
|
||
variables {α : Sort uA} {β : Sort uB} {φ : Sort uC}
|
||
variables [s₁ : Setoid α] [s₂ : Setoid β]
|
||
include s₁ s₂
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def lift₂
|
||
(f : α → β → φ)(c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂)
|
||
(q₁ : Quotient s₁) (q₂ : Quotient s₂) : φ :=
|
||
Quotient.lift
|
||
(λ (a₁ : α), Quotient.lift (f a₁) (λ (a b : β), c a₁ a a₁ b (Setoid.refl a₁)) q₂)
|
||
(λ (a b : α) (h : a ≈ b),
|
||
@Quotient.ind β s₂
|
||
(λ (a1 : Quotient s₂),
|
||
(Quotient.lift (f a) (λ (a1 b : β), c a a1 a b (Setoid.refl a)) a1)
|
||
=
|
||
(Quotient.lift (f b) (λ (a b1 : β), c b a b b1 (Setoid.refl b)) a1))
|
||
(λ (a' : β), c a a' b a' h (Setoid.refl a'))
|
||
q₂)
|
||
q₁
|
||
|
||
@[reducible, elabAsEliminator, inline]
|
||
protected def liftOn₂
|
||
(q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : α → β → φ) (c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) : φ :=
|
||
Quotient.lift₂ f c q₁ q₂
|
||
|
||
@[elabAsEliminator]
|
||
protected theorem ind₂ {φ : Quotient s₁ → Quotient s₂ → Prop} (h : ∀ a b, φ ⟦a⟧ ⟦b⟧) (q₁ : Quotient s₁) (q₂ : Quotient s₂) : φ q₁ q₂ :=
|
||
Quotient.ind (λ a₁, Quotient.ind (λ a₂, h a₁ a₂) q₂) q₁
|
||
|
||
@[elabAsEliminator]
|
||
protected theorem inductionOn₂
|
||
{φ : Quotient s₁ → Quotient s₂ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (h : ∀ a b, φ ⟦a⟧ ⟦b⟧) : φ q₁ q₂ :=
|
||
Quotient.ind (λ a₁, Quotient.ind (λ a₂, h a₁ a₂) q₂) q₁
|
||
|
||
@[elabAsEliminator]
|
||
protected theorem inductionOn₃
|
||
[s₃ : Setoid φ]
|
||
{δ : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (q₃ : Quotient s₃) (h : ∀ a b c, δ ⟦a⟧ ⟦b⟧ ⟦c⟧)
|
||
: δ q₁ q₂ q₃ :=
|
||
Quotient.ind (λ a₁, Quotient.ind (λ a₂, Quotient.ind (λ a₃, h a₁ a₂ a₃) q₃) q₂) q₁
|
||
end
|
||
|
||
section exact
|
||
variable {α : Sort u}
|
||
variable [s : Setoid α]
|
||
include s
|
||
|
||
private def rel (q₁ q₂ : Quotient s) : Prop :=
|
||
Quotient.liftOn₂ q₁ q₂
|
||
(λ a₁ a₂, a₁ ≈ a₂)
|
||
(λ a₁ a₂ b₁ b₂ a₁b₁ a₂b₂,
|
||
propext (Iff.intro
|
||
(λ a₁a₂, Setoid.trans (Setoid.symm a₁b₁) (Setoid.trans a₁a₂ a₂b₂))
|
||
(λ b₁b₂, Setoid.trans a₁b₁ (Setoid.trans b₁b₂ (Setoid.symm a₂b₂)))))
|
||
|
||
local infix `~` := rel
|
||
|
||
private theorem rel.refl : ∀ q : Quotient s, q ~ q :=
|
||
λ q, Quot.inductionOn q (λ a, Setoid.refl a)
|
||
|
||
private theorem eqImpRel {q₁ q₂ : Quotient s} : q₁ = q₂ → q₁ ~ q₂ :=
|
||
assume h, Eq.ndrecOn h (rel.refl q₁)
|
||
|
||
theorem exact {a b : α} : ⟦a⟧ = ⟦b⟧ → a ≈ b :=
|
||
assume h, eqImpRel h
|
||
end exact
|
||
|
||
section
|
||
universes uA uB uC
|
||
variables {α : Sort uA} {β : Sort uB}
|
||
variables [s₁ : Setoid α] [s₂ : Setoid β]
|
||
include s₁ s₂
|
||
|
||
@[reducible, elabAsEliminator]
|
||
protected def recOnSubsingleton₂
|
||
{φ : Quotient s₁ → Quotient s₂ → Sort uC} [h : ∀ a b, subsingleton (φ ⟦a⟧ ⟦b⟧)]
|
||
(q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : Π a b, φ ⟦a⟧ ⟦b⟧) : φ q₁ q₂:=
|
||
@Quotient.recOnSubsingleton _ s₁ (λ q, φ q q₂) (λ a, Quotient.ind (λ b, h a b) q₂) q₁
|
||
(λ a, Quotient.recOnSubsingleton q₂ (λ b, f a b))
|
||
|
||
end
|
||
end Quotient
|
||
|
||
section
|
||
variable {α : Type u}
|
||
variable (r : α → α → Prop)
|
||
|
||
inductive EqvGen : α → α → Prop
|
||
| rel {} : Π x y, r x y → EqvGen x y
|
||
| refl {} : Π x, EqvGen x x
|
||
| symm {} : Π x y, EqvGen x y → EqvGen y x
|
||
| trans {} : Π x y z, EqvGen x y → EqvGen y z → EqvGen x z
|
||
|
||
theorem EqvGen.isEquivalence : equivalence (@EqvGen α r) :=
|
||
mkEquivalence _ EqvGen.refl EqvGen.symm EqvGen.trans
|
||
|
||
def EqvGen.Setoid : Setoid α :=
|
||
Setoid.mk _ (EqvGen.isEquivalence r)
|
||
|
||
theorem Quot.exact {a b : α} (H : Quot.mk r a = Quot.mk r b) : EqvGen r a b :=
|
||
@Quotient.exact _ (EqvGen.Setoid r) a b (@congrArg _ _ _ _
|
||
(Quot.lift (@Quotient.mk _ (EqvGen.Setoid r)) (λx y h, Quot.sound (EqvGen.rel x y h))) H)
|
||
|
||
theorem Quot.eqvGenSound {r : α → α → Prop} {a b : α} (H : EqvGen r a b) : Quot.mk r a = Quot.mk r b :=
|
||
EqvGen.recOn H
|
||
(λ x y h, Quot.sound h)
|
||
(λ x, rfl)
|
||
(λ x y _ IH, Eq.symm IH)
|
||
(λ x y z _ _ IH₁ IH₂, Eq.trans IH₁ IH₂)
|
||
end
|
||
|
||
instance {α : Sort u} {s : Setoid α} [d : ∀ a b : α, Decidable (a ≈ b)] : DecidableEq (Quotient s) :=
|
||
{decEq := λ q₁ q₂ : Quotient s,
|
||
Quotient.recOnSubsingleton₂ q₁ q₂
|
||
(λ a₁ a₂,
|
||
match (d a₁ a₂) with
|
||
| (isTrue h₁) := isTrue (Quotient.sound h₁)
|
||
| (isFalse h₂) := isFalse (λ h, absurd (Quotient.exact h) h₂))}
|
||
|
||
/- Function extensionality -/
|
||
|
||
namespace Function
|
||
variables {α : Sort u} {β : α → Sort v}
|
||
|
||
protected def equiv (f₁ f₂ : Π x : α, β x) : Prop := ∀ x, f₁ x = f₂ x
|
||
|
||
local infix `~` := Function.equiv
|
||
|
||
protected theorem equiv.refl (f : Π x : α, β x) : f ~ f := assume x, rfl
|
||
|
||
protected theorem equiv.symm {f₁ f₂ : Π x: α, β x} : f₁ ~ f₂ → f₂ ~ f₁ :=
|
||
λ h x, Eq.symm (h x)
|
||
|
||
protected theorem equiv.trans {f₁ f₂ f₃ : Π x: α, β x} : f₁ ~ f₂ → f₂ ~ f₃ → f₁ ~ f₃ :=
|
||
λ h₁ h₂ x, Eq.trans (h₁ x) (h₂ x)
|
||
|
||
protected theorem equiv.isEquivalence (α : Sort u) (β : α → Sort v) : equivalence (@Function.equiv α β) :=
|
||
mkEquivalence (@Function.equiv α β) (@equiv.refl α β) (@equiv.symm α β) (@equiv.trans α β)
|
||
end Function
|
||
|
||
section
|
||
open Quotient
|
||
variables {α : Sort u} {β : α → Sort v}
|
||
|
||
@[instance]
|
||
private def funSetoid (α : Sort u) (β : α → Sort v) : Setoid (Π x : α, β x) :=
|
||
Setoid.mk (@Function.equiv α β) (Function.equiv.isEquivalence α β)
|
||
|
||
private def extfun (α : Sort u) (β : α → Sort v) : Sort (imax u v) :=
|
||
Quotient (funSetoid α β)
|
||
|
||
private def funToExtfun (f : Π x : α, β x) : extfun α β :=
|
||
⟦f⟧
|
||
private def extfunApp (f : extfun α β) : Π x : α, β x :=
|
||
assume x,
|
||
Quot.liftOn f
|
||
(λ f : Π x : α, β x, f x)
|
||
(λ f₁ f₂ h, h x)
|
||
|
||
theorem funext {f₁ f₂ : Π x : α, β x} (h : ∀ x, f₁ x = f₂ x) : f₁ = f₂ :=
|
||
show extfunApp ⟦f₁⟧ = extfunApp ⟦f₂⟧, from
|
||
congrArg extfunApp (sound h)
|
||
end
|
||
|
||
local infix `~` := Function.equiv
|
||
|
||
instance pi.subsingleton {α : Sort u} {β : α → Sort v} [∀ a, subsingleton (β a)] : subsingleton (Π a, β a) :=
|
||
⟨λ f₁ f₂, funext (λ a, subsingleton.elim (f₁ a) (f₂ a))⟩
|
||
|
||
/- Classical reasoning support -/
|
||
|
||
namespace Classical
|
||
|
||
axiom choice {α : Sort u} : nonempty α → α
|
||
|
||
noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop)
|
||
(h : ∃ x, p x) : {x // p x} :=
|
||
choice $ let ⟨x, px⟩ := h in ⟨⟨x, px⟩⟩
|
||
|
||
noncomputable def choose {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α :=
|
||
(indefiniteDescription p h).val
|
||
|
||
theorem chooseSpec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (choose h) :=
|
||
(indefiniteDescription p h).property
|
||
|
||
/- Diaconescu's theorem: excluded middle from choice, Function extensionality and propositional extensionality. -/
|
||
theorem em (p : Prop) : p ∨ ¬p :=
|
||
let U (x : Prop) : Prop := x = True ∨ p in
|
||
let V (x : Prop) : Prop := x = False ∨ p in
|
||
have exU : ∃ x, U x, from ⟨True, Or.inl rfl⟩,
|
||
have exV : ∃ x, V x, from ⟨False, Or.inl rfl⟩,
|
||
let u : Prop := choose exU in
|
||
let v : Prop := choose exV in
|
||
have uDef : U u, from chooseSpec exU,
|
||
have vDef : V v, from chooseSpec exV,
|
||
have notUvOrP : u ≠ v ∨ p, from
|
||
Or.elim uDef
|
||
(assume hut : u = True,
|
||
Or.elim vDef
|
||
(assume hvf : v = False,
|
||
have hne : u ≠ v, from hvf.symm ▸ hut.symm ▸ trueNeFalse,
|
||
Or.inl hne)
|
||
Or.inr)
|
||
Or.inr,
|
||
have pImpliesUv : p → u = v, from
|
||
assume hp : p,
|
||
have hpred : U = V, from
|
||
funext $ assume x : Prop,
|
||
have hl : (x = True ∨ p) → (x = False ∨ p), from
|
||
assume a, Or.inr hp,
|
||
have hr : (x = False ∨ p) → (x = True ∨ p), from
|
||
assume a, Or.inr hp,
|
||
show (x = True ∨ p) = (x = False ∨ p), from
|
||
propext (Iff.intro hl hr),
|
||
have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV, from
|
||
hpred ▸ λ exU exV, rfl,
|
||
show u = v, from h₀ _ _,
|
||
Or.elim notUvOrP
|
||
(assume hne : u ≠ v, Or.inr (mt pImpliesUv hne))
|
||
Or.inl
|
||
|
||
theorem existsTrueOfNonempty {α : Sort u} : nonempty α → ∃ x : α, True
|
||
| ⟨x⟩ := ⟨x, trivial⟩
|
||
|
||
noncomputable def inhabitedOfNonempty {α : Sort u} (h : nonempty α) : Inhabited α :=
|
||
⟨choice h⟩
|
||
|
||
noncomputable def inhabitedOfExists {α : Sort u} {p : α → Prop} (h : ∃ x, p x) :
|
||
Inhabited α :=
|
||
inhabitedOfNonempty (exists.elim h (λ w hw, ⟨w⟩))
|
||
|
||
/- all propositions are Decidable -/
|
||
noncomputable def propDecidable (a : Prop) : Decidable a :=
|
||
choice $ Or.elim (em a)
|
||
(assume ha, ⟨isTrue ha⟩)
|
||
(assume hna, ⟨isFalse hna⟩)
|
||
local attribute [instance] propDecidable
|
||
|
||
noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) :=
|
||
⟨propDecidable a⟩
|
||
local attribute [instance] decidableInhabited
|
||
|
||
noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
|
||
{decEq := λ x y, propDecidable (x = y)}
|
||
|
||
noncomputable def typeDecidable (α : Sort u) : PSum α (α → False) :=
|
||
match (propDecidable (nonempty α)) with
|
||
| (isTrue hp) := PSum.inl (@Inhabited.default _ (inhabitedOfNonempty hp))
|
||
| (isFalse hn) := PSum.inr (λ a, absurd (nonempty.intro a) hn)
|
||
|
||
noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop)
|
||
(h : nonempty α) : {x : α // (∃ y : α, p y) → p x} :=
|
||
if hp : ∃ x : α, p x then
|
||
let xp := indefiniteDescription _ hp in
|
||
⟨xp.val, λ h', xp.property⟩
|
||
else ⟨choice h, λ h, absurd h hp⟩
|
||
|
||
/- the Hilbert epsilon Function -/
|
||
|
||
noncomputable def epsilon {α : Sort u} [h : nonempty α] (p : α → Prop) : α :=
|
||
(strongIndefiniteDescription p h).val
|
||
|
||
theorem epsilonSpecAux {α : Sort u} (h : nonempty α) (p : α → Prop)
|
||
: (∃ y, p y) → p (@epsilon α h p) :=
|
||
(strongIndefiniteDescription p h).property
|
||
|
||
theorem epsilonSpec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) :
|
||
p (@epsilon α (nonemptyOfExists hex) p) :=
|
||
epsilonSpecAux (nonemptyOfExists hex) p hex
|
||
|
||
theorem epsilonSingleton {α : Sort u} (x : α) : @epsilon α ⟨x⟩ (λ y, y = x) = x :=
|
||
@epsilonSpec α (λ y, y = x) ⟨x, rfl⟩
|
||
|
||
/- the axiom of choice -/
|
||
|
||
theorem axiomOfChoice {α : Sort u} {β : α → Sort v} {r : Π x, β x → Prop} (h : ∀ x, ∃ y, r x y) :
|
||
∃ (f : Π x, β x), ∀ x, r x (f x) :=
|
||
⟨_, λ x, chooseSpec (h x)⟩
|
||
|
||
theorem skolem {α : Sort u} {b : α → Sort v} {p : Π x, b x → Prop} :
|
||
(∀ x, ∃ y, p x y) ↔ ∃ (f : Π x, b x), ∀ x, p x (f x) :=
|
||
⟨axiomOfChoice, λ ⟨f, hw⟩ x, ⟨f x, hw x⟩⟩
|
||
|
||
theorem propComplete (a : Prop) : a = True ∨ a = False :=
|
||
Or.elim (em a)
|
||
(λ t, Or.inl (eqTrueIntro t))
|
||
(λ f, Or.inr (eqFalseIntro f))
|
||
|
||
-- this supercedes byCases in Decidable
|
||
def byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
|
||
Decidable.byCases hpq hnpq
|
||
|
||
-- this supercedes byContradiction in Decidable
|
||
theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
|
||
Decidable.byContradiction h
|
||
|
||
end Classical
|