From 1d338c4fc4eaa3db9b26ae60d66cbe2dc5cc9b3e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 25 Oct 2020 08:54:37 -0700 Subject: [PATCH] chore: move `Core.lean` to new frontend --- src/Init/Core.lean | 1660 +++++++++++++++----------------- src/Init/Data/Fin/Basic.lean | 2 - src/Init/Data/Float.lean | 2 - src/Init/Data/Int/Basic.lean | 5 - src/Init/Data/List/Basic.lean | 2 +- src/Init/Data/Nat/Basic.lean | 135 --- src/Init/Data/Nat/Bitwise.lean | 4 +- src/Init/Data/UInt.lean | 11 +- src/Std/Data/HashMap.lean | 2 +- src/Std/Data/HashSet.lean | 2 +- 10 files changed, 792 insertions(+), 1033 deletions(-) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 2c7dac6471..9eb3f2763c 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -1,3 +1,4 @@ +#lang lean4 /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. @@ -7,87 +8,14 @@ notation, basic datatypes and type classes -/ prelude -notation `Prop` := Sort 0 -reserve infixr ` $ `:1 -notation f ` $ ` a := f a - -/- Logical operations and relations -/ - -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 infixr ` ▸ `:75 - -/- types and Type constructors -/ - -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 - -/- other symbols -/ - -reserve infixl ` ++ `:65 -reserve infixr ` :: `:67 - -/- Control -/ -reserve infixr ` <|> `:2 -reserve infixl ` >>= `:55 -reserve infixr ` >=> `:55 -reserve infixl ` <*> `:60 -reserve infixl ` <* ` :60 -reserve infixr ` *> ` :60 -reserve infixr ` >> ` :60 -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 : α → β → φ) : β → α → φ := -fun b a => f a b + fun b a => f a b /- The kernel definitional equality test (t =?= s) has special support for idDelta applications. @@ -103,12 +31,10 @@ This is mechanism for controlling the delta reduction (aka unfolding) used in th We use idDelta applications to address performance problems when Type checking theorems generated by the equation Compiler. -/ -@[inline] def idDelta {α : Sort u} (a : α) : α := -a +@[inline] def idDelta {α : Sort u} (a : α) : α := a /-- Gadget for optional parameter support. -/ -@[reducible] def optParam (α : Sort u) (default : α) : Sort u := -α +@[reducible] def optParam (α : Sort u) (default : α) : Sort u := α /-- Gadget for marking output parameters in type classes. -/ @[reducible] def outParam (α : Sort u) : Sort u := α @@ -123,8 +49,15 @@ a /-- Auxiliary Declaration used to implement the named patterns `x@p` -/ @[reducible] def namedPattern {α : Sort u} (x a : α) : α := a +/-- Auxiliary unsafe constant used by the Compiler when erasing proofs from code. -/ +unsafe axiom lcProof {α : Prop} : α + +/-- Auxiliary unsafe constant used by the Compiler to mark unreachable code. -/ +unsafe axiom lcUnreachable {α : Sort u} : α + +set_option bootstrap.inductiveCheckResultingUniverse false in inductive PUnit : Sort u -| unit : PUnit + | unit : PUnit /-- An abbreviation for `PUnit.{0}`, its most common instantiation. This Type should be preferred over `PUnit` where possible to avoid @@ -135,43 +68,42 @@ abbrev Unit : Type := PUnit /- Remark: thunks have an efficient implementation in the runtime. -/ structure Thunk (α : Type u) : Type u := -(fn : Unit → α) + (fn : Unit → α) attribute [extern "lean_mk_thunk"] Thunk.mk @[noinline, extern "lean_thunk_pure"] protected def Thunk.pure {α : Type u} (a : α) : Thunk α := -⟨fun _ => a⟩ + ⟨fun _ => a⟩ @[noinline, extern "lean_thunk_get_own"] protected def Thunk.get {α : Type u} (x : @& Thunk α) : α := -x.fn () + x.fn () @[noinline, extern "lean_thunk_map"] protected def Thunk.map {α : Type u} {β : Type v} (f : α → β) (x : Thunk α) : Thunk β := -⟨fun _ => f x.get⟩ + ⟨fun _ => f x.get⟩ @[noinline, extern "lean_thunk_bind"] protected def Thunk.bind {α : Type u} {β : Type v} (x : Thunk α) (f : α → Thunk β) : Thunk β := -⟨fun _ => (f x.get).get⟩ + ⟨fun _ => (f x.get).get⟩ inductive True : Prop -| intro : True + | 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 + | refl {} : Eq a a @[elabAsEliminator, inline, reducible] def Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : Eq a b) : motive b := -@Eq.rec α a (fun α _ => motive α) m b h + @Eq.rec α a (fun α _ => motive α) m b h @[elabAsEliminator, inline, reducible] def Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} {b : α} (h : Eq a b) (m : motive a) : motive b := -@Eq.rec α a (fun α _ => motive α) m b h + @Eq.rec α a (fun α _ => motive α) m b h /- Initialize the Quotient Module, which effectively adds the following definitions: @@ -188,157 +120,162 @@ constant Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} -/ init_quot -inductive HEq {α : Sort u} (a : α) : ∀ {β : Sort u}, β → Prop -| refl {} : HEq a +inductive HEq {α : Sort u} (a : α) : {β : Sort u} → β → Prop + | refl {} : HEq a a structure Prod (α : Type u) (β : Type v) := -(fst : α) (snd : β) + (fst : α) (snd : β) attribute [unbox] Prod /-- Similar to `Prod`, but `α` and `β` can be propositions. We use this Type internally to automatically generate the brecOn recursor. -/ structure PProd (α : Sort u) (β : Sort v) := -(fst : α) (snd : β) + (fst : α) (snd : β) /-- Similar to `Prod`, but `α` and `β` are in the same universe. -/ structure MProd (α β : Type u) := -(fst : α) (snd : β) + (fst : α) (snd : β) structure And (a b : Prop) : Prop := -intro :: (left : a) (right : b) + intro :: (left : a) (right : b) structure Iff (a b : Prop) : Prop := -intro :: (mp : a → b) (mpr : b → a) + 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 +@[macroInline] def cast {α β : Sort u} (h : α = β) (a : α) : β := +Eq.rec (motive := fun α _ => α) a h @[matchPattern] def HEq.rfl {α : Sort u} {a : α} : a ≅ a := HEq.refl a -theorem eqOfHEq {α : Sort u} {a a' : α} (h : a ≅ a') : a = a' := -have ∀ (α' : Sort u) (a' : α') (h₁ : @HEq α a α' a') (h₂ : α = α'), (Eq.recOn h₂ a : α') = a' := - fun (α' : Sort u) (a' : α') (h₁ : @HEq α a α' a') => HEq.recOn h₁ (fun (h₂ : α = α) => rfl); -show (Eq.ndrecOn (Eq.refl α) a : α) = a' from - this α a' h (Eq.refl α) +theorem eqOfHEq {α : Sort u} {a a' : α} (h : a ≅ a') : a = a' := by + have (α β : Sort u) → (a : α) → (b : β) → a ≅ b → (h : α = β) → cast h a = b by + intro α β a b h₁ h₂ + induction h₁ + exact rfl + show cast rfl a = a' + exact this α α a a' h rfl inductive Sum (α : Type u) (β : Type v) -| inl (val : α) : Sum -| inr (val : β) : Sum + | inl (val : α) : Sum α β + | inr (val : β) : Sum α β inductive PSum (α : Sort u) (β : Sort v) -| inl (val : α) : PSum -| inr (val : β) : PSum + | inl (val : α) : PSum α β + | inr (val : β) : PSum α β inductive Or (a b : Prop) : Prop -| inl (h : a) : Or -| inr (h : b) : Or + | inl (h : a) : Or a b + | inr (h : b) : Or a b def Or.introLeft {a : Prop} (b : Prop) (ha : a) : Or a b := -Or.inl ha + Or.inl ha def Or.introRight (a : Prop) {b : Prop} (hb : b) : Or a b := -Or.inr hb + Or.inr hb structure Sigma {α : Type u} (β : α → Type v) := -mk :: (fst : α) (snd : β fst) + mk :: (fst : α) (snd : β fst) attribute [unbox] Sigma structure PSigma {α : Sort u} (β : α → Sort v) := -mk :: (fst : α) (snd : β fst) + mk :: (fst : α) (snd : β fst) inductive Bool : Type -| false : Bool -| true : Bool + | 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) + (val : α) (property : p val) + inductive Exists {α : Sort u} (p : α → Prop) : Prop -| intro (w : α) (h : p w) : Exists + | intro (w : α) (h : p w) : Exists p /- Auxiliary type used to compile `for x in xs` notation. -/ inductive ForInStep (α : Type u) -| done : α → ForInStep -| yield : α → ForInStep + | done : α → ForInStep α + | yield : α → ForInStep α /- Auxiliary type used to compile `do` notation. -/ inductive DoResultPRBC (α β σ : Type u) -| «pure» : α → σ → DoResultPRBC -| «return» : β → σ → DoResultPRBC -| «break» : σ → DoResultPRBC -| «continue» : σ → DoResultPRBC + | «pure» : α → σ → DoResultPRBC α β σ + | «return» : β → σ → DoResultPRBC α β σ + | «break» : σ → DoResultPRBC α β σ + | «continue» : σ → DoResultPRBC α β σ /- Auxiliary type used to compile `do` notation. -/ inductive DoResultPR (α β σ : Type u) -| «pure» : α → σ → DoResultPR -| «return» : β → σ → DoResultPR + | «pure» : α → σ → DoResultPR α β σ + | «return» : β → σ → DoResultPR α β σ /- Auxiliary type used to compile `do` notation. -/ inductive DoResultBC (σ : Type u) -| «break» : σ → DoResultBC -| «continue» : σ → DoResultBC + | «break» : σ → DoResultBC σ + | «continue» : σ → DoResultBC σ /- Auxiliary type used to compile `do` notation. -/ inductive DoResultSBC (α σ : Type u) -| «pureReturn» : α → σ → DoResultSBC -| «break» : σ → DoResultSBC -| «continue» : σ → DoResultSBC + | «pureReturn» : α → σ → DoResultSBC α σ + | «break» : σ → DoResultSBC α σ + | «continue» : σ → DoResultSBC α σ class inductive Decidable (p : Prop) -| isFalse (h : ¬p) : Decidable -| isTrue (h : p) : Decidable + | isFalse (h : ¬p) : Decidable p + | isTrue (h : p) : Decidable p abbrev DecidablePred {α : Sort u} (r : α → Prop) := -∀ (a : α), Decidable (r a) + (a : α) → Decidable (r a) abbrev DecidableRel {α : Sort u} (r : α → α → Prop) := -∀ (a b : α), Decidable (r a b) + (a b : α) → Decidable (r a b) abbrev DecidableEq (α : Sort u) := -∀ (a b : α), Decidable (a = b) + (a b : α) → Decidable (a = b) def decEq {α : Sort u} [s : DecidableEq α] (a b : α) : Decidable (a = b) := -s a b + s a b inductive Option (α : Type u) -| none : Option -| some (val : α) : Option + | none : Option α + | some (val : α) : Option α attribute [unbox] 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 List (α : Type u) + | nil : List α + | cons (head : α) (tail : List α) : List α inductive Nat -| zero : Nat -| succ (n : Nat) : Nat + | zero : Nat + | succ (n : Nat) : Nat + +/- For numeric literals notation -/ +class HasOfNat (α : Type u) := + (ofNat : Nat → α) + +export HasOfNat (ofNat) + +instance : HasOfNat Nat := ⟨id⟩ /- Auxiliary axiom used to implement `sorry`. TODO: add this theorem on-demand. That is, @@ -346,9 +283,6 @@ inductive Nat axiom sorryAx (α : Sort u) (synthetic := true) : α /- Declare builtin and reserved notation -/ - -class HasZero (α : Type u) := mk {} :: (zero : α) -class HasOne (α : Type u) := mk {} :: (one : α) class HasAdd (α : Type u) := (add : α → α → α) class HasMul (α : Type u) := (mul : α → α → α) class HasNeg (α : Type u) := (neg : α → α) @@ -364,67 +298,25 @@ class HasOrelse (α : Type u) := (orelse : α → α → α) class HasAndthen (α : Type u) := (andthen : α → α → α) class HasEquiv (α : Sort u) := (Equiv : α → α → Prop) class HasEmptyc (α : Type u) := (emptyc : α) - -class HasPow (α : Type u) (β : Type v) := -(pow : α → β → α) - -infix `+` := HasAdd.add -infix `*` := HasMul.mul -infix `-` := HasSub.sub -infix `/` := HasDiv.div -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 `≈` := 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 +class HasPow (α : Type u) (β : Type v) := (pow : α → β → α) @[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 - -@[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 - /- Nat basic instances -/ + +set_option bootstrap.gen_matcher_code false in @[extern "lean_nat_add"] protected def Nat.add : (@& Nat) → (@& Nat) → Nat -| a, Nat.zero => a -| a, Nat.succ b => Nat.succ (Nat.add a b) + | 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)⟩ +attribute [matchPattern] Nat.add HasAdd.add HasNeg.neg 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 @@ -450,7 +342,7 @@ def std.prec.maxPlus : Nat := std.prec.max + 10 /- Remark: tasks have an efficient implementation in the runtime. -/ structure Task (α : Type u) : Type u := pure :: -(get : α) + (get : α) attribute [extern "lean_task_pure"] Task.pure attribute [extern "lean_task_get_own"] Task.get @@ -469,40 +361,30 @@ def Priority.dedicated : Priority := 9 @[noinline, extern "lean_task_spawn"] protected def spawn {α : Type u} (fn : Unit → α) (prio := Priority.default) : Task α := -⟨fn ()⟩ + ⟨fn ()⟩ + @[noinline, extern "lean_task_map"] protected def map {α : Type u} {β : Type v} (f : α → β) (x : Task α) (prio := Priority.default) : Task β := -⟨f x.get⟩ + ⟨f x.get⟩ + @[noinline, extern "lean_task_bind"] protected def bind {α : Type u} {β : Type v} (x : Task α) (f : α → Task β) (prio := Priority.default) : Task β := -⟨(f x.get).get⟩ + ⟨(f x.get).get⟩ end Task -infixr `×` := Prod --- notation for n-ary tuples - /- Some type that is not a scalar value in our runtime. -/ structure NonScalar := -(val : Nat) + (val : Nat) /- Some type that is not a scalar value in our runtime and is universe polymorphic. -/ inductive PNonScalar : Type u -| mk (v : Nat) : PNonScalar - -/- For numeric literals notation -/ -class HasOfNat (α : Type u) := -(ofNat : Nat → α) - -export HasOfNat (ofNat) - -instance : HasOfNat Nat := -⟨id⟩ + | mk (v : Nat) : PNonScalar /- sizeof -/ class HasSizeof (α : Sort u) := -(sizeof : α → Nat) + (sizeof : α → Nat) export HasSizeof (sizeof) @@ -513,78 +395,64 @@ From now on, the inductive Compiler will automatically generate sizeof instances /- Every Type `α` has a default HasSizeof instance that just returns 0 for every element of `α` -/ protected def default.sizeof (α : Sort u) : α → Nat -| a => 0 + | a => 0 -instance defaultHasSizeof (α : Sort u) : HasSizeof α := -⟨default.sizeof α⟩ +instance (α : Sort u) : HasSizeof α := + ⟨default.sizeof α⟩ -protected def Nat.sizeof : Nat → Nat -| n => n +instance : HasSizeof Nat := { + sizeof := fun n => n +} -instance : HasSizeof Nat := -⟨Nat.sizeof⟩ +instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Prod α β) := { + sizeof := fun (a, b) => 1 + sizeof a + sizeof b +} -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 (Sum α β) := { + sizeof := fun + | Sum.inl a => 1 + sizeof a + | Sum.inr b => 1 + sizeof b +} -instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Prod α β) := -⟨Prod.sizeof⟩ +instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (PSum α β) := { + sizeof := fun + | PSum.inl a => 1 + sizeof a + | PSum.inr b => 1 + sizeof b +} -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 α] [∀ a, HasSizeof (β a)] : HasSizeof (Sigma β) := { + sizeof := fun ⟨a, b⟩ => 1 + sizeof a + sizeof b +} -instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Sum α β) := -⟨Sum.sizeof⟩ +instance (α : Type u) (β : α → Type v) [HasSizeof α] [(a : α) → HasSizeof (β a)] : HasSizeof (PSigma β) := { + sizeof := fun ⟨a, b⟩ => 1 + sizeof a + sizeof b +} -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 : HasSizeof PUnit := { + sizeof := fun _ => 1 +} -instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (PSum α β) := -⟨PSum.sizeof⟩ +instance : HasSizeof Bool := { + sizeof := fun _ => 1 +} -protected def Sigma.sizeof {α : Type u} {β : α → Type v} [HasSizeof α] [∀ a, HasSizeof (β a)] : Sigma β → Nat -| ⟨a, b⟩ => 1 + sizeof a + sizeof b +instance (α : Type u) [HasSizeof α] : HasSizeof (Option α) := { + sizeof := fun + | none => 1 + | some a => 1 + sizeof a +} -instance (α : Type u) (β : α → Type v) [HasSizeof α] [∀ a, HasSizeof (β a)] : HasSizeof (Sigma β) := -⟨Sigma.sizeof⟩ +instance (α : Type u) [HasSizeof α] : HasSizeof (List α) := { + sizeof := fun as => + let rec loop + | List.nil => 1 + | List.cons x xs => 1 + sizeof x + loop xs + loop as +} -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⟩ +instance {α : Type u} [HasSizeof α] (p : α → Prop) : HasSizeof (Subtype p) := { + sizeof := fun ⟨a, _⟩ => sizeof a +} theorem natAddZero (n : Nat) : n + 0 = n := rfl @@ -597,57 +465,51 @@ theorem optParamEq (α : Sort u) (default : α) : optParam α default = α := rf /- Boolean operators -/ @[macroInline] def cond {a : Type u} : Bool → a → a → a -| true, x, y => x -| false, x, y => y + | true, x, y => x + | false, x, y => y @[inline] def condEq {β : Sort u} (b : Bool) (h₁ : b = true → β) (h₂ : b = false → β) : β := -@Bool.casesOn (λ x => b = x → β) b h₂ h₁ rfl + @Bool.casesOn (λ x => b = x → β) b h₂ h₁ rfl @[macroInline] def or : Bool → Bool → Bool -| true, _ => true -| false, b => b + | true, _ => true + | false, b => b @[macroInline] def and : Bool → Bool → Bool -| false, _ => false -| true, b => b + | false, _ => false + | true, b => b @[macroInline] def not : Bool → Bool -| true => false -| false => true + | true => false + | false => true @[macroInline] def xor : Bool → Bool → Bool -| true, b => not b -| false, b => b - -prefix `!` := not -infix `||` := or -infix `&&` := and + | true, b => not b + | false, b => b @[extern c inline "#1 || #2"] def strictOr (b₁ b₂ : Bool) := b₁ || b₂ @[extern c inline "#1 && #2"] def strictAnd (b₁ b₂ : Bool) := b₁ && b₂ @[inline] def bne {α : Type u} [HasBeq α] (a b : α) : Bool := -!(a == b) - -infix `!=` := bne + !(a == b) /- Logical connectives an equality -/ def implies (a b : Prop) := a → b theorem implies.trans {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) : implies p r := -fun hp => h₂ (h₁ hp) + fun hp => h₂ (h₁ hp) def trivial : True := ⟨⟩ @[macroInline] def False.elim {C : Sort u} (h : False) : C := -False.rec (fun _ => C) h + False.rec (fun _ => C) h @[macroInline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : ¬a) : b := -False.elim (h₂ h₁) + False.elim (h₂ h₁) theorem mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a := -fun ha => h₂ (h₁ ha) + fun ha => h₂ (h₁ ha) theorem notFalse : ¬False := id @@ -656,48 +518,45 @@ 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.mp {α β : Sort u} (h : α = β) (a : α) : β := + h ▸ a -@[macroInline] def Eq.mpr {α β : Sort u} : (α = β) → β → α := -fun h₁ h₂ => Eq.recOn (Eq.symm h₁) h₂ +@[macroInline] def Eq.mpr {α β : Sort u} (h : α = β) (b : β) : α := + h ▸ b @[elabAsEliminator] theorem Eq.substr {α : Sort u} {p : α → Prop} {a b : α} (h₁ : b = a) (h₂ : p a) : p b := -Eq.subst (Eq.symm h₁) h₂ + 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) + h₁ ▸ 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)) + h ▸ rfl theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂ := -congr rfl h + congr rfl h theorem transRelLeft {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c := -h₂ ▸ h₁ + h₂ ▸ h₁ theorem transRelRight {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : a = b) (h₂ : r b c) : r a c := -h₁.symm ▸ h₂ + h₁ ▸ h₂ theorem ofEqTrue {p : Prop} (h : p = True) : p := -h.symm ▸ trivial + h ▸ trivial theorem notOfEqFalse {p : Prop} (h : p = False) : ¬p := -fun hp => h ▸ hp + fun 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 castProofIrrel {α β : Sort u} (h₁ h₂ : α = β) (a : α) : cast h₁ a = cast h₂ a := rfl +theorem castEq {α : Sort u} (h : α = α) (a : α) : cast h a = 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 +@[reducible] def Ne {α : Sort u} (a b : α) := + ¬(a = b) section Ne variable {α : Sort u} @@ -710,546 +569,585 @@ theorem Ne.elim (h : a ≠ b) : a = b → False := h theorem Ne.irrefl (h : a ≠ a) : False := h rfl theorem Ne.symm (h : a ≠ b) : b ≠ a := -fun h₁ => h (h₁.symm) + fun h₁ => h (h₁.symm) theorem falseOfNe : a ≠ a → False := Ne.irrefl theorem neFalseOfSelf : p → p ≠ False := -fun (hp : p) (h : p = False) => h ▸ hp + fun (hp : p) (h : p = False) => h ▸ hp theorem neTrueOfNot : ¬p → p ≠ True := -fun (hnp : ¬p) (h : p = True) => (h ▸ hnp) trivial + fun (hnp : ¬p) (h : p = True) => + have ¬True from h ▸ hnp + this trivial theorem trueNeFalse : ¬True = False := -neFalseOfSelf trivial + neFalseOfSelf trivial + end Ne theorem eqFalseOfNeTrue : ∀ {b : Bool}, b ≠ true → b = false -| true, h => False.elim (h rfl) -| false, h => rfl + | 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) + | true, h => rfl + | false, h => False.elim (h rfl) theorem neFalseOfEqTrue : ∀ {b : Bool}, b = true → b ≠ false -| true, _ => fun h => Bool.noConfusion h -| false, h => Bool.noConfusion h + | true, _ => fun h => Bool.noConfusion h + | false, h => Bool.noConfusion h theorem neTrueOfEqFalse : ∀ {b : Bool}, b = false → b ≠ true -| true, h => Bool.noConfusion h -| false, _ => fun h => Bool.noConfusion h + | true, h => Bool.noConfusion h + | false, _ => fun h => Bool.noConfusion h section variables {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ} @[elabAsEliminator] -theorem HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : ∀ {β : Sort u2}, β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : a ≅ b) : motive b := -@HEq.rec α a (fun β b _ => motive b) m β b h +theorem HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : a ≅ b) : motive b := + @HEq.rec α a (fun b _ => motive b) m β b h @[elabAsEliminator] -theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : ∀ {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : motive a) : motive b := -@HEq.rec α a (fun β b _ => motive b) m β b h +theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : motive a) : motive b := + @HEq.rec α a (fun b _ => motive b) m β b h theorem HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b := -Eq.recOn (eqOfHEq h₁) h₂ + 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.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) + HEq.ndrecOn (motive := fun x => x ≅ a) h (HEq.refl a) theorem heqOfEq (h : a = a') : a ≅ a' := -Eq.subst h (HEq.refl a) + Eq.subst h (HEq.refl a) theorem HEq.trans (h₁ : a ≅ b) (h₂ : b ≅ c) : a ≅ c := -HEq.subst h₂ h₁ + HEq.subst h₂ h₁ theorem heqOfHEqOfEq (h₁ : a ≅ b) (h₂ : b = b') : a ≅ b' := -HEq.trans h₁ (heqOfEq h₂) + HEq.trans h₁ (heqOfEq h₂) theorem heqOfEqOfHEq (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b := -HEq.trans (heqOfEq h₁) h₂ + HEq.trans (heqOfEq h₁) h₂ def typeEqOfHEq (h : a ≅ b) : α = β := -HEq.ndrecOn h (Eq.refl α) + HEq.ndrecOn (motive := @fun (x : Sort u) _ => α = x) h (Eq.refl α) + end -theorem eqRecHEq {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} (h : a = a') (p : φ a), (Eq.recOn h p : φ a') ≅ p -| a, _, rfl, p => HEq.refl p +theorem eqRecHEq {α : Sort u} {φ : α → Sort v} : {a a' : α} → (h : a = a') → (p : φ a) → (Eq.recOn (motive := fun x _ => φ x) h p) ≅ p + | a, _, rfl, p => HEq.refl p theorem ofHEqTrue {a : Prop} (h : a ≅ True) : a := -ofEqTrue (eqOfHEq h) + ofEqTrue (eqOfHEq h) + +theorem heqOfEqRecEq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ : Eq.rec (motive := fun α _ => α) a h₁ = b) : a ≅ b := by + subst h₁ + apply heqOfEq + exact h₂ + done theorem castHEq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a -| α, _, rfl, a => HEq.refl a + | α, _, 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₁ + h₂ h₁.1 h₁.2 theorem And.swap : a ∧ b → b ∧ a := -fun ⟨ha, hb⟩ => ⟨hb, ha⟩ + fun ⟨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₁ + match h₁ with + | Or.inl h => h₂ h + | Or.inr h => h₃ h theorem Or.swap (h : a ∨ b) : b ∨ a := -Or.elim h Or.inr Or.inl + Or.elim h Or.inr Or.inl -def Or.symm := @Or.swap +def Or.symm := + @Or.swap /- xor -/ -def Xor (a b : Prop) : Prop := (a ∧ ¬ b) ∨ (b ∧ ¬ a) +def Xor (a b : Prop) : Prop := + (a ∧ ¬ b) ∨ (b ∧ ¬ a) @[recursor 5] theorem Iff.elim (h₁ : (a → b) → (b → a) → c) (h₂ : a ↔ b) : c := -Iff.rec h₁ h₂ + h₁ h₂.1 h₂.2 -theorem Iff.left : (a ↔ b) → a → b := Iff.mp +theorem Iff.left : (a ↔ b) → a → b := + Iff.mp -theorem Iff.right : (a ↔ b) → b → a := Iff.mpr +theorem Iff.right : (a ↔ b) → b → a := + Iff.mpr theorem iffIffImpliesAndImplies (a b : Prop) : (a ↔ b) ↔ (a → b) ∧ (b → a) := -Iff.intro (fun h => And.intro h.mp h.mpr) (fun h => Iff.intro h.left h.right) + Iff.intro (fun h => And.intro h.mp h.mpr) (fun h => Iff.intro h.left h.right) theorem Iff.refl (a : Prop) : a ↔ a := -Iff.intro (fun h => h) (fun h => h) + Iff.intro (fun h => h) (fun h => h) theorem Iff.rfl {a : Prop} : a ↔ a := -Iff.refl a + Iff.refl a theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c := -Iff.intro - (fun ha => Iff.mp h₂ (Iff.mp h₁ ha)) - (fun hc => Iff.mpr h₁ (Iff.mpr h₂ hc)) + Iff.intro + (fun ha => Iff.mp h₂ (Iff.mp h₁ ha)) + (fun hc => Iff.mpr h₁ (Iff.mpr h₂ hc)) theorem Iff.symm (h : a ↔ b) : b ↔ a := -Iff.intro (Iff.right h) (Iff.left h) + Iff.intro (Iff.right h) (Iff.left h) theorem Iff.comm : (a ↔ b) ↔ (b ↔ a) := -Iff.intro Iff.symm Iff.symm + Iff.intro Iff.symm Iff.symm theorem Eq.toIff {a b : Prop} (h : a = b) : a ↔ b := -Eq.recOn h Iff.rfl + h ▸ Iff.rfl theorem neqOfNotIff {a b : Prop} : ¬(a ↔ b) → a ≠ b := -fun h₁ h₂ => -have a ↔ b from Eq.subst h₂ (Iff.refl a); -absurd this h₁ + fun h₁ h₂ => + have a ↔ b from Eq.subst h₂ (Iff.refl a); + absurd this h₁ theorem notIffNotOfIff (h₁ : a ↔ b) : ¬a ↔ ¬b := -Iff.intro - (fun (hna : ¬ a) (hb : b) => hna (Iff.right h₁ hb)) - (fun (hnb : ¬ b) (ha : a) => hnb (Iff.left h₁ ha)) + Iff.intro + (fun (hna : ¬ a) (hb : b) => hna (Iff.right h₁ hb)) + (fun (hnb : ¬ b) (ha : a) => hnb (Iff.left h₁ ha)) theorem ofIffTrue (h : a ↔ True) : a := -Iff.mp (Iff.symm h) trivial + Iff.mp (Iff.symm h) trivial -theorem notOfIffFalse : (a ↔ False) → ¬a := Iff.mp +theorem notOfIffFalse : (a ↔ False) → ¬a := + Iff.mp theorem iffTrueIntro (h : a) : a ↔ True := -Iff.intro - (fun hl => trivial) - (fun hr => h) + Iff.intro + (fun hl => trivial) + (fun hr => h) theorem iffFalseIntro (h : ¬a) : a ↔ False := -Iff.intro h (False.rec (fun _ => a)) + Iff.intro h (False.rec (fun _ => a)) theorem notNotIntro (ha : a) : ¬¬a := -fun hna => hna ha + fun hna => hna ha theorem notTrue : (¬ True) ↔ False := -iffFalseIntro (notNotIntro trivial) + iffFalseIntro (notNotIntro trivial) /- or resolution rulses -/ theorem resolveLeft {a b : Prop} (h : a ∨ b) (na : ¬ a) : b := -Or.elim h (fun ha => absurd ha na) id + Or.elim h (fun ha => absurd ha na) id theorem negResolveLeft {a b : Prop} (h : ¬ a ∨ b) (ha : a) : b := -Or.elim h (fun na => absurd ha na) id + Or.elim h (fun na => absurd ha na) id theorem resolveRight {a b : Prop} (h : a ∨ b) (nb : ¬ b) : a := -Or.elim h id (fun hb => absurd hb nb) + Or.elim h id (fun hb => absurd hb nb) theorem negResolveRight {a b : Prop} (h : a ∨ ¬ b) (hb : b) : a := -Or.elim h id (fun nb => absurd hb nb) + Or.elim h id (fun nb => absurd hb nb) /- Exists -/ theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop} (h₁ : Exists (fun x => p x)) (h₂ : ∀ (a : α), p a → b) : b := -Exists.rec h₂ h₁ + h₂ h₁.1 h₁.2 /- Decidable -/ @[inlineIfReduce, nospecialize] def Decidable.decide (p : Prop) [h : Decidable p] : Bool := -Decidable.casesOn h (fun h₁ => false) (fun h₂ => true) + Decidable.casesOn (motive := fun _ => Bool) h (fun _ => false) (fun _ => true) export Decidable (isTrue isFalse decide) -instance beqOfEq {α : Type u} [DecidableEq α] : HasBeq α := -⟨fun a b => decide (a = b)⟩ +instance {α : Type u} [DecidableEq α] : HasBeq α := + ⟨fun a b => decide (a = b)⟩ theorem decideTrueEqTrue (h : Decidable True) : @decide True h = true := -match h with -| isTrue h => rfl -| isFalse h => False.elim (Iff.mp notTrue h) + match h with + | isTrue h => rfl + | isFalse h => False.elim (Iff.mp notTrue h) theorem decideFalseEqFalse (h : Decidable False) : @decide False h = false := -match h with -| isFalse h => rfl -| isTrue h => False.elim h + match h with + | isFalse h => rfl + | isTrue h => False.elim h theorem decideEqTrue : ∀ {p : Prop} [s : Decidable p], p → decide p = true -| _, isTrue _, _ => rfl -| _, isFalse h₁, h₂ => absurd h₂ h₁ + | _, isTrue _, _ => rfl + | _, isFalse h₁, h₂ => absurd h₂ h₁ theorem decideEqFalse : ∀ {p : Prop} [s : Decidable p], ¬p → decide p = false -| _, isTrue h₁, h₂ => absurd h₁ h₂ -| _, isFalse h, _ => rfl + | _, isTrue h₁, h₂ => absurd h₁ h₂ + | _, isFalse h, _ => rfl -theorem ofDecideEqTrue {p : Prop} [s : Decidable p] : decide p = true → p := -fun h => match s with +theorem ofDecideEqTrue {p : Prop} [s : Decidable p] : decide p = true → p := fun h => + match s with | isTrue h₁ => h₁ | isFalse h₁ => absurd h (neTrueOfEqFalse (decideEqFalse h₁)) -theorem ofDecideEqFalse {p : Prop} [s : Decidable p] : decide p = false → ¬p := -fun h => match s with +theorem ofDecideEqFalse {p : Prop} [s : Decidable p] : decide p = false → ¬p := fun h => + match s with | isTrue h₁ => absurd h (neFalseOfEqTrue (decideEqTrue h₁)) | isFalse h₁ => h₁ /-- Similar to `decide`, but uses an explicit instance -/ @[inline] def toBoolUsing {p : Prop} (d : Decidable p) : Bool := -@decide p d + @decide p d theorem toBoolUsingEqTrue {p : Prop} (d : Decidable p) (h : p) : toBoolUsing d = true := -@decideEqTrue _ d h + @decideEqTrue _ d h theorem ofBoolUsingEqTrue {p : Prop} {d : Decidable p} (h : toBoolUsing d = true) : p := -@ofDecideEqTrue _ d h + @ofDecideEqTrue _ d h theorem ofBoolUsingEqFalse {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) : ¬ p := -@ofDecideEqFalse _ d h + @ofDecideEqFalse _ d h instance : Decidable True := -isTrue trivial + isTrue trivial instance : Decidable False := -isFalse notFalse + isFalse notFalse -- We use "dependent" if-then-else to be able to communicate the if-then-else condition -- to the branches -@[macroInline] def dite {α : Sort u} (c : Prop) [h : Decidable c] : (c → α) → (¬ c → α) → α := -fun t e => Decidable.casesOn h e t +@[macroInline] def dite {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : ¬ c → α) : α := + Decidable.casesOn (motive := fun _ => α) h e t /- if-then-else -/ @[macroInline] def ite {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α := -Decidable.casesOn h (fun hnc => e) (fun hc => t) + Decidable.casesOn (motive := fun _ => α) h (fun _ => e) (fun _ => 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 (fun h => False.rec _ (h h₃)) (fun 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 (fun h => h₄) (fun 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 + match s with + | isTrue h => h1 h + | isFalse h => h2 h theorem em (p : Prop) [Decidable p] : p ∨ ¬p := -byCases Or.inl Or.inr + byCases Or.inl Or.inr theorem byContradiction [Decidable p] (h : ¬p → False) : p := -byCases id (fun np => False.elim (h np)) + byCases id (fun np => False.elim (h np)) theorem ofNotNot [Decidable p] : ¬ ¬ p → p := -fun hnn => byContradiction (fun hn => absurd hn hnn) + fun hnn => byContradiction (fun hn => absurd hn hnn) theorem notNotIff (p) [Decidable p] : (¬ ¬ p) ↔ p := -Iff.intro ofNotNot notNotIntro + Iff.intro ofNotNot notNotIntro theorem notAndIffOrNot (p q : Prop) [d₁ : Decidable p] [d₂ : Decidable q] : ¬ (p ∧ q) ↔ ¬ p ∨ ¬ q := -Iff.intro -(fun h => match d₁, d₂ with + Iff.intro + (fun h => match d₁, d₂ with | isTrue h₁, isTrue h₂ => absurd (And.intro h₁ h₂) h | _, isFalse h₂ => Or.inr h₂ | isFalse h₁, _ => Or.inl h₁) -(fun (h) ⟨hp, hq⟩ => Or.elim h (fun h => h hp) (fun h => h hq)) + (fun (h) ⟨hp, hq⟩ => Or.elim h (fun h => h hp) (fun h => h hq)) end Decidable section variables {p q : Prop} @[inline] def decidableOfDecidableOfIff (hp : Decidable p) (h : p ↔ q) : Decidable q := -if hp : p then isTrue (Iff.mp h hp) -else isFalse (Iff.mp (notIffNotOfIff h) hp) + 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 + decidableOfDecidableOfIff hp h.toIff end section variables {p q : Prop} @[macroInline] instance [Decidable p] [Decidable q] : Decidable (p ∧ q) := -if hp : p then - if hq : q then isTrue ⟨hp, hq⟩ - else isFalse (fun h => hq (And.right h)) -else isFalse (fun h => hp (And.left h)) + if hp : p then + if hq : q then isTrue ⟨hp, hq⟩ + else isFalse (fun h => hq (And.right h)) + else isFalse (fun h => hp (And.left h)) @[macroInline] instance [Decidable p] [Decidable q] : Decidable (p ∨ q) := -if hp : p then isTrue (Or.inl hp) else - if hq : q then isTrue (Or.inr hq) else - isFalse (fun h => Or.elim h hp hq) + if hp : p then isTrue (Or.inl hp) else + if hq : q then isTrue (Or.inr hq) else + isFalse (fun h => Or.elim h hp hq) instance [Decidable p] : Decidable (¬p) := -if hp : p then isFalse (absurd hp) else isTrue hp + 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 (fun h => hq) - else isFalse (fun h => absurd (h hp) hq) -else isTrue (fun h => absurd h hp) +@[macroInline] instance [Decidable p] [Decidable q] : Decidable (p → q) := + if hp : p then + if hq : q then isTrue (fun h => hq) + else isFalse (fun h => absurd (h hp) hq) + else isTrue (fun h => absurd h hp) instance [Decidable p] [Decidable q] : Decidable (p ↔ q) := -if hp : p then - if hq : q then isTrue ⟨fun _ => hq, fun _ => hp⟩ - else isFalse $ fun h => hq (h.1 hp) -else - if hq : q then isFalse $ fun h => hp (h.2 hq) - else isTrue $ ⟨fun h => absurd h hp, fun h => absurd h hq⟩ + if hp : p then + if hq : q then isTrue ⟨fun _ => hq, fun _ => hp⟩ + else isFalse $ fun h => hq (h.1 hp) + else + if hq : q then isFalse $ fun h => hp (h.2 hq) + else isTrue $ ⟨fun h => absurd h hp, fun h => absurd h hq⟩ instance [Decidable p] [Decidable q] : Decidable (Xor p q) := -if hp : p then - if hq : q then isFalse (fun h => Or.elim h (fun ⟨_, h⟩ => h hq : ¬(p ∧ ¬ q)) (fun ⟨_, h⟩ => h hp : ¬(q ∧ ¬ p))) - else isTrue $ Or.inl ⟨hp, hq⟩ -else - if hq : q then isTrue $ Or.inr ⟨hq, hp⟩ - else isFalse (fun h => Or.elim h (fun ⟨h, _⟩ => hp h : ¬(p ∧ ¬ q)) (fun ⟨h, _⟩ => hq h : ¬(q ∧ ¬ p))) + if hp : p then + if hq : q then isFalse (fun h => Or.elim h (fun ⟨_, h⟩ => h hq : ¬(p ∧ ¬ q)) (fun ⟨_, h⟩ => h hp : ¬(q ∧ ¬ p))) + else isTrue $ Or.inl ⟨hp, hq⟩ + else + if hq : q then isTrue $ Or.inr ⟨hq, hp⟩ + else isFalse (fun h => Or.elim h (fun ⟨h, _⟩ => hp h : ¬(p ∧ ¬ q)) (fun ⟨h, _⟩ => hq h : ¬(q ∧ ¬ p))) end @[inline] instance {α : Sort u} [DecidableEq α] (a b : α) : Decidable (a ≠ b) := -match decEq a b with -| isTrue h => isFalse $ fun h' => absurd h h' -| isFalse h => isTrue h + match decEq a b with + | isTrue h => isFalse $ fun h' => absurd h h' + | isFalse h => isTrue h theorem Bool.falseNeTrue (h : false = true) : False := -Bool.noConfusion h + Bool.noConfusion h @[inline] instance : DecidableEq Bool := -fun a b => match a, b with - | false, false => isTrue rfl - | false, true => isFalse Bool.falseNeTrue - | true, false => isFalse (Ne.symm Bool.falseNeTrue) - | true, true => isTrue rfl + fun a b => match a, b with + | false, false => isTrue rfl + | false, true => isFalse Bool.falseNeTrue + | true, false => isFalse (Ne.symm Bool.falseNeTrue) + | true, true => isTrue rfl /- if-then-else expression theorems -/ theorem ifPos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t e : α} : (ite c t e) = t := -match h with -| (isTrue hc) => rfl -| (isFalse hnc) => absurd hc hnc + 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 + match h with + | (isTrue hc) => absurd hc hnc + | (isFalse hnc) => rfl theorem difPos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = t hc := -match h with -| (isTrue hc) => rfl -| (isFalse hnc) => absurd hc hnc + 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 + match h with + | (isTrue hc) => absurd hc hnc + | (isFalse hnc) => rfl -- Remark: dite and ite are "defally equal" when we ignore the proofs. theorem difEqIf (c : Prop) [h : Decidable c] {α : Sort u} (t : α) (e : α) : dite c (fun h => t) (fun h => e) = ite c t e := -match h with -| (isTrue hc) => rfl -| (isFalse hnc) => rfl + 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 + 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 ULift.{r, s} (α : 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 + match dC with + | (isTrue hc) => dT hc + | (isFalse hc) => dE hc /-- Universe lifting operation from Sort to Type -/ structure PLift (α : Sort u) : Type u := -up :: (down : α) + up :: (down : α) -namespace PLift /- Bijection between α and PLift α -/ -theorem upDown {α : Sort u} : ∀ (b : PLift α), up (down b) = b -| up a => rfl +theorem PLift.upDown {α : Sort u} : ∀ (b : PLift α), up (down b) = b + | up a => rfl -theorem downUp {α : Sort u} (a : α) : down (up a) = a := rfl -end PLift +theorem PLift.downUp {α : Sort u} (a : α) : down (up a) = a := + rfl -/- pointed types -/ +/- Pointed types -/ structure PointedType := -(type : Type u) (val : type) + (type : Type u) + (val : type) + +/-- Universe lifting operation -/ +structure ULift.{r, s} (α : Type s) : Type (max s r) := + up :: (down : α) + +/- Bijection between α and ULift.{v} α -/ +theorem ULift.upDown {α : Type u} : ∀ (b : ULift.{v} α), up (down b) = b + | up a => rfl + +theorem ULift.downUp {α : Type u} (a : α) : down (up.{v} a) = a := + rfl /- Inhabited -/ class Inhabited (α : Sort u) := mk {} :: (default : α) -constant arbitrary (α : Sort u) [Inhabited α] : α := -Inhabited.default α +constant arbitrary (α : Sort u) [s : Inhabited α] : α := + @Inhabited.default α s -instance Prop.Inhabited : Inhabited Prop := -⟨True⟩ +instance : Inhabited Prop := { + default := True +} -instance Fun.Inhabited (α : Sort u) {β : Sort v} [h : Inhabited β] : Inhabited (α → β) := -Inhabited.casesOn h (fun b => ⟨fun a => b⟩) +instance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) := { + default := fun _ => arbitrary β +} -instance Forall.Inhabited (α : Sort u) {β : α → Sort v} [∀ x, Inhabited (β x)] : Inhabited (∀ x, β x) := -⟨fun a => arbitrary (β a)⟩ +instance (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] : Inhabited ((a : α) → β a) := { + default := fun a => arbitrary (β a) +} -instance : Inhabited Bool := ⟨false⟩ +instance : Inhabited Bool := { + default := false +} -instance : Inhabited True := ⟨trivial⟩ +instance : Inhabited True := { + default := trivial +} -instance : Inhabited Nat := ⟨0⟩ +instance : Inhabited Nat := { + default := 0 +} -instance : Inhabited NonScalar := ⟨⟨arbitrary _⟩⟩ +instance : Inhabited NonScalar := { + default := ⟨arbitrary _⟩ +} -instance : Inhabited PNonScalar.{u} := ⟨⟨arbitrary _⟩⟩ +instance : Inhabited PNonScalar.{u} := { + default := ⟨arbitrary _⟩ +} -instance : Inhabited PointedType := ⟨{type := PUnit, val := ⟨⟩}⟩ +instance : Inhabited PointedType := { + default := {type := PUnit, val := ⟨⟩} +} -instance {α} [Inhabited α] : Inhabited (ForInStep α) := ⟨ForInStep.done (arbitrary _)⟩ +instance {α} [Inhabited α] : Inhabited (ForInStep α) := { + default:= ForInStep.done (arbitrary _) +} class inductive Nonempty (α : Sort u) : Prop -| intro (val : α) : Nonempty + | intro (val : α) : Nonempty α protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p := -Nonempty.rec h₂ h₁ + h₂ h₁.1 -instance nonemptyOfInhabited {α : Sort u} [Inhabited α] : Nonempty α := -⟨arbitrary α⟩ +instance {α : Sort u} [Inhabited α] : Nonempty α := { + val := arbitrary α +} theorem nonemptyOfExists {α : Sort u} {p : α → Prop} : Exists (fun x => p x) → Nonempty α -| ⟨w, h⟩ => ⟨w⟩ + | ⟨w, h⟩ => ⟨w⟩ /- Subsingleton -/ class inductive Subsingleton (α : Sort u) : Prop -| intro (h : ∀ (a b : α), a = b) : Subsingleton + | intro (h : (a b : α) → a = b) : Subsingleton α -protected def Subsingleton.elim {α : Sort u} [h : Subsingleton α] : ∀ (a b : α), a = b := -Subsingleton.casesOn h (fun p => p) +protected def Subsingleton.elim {α : Sort u} [h : Subsingleton α] : (a b : α) → a = b := + match h with + | intro h => h -protected def Subsingleton.helim {α β : Sort u} [h : Subsingleton α] (h : α = β) : ∀ (a : α) (b : β), a ≅ b := -Eq.recOn h (fun a b => heqOfEq (Subsingleton.elim a b)) +protected def Subsingleton.helim {α β : Sort u} [h₁ : Subsingleton α] (h₂ : α = β) (a : α) (b : β) : a ≅ b := by + subst h₂ + apply heqOfEq + apply Subsingleton.elim -instance subsingletonProp (p : Prop) : Subsingleton p := -⟨fun a b => proofIrrel a b⟩ +instance (p : Prop) : Subsingleton p := + ⟨fun a b => proofIrrel a b⟩ instance (p : Prop) : Subsingleton (Decidable p) := -Subsingleton.intro $ fun d₁ => - match d₁ with - | (isTrue t₁) => fun d₂ => - match d₂ with - | (isTrue t₂) => Eq.recOn (proofIrrel t₁ t₂) rfl - | (isFalse f₂) => absurd t₁ f₂ - | (isFalse f₁) => fun d₂ => - match d₂ with - | (isTrue t₂) => absurd t₂ f₁ - | (isFalse f₂) => Eq.recOn (proofIrrel f₁ f₂) rfl + Subsingleton.intro fun + | (isTrue t₁) => fun + | (isTrue t₂) => proofIrrel t₁ t₂ ▸ rfl + | (isFalse f₂) => absurd t₁ f₂ + | (isFalse f₁) => fun + | (isTrue t₂) => absurd t₂ f₁ + | (isFalse f₂) => proofIrrel f₁ f₂ ▸ rfl -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 +theorem recSubsingleton + {p : Prop} [h : Decidable p] + {h₁ : p → Sort u} + {h₂ : ¬p → Sort u} + [h₃ : ∀ (h : p), Subsingleton (h₁ h)] + [h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)] + : Subsingleton (Decidable.casesOn (motive := fun _ => Sort u) h h₂ h₁) := + match h with + | (isTrue h) => h₃ h + | (isFalse h) => h₄ h section relation variables {α : Sort u} {β : Sort v} (r : β → β → Prop) -def Reflexive := ∀ x, r x x +def Reflexive := + ∀ x, r x x -def Symmetric := ∀ {x y}, r x y → r y 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 Transitive := + ∀ {x y z}, r x y → r y z → r x z -def Equivalence := Reflexive r ∧ Symmetric r ∧ Transitive r +def Equivalence := -- TODO: use structure? + Reflexive r ∧ Symmetric r ∧ Transitive r -def Total := ∀ x y, r x y ∨ r y x +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⟩ + ⟨rfl, ⟨symm, trans⟩⟩ -def Irreflexive := ∀ x, ¬ r x x +def Irreflexive := + ∀ x, ¬ r x x -def AntiSymmetric := ∀ {x y}, r x y → r y x → x = y +def AntiSymmetric := + ∀ {x y}, r x y → r y x → x = y -def emptyRelation (a₁ a₂ : α) : Prop := False +def emptyRelation (a₁ a₂ : α) : Prop := + False -def Subrelation (q r : β → β → Prop) := ∀ {x y}, q x y → r x y +def Subrelation (q r : β → β → Prop) := + ∀ {x y}, q x y → r x y def InvImage (f : α → β) : α → α → Prop := -fun a₁ a₂ => r (f a₁) (f a₂) + fun a₁ a₂ => r (f a₁) (f a₂) theorem InvImage.Transitive (f : α → β) (h : Transitive r) : Transitive (InvImage r f) := -fun (a₁ a₂ a₃ : α) (h₁ : InvImage r f a₁ a₂) (h₂ : InvImage r f a₂ a₃) => h h₁ h₂ + fun h₁ h₂ => h h₁ h₂ theorem InvImage.Irreflexive (f : α → β) (h : Irreflexive r) : Irreflexive (InvImage r f) := -fun (a : α) (h₁ : InvImage r f a a) => h (f a) h₁ + fun (a : α) (h₁ : InvImage r f a a) => h (f a) h₁ inductive TC {α : Sort u} (r : α → α → Prop) : α → α → Prop -| base : ∀ a b, r a b → TC a b -| trans : ∀ a b c, TC a b → TC b c → TC a c + | base : ∀ a b, r a b → TC r a b + | trans : ∀ a b c, TC r a b → TC r b c → TC r a c @[elabAsEliminator] -theorem TC.ndrec.{u1, u2} {α : Sort u} {r : α → α → Prop} {C : α → α → Prop} +theorem TC.ndrec {α : Sort u} {r : α → α → Prop} {C : α → α → Prop} (m₁ : ∀ (a b : α), r a b → C a b) (m₂ : ∀ (a b c : α), TC r a b → TC r b c → C a b → C b c → C a c) {a b : α} (h : TC r a b) : C a b := -@TC.rec α r (fun a b _ => C a b) m₁ m₂ a b h + @TC.rec α r (fun a b _ => C a b) m₁ m₂ a b h @[elabAsEliminator] -theorem TC.ndrecOn.{u1, u2} {α : Sort u} {r : α → α → Prop} {C : α → α → Prop} +theorem TC.ndrecOn {α : Sort u} {r : α → α → Prop} {C : α → α → Prop} {a b : α} (h : TC r a b) (m₁ : ∀ (a b : α), r a b → C a b) (m₂ : ∀ (a b c : α), TC r a b → TC r b c → C a b → C b c → C a c) : C a b := -@TC.rec α r (fun a b _ => C a b) m₁ m₂ a b h + @TC.rec α r (fun a b _ => C a b) m₁ m₂ a b h end relation @@ -1257,18 +1155,25 @@ 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) +def Commutative := + ∀ a b, f a b = f b a + +def Associative := + ∀ a b c, f (f a b) c = f a (f b c) + +def RightCommutative (h : β → α → β) := + ∀ b a₁ a₂, h (h b a₁) a₂ = h (h b a₂) a₁ + +def LeftCommutative (h : α → β → β) := + ∀ a₁ a₂ b, h a₁ (h a₂ b) = h a₂ (h a₁ b) theorem leftComm : Commutative f → Associative f → LeftCommutative f := -fun hcomm hassoc a b c => -((Eq.symm (hassoc a b c)).trans (hcomm a b ▸ rfl : f (f a b) c = f (f b a) c)).trans (hassoc b a c) + fun hcomm hassoc a b c => + ((Eq.symm (hassoc a b c)).trans (hcomm a b ▸ rfl : f (f a b) c = f (f b a) c)).trans (hassoc b a c) theorem rightComm : Commutative f → Associative f → RightCommutative f := -fun hcomm hassoc a b c => -((hassoc a b c).trans (hcomm b c ▸ rfl : f a (f b c) = f a (f c b))).trans (Eq.symm (hassoc a c b)) + fun hcomm hassoc a b c => + ((hassoc a b c).trans (hcomm b c ▸ rfl : f a (f b c) = f a (f c b))).trans (Eq.symm (hassoc a c b)) end Binary @@ -1276,26 +1181,29 @@ end Binary namespace Subtype def existsOfSubtype {α : Type u} {p : α → Prop} : { x // p x } → Exists (fun x => p x) -| ⟨a, h⟩ => ⟨a, h⟩ + | ⟨a, h⟩ => ⟨a, h⟩ variables {α : Type u} {p : α → Prop} theorem tagIrrelevant {a : α} (h1 h2 : p a) : mk a h1 = mk a h2 := -rfl + rfl protected theorem eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2 -| ⟨x, h1⟩, ⟨.(x), h2⟩, rfl => rfl + | ⟨x, h1⟩, ⟨_, _⟩, rfl => rfl -theorem eta (a : {x // p x}) (h : p (val a)) : mk (val a) h = a := -Subtype.eq rfl +theorem eta (a : {x // p x}) (h : p (val a)) : mk (val a) h = a := by + cases a + exact rfl -instance {α : Type u} {p : α → Prop} {a : α} (h : p a) : Inhabited {x // p x} := -⟨⟨a, h⟩⟩ +instance {α : Type u} {p : α → Prop} {a : α} (h : p a) : Inhabited {x // p x} := { + default := ⟨a, h⟩ +} instance {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} := -fun ⟨a, h₁⟩ ⟨b, h₂⟩ => - if h : a = b then isTrue (Subtype.eq h) - else isFalse (fun h' => Subtype.noConfusion h' (fun h' => absurd h' h)) + fun ⟨a, h₁⟩ ⟨b, h₂⟩ => + if h : a = b then isTrue (by subst h; exact rfl) + else isFalse (fun h' => Subtype.noConfusion h' (fun h' => absurd h' h)) + end Subtype /- Sum -/ @@ -1303,23 +1211,25 @@ end Subtype section variables {α : Type u} {β : Type v} -instance Sum.inhabitedLeft [h : Inhabited α] : Inhabited (Sum α β) := -⟨Sum.inl (arbitrary α)⟩ +instance Sum.inhabitedLeft [h : Inhabited α] : Inhabited (Sum α β) := { + default := Sum.inl (arbitrary α) +} -instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (Sum α β) := -⟨Sum.inr (arbitrary β)⟩ +instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (Sum α β) := { + default := Sum.inr (arbitrary β) +} + +instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (Sum α β) := fun a b => + match a, b with + | (Sum.inl a), (Sum.inl b) => + if h : a = b then isTrue (h ▸ rfl) + else isFalse (fun h' => Sum.noConfusion h' (fun h' => absurd h' h)) + | (Sum.inr a), (Sum.inr b) => + if h : a = b then isTrue (h ▸ rfl) + else isFalse (fun h' => Sum.noConfusion h' (fun h' => absurd h' h)) + | (Sum.inr a), (Sum.inl b) => isFalse (fun h => Sum.noConfusion h) + | (Sum.inl a), (Sum.inr b) => isFalse (fun h => Sum.noConfusion h) -instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (Sum α β) := -fun a b => - match a, b with - | (Sum.inl a), (Sum.inl b) => - if h : a = b then isTrue (h ▸ rfl) - else isFalse (fun h' => Sum.noConfusion h' (fun h' => absurd h' h)) - | (Sum.inr a), (Sum.inr b) => - if h : a = b then isTrue (h ▸ rfl) - else isFalse (fun h' => Sum.noConfusion h' (fun h' => absurd h' h)) - | (Sum.inr a), (Sum.inl b) => isFalse (fun h => Sum.noConfusion h) - | (Sum.inl a), (Sum.inr b) => isFalse (fun h => Sum.noConfusion h) end /- Product -/ @@ -1327,116 +1237,110 @@ end section variables {α : Type u} {β : Type v} -instance [Inhabited α] [Inhabited β] : Inhabited (Prod α β) := -⟨(arbitrary α, arbitrary β)⟩ +instance [Inhabited α] [Inhabited β] : Inhabited (α × β) := { + default := (arbitrary α, arbitrary β) +} instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) := -fun ⟨a, b⟩ ⟨a', b'⟩ => - match (decEq a a') with - | (isTrue e₁) => - match (decEq b b') with - | (isTrue e₂) => isTrue (Eq.recOn e₁ (Eq.recOn e₂ rfl)) - | (isFalse n₂) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₂' n₂)) - | (isFalse n₁) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₁' n₁)) + fun ⟨a, b⟩ ⟨a', b'⟩ => + match (decEq a a') with + | (isTrue e₁) => + match (decEq b b') with + | (isTrue e₂) => isTrue (e₁ ▸ e₂ ▸ rfl) + | (isFalse n₂) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₂' n₂)) + | (isFalse n₁) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₁' n₁)) -instance [HasBeq α] [HasBeq β] : HasBeq (α × β) := -⟨fun ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ => a₁ == a₂ && b₁ == b₂⟩ +instance [HasBeq α] [HasBeq β] : HasBeq (α × β) := { + beq := fun ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ => a₁ == a₂ && b₁ == b₂ +} -instance [HasLess α] [HasLess β] : HasLess (α × β) := -⟨fun s t => s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)⟩ +instance [HasLess α] [HasLess β] : HasLess (α × β) := { + Less := fun 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) := -fun t s => Or.Decidable + [(a b : α) → Decidable (a < b)] [(a b : β) → Decidable (a < b)] + : (s t : α × β) → Decidable (s < t) := + fun t s => inferInstanceAs (Decidable (_ ∨ _)) theorem Prod.ltDef [HasLess α] [HasLess β] (s t : α × β) : (s < t) = (s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)) := -rfl + rfl end def Prod.map.{u₁, u₂, v₁, v₂} {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂} - (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂ -| (a, b) => (f a, g b) + (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 (fun x => p x)) → Exists (fun x => p x) | ⟨x, hx⟩ => ⟨x, hx⟩ -section -variables {α : Type u} {β : α → Type v} - -protected theorem Sigma.eq : ∀ {p₁ p₂ : Sigma (fun 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 +protected theorem PSigma.eta {α : Sort u} {β : α → Sort v} {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} + (h₁ : a₁ = a₂) (h₂ : Eq.rec (motive := fun a _ => β a) b₁ h₁ = b₂) : PSigma.mk a₁ b₁ = PSigma.mk a₂ b₂ := by + subst h₁ + subst h₂ + exact rfl /- Universe polymorphic unit -/ -theorem punitEq (a b : PUnit) : a = b := -PUnit.recOn a (PUnit.recOn b rfl) +theorem punitEq (a b : PUnit) : a = b := by + cases a; cases b; exact rfl theorem punitEqPUnit (a : PUnit) : a = () := -punitEq a () + punitEq a () instance : Subsingleton PUnit := -Subsingleton.intro punitEq + Subsingleton.intro punitEq -instance : Inhabited PUnit := -⟨⟨⟩⟩ +instance : Inhabited PUnit := { + default := ⟨⟩ +} instance : DecidableEq PUnit := -fun a b => isTrue (punitEq a b) + fun a b => isTrue (punitEq a b) /- Setoid -/ class Setoid (α : Sort u) := -(r : α → α → Prop) (iseqv {} : Equivalence r) + (r : α → α → Prop) + (iseqv {} : Equivalence r) -instance setoidHasEquiv {α : Sort u} [Setoid α] : HasEquiv α := -⟨Setoid.r⟩ +instance {α : 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 + (Setoid.iseqv α).1 a theorem symm {a b : α} (hab : a ≈ b) : b ≈ a := -match Setoid.iseqv α with -| ⟨hRefl, hSymm, hTrans⟩ => hSymm hab + (Setoid.iseqv α).2.1 hab theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c := -match Setoid.iseqv α with -| ⟨hRefl, hSymm, hTrans⟩ => hTrans hab hbc + (Setoid.iseqv α).2.2 hab hbc + end Setoid + /- Propositional extensionality -/ axiom propext {a b : Prop} : (a ↔ b) → a = b theorem eqTrueIntro {a : Prop} (h : a) : a = True := -propext (iffTrueIntro h) + propext (iffTrueIntro h) theorem eqFalseIntro {a : Prop} (h : ¬a) : a = False := -propext (iffFalseIntro h) + 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₂ + 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 @@ -1444,21 +1348,21 @@ axiom sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Q 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 + 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 + 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 + 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 + ind h q theorem existsRep {α : Sort u} {r : α → α → Prop} (q : Quot r) : Exists (fun a => (Quot.mk r a) = q) := -Quot.inductionOn q (fun a => ⟨a, rfl⟩) + Quot.inductionOn (β := fun q => Exists (fun a => (Quot.mk r a) = q)) q (fun a => ⟨a, rfl⟩) section variable {α : Sort u} @@ -1467,75 +1371,84 @@ variable {β : Quot r → Sort v} @[reducible, macroInline] protected def indep (f : ∀ a, β (Quot.mk r a)) (a : α) : PSigma β := -⟨Quot.mk r a, f a⟩ + ⟨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 := -fun a b e => PSigma.eq (sound e) (h a b e) +protected theorem indepCoherent + (f : (a : α) → β (Quot.mk r a)) + (h : ∀ (a b : α) (p : r a b), (Eq.rec (motive := fun x _ => β x) (f a) (sound p)) = f b) + : ∀ a b, r a b → Quot.indep f a = Quot.indep f b := + fun a b e => PSigma.eta (sound e) (h a b e) protected theorem liftIndepPr1 - (f : ∀ a, β (Quot.mk r a)) (h : ∀ (a b : α) (p : r a b), (Eq.rec (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 (fun (a : α) => Eq.refl (Quot.indep f a).1) q + (f : ∀ a, β (Quot.mk r a)) + (h : ∀ (a b : α) (p : r a b), (Eq.rec (motive := fun x _ => β x) (f a) (sound p)) = f b) + (q : Quot r) : (lift (Quot.indep f) (Quot.indepCoherent f h) q).1 = q := by + induction q using Quot.ind + exact rfl @[reducible, elabAsEliminator, inline] protected def rec - (f : ∀ a, β (Quot.mk r a)) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β (Quot.mk r b)) = f b) + (f : ∀ a, β (Quot.mk r a)) + (h : ∀ (a b : α) (p : r a b), (Eq.rec (motive := fun x _ => β x) (f a) (sound p)) = f b) (q : Quot r) : β q := -Eq.ndrecOn (Quot.liftIndepPr1 f h q) ((lift (Quot.indep f) (Quot.indepCoherent f h) q).2) + 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 + (q : Quot r) + (f : ∀ a, β (Quot.mk r a)) + (h : ∀ (a b : α) (p : r a b), (Eq.rec (motive := fun x _ => β x) (f a) (sound p)) = f b) + : β q := + Quot.rec f h q @[reducible, elabAsEliminator, inline] protected def recOnSubsingleton - [h : ∀ a, Subsingleton (β (Quot.mk r a))] (q : Quot r) (f : ∀ a, β (Quot.mk r a)) : β q := -Quot.rec f (fun a b h => Subsingleton.elim _ (f b)) q + [h : ∀ a, Subsingleton (β (Quot.mk r a))] (q : Quot r) (f : ∀ a, β (Quot.mk r a)) : β q := by + induction q using Quot.rec + apply f + apply Subsingleton.elim @[reducible, elabAsEliminator, inline] protected def hrecOn - (q : Quot r) (f : ∀ a, β (Quot.mk r a)) (c : ∀ (a b : α) (p : r a b), f a ≅ f b) : β q := -Quot.recOn q f $ - fun a b p => eqOfHEq $ - have p₁ : (Eq.rec (f a) (sound p) : β (Quot.mk r b)) ≅ f a := eqRecHEq (sound p) (f a); - HEq.trans p₁ (c a b p) + (q : Quot r) (f : ∀ a, β (Quot.mk r a)) (c : ∀ (a b : α) (p : r a b), f a ≅ f b) : β q := + Quot.recOn q f $ + fun a b p => eqOfHEq $ + have p₁ : (Eq.rec (motive := fun x _ => β x) (f a) (sound p)) ≅ f a := eqRecHEq (sound p) (f a); + HEq.trans p₁ (c a b p) end end Quot def Quotient {α : Sort u} (s : Setoid α) := -@Quot α Setoid.r + @Quot α Setoid.r namespace Quotient @[inline] protected def mk {α : Sort u} [s : Setoid α] (a : α) : Quotient s := -Quot.mk Setoid.r a + Quot.mk Setoid.r a def sound {α : Sort u} [s : Setoid α] {a b : α} : a ≈ b → Quotient.mk a = Quotient.mk b := -Quot.sound + 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 + Quot.lift f @[elabAsEliminator] protected theorem ind {α : Sort u} [s : Setoid α] {β : Quotient s → Prop} : (∀ a, β (Quotient.mk a)) → ∀ q, β q := -Quot.ind + 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 + Quot.liftOn q f c @[elabAsEliminator] protected theorem inductionOn {α : Sort u} [s : Setoid α] {β : Quotient s → Prop} (q : Quotient s) (h : ∀ a, β (Quotient.mk a)) : β q := -Quot.inductionOn q h + Quot.inductionOn q h theorem existsRep {α : Sort u} [s : Setoid α] (q : Quotient s) : Exists (fun (a : α) => Quotient.mk a = q) := -Quot.existsRep q + Quot.existsRep q section variable {α : Sort u} @@ -1544,24 +1457,31 @@ variable {β : Quotient s → Sort v} @[inline] protected def rec - (f : ∀ a, β (Quotient.mk a)) (h : ∀ (a b : α) (p : a ≈ b), (Eq.rec (f a) (Quotient.sound p) : β (Quotient.mk b)) = f b) - (q : Quotient s) : β q := -Quot.rec f h q + (f : ∀ a, β (Quotient.mk a)) + (h : ∀ (a b : α) (p : a ≈ b), (Eq.rec (motive := fun a _ => β a) (f a) (Quotient.sound p)) = f b) + (q : Quotient s) : β q := + Quot.rec f h q @[reducible, elabAsEliminator, inline] protected def recOn - (q : Quotient s) (f : ∀ a, β (Quotient.mk a)) (h : ∀ (a b : α) (p : a ≈ b), (Eq.rec (f a) (Quotient.sound p) : β (Quotient.mk b)) = f b) : β q := -Quot.recOn q f h + (q : Quotient s) + (f : ∀ a, β (Quotient.mk a)) + (h : ∀ (a b : α) (p : a ≈ b), (Eq.rec (motive := fun a _ => β a) (f a) (Quotient.sound p)) = f b) := + Quot.recOn q f h @[reducible, elabAsEliminator, inline] protected def recOnSubsingleton - [h : ∀ a, Subsingleton (β (Quotient.mk a))] (q : Quotient s) (f : ∀ a, β (Quotient.mk a)) : β q := -@Quot.recOnSubsingleton _ _ _ h q f + [h : ∀ a, Subsingleton (β (Quotient.mk a))] + (q : Quotient s) + (f : ∀ a, β (Quotient.mk a)) : β q := + @Quot.recOnSubsingleton _ _ _ h q f @[reducible, elabAsEliminator, inline] protected def hrecOn - (q : Quotient s) (f : ∀ a, β (Quotient.mk a)) (c : ∀ (a b : α) (p : a ≈ b), f a ≅ f b) : β q := -Quot.hrecOn q f c + (q : Quotient s) + (f : ∀ a, β (Quotient.mk a)) + (c : ∀ (a b : α) (p : a ≈ b), f a ≅ f b) : β q := + Quot.hrecOn q f c end section @@ -1571,61 +1491,74 @@ variables [s₁ : Setoid α] [s₂ : Setoid β] @[reducible, elabAsEliminator, inline] protected def lift₂ - (f : α → β → φ)(c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) - (q₁ : Quotient s₁) (q₂ : Quotient s₂) : φ := -Quotient.lift - (fun (a₁ : α) => Quotient.lift (f a₁) (fun (a b : β) => c a₁ a a₁ b (Setoid.refl a₁)) q₂) - (fun (a b : α) (h : a ≈ b) => - @Quotient.ind β s₂ - (fun (a1 : Quotient s₂) => - (Quotient.lift (f a) (fun (a1 b : β) => c a a1 a b (Setoid.refl a)) a1) - = - (Quotient.lift (f b) (fun (a b1 : β) => c b a b b1 (Setoid.refl b)) a1)) - (fun (a' : β) => c a a' b a' h (Setoid.refl a')) - q₂) - q₁ + (f : α → β → φ)(c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) + (q₁ : Quotient s₁) (q₂ : Quotient s₂) : φ := + Quotient.lift + (fun (a₁ : α) => Quotient.lift (f a₁) (fun (a b : β) => c a₁ a a₁ b (Setoid.refl a₁)) q₂) + (fun (a b : α) (h : a ≈ b) => + @Quotient.ind β s₂ + (fun (a1 : Quotient s₂) => + (Quotient.lift (f a) (fun (a1 b : β) => c a a1 a b (Setoid.refl a)) a1) + = + (Quotient.lift (f b) (fun (a b1 : β) => c b a b b1 (Setoid.refl b)) a1)) + (fun (a' : β) => c a a' b a' h (Setoid.refl a')) + q₂) + q₁ @[reducible, elabAsEliminator, inline] protected def liftOn₂ - (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : α → β → φ) (c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) : φ := -Quotient.lift₂ f c q₁ q₂ + (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : α → β → φ) (c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) : φ := + Quotient.lift₂ f c q₁ q₂ @[elabAsEliminator] -protected theorem ind₂ {φ : Quotient s₁ → Quotient s₂ → Prop} (h : ∀ a b, φ (Quotient.mk a) (Quotient.mk b)) (q₁ : Quotient s₁) (q₂ : Quotient s₂) : φ q₁ q₂ := -Quotient.ind (fun a₁ => Quotient.ind (fun a₂ => h a₁ a₂) q₂) q₁ +protected theorem ind₂ {φ : Quotient s₁ → Quotient s₂ → Prop} (h : ∀ a b, φ (Quotient.mk a) (Quotient.mk b)) (q₁ : Quotient s₁) (q₂ : Quotient s₂) : φ q₁ q₂ := by + induction q₁ using Quotient.ind + induction q₂ using Quotient.ind + apply h + +-- Quotient.ind (fun a₁ => Quotient.ind (fun a₂ => h a₁ a₂) q₂) q₁ @[elabAsEliminator] protected theorem inductionOn₂ - {φ : Quotient s₁ → Quotient s₂ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (h : ∀ a b, φ (Quotient.mk a) (Quotient.mk b)) : φ q₁ q₂ := -Quotient.ind (fun a₁ => Quotient.ind (fun a₂ => h a₁ a₂) q₂) q₁ + {φ : Quotient s₁ → Quotient s₂ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (h : ∀ a b, φ (Quotient.mk a) (Quotient.mk b)) : φ q₁ q₂ := by + induction q₁ using Quotient.ind + induction q₂ using Quotient.ind + apply h @[elabAsEliminator] protected theorem inductionOn₃ - [s₃ : Setoid φ] - {δ : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (q₃ : Quotient s₃) (h : ∀ a b c, δ (Quotient.mk a) (Quotient.mk b) (Quotient.mk c)) - : δ q₁ q₂ q₃ := -Quotient.ind (fun a₁ => Quotient.ind (fun a₂ => Quotient.ind (fun a₃ => h a₁ a₂ a₃) q₃) q₂) q₁ + [s₃ : Setoid φ] + {δ : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (q₃ : Quotient s₃) + (h : ∀ a b c, δ (Quotient.mk a) (Quotient.mk b) (Quotient.mk c)) + : δ q₁ q₂ q₃ := by + induction q₁ using Quotient.ind + induction q₂ using Quotient.ind + induction q₃ using Quotient.ind + apply h + end section Exact + variable {α : Sort u} private def rel [s : Setoid α] (q₁ q₂ : Quotient s) : Prop := -Quotient.liftOn₂ q₁ q₂ - (fun a₁ a₂ => a₁ ≈ a₂) - (fun a₁ a₂ b₁ b₂ a₁b₁ a₂b₂ => - propext (Iff.intro - (fun a₁a₂ => Setoid.trans (Setoid.symm a₁b₁) (Setoid.trans a₁a₂ a₂b₂)) - (fun b₁b₂ => Setoid.trans a₁b₁ (Setoid.trans b₁b₂ (Setoid.symm a₂b₂))))) + Quotient.liftOn₂ q₁ q₂ + (fun a₁ a₂ => a₁ ≈ a₂) + (fun a₁ a₂ b₁ b₂ a₁b₁ a₂b₂ => + propext (Iff.intro + (fun a₁a₂ => Setoid.trans (Setoid.symm a₁b₁) (Setoid.trans a₁a₂ a₂b₂)) + (fun b₁b₂ => Setoid.trans a₁b₁ (Setoid.trans b₁b₂ (Setoid.symm a₂b₂))))) -private theorem rel.refl [s : Setoid α] : ∀ (q : Quotient s), rel q q := -fun q => Quot.inductionOn q (fun a => Setoid.refl a) +private theorem rel.refl [s : Setoid α] (q : Quotient s) : rel q q := + Quot.inductionOn (β := fun q => rel q q) q (fun a => Setoid.refl a) private theorem eqImpRel [s : Setoid α] {q₁ q₂ : Quotient s} : q₁ = q₂ → rel q₁ q₂ := -fun h => Eq.ndrecOn h (rel.refl q₁) + fun h => Eq.ndrecOn h (rel.refl q₁) theorem exact [s : Setoid α] {a b : α} : Quotient.mk a = Quotient.mk b → a ≈ b := -fun h => eqImpRel h + fun h => eqImpRel h + end Exact section @@ -1635,10 +1568,17 @@ variables [s₁ : Setoid α] [s₂ : Setoid β] @[reducible, elabAsEliminator] protected def recOnSubsingleton₂ - {φ : Quotient s₁ → Quotient s₂ → Sort uC} [h : ∀ a b, Subsingleton (φ (Quotient.mk a) (Quotient.mk b))] - (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : ∀ a b, φ (Quotient.mk a) (Quotient.mk b)) : φ q₁ q₂:= -@Quotient.recOnSubsingleton _ s₁ (fun q => φ q q₂) (fun a => Quotient.ind (fun b => h a b) q₂) q₁ - (fun a => Quotient.recOnSubsingleton q₂ (fun b => f a b)) + {φ : Quotient s₁ → Quotient s₂ → Sort uC} + [s : ∀ a b, Subsingleton (φ (Quotient.mk a) (Quotient.mk b))] + (q₁ : Quotient s₁) + (q₂ : Quotient s₂) + (g : ∀ a b, φ (Quotient.mk a) (Quotient.mk b)) : φ q₁ q₂ := by + induction q₁ using Quot.recOnSubsingleton + induction q₂ using Quot.recOnSubsingleton + intro a; apply s + induction q₂ using Quot.recOnSubsingleton + intro a; apply s + apply g end end Quotient @@ -1647,37 +1587,13 @@ 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)) (fun 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 - (fun x y h => Quot.sound h) - (fun x => rfl) - (fun x y _ IH => Eq.symm IH) - (fun x y z _ _ IH₁ IH₂ => Eq.trans IH₁ IH₂) -end - instance {α : Sort u} {s : Setoid α} [d : ∀ (a b : α), Decidable (a ≈ b)] : DecidableEq (Quotient s) := -fun (q₁ q₂ : Quotient s) => - Quotient.recOnSubsingleton₂ q₁ q₂ - (fun a₁ a₂ => - match (d a₁ a₂) with - | (isTrue h₁) => isTrue (Quotient.sound h₁) - | (isFalse h₂) => isFalse (fun h => absurd (Quotient.exact h) h₂)) + fun (q₁ q₂ : Quotient s) => + Quotient.recOnSubsingleton₂ (φ := fun a b => Decidable (a = b)) q₁ q₂ + (fun a₁ a₂ => + match (d a₁ a₂) with + | (isTrue h₁) => isTrue (Quotient.sound h₁) + | (isFalse h₂) => isFalse (fun h => absurd (Quotient.exact h) h₂)) /- Function extensionality -/ @@ -1687,16 +1603,16 @@ variables {α : Sort u} {β : α → Sort v} def Equiv (f₁ f₂ : ∀ (x : α), β x) : Prop := ∀ x, f₁ x = f₂ x protected theorem Equiv.refl (f : ∀ (x : α), β x) : Equiv f f := -fun x => rfl + fun x => rfl protected theorem Equiv.symm {f₁ f₂ : ∀ (x : α), β x} : Equiv f₁ f₂ → Equiv f₂ f₁ := -fun h x => Eq.symm (h x) + fun h x => Eq.symm (h x) protected theorem Equiv.trans {f₁ f₂ f₃ : ∀ (x : α), β x} : Equiv f₁ f₂ → Equiv f₂ f₃ → Equiv f₁ f₃ := -fun h₁ h₂ x => Eq.trans (h₁ x) (h₂ x) + fun h₁ h₂ x => Eq.trans (h₁ x) (h₂ x) protected theorem Equiv.isEquivalence (α : Sort u) (β : α → Sort v) : Equivalence (@Function.Equiv α β) := -mkEquivalence (@Function.Equiv α β) (@Equiv.refl α β) (@Equiv.symm α β) (@Equiv.trans α β) + mkEquivalence (@Function.Equiv α β) (@Equiv.refl α β) (@Equiv.symm α β) (@Equiv.trans α β) end Function section @@ -1705,21 +1621,23 @@ variables {α : Sort u} {β : α → Sort v} @[instance] private def funSetoid (α : Sort u) (β : α → Sort v) : Setoid (∀ (x : α), β x) := -Setoid.mk (@Function.Equiv α β) (Function.Equiv.isEquivalence α β) + Setoid.mk (@Function.Equiv α β) (Function.Equiv.isEquivalence α β) -private def extfunApp (f : Quotient $ funSetoid α β) : ∀ (x : α), β x := -fun x => -Quot.liftOn f - (fun (f : ∀ (x : α), β x) => f x) - (fun f₁ f₂ h => h x) +private def extfunApp (f : Quotient $ funSetoid α β) (x : α) : β x := + Quot.liftOn f + (fun (f : ∀ (x : α), β x) => f x) + (fun f₁ f₂ h => h x) + +theorem funext {f₁ f₂ : ∀ (x : α), β x} (h : ∀ x, f₁ x = f₂ x) : f₁ = f₂ := by + show extfunApp (Quotient.mk f₁) = extfunApp (Quotient.mk f₂) + apply congrArg + apply Quotient.sound + exact h -theorem funext {f₁ f₂ : ∀ (x : α), β x} (h : ∀ x, f₁ x = f₂ x) : f₁ = f₂ := -show extfunApp (Quotient.mk f₁) = extfunApp (Quotient.mk f₂) from -congrArg extfunApp (sound h) end -instance Forall.Subsingleton {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] : Subsingleton (∀ a, β a) := -⟨fun f₁ f₂ => funext (fun a => Subsingleton.elim (f₁ a) (f₂ a))⟩ +instance {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] : Subsingleton (∀ a, β a) := + ⟨fun f₁ f₂ => funext (fun a => Subsingleton.elim (f₁ a) (f₂ a))⟩ /- General operations on functions -/ namespace Function @@ -1727,22 +1645,19 @@ universes u₁ u₂ u₃ u₄ variables {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} {ζ : Sort u₁} @[inline, reducible] def comp (f : β → φ) (g : α → β) : α → φ := -fun x => f (g x) - -infixr ` ∘ ` := Function.comp + fun x => f (g x) @[inline, reducible] def onFun (f : β → β → φ) (g : α → β) : α → α → φ := -fun x y => f (g x) (g y) + fun x y => f (g x) (g y) -@[inline, reducible] def combine (f : α → β → φ) (op : φ → δ → ζ) (g : α → β → δ) - : α → β → ζ := -fun x y => op (f x y) (g x y) +@[inline, reducible] def combine (f : α → β → φ) (op : φ → δ → ζ) (g : α → β → δ) : α → β → ζ := + fun x y => op (f x y) (g x y) @[inline, reducible] def const (β : Sort u₂) (a : α) : β → α := -fun x => a + fun x => a @[inline, reducible] def swap {φ : α → β → Sort u₃} (f : ∀ x y, φ x y) : ∀ y x, φ x y := -fun y x => f x y + fun y x => f x y end Function @@ -1752,14 +1667,18 @@ def Squash (α : Type u) := Quot (fun (a b : α) => True) def Squash.mk {α : Type u} (x : α) : Squash α := Quot.mk _ x -theorem Squash.ind {α : Type u} {β : Squash α → Prop} (h : ∀ (a : α), β (Squash.mk a)) : ∀ (q : Squash α), β q := -Quot.ind h +theorem Squash.ind {α : Type u} {motive : Squash α → Prop} (h : ∀ (a : α), motive (Squash.mk a)) : ∀ (q : Squash α), motive q := + Quot.ind h @[inline] def Squash.lift {α β} [Subsingleton β] (s : Squash α) (f : α → β) : β := -Quot.lift f (fun a b _ => Subsingleton.elim _ _) s + Quot.lift f (fun a b _ => Subsingleton.elim _ _) s -instance Squash.Subsingleton {α} : Subsingleton (Squash α) := -⟨Squash.ind (fun (a : α) => Squash.ind (fun (b : α) => Quot.sound trivial))⟩ +instance {α} : Subsingleton (Squash α) := ⟨fun a b => + Squash.ind (motive := fun a => a = b) + (fun a => Squash.ind (motive := fun b => Squash.mk a = b) + (fun b => show Quot.mk _ a = Quot.mk _ b by apply Quot.sound; exact trivial) + b) + a⟩ namespace Lean /- Kernel reduction hints -/ @@ -1804,125 +1723,118 @@ namespace Classical axiom choice {α : Sort u} : Nonempty α → α -noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop) - (h : Exists (fun x => p x)) : {x // p x} := -choice $ let ⟨x, px⟩ := h; ⟨⟨x, px⟩⟩ +noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop) (h : Exists (fun x => p x)) : {x // p x} := + choice $ let ⟨x, px⟩ := h; ⟨⟨x, px⟩⟩ noncomputable def choose {α : Sort u} {p : α → Prop} (h : Exists (fun x => p x)) : α := -(indefiniteDescription p h).val + (indefiniteDescription p h).val theorem chooseSpec {α : Sort u} {p : α → Prop} (h : Exists (fun x => p x)) : p (choose h) := -(indefiniteDescription p h).property + (indefiniteDescription p h).property /- Diaconescu's theorem: excluded middle from choice, Function extensionality and propositional extensionality. -/ theorem em (p : Prop) : p ∨ ¬p := -let U (x : Prop) : Prop := x = True ∨ p; -let V (x : Prop) : Prop := x = False ∨ p; -have exU : Exists (fun x => U x) from ⟨True, Or.inl rfl⟩; -have exV : Exists (fun x => V x) from ⟨False, Or.inl rfl⟩; -let u : Prop := choose exU; -let v : Prop := choose exV; -have uDef : U u from chooseSpec exU; -have vDef : V v from chooseSpec exV; -have notUvOrP : u ≠ v ∨ p from - Or.elim uDef - (fun hut => - Or.elim vDef - (fun hvf => - have hne : u ≠ v from hvf.symm ▸ hut.symm ▸ trueNeFalse; - Or.inl hne) - Or.inr) - Or.inr; -have pImpliesUv : p → u = v from - fun hp => - have hpred : U = V from - funext $ fun x => - have hl : (x = True ∨ p) → (x = False ∨ p) from - fun a => Or.inr hp; - have hr : (x = False ∨ p) → (x = True ∨ p) from - fun a => Or.inr hp; - show (x = True ∨ p) = (x = False ∨ p) from - propext (Iff.intro hl hr); - have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV from - hpred ▸ fun exU exV => rfl; - show u = v from h₀ _ _; -Or.elim notUvOrP - (fun (hne : u ≠ v) => Or.inr (mt pImpliesUv hne)) - Or.inl + let U (x : Prop) : Prop := x = True ∨ p; + let V (x : Prop) : Prop := x = False ∨ p; + have exU : Exists (fun x => U x) from ⟨True, Or.inl rfl⟩; + have exV : Exists (fun x => V x) from ⟨False, Or.inl rfl⟩; + let u : Prop := choose exU; + let v : Prop := choose exV; + have uDef : U u from chooseSpec exU; + have vDef : V v from chooseSpec exV; + have notUvOrP : u ≠ v ∨ p from + Or.elim uDef + (fun hut => + Or.elim vDef + (fun hvf => + have hne : u ≠ v from hvf.symm ▸ hut.symm ▸ trueNeFalse; + Or.inl hne) + Or.inr) + Or.inr; + have pImpliesUv : p → u = v from + fun hp => + have hpred : U = V from + funext $ fun x => + have hl : (x = True ∨ p) → (x = False ∨ p) from + fun a => Or.inr hp; + have hr : (x = False ∨ p) → (x = True ∨ p) from + fun a => Or.inr hp; + show (x = True ∨ p) = (x = False ∨ p) from + propext (Iff.intro hl hr); + have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV from + hpred ▸ fun exU exV => rfl; + show u = v from h₀ _ _; + Or.elim notUvOrP + (fun (hne : u ≠ v) => Or.inr (mt pImpliesUv hne)) + Or.inl theorem existsTrueOfNonempty {α : Sort u} : Nonempty α → Exists (fun (x : α) => True) -| ⟨x⟩ => ⟨x, trivial⟩ + | ⟨x⟩ => ⟨x, trivial⟩ noncomputable def inhabitedOfNonempty {α : Sort u} (h : Nonempty α) : Inhabited α := -⟨choice h⟩ + ⟨choice h⟩ -noncomputable def inhabitedOfExists {α : Sort u} {p : α → Prop} (h : Exists (fun x => p x)) : - Inhabited α := -inhabitedOfNonempty (Exists.elim h (fun w hw => ⟨w⟩)) +noncomputable def inhabitedOfExists {α : Sort u} {p : α → Prop} (h : Exists (fun x => p x)) : Inhabited α := + inhabitedOfNonempty (Exists.elim h (fun w hw => ⟨w⟩)) /- all propositions are Decidable -/ noncomputable def propDecidable (a : Prop) : Decidable a := -choice $ Or.elim (em a) - (fun ha => ⟨isTrue ha⟩) - (fun hna => ⟨isFalse hna⟩) + choice $ Or.elim (em a) + (fun ha => ⟨isTrue ha⟩) + (fun hna => ⟨isFalse hna⟩) noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) := -⟨propDecidable a⟩ + ⟨propDecidable a⟩ noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α := -fun x y => propDecidable (x = y) + fun x y => propDecidable (x = y) noncomputable def typeDecidable (α : Sort u) : PSum α (α → False) := -match (propDecidable (Nonempty α)) with -| (isTrue hp) => PSum.inl (@arbitrary _ (inhabitedOfNonempty hp)) -| (isFalse hn) => PSum.inr (fun a => absurd (Nonempty.intro a) hn) + match (propDecidable (Nonempty α)) with + | (isTrue hp) => PSum.inl (@arbitrary _ (inhabitedOfNonempty hp)) + | (isFalse hn) => PSum.inr (fun a => absurd (Nonempty.intro a) hn) -noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop) - (h : Nonempty α) : {x : α // Exists (fun (y : α) => p y) → p x} := -@dite _ (Exists (fun (x : α) => p x)) (propDecidable _) - (fun (hp : Exists (fun (x : α) => p x)) => - show {x : α // Exists (fun (y : α) => p y) → p x} from - let xp := indefiniteDescription _ hp; - ⟨xp.val, fun h' => xp.property⟩) - (fun hp => ⟨choice h, fun h => absurd h hp⟩) +noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop) (h : Nonempty α) : {x : α // Exists (fun (y : α) => p y) → p x} := + @dite _ (Exists (fun (x : α) => p x)) (propDecidable _) + (fun (hp : Exists (fun (x : α) => p x)) => + show {x : α // Exists (fun (y : α) => p y) → p x} from + let xp := indefiniteDescription _ hp; + ⟨xp.val, fun h' => xp.property⟩) + (fun hp => ⟨choice h, fun h => absurd h hp⟩) /- the Hilbert epsilon Function -/ noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α := -(strongIndefiniteDescription p h).val + (strongIndefiniteDescription p h).val -theorem epsilonSpecAux {α : Sort u} (h : Nonempty α) (p : α → Prop) - : Exists (fun y => p y) → p (@epsilon α h p) := -(strongIndefiniteDescription p h).property +theorem epsilonSpecAux {α : Sort u} (h : Nonempty α) (p : α → Prop) : Exists (fun y => p y) → p (@epsilon α h p) := + (strongIndefiniteDescription p h).property -theorem epsilonSpec {α : Sort u} {p : α → Prop} (hex : Exists (fun y => p y)) : - p (@epsilon α (nonemptyOfExists hex) p) := -epsilonSpecAux (nonemptyOfExists hex) p hex +theorem epsilonSpec {α : Sort u} {p : α → Prop} (hex : Exists (fun y => p y)) : p (@epsilon α (nonemptyOfExists hex) p) := + epsilonSpecAux (nonemptyOfExists hex) p hex theorem epsilonSingleton {α : Sort u} (x : α) : @epsilon α ⟨x⟩ (fun y => y = x) = x := -@epsilonSpec α (fun y => y = x) ⟨x, rfl⟩ + @epsilonSpec α (fun y => y = x) ⟨x, rfl⟩ /- the axiom of choice -/ -theorem axiomOfChoice {α : Sort u} {β : α → Sort v} {r : ∀ x, β x → Prop} (h : ∀ x, Exists (fun y => r x y)) : - Exists (fun (f : ∀ x, β x) => ∀ x, r x (f x)) := -⟨_, fun x => chooseSpec (h x)⟩ +theorem axiomOfChoice {α : Sort u} {β : α → Sort v} {r : ∀ x, β x → Prop} (h : ∀ x, Exists (fun y => r x y)) : Exists (fun (f : ∀ x, β x) => ∀ x, r x (f x)) := + ⟨_, fun x => chooseSpec (h x)⟩ -theorem skolem {α : Sort u} {b : α → Sort v} {p : ∀ x, b x → Prop} : - (∀ x, Exists (fun y => p x y)) ↔ Exists (fun (f : ∀ x, b x) => ∀ x, p x (f x)) := -⟨axiomOfChoice, fun ⟨f, hw⟩ (x) => ⟨f x, hw x⟩⟩ +theorem skolem {α : Sort u} {b : α → Sort v} {p : ∀ x, b x → Prop} : (∀ x, Exists (fun y => p x y)) ↔ Exists (fun (f : ∀ x, b x) => ∀ x, p x (f x)) := + ⟨axiomOfChoice, fun ⟨f, hw⟩ (x) => ⟨f x, hw x⟩⟩ theorem propComplete (a : Prop) : a = True ∨ a = False := -Or.elim (em a) - (fun t => Or.inl (eqTrueIntro t)) - (fun f => Or.inr (eqFalseIntro f)) + Or.elim (em a) + (fun t => Or.inl (eqTrueIntro t)) + (fun f => Or.inr (eqFalseIntro f)) -- this supercedes byCases in Decidable theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q := -@Decidable.byCases _ _ (propDecidable _) hpq hnpq + @Decidable.byCases _ _ (propDecidable _) hpq hnpq -- this supercedes byContradiction in Decidable theorem byContradiction {p : Prop} (h : ¬p → False) : p := -@Decidable.byContradiction _ (propDecidable _) h + @Decidable.byContradiction _ (propDecidable _) h end Classical diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean index 1f97c55c80..32d18ef54c 100644 --- a/src/Init/Data/Fin/Basic.lean +++ b/src/Init/Data/Fin/Basic.lean @@ -81,8 +81,6 @@ def land : Fin n → Fin n → Fin n def lor : Fin n → Fin n → Fin n | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.lor a b) % n, mlt h⟩ -instance : HasZero (Fin (succ n)) := ⟨⟨0, succPos n⟩⟩ -instance : HasOne (Fin (succ n)) := ⟨ofNat 1⟩ instance : HasAdd (Fin n) := ⟨Fin.add⟩ instance : HasSub (Fin n) := ⟨Fin.sub⟩ instance : HasMul (Fin n) := ⟨Fin.mul⟩ diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean index 9c3f611a9c..789c113f39 100644 --- a/src/Init/Data/Float.lean +++ b/src/Init/Data/Float.lean @@ -45,8 +45,6 @@ def Float.lt : Float → Float → Prop := fun a b => def Float.le : Float → Float → Prop := fun a b => floatSpec.le a.val b.val -instance : HasZero Float := ⟨Float.ofNat 0⟩ -instance : HasOne Float := ⟨Float.ofNat 1⟩ instance : HasOfNat Float := ⟨Float.ofNat⟩ instance : HasAdd Float := ⟨Float.add⟩ instance : HasSub Float := ⟨Float.sub⟩ diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean index 3355267e7e..a885bb8085 100644 --- a/src/Init/Data/Int/Basic.lean +++ b/src/Init/Data/Int/Basic.lean @@ -25,11 +25,6 @@ attribute [extern "lean_int_neg_succ_of_nat"] Int.negSucc instance : Coe Nat Int := ⟨Int.ofNat⟩ namespace Int -protected def zero : Int := ofNat 0 -protected def one : Int := ofNat 1 - -instance : HasZero Int := ⟨Int.zero⟩ -instance : HasOne Int := ⟨Int.one⟩ instance : Inhabited Int := ⟨ofNat 0⟩ def negOfNat : Nat → Int diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 48041f3c14..aefc696ae9 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -330,7 +330,7 @@ instance hasDecidableLt [HasLess α] [h : DecidableRel (α:=α) (·<·)] : (l₁ instance [HasLess α] : HasLessEq (List α) := ⟨List.LessEq⟩ instance [HasLess α] [h : DecidableRel (HasLess.Less : α → α → Prop)] : (l₁ l₂ : List α) → Decidable (l₁ ≤ l₂) := - fun a b => Not.Decidable + fun a b => inferInstanceAs (Decidable (Not _)) /-- `isPrefixOf l₁ l₂` returns `true` Iff `l₁` is a prefix of `l₂`. -/ def isPrefixOf [HasBeq α] : List α → List α → Bool diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index 4e7ba73e53..3f08994f37 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -518,141 +518,6 @@ protected theorem zeroNeOne : 0 ≠ (1 : Nat) := theorem succNeZero (n : Nat) : succ n ≠ 0 := fun h => Nat.noConfusion h -protected theorem bit0SuccEq (n : Nat) : bit0 (succ n) = succ (succ (bit0 n)) := - show succ (succ n + n) = succ (succ (n + n)) from - congrArg succ (succAdd n n) - -protected theorem zeroLtBit0 : ∀ {n : Nat}, n ≠ 0 → 0 < bit0 n - | 0, h => absurd rfl h - | succ n, h => - have h₁ : 0 < succ (succ (bit0 n)) from zeroLtSucc _ - have h₂ : succ (succ (bit0 n)) = bit0 (succ n) from (Nat.bit0SuccEq n).symm - transRelLeft (fun a b => a < b) h₁ h₂ - -protected theorem zeroLtBit1 (n : Nat) : 0 < bit1 n := - zeroLtSucc _ - -protected theorem bit0NeZero : ∀ {n : Nat}, n ≠ 0 → bit0 n ≠ 0 - | 0, h => absurd rfl h - | n+1, _ => fun h => Nat.noConfusion h - -protected theorem bit1NeZero (n : Nat) : bit1 n ≠ 0 := - show succ (n + n) ≠ 0 from - fun h => Nat.noConfusion h - -protected theorem bit1EqSuccBit0 (n : Nat) : bit1 n = succ (bit0 n) := - rfl - -protected theorem bit1SuccEq (n : Nat) : bit1 (succ n) = succ (succ (bit1 n)) := - Eq.trans (Nat.bit1EqSuccBit0 (succ n)) (congrArg succ (Nat.bit0SuccEq n)) - -protected theorem bit1NeOne : ∀ {n : Nat}, n ≠ 0 → bit1 n ≠ 1 - | 0, h, h1 => absurd rfl h - | n+1, h, h1 => Nat.noConfusion h1 (fun h2 => absurd h2 (succNeZero _)) - -protected theorem bit0NeOne : ∀ (n : Nat), bit0 n ≠ 1 - | 0, h => absurd h (Ne.symm Nat.oneNeZero) - | n+1, h => - have h1 : succ (succ (n + n)) = 1 from succAdd n n ▸ h - Nat.noConfusion h1 - (fun h2 => absurd h2 (succNeZero (n + n))) - -protected theorem addSelfNeOne : ∀ (n : Nat), n + n ≠ 1 - | 0, h => Nat.noConfusion h - | n+1, h => - have h1 : succ (succ (n + n)) = 1 from succAdd n n ▸ h - Nat.noConfusion h1 (fun h2 => absurd h2 (Nat.succNeZero (n + n))) - -protected theorem bit1NeBit0 : ∀ (n m : Nat), bit1 n ≠ bit0 m - | 0, m, h => absurd h (Ne.symm (Nat.addSelfNeOne m)) - | n+1, 0, h => - have h1 : succ (bit0 (succ n)) = 0 from h - absurd h1 (Nat.succNeZero _) - | n+1, m+1, h => - have h1 : succ (succ (bit1 n)) = succ (succ (bit0 m)) from - Nat.bit0SuccEq m ▸ Nat.bit1SuccEq n ▸ h - have h2 : bit1 n = bit0 m from - Nat.noConfusion h1 (fun h2' => Nat.noConfusion h2' (fun h2'' => h2'')) - absurd h2 (Nat.bit1NeBit0 n m) - -protected theorem bit0NeBit1 : ∀ (n m : Nat), bit0 n ≠ bit1 m := - fun n m => Ne.symm (Nat.bit1NeBit0 m n) - -protected theorem bit0Inj : ∀ {n m : Nat}, bit0 n = bit0 m → n = m - | 0, 0, h => rfl - | 0, m+1, h => absurd h.symm (succNeZero _) - | n+1, 0, h => absurd h (succNeZero _) - | n+1, m+1, h => - have (n+1) + n = (m+1) + m from Nat.noConfusion h id - have n + (n+1) = m + (m+1) from Nat.addComm (m+1) m ▸ Nat.addComm (n+1) n ▸ this - have succ (n + n) = succ (m + m) from this - have n + n = m + m from Nat.noConfusion this id - have n = m from Nat.bit0Inj this - congrArg (fun a => a + 1) this - -protected theorem bit1Inj {n m : Nat} : bit1 n = bit1 m → n = m := - fun h => - have succ (bit0 n) = succ (bit0 m) from Nat.bit1EqSuccBit0 n ▸ Nat.bit1EqSuccBit0 m ▸ h - have bit0 n = bit0 m from Nat.noConfusion this id - Nat.bit0Inj this - -protected theorem bit0Ne {n m : Nat} : n ≠ m → bit0 n ≠ bit0 m := - fun h₁ h₂ => absurd (Nat.bit0Inj h₂) h₁ - -protected theorem bit1Ne {n m : Nat} : n ≠ m → bit1 n ≠ bit1 m := - fun h₁ h₂ => absurd (Nat.bit1Inj h₂) h₁ - -protected theorem zeroNeBit0 {n : Nat} : n ≠ 0 → 0 ≠ bit0 n := - fun h => Ne.symm (Nat.bit0NeZero h) - -protected theorem zeroNeBit1 (n : Nat) : 0 ≠ bit1 n := - Ne.symm (Nat.bit1NeZero n) - -protected theorem oneNeBit0 (n : Nat) : 1 ≠ bit0 n := - Ne.symm (Nat.bit0NeOne n) - -protected theorem oneNeBit1 {n : Nat} : n ≠ 0 → 1 ≠ bit1 n := - fun h => Ne.symm (Nat.bit1NeOne h) - -protected theorem oneLtBit1 : ∀ {n : Nat}, n ≠ 0 → 1 < bit1 n -| 0, h => absurd rfl h -| succ n, h => - have succ 0 < succ (succ (bit1 n)) from succLtSucc (zeroLtSucc _) - (Nat.bit1SuccEq n).symm ▸ this - -protected theorem oneLtBit0 : ∀ {n : Nat}, n ≠ 0 → 1 < bit0 n -| 0, h => absurd rfl h -| succ n, h => - have succ 0 < succ (succ (bit0 n)) from succLtSucc (zeroLtSucc _) - (Nat.bit0SuccEq n).symm ▸ this - -protected theorem bit0Lt {n m : Nat} (h : n < m) : bit0 n < bit0 m := - Nat.addLtAdd h h - -protected theorem bit1Lt {n m : Nat} (h : n < m) : bit1 n < bit1 m := - succLtSucc (Nat.addLtAdd h h) - -protected theorem bit0LtBit1 {n m : Nat} (h : n ≤ m) : bit0 n < bit1 m := - ltSuccOfLe (Nat.addLeAdd h h) - -protected theorem bit1LtBit0 : ∀ {n m : Nat}, n < m → bit1 n < bit0 m - | n, 0, h => absurd h (notLtZero _) - | n, succ m, h => - have n ≤ m from leOfLtSucc h - have succ (n + n) ≤ succ (m + m) from succLeSucc (addLeAdd this this) - have succ (n + n) ≤ succ m + m from (succAdd m m).symm ▸ this - show succ (n + n) < succ (succ m + m) from ltSuccOfLe this - -protected theorem oneLeBit1 (n : Nat) : 1 ≤ bit1 n := - show 1 ≤ succ (bit0 n) from - succLeSucc (zeroLe (bit0 n)) - -protected theorem oneLeBit0 : ∀ (n : Nat), n ≠ 0 → 1 ≤ bit0 n - | 0, h => absurd rfl h - | n+1, h => - have 1 ≤ succ (succ (bit0 n)) from succLeSucc (zeroLe (succ (bit0 n))) - Eq.symm (Nat.bit0SuccEq n) ▸ this - /- mul + order -/ theorem mulLeMulLeft {n m : Nat} (k : Nat) (h : n ≤ m) : k * n ≤ k * m := diff --git a/src/Init/Data/Nat/Bitwise.lean b/src/Init/Data/Nat/Bitwise.lean index bd4613d58d..620d947397 100644 --- a/src/Init/Data/Nat/Bitwise.lean +++ b/src/Init/Data/Nat/Bitwise.lean @@ -23,9 +23,9 @@ partial def bitwise (f : Bool → Bool → Bool) (n m : Nat) : Nat := let b₂ := m % 2 = 1 let r := bitwise f n' m' if f b₁ b₂ then - bit1 r + r+r+1 else - bit0 r + r+r @[extern "lean_nat_land"] def land : Nat → Nat → Nat := bitwise and diff --git a/src/Init/Data/UInt.lean b/src/Init/Data/UInt.lean index 964b714485..6be512e5fc 100644 --- a/src/Init/Data/UInt.lean +++ b/src/Init/Data/UInt.lean @@ -38,8 +38,6 @@ def UInt8.lor (a b : UInt8) : UInt8 := ⟨Fin.lor a.val b.val⟩ def UInt8.lt (a b : UInt8) : Prop := a.val < b.val def UInt8.le (a b : UInt8) : Prop := a.val ≤ b.val -instance : HasZero UInt8 := ⟨UInt8.ofNat 0⟩ -instance : HasOne UInt8 := ⟨UInt8.ofNat 1⟩ instance : HasOfNat UInt8 := ⟨UInt8.ofNat⟩ instance : HasAdd UInt8 := ⟨UInt8.add⟩ instance : HasSub UInt8 := ⟨UInt8.sub⟩ @@ -101,8 +99,7 @@ def UInt16.lor (a b : UInt16) : UInt16 := ⟨Fin.lor a.val b.val⟩ def UInt16.lt (a b : UInt16) : Prop := a.val < b.val def UInt16.le (a b : UInt16) : Prop := a.val ≤ b.val -instance : HasZero UInt16 := ⟨UInt16.ofNat 0⟩ -instance : HasOne UInt16 := ⟨UInt16.ofNat 1⟩ + instance : HasOfNat UInt16 := ⟨UInt16.ofNat⟩ instance : HasAdd UInt16 := ⟨UInt16.add⟩ instance : HasSub UInt16 := ⟨UInt16.sub⟩ @@ -172,8 +169,6 @@ def UInt32.toUInt16 (a : UInt32) : UInt16 := a.toNat.toUInt16 @[extern c inline "((uint32_t)#1)"] def UInt8.toUInt32 (a : UInt8) : UInt32 := a.toNat.toUInt32 -instance : HasZero UInt32 := ⟨UInt32.ofNat 0⟩ -instance : HasOne UInt32 := ⟨UInt32.ofNat 1⟩ instance : HasOfNat UInt32 := ⟨UInt32.ofNat⟩ instance : HasAdd UInt32 := ⟨UInt32.add⟩ instance : HasSub UInt32 := ⟨UInt32.sub⟩ @@ -254,8 +249,6 @@ constant UInt64.shiftLeft (a b : UInt64) : UInt64 := (arbitrary Nat).toUInt64 @[extern c inline "#1 >> #2"] constant UInt64.shiftRight (a b : UInt64) : UInt64 := (arbitrary Nat).toUInt64 -instance : HasZero UInt64 := ⟨UInt64.ofNat 0⟩ -instance : HasOne UInt64 := ⟨UInt64.ofNat 1⟩ instance : HasOfNat UInt64 := ⟨UInt64.ofNat⟩ instance : HasAdd UInt64 := ⟨UInt64.add⟩ instance : HasSub UInt64 := ⟨UInt64.sub⟩ @@ -335,8 +328,6 @@ constant USize.shiftRight (a b : USize) : USize := (arbitrary Nat).toUSize def USize.lt (a b : USize) : Prop := a.val < b.val def USize.le (a b : USize) : Prop := a.val ≤ b.val -instance : HasZero USize := ⟨USize.ofNat 0⟩ -instance : HasOne USize := ⟨USize.ofNat 1⟩ instance : HasOfNat USize := ⟨USize.ofNat⟩ instance : HasAdd USize := ⟨USize.add⟩ instance : HasSub USize := ⟨USize.sub⟩ diff --git a/src/Std/Data/HashMap.lean b/src/Std/Data/HashMap.lean index f306406ab4..d5b38e5387 100644 --- a/src/Std/Data/HashMap.lean +++ b/src/Std/Data/HashMap.lean @@ -86,7 +86,7 @@ partial def moveEntries [Hashable α] : Nat → Array (AssocList α β) → Hash def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β := let nbuckets := buckets.val.size * 2 -have nbuckets > 0 from Nat.mulPos buckets.property (Nat.zeroLtBit0 Nat.oneNeZero) +have nbuckets > 0 from Nat.mulPos buckets.property (decide! : 2 > 0) have (mkArray nbuckets (@AssocList.nil α β)).size = nbuckets from Array.szMkArrayEq _ _ have Array.size (mkArray nbuckets AssocList.nil) > 0 by rw this; assumption let new_buckets : HashMapBucket α β := ⟨mkArray nbuckets AssocList.nil, this⟩ diff --git a/src/Std/Data/HashSet.lean b/src/Std/Data/HashSet.lean index 9a7fce4030..68332276cc 100644 --- a/src/Std/Data/HashSet.lean +++ b/src/Std/Data/HashSet.lean @@ -79,7 +79,7 @@ partial def moveEntries [Hashable α] : Nat → Array (List α) → HashSetBucke def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α := let nbuckets := buckets.val.size * 2 -have nbuckets > 0 from Nat.mulPos buckets.property (Nat.zeroLtBit0 Nat.oneNeZero) +have nbuckets > 0 from Nat.mulPos buckets.property (decide! : 2 > 0) have (mkArray nbuckets ([] : List α)).size = nbuckets from Array.szMkArrayEq _ _ have Array.size (mkArray nbuckets List.nil) > 0 by rw this; assumption let new_buckets : HashSetBucket α := ⟨mkArray nbuckets [], this⟩;