From fe20860c3d612ed3877cbdec3dc74dba7d60b62c Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 16 Jun 2020 13:44:29 +0200 Subject: [PATCH] chore: delete unused file --- tests/bench/frontend_test.lean | 1813 -------------------------------- 1 file changed, 1813 deletions(-) delete mode 100644 tests/bench/frontend_test.lean diff --git a/tests/bench/frontend_test.lean b/tests/bench/frontend_test.lean deleted file mode 100644 index 6506251a5a..0000000000 --- a/tests/bench/frontend_test.lean +++ /dev/null @@ -1,1813 +0,0 @@ -/- -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