From e304d778a1960153ebc5de7a704e6d809398272b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 24 Sep 2016 16:38:39 -0700 Subject: [PATCH] chore(library/init): cleanup --- library/init/alternative.lean | 9 +- library/init/applicative.lean | 6 +- library/init/char.lean | 3 +- library/init/classical.lean | 16 +-- library/init/coe.lean | 1 - library/init/combinator.lean | 6 +- library/init/datatypes.lean | 12 +- library/init/functor.lean | 3 +- library/init/funext.lean | 7 +- library/init/list.lean | 15 +-- library/init/list_classes.lean | 15 ++- library/init/logic.lean | 4 +- library/init/monad.lean | 13 +-- library/init/monad_combinators.lean | 32 +++--- library/init/nat.lean | 166 ++++++++++++++-------------- library/init/nat_div.lean | 14 +-- library/init/num.lean | 18 +-- library/init/option.lean | 34 +++--- library/init/ordering.lean | 8 +- library/init/quot.lean | 38 +++---- library/init/relation.lean | 26 ++--- library/init/set.lean | 28 ++--- library/init/setoid.lean | 6 +- library/init/sigma.lean | 2 +- library/init/sigma_lex.lean | 25 ++--- library/init/state.lean | 30 ++--- library/init/string.lean | 19 ++-- library/init/subtype.lean | 6 +- library/init/timeit.lean | 2 +- library/init/to_string.lean | 14 +-- library/init/trace.lean | 2 +- library/init/unit.lean | 4 +- library/init/unsigned.lean | 8 +- library/init/wf.lean | 48 ++++---- 34 files changed, 304 insertions(+), 336 deletions(-) diff --git a/library/init/alternative.lean b/library/init/alternative.lean index 8337328282..c5cb7bf80f 100644 --- a/library/init/alternative.lean +++ b/library/init/alternative.lean @@ -11,16 +11,13 @@ class alternative (F : Type u → Type v) extends applicative F : Type (max u+1 (failure : Π {A : Type u}, F A) (orelse : Π {A : Type u}, F A → F A → F A) -attribute [inline] -def failure {F : Type u → Type v} [alternative F] {A : Type u} : F A := +@[inline] def failure {F : Type u → Type v} [alternative F] {A : Type u} : F A := alternative.failure F -attribute [inline] -def orelse {F : Type u → Type v} [alternative F] {A : Type u} : F A → F A → F A := +@[inline] def orelse {F : Type u → Type v} [alternative F] {A : Type u} : F A → F A → F A := alternative.orelse infixr ` <|> `:2 := orelse -attribute [inline] -def guard {F : Type → Type v} [alternative F] (P : Prop) [decidable P] : F unit := +@[inline] def guard {F : Type → Type v} [alternative F] (P : Prop) [decidable P] : F unit := if P then pure () else failure diff --git a/library/init/applicative.lean b/library/init/applicative.lean index 5d86142463..af11f42e4d 100644 --- a/library/init/applicative.lean +++ b/library/init/applicative.lean @@ -11,12 +11,10 @@ class applicative (F : Type u → Type v) extends functor F : Type (max u+1 v):= (pure : Π {A : Type u}, A → F A) (seq : Π {A B : Type u}, F (A → B) → F A → F B) -attribute [inline] -def pure {F : Type u → Type v} [applicative F] {A : Type u} : A → F A := +@[inline] def pure {F : Type u → Type v} [applicative F] {A : Type u} : A → F A := applicative.pure F -attribute [inline] -def seq_app {A B : Type u} {F : Type u → Type v} [applicative F] : F (A → B) → F A → F B := +@[inline] def seq_app {A B : Type u} {F : Type u → Type v} [applicative F] : F (A → B) → F A → F B := applicative.seq infixr ` <*> `:2 := seq_app diff --git a/library/init/char.lean b/library/init/char.lean index c9c6363968..2d6b271027 100644 --- a/library/init/char.lean +++ b/library/init/char.lean @@ -16,8 +16,7 @@ namespace char private lemma zero_lt_char_sz : 0 < char_sz := zero_lt_succ _ -attribute [pattern] -def of_nat (n : nat) : char := +@[pattern] def of_nat (n : nat) : char := if H : n < char_sz then fin.mk n H else fin.mk 0 zero_lt_char_sz def to_nat (c : char) : nat := diff --git a/library/init/classical.lean b/library/init/classical.lean index a7194dce9f..0d7327a293 100644 --- a/library/init/classical.lean +++ b/library/init/classical.lean @@ -5,15 +5,15 @@ Authors: Leonardo de Moura, Jeremy Avigad -/ prelude import init.subtype init.funext -namespace classical open subtype + +namespace classical universe variables u v /- the axiom -/ -- In the presence of classical logic, we could prove this from a weaker statement: -- axiom indefinite_description {A : Type u} {p : A->Prop} (H : ∃ x, p x) : {x : A, p x} -axiom strong_indefinite_description {A : Type u} (p : A → Prop) (H : nonempty A) : - { x : A // (∃ y : A, p y) → p x} +axiom strong_indefinite_description {A : Type u} (p : A → Prop) (H : nonempty A) : { x : A // (∃ y : A, p y) → p x} theorem exists_true_of_nonempty {A : Type u} (h : nonempty A) : ∃ x : A, true := nonempty.elim h (take x, ⟨x, trivial⟩) @@ -68,11 +68,11 @@ The proof follows Diaconescu proof that shows that the axiom of choice implies t section diaconescu parameter p : Prop -private definition U (x : Prop) : Prop := x = true ∨ p -private definition V (x : Prop) : Prop := x = false ∨ p +private def U (x : Prop) : Prop := x = true ∨ p +private def V (x : Prop) : Prop := x = false ∨ p -private noncomputable definition u := epsilon U -private noncomputable definition v := epsilon V +private noncomputable def u := epsilon U +private noncomputable def v := epsilon V private lemma u_def : U u := epsilon_spec ⟨true, or.inl rfl⟩ @@ -128,7 +128,7 @@ theorem cases_on (a : Prop) {p : Prop → Prop} (h1 : p true) (h2 : p false) : p cases_true_false p h1 h2 a -- this supercedes by_cases in decidable -definition by_cases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q := +def by_cases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q := or.elim (em p) (assume hp, hpq hp) (assume hnp, hnpq hnp) -- this supercedes by_contradiction in decidable diff --git a/library/init/coe.lean b/library/init/coe.lean index 9f1955c268..15285e3232 100644 --- a/library/init/coe.lean +++ b/library/init/coe.lean @@ -59,7 +59,6 @@ def coe_b {A : Type u} {B : Type v} [has_coe A B] : A → B := def coe_t {A : Type u} {B : Type v} [has_coe_t A B] : A → B := @has_coe_t.coe A B _ -set_option pp.all true def coe_fn_b {A : Type u} [has_coe_to_fun.{u v} A] : A → has_coe_to_fun.F.{u v} A := has_coe_to_fun.coe diff --git a/library/init/combinator.lean b/library/init/combinator.lean index cfcd1535bb..61b02eca49 100644 --- a/library/init/combinator.lean +++ b/library/init/combinator.lean @@ -7,7 +7,7 @@ prelude /- Combinator calculus -/ namespace combinator universe variables u₁ u₂ u₃ -definition I {A : Type u₁} (a : A) := a -definition K {A : Type u₁} {B : Type u₂} (a : A) (b : B) := a -definition S {A : Type u₁} {B : Type u₂} {C : Type u₃} (x : A → B → C) (y : A → B) (z : A) := x z (y z) +def I {A : Type u₁} (a : A) := a +def K {A : Type u₁} {B : Type u₂} (a : A) (b : B) := a +def S {A : Type u₁} {B : Type u₂} {C : Type u₃} (x : A → B → C) (y : A → B) (z : A) := x z (y z) end combinator diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean index 6690ead61b..4858351e83 100644 --- a/library/init/datatypes.lean +++ b/library/init/datatypes.lean @@ -3,7 +3,7 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -Basic datatypes +Basic datatypes and notation -/ prelude @@ -139,10 +139,8 @@ def lt {A : Type u} [has_lt A] : A → A → Prop := has_lt.lt def append {A : Type u} [has_append A] : A → A → A := has_append.append def andthen {A : Type u} [has_andthen A] : A → A → A := has_andthen.andthen -attribute [reducible] -def ge {A : Type u} [s : has_le A] (a b : A) : Prop := le b a -attribute [reducible] -def gt {A : Type u} [s : has_lt A] (a b : A) : Prop := lt b a +@[reducible] def ge {A : Type u} [s : has_le A] (a b : A) : Prop := le b a +@[reducible] def gt {A : Type u} [s : has_lt A] (a b : A) : Prop := lt b a def bit0 {A : Type u} [s : has_add A] (a : A) : A := add a a def bit1 {A : Type u} [s₁ : has_one A] [s₂ : has_add A] (a : A) : A := add (bit0 a) one @@ -251,7 +249,6 @@ reserve infix ` ≠ `:50 reserve infix ` ≈ `:50 reserve infix ` ~ `:50 reserve infix ` ≡ `:50 - reserve infixl ` ⬝ `:75 reserve infixr ` ▸ `:75 reserve infixr ` ▹ `:75 @@ -324,8 +321,7 @@ infix ; := andthen /- eq basic support -/ notation a = b := eq a b -attribute [pattern] -def rfl {A : Type u} {a : A} : a = a := eq.refl a +@[pattern] def rfl {A : Type u} {a : A} : a = a := eq.refl a namespace eq variables {A : Type u} diff --git a/library/init/functor.lean b/library/init/functor.lean index 6c1d652dec..db9cd00b48 100644 --- a/library/init/functor.lean +++ b/library/init/functor.lean @@ -9,8 +9,7 @@ universe variables u v class functor (F : Type u → Type v) : Type (max u+1 v) := (map : Π {A B : Type u}, (A → B) → F A → F B) -attribute [inline] -definition fmap {F : Type u → Type v} [functor F] {A B : Type u} : (A → B) → F A → F B := +@[inline] definition fmap {F : Type u → Type v} [functor F] {A B : Type u} : (A → B) → F A → F B := functor.map infixr ` <$> `:100 := fmap diff --git a/library/init/funext.lean b/library/init/funext.lean index b5e7563d9f..d275c34894 100644 --- a/library/init/funext.lean +++ b/library/init/funext.lean @@ -8,8 +8,9 @@ Extensional equality for functions, and a proof of function extensionality from prelude import init.quot init.logic +universe variables u v + namespace function - universe variables u v variables {A : Type u} {B : A → Type v} protected definition equiv (f₁ f₂ : Π x : A, B x) : Prop := ∀ x, f₁ x = f₂ x @@ -30,7 +31,6 @@ end function section open quot - universe variables u v variables {A : Type u} {B : A → Type v} attribute [instance] @@ -59,7 +59,6 @@ attribute funext [intro!] local infix `~` := function.equiv -attribute [instance] -definition {u v} subsingleton_pi {A : Type u} {B : A → Type v} (H : ∀ a, subsingleton (B a)) : +instance pi.subsingleton {A : Type u} {B : A → Type v} (H : ∀ a, subsingleton (B a)) : subsingleton (Π a, B a) := ⟨λ f₁ f₂, funext (λ a, subsingleton.elim (f₁ a) (f₂ a))⟩ diff --git a/library/init/list.lean b/library/init/list.lean index 4df0a26a9d..5c177c444e 100644 --- a/library/init/list.lean +++ b/library/init/list.lean @@ -7,21 +7,24 @@ prelude import init.logic init.nat open decidable list +notation h :: t := cons h t +notation `[` l:(foldr `, ` (h t, cons h t) nil `]`) := l + universe variables u v instance (A : Type u) : inhabited (list A) := ⟨list.nil⟩ -notation h :: t := cons h t -notation `[` l:(foldr `, ` (h t, cons h t) nil `]`) := l - -namespace list variables {A : Type u} {B : Type v} +namespace list def append : list A → list A → list A | [] l := l | (h :: s) t := h :: (append s t) +instance : has_append (list A) := +⟨append⟩ + def length : list A → nat | [] := 0 | (a :: l) := length l + 1 @@ -68,7 +71,5 @@ def dropn : ℕ → list A → list A | 0 a := a | (succ n) [] := [] | (succ n) (x::r) := dropn n r -end list -instance {A : Type u} : has_append (list A) := -⟨list.append⟩ +end list diff --git a/library/init/list_classes.lean b/library/init/list_classes.lean index d122bfb9bf..5b42bb493d 100644 --- a/library/init/list_classes.lean +++ b/library/init/list_classes.lean @@ -6,21 +6,20 @@ Author: Leonardo de Moura prelude import init.monad init.alternative open list + universe variables u v -attribute [inline] -def list_fmap {A : Type u} {B : Type v} (f : A → B) (l : list A) : list B := + +@[inline] def list_fmap {A : Type u} {B : Type v} (f : A → B) (l : list A) : list B := map f l -attribute [inline] -def list_bind {A : Type u} {B : Type v} (a : list A) (b : A → list B) : list B := +@[inline] def list_bind {A : Type u} {B : Type v} (a : list A) (b : A → list B) : list B := join (map b a) -attribute [inline] -def list_return {A : Type u} (a : A) : list A := +@[inline] def list_return {A : Type u} (a : A) : list A := [a] instance : monad list := -monad.mk @list_fmap @list_return @list_bind +⟨@list_fmap, @list_return, @list_bind⟩ instance : alternative list := -alternative.mk @list_fmap @list_return (@fapp _ _) @nil @list.append +⟨@list_fmap, @list_return, @fapp _ _, @nil, @list.append⟩ diff --git a/library/init/logic.lean b/library/init/logic.lean index 1062aac1db..75933c3fed 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -760,7 +760,7 @@ instance prop.inhabited : inhabited Prop := instance fun.inhabited (A : Type u) {B : Type v} [h : inhabited B] : inhabited (A → B) := inhabited.rec_on h (λ b, ⟨λ a, b⟩) -instance pi.inhabite (A : Type u) {B : A → Type v} [Π x, inhabited (B x)] : inhabited (Π x, B x) := +instance pi.inhabited (A : Type u) {B : A → Type v} [Π x, inhabited (B x)] : inhabited (Π x, B x) := ⟨λ a, default (B a)⟩ instance : inhabited bool := @@ -798,7 +798,7 @@ eq.rec_on h (λ a b : A, heq_of_eq (subsingleton.elim a b)) instance subsingleton_prop (p : Prop) : subsingleton p := ⟨λ a b, proof_irrel a b⟩ -instance subsingleton_decidable (p : Prop) : subsingleton (decidable p) := +instance (p : Prop) : subsingleton (decidable p) := subsingleton.intro (λ d₁, match d₁ with | (is_true t₁) := (λ d₂, diff --git a/library/init/monad.lean b/library/init/monad.lean index b0be807301..ea813b92b3 100644 --- a/library/init/monad.lean +++ b/library/init/monad.lean @@ -11,21 +11,18 @@ class monad (M : Type u → Type v) extends functor M : Type (max u+1 v) := (ret : Π {A : Type u}, A → M A) (bind : Π {A B : Type u}, M A → (A → M B) → M B) -attribute [inline] -definition return {M : Type u → Type v} [monad M] {A : Type u} : A → M A := +@[inline] def return {M : Type u → Type v} [monad M] {A : Type u} : A → M A := monad.ret M -definition fapp {M : Type u → Type v} [monad M] {A B : Type u} (f : M (A → B)) (a : M A) : M B := +def fapp {M : Type u → Type v} [monad M] {A B : Type u} (f : M (A → B)) (a : M A) : M B := do g ← f, b ← a, return (g b) -attribute [inline, instance] -definition monad_is_applicative (M : Type u → Type v) [monad M] : applicative M := -applicative.mk (@fmap _ _) (@return _ _) (@fapp _ _) +@[inline] instance monad_is_applicative (M : Type u → Type v) [monad M] : applicative M := +⟨@fmap _ _, @return _ _, @fapp _ _⟩ -attribute [inline] -definition monad.and_then {A B : Type u} {M : Type u → Type v} [monad M] (a : M A) (b : M B) : M B := +@[inline] def monad.and_then {A B : Type u} {M : Type u → Type v} [monad M] (a : M A) (b : M B) : M B := do a, b infixl ` >>= `:2 := monad.bind diff --git a/library/init/monad_combinators.lean b/library/init/monad_combinators.lean index 5cbbb63ac7..17b38d7cb8 100644 --- a/library/init/monad_combinators.lean +++ b/library/init/monad_combinators.lean @@ -9,25 +9,25 @@ prelude import init.monad init.list namespace monad -definition mapM {m : Type → Type} [monad m] {A B : Type} (f : A → m B) : list A → m (list B) +def mapM {m : Type → Type} [monad m] {A B : Type} (f : A → m B) : list A → m (list B) | [] := return [] | (h :: t) := do h' ← f h, t' ← mapM t, return (h' :: t') -definition mapM' {m : Type → Type} [monad m] {A B : Type} (f : A → m B) : list A → m unit +def mapM' {m : Type → Type} [monad m] {A B : Type} (f : A → m B) : list A → m unit | [] := return () | (h :: t) := f h >> mapM' t -definition forM {m : Type → Type} [monad m] {A B : Type} (l : list A) (f : A → m B) : m (list B) := +def forM {m : Type → Type} [monad m] {A B : Type} (l : list A) (f : A → m B) : m (list B) := mapM f l -definition forM' {m : Type → Type} [monad m] {A B : Type} (l : list A) (f : A → m B) : m unit := +def forM' {m : Type → Type} [monad m] {A B : Type} (l : list A) (f : A → m B) : m unit := mapM' f l -definition sequence {m : Type → Type} [monad m] {A : Type} : list (m A) → m (list A) +def sequence {m : Type → Type} [monad m] {A : Type} : list (m A) → m (list A) | [] := return [] | (h :: t) := do h' ← h, t' ← sequence t, return (h' :: t') -definition sequence' {m : Type → Type} [monad m] {A : Type} : list (m A) → m unit +def sequence' {m : Type → Type} [monad m] {A : Type} : list (m A) → m unit | [] := return () | (h :: t) := h >> sequence' t @@ -37,38 +37,38 @@ infix ` >=> `:2 := λ s t a, s a >>= t infix ` <=< `:2 := λ t s a, s a >>= t -definition join {m : Type → Type} [monad m] {A : Type} (a : m (m A)) : m A := +def join {m : Type → Type} [monad m] {A : Type} (a : m (m A)) : m A := bind a id -definition filterM {m : Type → Type} [monad m] {A : Type} (f : A → m bool) : list A → m (list A) +def filterM {m : Type → Type} [monad m] {A : Type} (f : A → m bool) : list A → m (list A) | [] := return [] | (h :: t) := do b ← f h, t' ← filterM t, bool.cond b (return (h :: t')) (return t') -definition whenb {m : Type → Type} [monad m] (b : bool) (t : m unit) : m unit := +def whenb {m : Type → Type} [monad m] (b : bool) (t : m unit) : m unit := bool.cond b t (return ()) -definition unlessb {m : Type → Type} [monad m] (b : bool) (t : m unit) : m unit := +def unlessb {m : Type → Type} [monad m] (b : bool) (t : m unit) : m unit := bool.cond b (return ()) t -definition condM {m : Type → Type} [monad m] {A : Type} (mbool : m bool) +def condM {m : Type → Type} [monad m] {A : Type} (mbool : m bool) (tm fm : m A) : m A := do b ← mbool, bool.cond b tm fm -definition liftM {m : Type → Type} [monad m] {A R : Type} (f : A → R) (ma : m A) : m R := +def liftM {m : Type → Type} [monad m] {A R : Type} (f : A → R) (ma : m A) : m R := do a ← ma, return (f a) -definition liftM₂ {m : Type → Type} [monad m] {A R : Type} (f : A → A → R) (ma₁ ma₂: m A) : m R := +def liftM₂ {m : Type → Type} [monad m] {A R : Type} (f : A → A → R) (ma₁ ma₂: m A) : m R := do a₁ ← ma₁, a₂ ← ma₂, return (f a₁ a₂) -definition liftM₃ {m : Type → Type} [monad m] {A R : Type} (f : A → A → A → R) +def liftM₃ {m : Type → Type} [monad m] {A R : Type} (f : A → A → A → R) (ma₁ ma₂ ma₃ : m A) : m R := do a₁ ← ma₁, a₂ ← ma₂, a₃ ← ma₃, return (f a₁ a₂ a₃) -definition liftM₄ {m : Type → Type} [monad m] {A R : Type} (f : A → A → A → A → R) +def liftM₄ {m : Type → Type} [monad m] {A R : Type} (f : A → A → A → A → R) (ma₁ ma₂ ma₃ ma₄ : m A) : m R := do a₁ ← ma₁, a₂ ← ma₂, a₃ ← ma₃, a₄ ← ma₄, return (f a₁ a₂ a₃ a₄) -definition liftM₅ {m : Type → Type} [monad m] {A R : Type} (f : A → A → A → A → A → R) +def liftM₅ {m : Type → Type} [monad m] {A R : Type} (f : A → A → A → A → A → R) (ma₁ ma₂ ma₃ ma₄ ma₅ : m A) : m R := do a₁ ← ma₁, a₂ ← ma₂, a₃ ← ma₃, a₄ ← ma₄, a₅ ← ma₅, return (f a₁ a₂ a₃ a₄ a₅) diff --git a/library/init/nat.lean b/library/init/nat.lean index 19ff81f84e..1a1e137219 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -9,67 +9,67 @@ import init.relation init.num notation `ℕ` := nat namespace nat - protected theorem zero_add : ∀ n : ℕ, 0 + n = n + protected lemma zero_add : ∀ n : ℕ, 0 + n = n | 0 := rfl | (n+1) := congr_arg succ (zero_add n) - theorem succ_add : ∀ n m : ℕ, (succ n) + m = succ (n + m) + lemma succ_add : ∀ n m : ℕ, (succ n) + m = succ (n + m) | n 0 := rfl | n (m+1) := congr_arg succ (succ_add n m) - protected theorem add_comm : ∀ n m : ℕ, n + m = m + n + protected lemma add_comm : ∀ n m : ℕ, n + m = m + n | n 0 := eq.symm (nat.zero_add n) | n (m+1) := suffices succ (n + m) = succ (m + n), from eq.symm (succ_add m n) ▸ this, congr_arg succ (add_comm n m) - protected theorem bit0_succ_eq (n : ℕ) : bit0 (succ n) = succ (succ (bit0 n)) := + protected lemma bit0_succ_eq (n : ℕ) : bit0 (succ n) = succ (succ (bit0 n)) := show succ (succ n + n) = succ (succ (n + n)), from succ_add n n ▸ rfl - protected theorem bit1_eq_succ_bit0 (n : ℕ) : bit1 n = succ (bit0 n) := + protected lemma bit1_eq_succ_bit0 (n : ℕ) : bit1 n = succ (bit0 n) := rfl - protected theorem bit1_succ_eq (n : ℕ) : bit1 (succ n) = succ (succ (bit1 n)) := + protected lemma bit1_succ_eq (n : ℕ) : bit1 (succ n) = succ (succ (bit1 n)) := eq.trans (nat.bit1_eq_succ_bit0 (succ n)) (congr_arg succ (nat.bit0_succ_eq n)) - theorem succ_ne_zero (n : ℕ) : succ n ≠ 0 := + lemma succ_ne_zero (n : ℕ) : succ n ≠ 0 := assume h, nat.no_confusion h - theorem succ_ne_self : ∀ n : ℕ, succ n ≠ n + lemma succ_ne_self : ∀ n : ℕ, succ n ≠ n | 0 h := absurd h (nat.succ_ne_zero 0) | (n+1) h := succ_ne_self n (nat.no_confusion h (λ h, h)) - protected theorem one_ne_zero : 1 ≠ (0 : ℕ) := + protected lemma one_ne_zero : 1 ≠ (0 : ℕ) := assume h, nat.no_confusion h - protected theorem bit0_ne_zero : ∀ n : ℕ, n ≠ 0 → bit0 n ≠ 0 + protected lemma bit0_ne_zero : ∀ n : ℕ, n ≠ 0 → bit0 n ≠ 0 | 0 h := absurd rfl h | (n+1) h := nat.succ_ne_zero _ - protected theorem bit1_ne_zero (n : ℕ) : bit1 n ≠ 0 := + protected lemma bit1_ne_zero (n : ℕ) : bit1 n ≠ 0 := show succ (n + n) ≠ 0, from succ_ne_zero (n + n) - protected theorem bit1_ne_one : ∀ n : ℕ, n ≠ 0 → bit1 n ≠ 1 + protected lemma bit1_ne_one : ∀ n : ℕ, n ≠ 0 → bit1 n ≠ 1 | 0 h h1 := absurd rfl h | (n+1) h h1 := nat.no_confusion h1 (λ h2, absurd h2 (nat.succ_ne_zero _)) - protected theorem bit0_ne_one : ∀ n : ℕ, bit0 n ≠ 1 + protected lemma bit0_ne_one : ∀ n : ℕ, bit0 n ≠ 1 | 0 h := absurd h (ne.symm nat.one_ne_zero) | (n+1) h := have h1 : succ (succ (n + n)) = 1, from succ_add n n ▸ h, nat.no_confusion h1 (λ h2, absurd h2 (succ_ne_zero (n + n))) - protected theorem add_self_ne_one : ∀ (n : ℕ), n + n ≠ 1 + protected lemma add_self_ne_one : ∀ (n : ℕ), n + n ≠ 1 | 0 h := nat.no_confusion h | (n+1) h := have h1 : succ (succ (n + n)) = 1, from succ_add n n ▸ h, nat.no_confusion h1 (λ h2, absurd h2 (nat.succ_ne_zero (n + n))) - protected theorem bit1_ne_bit0 : ∀ (n m : ℕ), bit1 n ≠ bit0 m + protected lemma bit1_ne_bit0 : ∀ (n m : ℕ), bit1 n ≠ bit0 m | 0 m h := absurd h (ne.symm (nat.add_self_ne_one m)) | (n+1) 0 h := have h1 : succ (bit0 (succ n)) = 0, from h, @@ -89,23 +89,23 @@ namespace nat ⟨nat.le⟩ attribute [refl] - protected definition le_refl : ∀ a : ℕ, a ≤ a := + protected def le_refl : ∀ a : ℕ, a ≤ a := le.nat_refl - @[reducible] protected definition lt (n m : ℕ) := succ n ≤ m + @[reducible] protected def lt (n m : ℕ) := succ n ≤ m instance : has_lt ℕ := ⟨nat.lt⟩ - definition pred : ℕ → ℕ + def pred : ℕ → ℕ | 0 := 0 | (a+1) := a - protected definition sub : ℕ → ℕ → ℕ + protected def sub : ℕ → ℕ → ℕ | a 0 := a | a (b+1) := pred (sub a b) - protected definition mul (a b : ℕ) : ℕ := + protected def mul (a b : ℕ) : ℕ := nat.rec_on b zero (λ b₁ r, r + a) instance : has_sub ℕ := @@ -126,142 +126,142 @@ namespace nat /- properties of inequality -/ - protected theorem le_of_eq {n m : ℕ} (p : n = m) : n ≤ m := + protected lemma le_of_eq {n m : ℕ} (p : n = m) : n ≤ m := p ▸ le.nat_refl n - theorem le_succ (n : ℕ) : n ≤ succ n := + lemma le_succ (n : ℕ) : n ≤ succ n := le.step (nat.le_refl n) - theorem pred_le : ∀ (n : ℕ), pred n ≤ n + lemma pred_le : ∀ (n : ℕ), pred n ≤ n | 0 := le.nat_refl 0 | (succ a) := le.step (le.nat_refl a) attribute [simp] - theorem le_succ_iff_true (n : ℕ) : n ≤ succ n ↔ true := + lemma le_succ_iff_true (n : ℕ) : n ≤ succ n ↔ true := iff_true_intro (le_succ n) attribute [simp] - theorem pred_le_iff_true (n : ℕ) : pred n ≤ n ↔ true := + lemma pred_le_iff_true (n : ℕ) : pred n ≤ n ↔ true := iff_true_intro (pred_le n) - protected theorem le_trans {n m k : ℕ} (h1 : n ≤ m) : m ≤ k → n ≤ k := + protected lemma le_trans {n m k : ℕ} (h1 : n ≤ m) : m ≤ k → n ≤ k := le.rec h1 (λ p h2, le.step) - theorem le_succ_of_le {n m : ℕ} (h : n ≤ m) : n ≤ succ m := + lemma le_succ_of_le {n m : ℕ} (h : n ≤ m) : n ≤ succ m := nat.le_trans h (le_succ m) - theorem le_of_succ_le {n m : ℕ} (h : succ n ≤ m) : n ≤ m := + lemma le_of_succ_le {n m : ℕ} (h : succ n ≤ m) : n ≤ m := nat.le_trans (le_succ n) h - protected theorem le_of_lt {n m : ℕ} (h : n < m) : n ≤ m := + protected lemma le_of_lt {n m : ℕ} (h : n < m) : n ≤ m := le_of_succ_le h - theorem succ_le_succ {n m : ℕ} : n ≤ m → succ n ≤ succ m := + lemma succ_le_succ {n m : ℕ} : n ≤ m → succ n ≤ succ m := λ h, le.rec (nat.le_refl (succ n)) (λ a b, le.step) h - theorem pred_le_pred {n m : ℕ} : n ≤ m → pred n ≤ pred m := + lemma pred_le_pred {n m : ℕ} : n ≤ m → pred n ≤ pred m := λ h, le.rec (nat.le_refl (pred n)) (λ n, nat.rec (λ a b, b) (λ a b c, le.step) n) h - theorem le_of_succ_le_succ {n m : ℕ} : succ n ≤ succ m → n ≤ m := + lemma le_of_succ_le_succ {n m : ℕ} : succ n ≤ succ m → n ≤ m := pred_le_pred - theorem le_succ_of_pred_le {n m : ℕ} : pred n ≤ m → n ≤ succ m := + lemma le_succ_of_pred_le {n m : ℕ} : pred n ≤ m → n ≤ succ m := nat.cases_on n le.step (λ a, succ_le_succ) - theorem not_succ_le_zero : ∀ (n : ℕ), succ n ≤ 0 → false + lemma not_succ_le_zero : ∀ (n : ℕ), succ n ≤ 0 → false . - theorem succ_le_zero_iff_false (n : ℕ) : succ n ≤ 0 ↔ false := + lemma succ_le_zero_iff_false (n : ℕ) : succ n ≤ 0 ↔ false := iff_false_intro (not_succ_le_zero n) - theorem not_succ_le_self : ∀ n : ℕ, ¬succ n ≤ n := + lemma not_succ_le_self : ∀ n : ℕ, ¬succ n ≤ n := λ n, nat.rec (not_succ_le_zero 0) (λ a b c, b (le_of_succ_le_succ c)) n attribute [simp] - theorem succ_le_self_iff_false (n : ℕ) : succ n ≤ n ↔ false := + lemma succ_le_self_iff_false (n : ℕ) : succ n ≤ n ↔ false := iff_false_intro (not_succ_le_self n) - theorem zero_le : ∀ (n : ℕ), 0 ≤ n + lemma zero_le : ∀ (n : ℕ), 0 ≤ n | 0 := nat.le_refl 0 | (n+1) := le.step (zero_le n) attribute [simp] - theorem zero_le_iff_true (n : ℕ) : 0 ≤ n ↔ true := + lemma zero_le_iff_true (n : ℕ) : 0 ≤ n ↔ true := iff_true_intro (zero_le n) - protected theorem one_le_bit1 (n : ℕ) : 1 ≤ bit1 n := + protected lemma one_le_bit1 (n : ℕ) : 1 ≤ bit1 n := show 1 ≤ succ (bit0 n), from succ_le_succ (zero_le (bit0 n)) - protected theorem one_le_bit0 : ∀ (n : ℕ), n ≠ 0 → 1 ≤ bit0 n + protected lemma one_le_bit0 : ∀ (n : ℕ), n ≠ 0 → 1 ≤ bit0 n | 0 h := absurd rfl h | (n+1) h := suffices 1 ≤ succ (succ (bit0 n)), from eq.symm (nat.bit0_succ_eq n) ▸ this, succ_le_succ (zero_le (succ (bit0 n))) - definition lt.step {n m : ℕ} : n < m → n < succ m := le.step + def lt.step {n m : ℕ} : n < m → n < succ m := le.step - theorem zero_lt_succ (n : ℕ) : 0 < succ n := + lemma zero_lt_succ (n : ℕ) : 0 < succ n := succ_le_succ (zero_le n) attribute [simp] - theorem zero_lt_succ_iff_true (n : ℕ) : 0 < succ n ↔ true := + lemma zero_lt_succ_iff_true (n : ℕ) : 0 < succ n ↔ true := iff_true_intro (zero_lt_succ n) - protected theorem lt_trans {n m k : ℕ} (h₁ : n < m) : m < k → n < k := + protected lemma lt_trans {n m k : ℕ} (h₁ : n < m) : m < k → n < k := nat.le_trans (le.step h₁) - protected theorem lt_of_le_of_lt {n m k : ℕ} (h₁ : n ≤ m) : m < k → n < k := + protected lemma lt_of_le_of_lt {n m k : ℕ} (h₁ : n ≤ m) : m < k → n < k := nat.le_trans (succ_le_succ h₁) - protected theorem lt_of_lt_of_le {n m k : ℕ} : n < m → m ≤ k → n < k := nat.le_trans + protected lemma lt_of_lt_of_le {n m k : ℕ} : n < m → m ≤ k → n < k := nat.le_trans - protected theorem lt_irrefl (n : ℕ) : ¬n < n := + protected lemma lt_irrefl (n : ℕ) : ¬n < n := not_succ_le_self n - theorem lt_self_iff_false (n : ℕ) : n < n ↔ false := + lemma lt_self_iff_false (n : ℕ) : n < n ↔ false := iff_false_intro (λ h, absurd h (nat.lt_irrefl n)) - theorem self_lt_succ (n : ℕ) : n < succ n := nat.le_refl (succ n) + lemma self_lt_succ (n : ℕ) : n < succ n := nat.le_refl (succ n) attribute [simp] - theorem self_lt_succ_iff_true (n : ℕ) : n < succ n ↔ true := + lemma self_lt_succ_iff_true (n : ℕ) : n < succ n ↔ true := iff_true_intro (self_lt_succ n) - definition lt.base (n : ℕ) : n < succ n := nat.le_refl (succ n) + def lt.base (n : ℕ) : n < succ n := nat.le_refl (succ n) - theorem le_lt_antisymm {n m : ℕ} (h₁ : n ≤ m) (h₂ : m < n) : false := + lemma le_lt_antisymm {n m : ℕ} (h₁ : n ≤ m) (h₂ : m < n) : false := nat.lt_irrefl n (nat.lt_of_le_of_lt h₁ h₂) - protected theorem le_antisymm {n m : ℕ} (h₁ : n ≤ m) : m ≤ n → n = m := + protected lemma le_antisymm {n m : ℕ} (h₁ : n ≤ m) : m ≤ n → n = m := le.cases_on h₁ (λ a, rfl) (λ a b c, absurd (nat.lt_of_le_of_lt b c) (nat.lt_irrefl n)) - theorem lt_le_antisymm {n m : ℕ} (h₁ : n < m) (h₂ : m ≤ n) : false := + lemma lt_le_antisymm {n m : ℕ} (h₁ : n < m) (h₂ : m ≤ n) : false := le_lt_antisymm h₂ h₁ - protected theorem nat.lt_asymm {n m : ℕ} (h₁ : n < m) : ¬ m < n := + protected lemma nat.lt_asymm {n m : ℕ} (h₁ : n < m) : ¬ m < n := le_lt_antisymm (nat.le_of_lt h₁) - theorem not_lt_zero (a : ℕ) : ¬ a < 0 := not_succ_le_zero a + lemma not_lt_zero (a : ℕ) : ¬ a < 0 := not_succ_le_zero a attribute [simp] - theorem lt_zero_iff_false (a : ℕ) : a < 0 ↔ false := + lemma lt_zero_iff_false (a : ℕ) : a < 0 ↔ false := iff_false_intro (not_lt_zero a) - protected theorem eq_or_lt_of_le {a b : ℕ} (h : a ≤ b) : a = b ∨ a < b := + protected lemma eq_or_lt_of_le {a b : ℕ} (h : a ≤ b) : a = b ∨ a < b := le.cases_on h (or.inl rfl) (λ n h, or.inr (succ_le_succ h)) - protected theorem le_of_eq_or_lt {a b : ℕ} (h : a = b ∨ a < b) : a ≤ b := + protected lemma le_of_eq_or_lt {a b : ℕ} (h : a = b ∨ a < b) : a ≤ b := or.elim h nat.le_of_eq nat.le_of_lt - theorem succ_lt_succ {a b : ℕ} : a < b → succ a < succ b := + lemma succ_lt_succ {a b : ℕ} : a < b → succ a < succ b := succ_le_succ - theorem lt_of_succ_lt {a b : ℕ} : succ a < b → a < b := + lemma lt_of_succ_lt {a b : ℕ} : succ a < b → a < b := le_of_succ_le - theorem lt_of_succ_lt_succ {a b : ℕ} : succ a < succ b → a < b := + lemma lt_of_succ_lt_succ {a b : ℕ} : succ a < succ b → a < b := le_of_succ_le_succ instance decidable_le : ∀ a b : ℕ, decidable (a ≤ b) @@ -276,7 +276,7 @@ namespace nat instance decidable_lt : ∀ a b : ℕ, decidable (a < b) := λ a b, nat.decidable_le (succ a) b - protected theorem lt_or_ge : ∀ (a b : ℕ), a < b ∨ a ≥ b + protected lemma lt_or_ge : ∀ (a b : ℕ), a < b ∨ a ≥ b | a 0 := or.inr (zero_le a) | a (b+1) := match lt_or_ge a b with @@ -288,54 +288,54 @@ namespace nat end end - protected definition {u} lt_ge_by_cases {a b : ℕ} {C : Type u} (h₁ : a < b → C) (h₂ : a ≥ b → C) : C := + protected def {u} lt_ge_by_cases {a b : ℕ} {C : Type u} (h₁ : a < b → C) (h₂ : a ≥ b → C) : C := decidable.by_cases h₁ (λ h, h₂ (or.elim (nat.lt_or_ge a b) (λ a, absurd a h) (λ a, a))) - protected definition {u} lt_by_cases {a b : ℕ} {C : Type u} (h₁ : a < b → C) (h₂ : a = b → C) + protected def {u} lt_by_cases {a b : ℕ} {C : Type u} (h₁ : a < b → C) (h₂ : a = b → C) (h₃ : b < a → C) : C := nat.lt_ge_by_cases h₁ (λ h₁, nat.lt_ge_by_cases h₃ (λ h, h₂ (nat.le_antisymm h h₁))) - protected theorem lt_trichotomy (a b : ℕ) : a < b ∨ a = b ∨ b < a := + protected lemma lt_trichotomy (a b : ℕ) : a < b ∨ a = b ∨ b < a := nat.lt_by_cases (λ h, or.inl h) (λ h, or.inr (or.inl h)) (λ h, or.inr (or.inr h)) - protected theorem eq_or_lt_of_not_lt {a b : ℕ} (hnlt : ¬ a < b) : a = b ∨ b < a := + protected lemma eq_or_lt_of_not_lt {a b : ℕ} (hnlt : ¬ a < b) : a = b ∨ b < a := or.elim (nat.lt_trichotomy a b) (λ hlt, absurd hlt hnlt) (λ h, h) - theorem lt_succ_of_le {a b : ℕ} : a ≤ b → a < succ b := + lemma lt_succ_of_le {a b : ℕ} : a ≤ b → a < succ b := succ_le_succ - theorem lt_of_succ_le {a b : ℕ} (h : succ a ≤ b) : a < b := h + lemma lt_of_succ_le {a b : ℕ} (h : succ a ≤ b) : a < b := h - theorem succ_le_of_lt {a b : ℕ} (h : a < b) : succ a ≤ b := h + lemma succ_le_of_lt {a b : ℕ} (h : a < b) : succ a ≤ b := h attribute [simp] - theorem succ_sub_succ_eq_sub (a b : ℕ) : succ a - succ b = a - b := + lemma succ_sub_succ_eq_sub (a b : ℕ) : succ a - succ b = a - b := nat.rec_on b (show succ a - succ zero = a - zero, from (eq.refl (succ a - succ zero))) (λ b, congr_arg pred) - theorem sub_eq_succ_sub_succ (a b : ℕ) : a - b = succ a - succ b := + lemma sub_eq_succ_sub_succ (a b : ℕ) : a - b = succ a - succ b := eq.symm (succ_sub_succ_eq_sub a b) attribute [simp] - theorem zero_sub_eq_zero : ∀ a : ℕ, 0 - a = 0 + lemma zero_sub_eq_zero : ∀ a : ℕ, 0 - a = 0 | 0 := rfl | (a+1) := congr_arg pred (zero_sub_eq_zero a) - theorem zero_eq_zero_sub (a : ℕ) : 0 = 0 - a := + lemma zero_eq_zero_sub (a : ℕ) : 0 = 0 - a := eq.symm (zero_sub_eq_zero a) - theorem sub_le (a b : ℕ) : a - b ≤ a := + lemma sub_le (a b : ℕ) : a - b ≤ a := nat.rec_on b (nat.le_refl (a - 0)) (λ b₁, nat.le_trans (pred_le (a - b₁))) attribute [simp] - theorem sub_le_iff_true (a b : ℕ) : a - b ≤ a ↔ true := + lemma sub_le_iff_true (a b : ℕ) : a - b ≤ a ↔ true := iff_true_intro (sub_le a b) - theorem sub_lt : ∀ {a b : ℕ}, 0 < a → 0 < b → a - b < a + lemma sub_lt : ∀ {a b : ℕ}, 0 < a → 0 < b → a - b < a | 0 b h1 h2 := absurd h1 (nat.lt_irrefl 0) | (a+1) 0 h1 h2 := absurd h2 (nat.lt_irrefl 0) | (a+1) (b+1) h1 h2 := @@ -343,21 +343,21 @@ namespace nat show a - b < succ a, from lt_succ_of_le (sub_le a b) - theorem sub_lt_succ (a b : ℕ) : a - b < succ a := + lemma sub_lt_succ (a b : ℕ) : a - b < succ a := lt_succ_of_le (sub_le a b) attribute [simp] - theorem sub_lt_succ_iff_true (a b : ℕ) : a - b < succ a ↔ true := + lemma sub_lt_succ_iff_true (a b : ℕ) : a - b < succ a ↔ true := iff_true_intro (sub_lt_succ a b) - theorem le_add_right : ∀ (n k : ℕ), n ≤ n + k + lemma le_add_right : ∀ (n k : ℕ), n ≤ n + k | n 0 := nat.le_refl n | n (k+1) := le_succ_of_le (le_add_right n k) - theorem le_add_left (n m : ℕ): n ≤ m + n := + lemma le_add_left (n m : ℕ): n ≤ m + n := nat.add_comm n m ▸ le_add_right n m - definition {u} repeat {A : Type u} (f : ℕ → A → A) : ℕ → A → A + def {u} repeat {A : Type u} (f : ℕ → A → A) : ℕ → A → A | 0 a := a | (succ n) a := f n (repeat n a) diff --git a/library/init/nat_div.lean b/library/init/nat_div.lean index 69ebcca746..71c41540a5 100644 --- a/library/init/nat_div.lean +++ b/library/init/nat_div.lean @@ -7,29 +7,29 @@ prelude import init.wf init.nat namespace nat -private definition div_rec_lemma {x y : nat} : 0 < y ∧ y ≤ x → x - y < x := +private def div_rec_lemma {x y : nat} : 0 < y ∧ y ≤ x → x - y < x := λ h, and.rec (λ ypos ylex, sub_lt (nat.lt_of_lt_of_le ypos ylex) ypos) h -private definition div.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat := +private def div.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat := if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y + 1 else zero -protected definition div := well_founded.fix lt_wf div.F +protected def div := well_founded.fix lt_wf div.F instance : has_div nat := ⟨nat.div⟩ -theorem div_def (x y : nat) : div x y = if H : 0 < y ∧ y ≤ x then div (x - y) y + 1 else 0 := +lemma div_def (x y : nat) : div x y = if H : 0 < y ∧ y ≤ x then div (x - y) y + 1 else 0 := congr_fun (well_founded.fix_eq lt_wf div.F x) y -private definition mod.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat := +private def mod.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat := if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y else x -protected definition mod := well_founded.fix lt_wf mod.F +protected def mod := well_founded.fix lt_wf mod.F instance : has_mod nat := ⟨nat.mod⟩ -theorem mod_def (x y : nat) : mod x y = if H : 0 < y ∧ y ≤ x then mod (x - y) y else x := +lemma mod_def (x y : nat) : mod x y = if H : 0 < y ∧ y ≤ x then mod (x - y) y else x := congr_fun (well_founded.fix_eq lt_wf mod.F x) y end nat diff --git a/library/init/num.lean b/library/init/num.lean index 79c53da704..9dd6c8e455 100644 --- a/library/init/num.lean +++ b/library/init/num.lean @@ -7,13 +7,13 @@ prelude import init.bool namespace pos_num - protected definition mul (a b : pos_num) : pos_num := + protected def mul (a b : pos_num) : pos_num := pos_num.rec_on a b (λ n r, bit0 r + b) (λ n r, bit0 r) - definition lt (a b : pos_num) : bool := + def lt (a b : pos_num) : bool := pos_num.rec_on a (λ b, pos_num.cases_on b ff @@ -29,7 +29,7 @@ namespace pos_num (λ m, f m)) b - definition le (a b : pos_num) : bool := + def le (a b : pos_num) : bool := pos_num.lt a (succ b) end pos_num @@ -39,13 +39,13 @@ instance : has_mul pos_num := namespace num open pos_num - definition pred (a : num) : num := + def pred (a : num) : num := num.rec_on a zero (λ p, bool.cond (is_one p) zero (pos (pred p))) - definition size (a : num) : num := + def size (a : num) : num := num.rec_on a (pos pos_num.one) (λ p, pos (size p)) - protected definition mul (a b : num) : num := + protected def mul (a b : num) : num := num.rec_on a zero (λ pa, num.rec_on b zero (λ pb, pos (pos_num.mul pa pb))) end num @@ -53,10 +53,10 @@ instance : has_mul num := ⟨num.mul⟩ namespace num - protected definition le (a b : num) : bool := + protected def le (a b : num) : bool := num.rec_on a tt (λ pa, num.rec_on b ff (λ pb, pos_num.le pa pb)) - private definition psub (a b : pos_num) : num := + private def psub (a b : pos_num) : num := pos_num.rec_on a (λ b, zero) (λ n f b, @@ -75,7 +75,7 @@ namespace num (λ m, 2 * f m))) b - protected definition sub (a b : num) : num := + protected def sub (a b : num) : num := num.rec_on a zero (λ pa, num.rec_on b a (λ pb, psub pa pb)) end num diff --git a/library/init/option.lean b/library/init/option.lean index ccc50fd004..d52c051560 100644 --- a/library/init/option.lean +++ b/library/init/option.lean @@ -22,20 +22,18 @@ instance {A : Type u} [H : decidable_eq A] : decidable_eq (option A) | (is_false n) := is_false (λ H, option.no_confusion H (λ e, absurd e n)) end -attribute [inline] -definition option_fmap {A : Type u} {B : Type v} (f : A → B) : option A → option B +@[inline] def option_fmap {A : Type u} {B : Type v} (f : A → B) : option A → option B | none := none | (some a) := some (f a) -attribute [inline] -definition option_bind {A : Type u} {B : Type v} : option A → (A → option B) → option B +@[inline] def option_bind {A : Type u} {B : Type v} : option A → (A → option B) → option B | none b := none | (some a) b := b a instance : monad option := monad.mk @option_fmap @some @option_bind -definition option_orelse {A : Type u} : option A → option A → option A +def option_orelse {A : Type u} : option A → option A → option A | (some a) o := some a | none (some a) := some a | none none := none @@ -43,11 +41,10 @@ definition option_orelse {A : Type u} : option A → option A → option A instance {A : Type u} : alternative option := alternative.mk @option_fmap @some (@fapp _ _) @none @option_orelse -definition optionT (M : Type (max 1 u) → Type v) [monad M] (A : Type u) : Type v := +def optionT (M : Type (max 1 u) → Type v) [monad M] (A : Type u) : Type v := M (option A) -attribute [inline] -definition optionT_fmap {M : Type (max 1 u) → Type v} [monad M] {A B : Type u} (f : A → B) (e : optionT M A) : optionT M B := +@[inline] def optionT_fmap {M : Type (max 1 u) → Type v} [monad M] {A B : Type u} (f : A → B) (e : optionT M A) : optionT M B := show M (option B), from do o ← e, match o with @@ -55,8 +52,7 @@ do o ← e, | (some a) := return (some (f a)) end -attribute [inline] -definition optionT_bind {M : Type (max 1 u) → Type v} [monad M] {A B : Type u} (a : optionT M A) (b : A → optionT M B) +@[inline] def optionT_bind {M : Type (max 1 u) → Type v} [monad M] {A B : Type u} (a : optionT M A) (b : A → optionT M B) : optionT M B := show M (option B), from do o ← a, @@ -65,15 +61,14 @@ do o ← a, | (some a) := b a end -attribute [inline] -definition optionT_return {M : Type (max 1 u) → Type v} [monad M] {A : Type u} (a : A) : optionT M A := +@[inline] def optionT_return {M : Type (max 1 u) → Type v} [monad M] {A : Type u} (a : A) : optionT M A := show M (option A), from return (some a) instance {M : Type (max 1 u) → Type v} [monad M] {A : Type u} : monad (optionT M) := monad.mk (@optionT_fmap M _) (@optionT_return M _) (@optionT_bind M _) -definition optionT_orelse {M : Type (max 1 u) → Type v} [monad M] {A : Type u} (a : optionT M A) (b : optionT M A) : optionT M A := +def optionT_orelse {M : Type (max 1 u) → Type v} [monad M] {A : Type u} (a : optionT M A) (b : optionT M A) : optionT M A := show M (option A), from do o ← a, match o with @@ -81,14 +76,13 @@ do o ← a, | (some v) := return (some v) end -definition optionT_fail {M : Type (max 1 u) → Type v} [monad M] {A : Type u} : optionT M A := +def optionT_fail {M : Type (max 1 u) → Type v} [monad M] {A : Type u} : optionT M A := show M (option A), from return none instance {M : Type (max 1 u) → Type v} [monad M] {A : Type u} : alternative (optionT M) := -alternative.mk - (@optionT_fmap M _) - (@optionT_return M _) - (@fapp (optionT M) (@optionT.monad M _ A)) - (@optionT_fail M _) - (@optionT_orelse M _) +{map := @optionT_fmap M _, + pure := @optionT_return M _, + seq := @fapp (optionT M) (@optionT.monad M _ A), + failure := @optionT_fail M _, + orelse := @optionT_orelse M _} diff --git a/library/init/ordering.lean b/library/init/ordering.lean index 3363864c2f..ea467499e9 100644 --- a/library/init/ordering.lean +++ b/library/init/ordering.lean @@ -17,7 +17,7 @@ has_to_string.mk (λ s, match s with | ordering.lt := "lt" | ordering.eq := "eq" class has_ordering (A : Type) := (cmp : A → A → ordering) -definition nat.cmp (a b : nat) : ordering := +def nat.cmp (a b : nat) : ordering := if a < b then ordering.lt else if a = b then ordering.eq else ordering.gt @@ -30,7 +30,7 @@ open prod variables {A B : Type} [has_ordering A] [has_ordering B] -definition prod.cmp : A × B → A × B → ordering +def prod.cmp : A × B → A × B → ordering | (a₁, b₁) (a₂, b₂) := match (has_ordering.cmp a₁ a₂) with | ordering.lt := lt @@ -47,7 +47,7 @@ open sum variables {A B : Type} [has_ordering A] [has_ordering B] -definition sum.cmp : A ⊕ B → A ⊕ B → ordering +def sum.cmp : A ⊕ B → A ⊕ B → ordering | (inl a₁) (inl a₂) := has_ordering.cmp a₁ a₂ | (inr b₁) (inr b₂) := has_ordering.cmp b₁ b₂ | (inl a₁) (inr b₂) := lt @@ -62,7 +62,7 @@ open option variables {A : Type} [has_ordering A] -definition option.cmp : option A → option A → ordering +def option.cmp : option A → option A → ordering | (some a₁) (some a₂) := has_ordering.cmp a₁ a₂ | (some a₁) none := gt | none (some a₂) := lt diff --git a/library/init/quot.lean b/library/init/quot.lean index 4cb6310810..9bab5ec7e2 100644 --- a/library/init/quot.lean +++ b/library/init/quot.lean @@ -17,7 +17,7 @@ constant propext {a b : Prop} : (a ↔ b) → a = b -- iff can now be used to do substitutions in a calculation attribute [subst] -theorem iff_subst {a b : Prop} {P : Prop → Prop} (H₁ : a ↔ b) (H₂ : P a) : P b := +lemma iff_subst {a b : Prop} {P : Prop → Prop} (H₁ : a ↔ b) (H₂ : P a) : P b := eq.subst (propext H₁) H₂ namespace quot @@ -32,21 +32,21 @@ namespace quot init_quotient - protected theorem lift_beta {A : Type u} {B : Type v} [setoid A] (f : A → B) (c : ∀ a b, a ≈ b → f a = f b) (a : A) : lift f c ⟦a⟧ = f a := + protected lemma lift_beta {A : Type u} {B : Type v} [setoid A] (f : A → B) (c : ∀ a b, a ≈ b → f a = f b) (a : A) : lift f c ⟦a⟧ = f a := rfl - protected theorem ind_beta {A : Type u} [s : setoid A] {B : quot s → Prop} (p : ∀ a, B ⟦a⟧) (a : A) : (ind p ⟦a⟧ : B ⟦a⟧) = p a := + protected lemma ind_beta {A : Type u} [s : setoid A] {B : quot s → Prop} (p : ∀ a, B ⟦a⟧) (a : A) : (ind p ⟦a⟧ : B ⟦a⟧) = p a := rfl attribute [reducible, elab_as_eliminator] - protected definition lift_on {A : Type u} {B : Type v} [s : setoid A] (q : quot s) (f : A → B) (c : ∀ a b, a ≈ b → f a = f b) : B := + protected def lift_on {A : Type u} {B : Type v} [s : setoid A] (q : quot s) (f : A → B) (c : ∀ a b, a ≈ b → f a = f b) : B := lift f c q attribute [elab_as_eliminator] - protected theorem induction_on {A : Type u} [s : setoid A] {B : quot s → Prop} (q : quot s) (H : ∀ a, B ⟦a⟧) : B q := + protected lemma induction_on {A : Type u} [s : setoid A] {B : quot s → Prop} (q : quot s) (H : ∀ a, B ⟦a⟧) : B q := ind H q - theorem exists_rep {A : Type u} [s : setoid A] (q : quot s) : ∃ a : A, ⟦a⟧ = q := + lemma exists_rep {A : Type u} [s : setoid A] (q : quot s) : ∃ a : A, ⟦a⟧ = q := quot.induction_on q (λ a, ⟨a, rfl⟩) section @@ -56,7 +56,7 @@ namespace quot include s attribute [reducible] - protected definition indep (f : Π a, B ⟦a⟧) (a : A) : Σ q, B q := + protected def indep (f : Π a, B ⟦a⟧) (a : A) : Σ q, B q := ⟨⟦a⟧, f a⟩ protected lemma indep_coherent (f : Π a, B ⟦a⟧) @@ -70,23 +70,23 @@ namespace quot quot.ind (λ (a : A), eq.refl (quot.indep f a).1) q attribute [reducible, elab_as_eliminator] - protected definition rec + protected def rec (f : Π a, B ⟦a⟧) (H : ∀ (a b : A) (p : a ≈ b), (eq.rec (f a) (sound p) : B ⟦b⟧) = f b) (q : quot s) : B q := eq.rec_on (quot.lift_indep_pr1 f H q) ((lift (quot.indep f) (quot.indep_coherent f H) q).2) attribute [reducible, elab_as_eliminator] - protected definition rec_on + protected def rec_on (q : quot s) (f : Π a, B ⟦a⟧) (H : ∀ (a b : A) (p : a ≈ b), (eq.rec (f a) (sound p) : B ⟦b⟧) = f b) : B q := quot.rec f H q attribute [reducible, elab_as_eliminator] - protected definition rec_on_subsingleton + protected def rec_on_subsingleton [H : ∀ a, subsingleton (B ⟦a⟧)] (q : quot s) (f : Π a, B ⟦a⟧) : B q := quot.rec f (λ a b h, subsingleton.elim _ (f b)) q attribute [reducible, elab_as_eliminator] - protected definition hrec_on + protected def hrec_on (q : quot s) (f : Π a, B ⟦a⟧) (c : ∀ (a b : A) (p : a ≈ b), f a == f b) : B q := quot.rec_on q f (λ a b p, eq_of_heq (calc @@ -101,7 +101,7 @@ namespace quot include s₁ s₂ attribute [reducible, elab_as_eliminator] - protected definition lift₂ + protected def lift₂ (f : A → B → C)(c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) (q₁ : quot s₁) (q₂ : quot s₂) : C := quot.lift @@ -117,21 +117,21 @@ namespace quot q₁ attribute [reducible, elab_as_eliminator] - protected definition lift_on₂ + protected def lift_on₂ (q₁ : quot s₁) (q₂ : quot s₂) (f : A → B → C) (c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) : C := quot.lift₂ f c q₁ q₂ attribute [elab_as_eliminator] - protected theorem ind₂ {C : quot s₁ → quot s₂ → Prop} (H : ∀ a b, C ⟦a⟧ ⟦b⟧) (q₁ : quot s₁) (q₂ : quot s₂) : C q₁ q₂ := + protected lemma ind₂ {C : quot s₁ → quot s₂ → Prop} (H : ∀ a b, C ⟦a⟧ ⟦b⟧) (q₁ : quot s₁) (q₂ : quot s₂) : C q₁ q₂ := quot.ind (λ a₁, quot.ind (λ a₂, H a₁ a₂) q₂) q₁ attribute [elab_as_eliminator] - protected theorem induction_on₂ + protected lemma induction_on₂ {C : quot s₁ → quot s₂ → Prop} (q₁ : quot s₁) (q₂ : quot s₂) (H : ∀ a b, C ⟦a⟧ ⟦b⟧) : C q₁ q₂ := quot.ind (λ a₁, quot.ind (λ a₂, H a₁ a₂) q₂) q₁ attribute [elab_as_eliminator] - protected theorem induction_on₃ + protected lemma induction_on₃ [s₃ : setoid C] {D : quot s₁ → quot s₂ → quot s₃ → Prop} (q₁ : quot s₁) (q₂ : quot s₂) (q₃ : quot s₃) (H : ∀ a b c, D ⟦a⟧ ⟦b⟧ ⟦c⟧) : D q₁ q₂ q₃ := @@ -143,7 +143,7 @@ namespace quot variable [s : setoid A] include s - private definition rel (q₁ q₂ : quot s) : Prop := + private def rel (q₁ q₂ : quot s) : Prop := quot.lift_on₂ q₁ q₂ (λ a₁ a₂, a₁ ≈ a₂) (λ a₁ a₂ b₁ b₂ a₁b₁ a₂b₂, @@ -159,7 +159,7 @@ namespace quot private lemma eq_imp_rel {q₁ q₂ : quot s} : q₁ = q₂ → q₁ ~ q₂ := assume h, eq.rec_on h (rel.refl q₁) - theorem exact {a b : A} : ⟦a⟧ = ⟦b⟧ → a ≈ b := + lemma exact {a b : A} : ⟦a⟧ = ⟦b⟧ → a ≈ b := assume h, eq_imp_rel h end exact @@ -170,7 +170,7 @@ namespace quot include s₁ s₂ attribute [reducible, elab_as_eliminator] - protected definition rec_on_subsingleton₂ + protected def rec_on_subsingleton₂ {C : quot s₁ → quot s₂ → Type u_c} [H : ∀ a b, subsingleton (C ⟦a⟧ ⟦b⟧)] (q₁ : quot s₁) (q₂ : quot s₂) (f : Π a b, C ⟦a⟧ ⟦b⟧) : C q₁ q₂:= @quot.rec_on_subsingleton _ s₁ (λ q, C q q₂) (λ a, quot.ind (λ b, H a b) q₂) q₁ diff --git a/library/init/relation.lean b/library/init/relation.lean index 8a4e7ba4a2..32df527ffe 100644 --- a/library/init/relation.lean +++ b/library/init/relation.lean @@ -14,34 +14,34 @@ universe variables u v variables {A : Type u} {B : Type v} (R : B → B → Prop) local infix `≺`:50 := R -definition reflexive := ∀ x, x ≺ x +def reflexive := ∀ x, x ≺ x -definition symmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x +def symmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x -definition transitive := ∀ ⦃x y z⦄, x ≺ y → y ≺ z → x ≺ z +def transitive := ∀ ⦃x y z⦄, x ≺ y → y ≺ z → x ≺ z -definition equivalence := reflexive R ∧ symmetric R ∧ transitive R +def equivalence := reflexive R ∧ symmetric R ∧ transitive R -definition total := ∀ x y, x ≺ y ∨ y ≺ x +def total := ∀ x y, x ≺ y ∨ y ≺ x -definition mk_equivalence (r : reflexive R) (s : symmetric R) (t : transitive R) : equivalence R := +def mk_equivalence (r : reflexive R) (s : symmetric R) (t : transitive R) : equivalence R := ⟨r, s, t⟩ -definition irreflexive := ∀ x, ¬ x ≺ x +def irreflexive := ∀ x, ¬ x ≺ x -definition anti_symmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x → x = y +def anti_symmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x → x = y -definition empty_relation := λ a₁ a₂ : A, false +def empty_relation := λ a₁ a₂ : A, false -definition subrelation (Q R : B → B → Prop) := ∀ ⦃x y⦄, Q x y → R x y +def subrelation (Q R : B → B → Prop) := ∀ ⦃x y⦄, Q x y → R x y -definition inv_image (f : A → B) : A → A → Prop := +def inv_image (f : A → B) : A → A → Prop := λ a₁ a₂, f a₁ ≺ f a₂ -theorem inv_image.trans (f : A → B) (H : transitive R) : transitive (inv_image R f) := +lemma inv_image.trans (f : A → B) (H : transitive R) : transitive (inv_image R f) := λ (a₁ a₂ a₃ : A) (H₁ : inv_image R f a₁ a₂) (H₂ : inv_image R f a₂ a₃), H H₁ H₂ -theorem inv_image.irreflexive (f : A → B) (H : irreflexive R) : irreflexive (inv_image R f) := +lemma inv_image.irreflexive (f : A → B) (H : irreflexive R) : irreflexive (inv_image R f) := λ (a : A) (H₁ : inv_image R f a a), H (f a) H₁ inductive tc {A : Type u} (R : A → A → Prop) : A → A → Prop diff --git a/library/init/set.lean b/library/init/set.lean index fdc58a896f..b88017d29f 100644 --- a/library/init/set.lean +++ b/library/init/set.lean @@ -8,66 +8,66 @@ import init.logic init.collection universe variables u v -definition set (A : Type u) := A → Prop +def set (A : Type u) := A → Prop -definition set_of {A : Type u} (p : A → Prop) : set A := +def set_of {A : Type u} (p : A → Prop) : set A := p namespace set variables {A : Type u} {B : Type v} -definition mem (a : A) (s : set A) := +def mem (a : A) (s : set A) := s a infix ∈ := mem notation a ∉ s := ¬ mem a s -definition subset (s₁ s₂ : set A) : Prop := +def subset (s₁ s₂ : set A) : Prop := ∀ ⦃a⦄, a ∈ s₁ → a ∈ s₂ infix ⊆ := subset -definition superset (s₁ s₂ : set A) : Prop := +def superset (s₁ s₂ : set A) : Prop := s₂ ⊆ s₁ infix ⊇ := superset -private definition sep (p : A → Prop) (s : set A) : set A := +private def sep (p : A → Prop) (s : set A) : set A := {a | a ∈ s ∧ p a} instance : separable A set := ⟨sep⟩ -private definition empty : set A := +private def empty : set A := λ a, false -private definition insert (a : A) (s : set A) : set A := +private def insert (a : A) (s : set A) : set A := {b | b = a ∨ b ∈ s} instance : insertable A set := ⟨empty, insert⟩ -definition union (s₁ s₂ : set A) : set A := +def union (s₁ s₂ : set A) : set A := {a | a ∈ s₁ ∨ a ∈ s₂} notation s₁ ∪ s₂ := union s₁ s₂ -definition inter (s₁ s₂ : set A) : set A := +def inter (s₁ s₂ : set A) : set A := {a | a ∈ s₁ ∧ a ∈ s₂} notation s₁ ∩ s₂ := inter s₁ s₂ -definition compl (s : set A) : set A := +def compl (s : set A) : set A := {a | a ∉ s} instance : has_neg (set A) := ⟨compl⟩ -definition diff (s t : set A) : set A := +def diff (s t : set A) : set A := {a ∈ s | a ∉ t} infix `\`:70 := diff -definition powerset (s : set A) : set (set A) := +def powerset (s : set A) : set (set A) := {t | t ⊆ s} prefix `𝒫`:100 := powerset -definition image (f : A → B) (s : set A) : set B := +def image (f : A → B) (s : set A) : set B := {b | ∃ a, a ∈ s ∧ f a = b} infix ` ' ` := image end set diff --git a/library/init/setoid.lean b/library/init/setoid.lean index 2b6e7f300b..ab9eb01a31 100644 --- a/library/init/setoid.lean +++ b/library/init/setoid.lean @@ -18,19 +18,19 @@ namespace setoid include s attribute [refl] - theorem refl (a : A) : a ≈ a := + lemma refl (a : A) : a ≈ a := match setoid.iseqv A with | ⟨H_refl, H_symm, H_trans⟩ := H_refl a end attribute [symm] - theorem symm {a b : A} (Hab : a ≈ b) : b ≈ a := + lemma symm {a b : A} (Hab : a ≈ b) : b ≈ a := match setoid.iseqv A with | ⟨H_refl, H_symm, H_trans⟩ := H_symm Hab end attribute [trans] - theorem trans {a b c : A} (Hab : a ≈ b) (Hbc : b ≈ c) : a ≈ c := + lemma trans {a b c : A} (Hab : a ≈ b) (Hbc : b ≈ c) : a ≈ c := match setoid.iseqv A with | ⟨H_refl, H_symm, H_trans⟩ := H_trans Hab Hbc end diff --git a/library/init/sigma.lean b/library/init/sigma.lean index 86bfdd5f06..fdf24a3ab4 100644 --- a/library/init/sigma.lean +++ b/library/init/sigma.lean @@ -17,7 +17,7 @@ lemma ex_of_sig {A : Type u} {P : A → Prop} : (Σ x, P x) → ∃ x, P x namespace sigma variables {A : Type u} {B : A → Type v} - protected theorem eq : ∀ {p₁ p₂ : Σ a : A, B a} (H₁ : p₁.1 = p₂.1), (eq.rec_on H₁ p₁.2 : B p₂.1) = p₂.2 → p₁ = p₂ + protected lemma eq : ∀ {p₁ p₂ : Σ a : A, B a} (H₁ : p₁.1 = p₂.1), (eq.rec_on H₁ p₁.2 : B p₂.1) = p₂.2 → p₁ = p₂ | ⟨a, b⟩ ⟨.a, .b⟩ rfl rfl := rfl end sigma diff --git a/library/init/sigma_lex.lean b/library/init/sigma_lex.lean index 5aa6ae1849..22bddf90d8 100644 --- a/library/init/sigma_lex.lean +++ b/library/init/sigma_lex.lean @@ -18,15 +18,14 @@ section | right : ∀ (a : A) {b₁ b₂ : B a}, Rb a b₁ b₂ → lex (sigma.mk a b₁) (sigma.mk a b₂) end - section open well_founded tactic parameters {A : Type u} {B : A → Type v} parameters {Ra : A → A → Prop} {Rb : Π a : A, B a → B a → Prop} local infix `≺`:50 := lex Ra Rb - definition lex_accessible {a} (aca : acc Ra a) (acb : ∀ a, well_founded (Rb a)) - : ∀ (b : B a), acc (lex Ra Rb) (sigma.mk a b) := + def lex_accessible {a} (aca : acc Ra a) (acb : ∀ a, well_founded (Rb a)) + : ∀ (b : B a), acc (lex Ra Rb) (sigma.mk a b) := acc.rec_on aca (λ xa aca (iHa : ∀ y, Ra y xa → ∀ b : B y, acc (lex Ra Rb) (sigma.mk y b)), λ b : B xa, acc.rec_on (well_founded.apply (acb xa) b) @@ -49,18 +48,18 @@ section aux rfl (heq.refl xb)))) -- The lexicographical order of well founded relations is well-founded - definition lex_wf (Ha : well_founded Ra) (Hb : ∀ x, well_founded (Rb x)) : well_founded (lex Ra Rb) := + def lex_wf (Ha : well_founded Ra) (Hb : ∀ x, well_founded (Rb x)) : well_founded (lex Ra Rb) := well_founded.intro (λ p, destruct p (λ a b, lex_accessible (well_founded.apply Ha a) Hb b)) end section parameters {A : Type u} {B : Type v} - definition lex_ndep (Ra : A → A → Prop) (Rb : B → B → Prop) := + def lex_ndep (Ra : A → A → Prop) (Rb : B → B → Prop) := lex Ra (λ a : A, Rb) - definition lex_ndep_wf {Ra : A → A → Prop} {Rb : B → B → Prop} (Ha : well_founded Ra) (Hb : well_founded Rb) - : well_founded (lex_ndep Ra Rb) := + def lex_ndep_wf {Ra : A → A → Prop} {Rb : B → B → Prop} (Ha : well_founded Ra) (Hb : well_founded Rb) + : well_founded (lex_ndep Ra Rb) := well_founded.intro (λ p, destruct p (λ a b, lex_accessible (well_founded.apply Ha a) (λ x, Hb) b)) end @@ -81,7 +80,7 @@ section parameters {Ra : A → A → Prop} {Rb : B → B → Prop} local infix `≺`:50 := rev_lex Ra Rb - definition rev_lex_accessible {b} (acb : acc Rb b) (aca : ∀ a, acc Ra a): ∀ a, acc (rev_lex Ra Rb) (sigma.mk a b) := + def rev_lex_accessible {b} (acb : acc Rb b) (aca : ∀ a, acc Ra a): ∀ a, acc (rev_lex Ra Rb) (sigma.mk a b) := acc.rec_on acb (λ xb acb (iHb : ∀ y, Rb y xb → ∀ a, acc (rev_lex Ra Rb) (sigma.mk a y)), λ a, acc.rec_on (aca a) @@ -101,19 +100,19 @@ section iHb b₁ Rb₁ a₁), aux rfl rfl))) - definition rev_lex_wf (Ha : well_founded Ra) (Hb : well_founded Rb) : well_founded (rev_lex Ra Rb) := + def rev_lex_wf (Ha : well_founded Ra) (Hb : well_founded Rb) : well_founded (rev_lex Ra Rb) := well_founded.intro (λ p, destruct p (λ a b, rev_lex_accessible (apply Hb b) (well_founded.apply Ha) a)) end section - definition skip_left (A : Type u) {B : Type v} (Rb : B → B → Prop) : @sigma A (λ a, B) → @sigma A (λ a, B) → Prop := + def skip_left (A : Type u) {B : Type v} (Rb : B → B → Prop) : @sigma A (λ a, B) → @sigma A (λ a, B) → Prop := rev_lex empty_relation Rb - definition skip_left_wf (A : Type u) {B : Type v} {Rb : B → B → Prop} (Hb : well_founded Rb) : well_founded (skip_left A Rb) := + def skip_left_wf (A : Type u) {B : Type v} {Rb : B → B → Prop} (Hb : well_founded Rb) : well_founded (skip_left A Rb) := rev_lex_wf empty_wf Hb - definition mk_skip_left {A : Type u} {B : Type v} {b₁ b₂ : B} {Rb : B → B → Prop} - (a₁ a₂ : A) (H : Rb b₁ b₂) : skip_left A Rb (sigma.mk a₁ b₁) (sigma.mk a₂ b₂) := + def mk_skip_left {A : Type u} {B : Type v} {b₁ b₂ : B} {Rb : B → B → Prop} + (a₁ a₂ : A) (H : Rb b₁ b₂) : skip_left A Rb (sigma.mk a₁ b₁) (sigma.mk a₂ b₂) := rev_lex.right _ _ _ H end end sigma diff --git a/library/init/state.lean b/library/init/state.lean index a7befcb555..10dd6aa758 100644 --- a/library/init/state.lean +++ b/library/init/state.lean @@ -6,23 +6,19 @@ Authors: Leonardo de Moura prelude import init.logic init.monad init.alternative init.prod -definition state (S : Type) (A : Type) : Type := +def state (S : Type) (A : Type) : Type := S → A × S section -set_option pp.all true variables {S : Type} {A B : Type} -attribute [inline] -definition state_fmap (f : A → B) (a : state S A) : state S B := +@[inline] def state_fmap (f : A → B) (a : state S A) : state S B := λ s, match (a s) with (a', s') := (f a', s') end -attribute [inline] -definition state_return (a : A) : state S A := +@[inline] def state_return (a : A) : state S A := λ s, (a, s) -attribute [inline] -definition state_bind (a : state S A) (b : A → state S B) : state S B := +@[inline] def state_bind (a : state S A) (b : A → state S B) : state S B := λ s, match (a s) with (a', s') := b a' s' end instance (S : Type) : monad (state S) := @@ -30,16 +26,14 @@ instance (S : Type) : monad (state S) := end namespace state -attribute [inline] -definition read {S : Type} : state S S := +@[inline] def read {S : Type} : state S S := λ s, (s, s) -attribute [inline] -definition write {S : Type} : S → state S unit := +@[inline] def write {S : Type} : S → state S unit := λ s' s, ((), s') end state -definition stateT (S : Type) (M : Type → Type) [monad M] (A : Type) : Type := +def stateT (S : Type) (M : Type → Type) [monad M] (A : Type) : Type := S → M (A × S) section @@ -48,16 +42,16 @@ section variable [monad M] variables {A B : Type} - definition stateT_fmap (f : A → B) (act : stateT S M A) : stateT S M B := + def stateT_fmap (f : A → B) (act : stateT S M A) : stateT S M B := λ s, show M (B × S), from do (a, new_s) ← act s, return (f a, new_s) - definition stateT_return (a : A) : stateT S M A := + def stateT_return (a : A) : stateT S M A := λ s, show M (A × S), from return (a, s) - definition stateT_bind (act₁ : stateT S M A) (act₂ : A → stateT S M B) : stateT S M B := + def stateT_bind (act₁ : stateT S M A) (act₂ : A → stateT S M B) : stateT S M B := λ s, show M (B × S), from do (a, new_s) ← act₁ s, act₂ a new_s @@ -67,9 +61,9 @@ instance (S : Type) (M : Type → Type) [monad M] : monad (stateT S M) := ⟨@stateT_fmap S M _, @stateT_return S M _, @stateT_bind S M _⟩ namespace stateT -definition read {S : Type} {M : Type → Type} [monad M] : stateT S M S := +def read {S : Type} {M : Type → Type} [monad M] : stateT S M S := λ s, return (s, s) -definition write {S : Type} {M : Type → Type} [monad M] : S → stateT S M unit := +def write {S : Type} {M : Type → Type} [monad M] : S → stateT S M unit := λ s' s, return ((), s') end stateT diff --git a/library/init/string.lean b/library/init/string.lean index 8da5f1cc62..a1ca87998f 100644 --- a/library/init/string.lean +++ b/library/init/string.lean @@ -5,27 +5,24 @@ Author: Leonardo de Moura -/ prelude import init.char init.list -attribute [reducible] -definition string := list char + +@[reducible] def string := list char namespace string +@[pattern] def empty : string := list.nil -attribute [pattern] -definition empty : string := list.nil +@[pattern] def str : char → string → string := list.cons -attribute [pattern] -definition str : char → string → string := list.cons - -definition concat (a b : string) : string := +def concat (a b : string) : string := list.append b a -end string instance : has_append string := ⟨string.concat⟩ +end string open list -private definition utf8_length_aux : nat → nat → string → nat +private def utf8_length_aux : nat → nat → string → nat | 0 r (c::s) := let n := char.to_nat c in if n < 0x80 then utf8_length_aux 0 (r+1) s @@ -38,5 +35,5 @@ private definition utf8_length_aux : nat → nat → string → nat | (n+1) r (c::s) := utf8_length_aux n r s | n r [] := r -definition utf8_length : string → nat +def utf8_length : string → nat | s := utf8_length_aux 0 0 (reverse s) diff --git a/library/init/subtype.lean b/library/init/subtype.lean index 9878a56ee7..ac27f43f55 100644 --- a/library/init/subtype.lean +++ b/library/init/subtype.lean @@ -14,15 +14,15 @@ tag :: (elt_of : A) (has_property : p elt_of) namespace subtype - definition exists_of_subtype {A : Type u} {p : A → Prop} : { x // p x } → ∃ x, p x + def exists_of_subtype {A : Type u} {p : A → Prop} : { x // p x } → ∃ x, p x | ⟨a, h⟩ := ⟨a, h⟩ variables {A : Type u} {p : A → Prop} - theorem tag_irrelevant {a : A} (h1 h2 : p a) : tag a h1 = tag a h2 := + lemma tag_irrelevant {a : A} (h1 h2 : p a) : tag a h1 = tag a h2 := rfl - protected theorem eq : ∀ {a1 a2 : {x // p x}}, elt_of a1 = elt_of a2 → a1 = a2 + protected lemma eq : ∀ {a1 a2 : {x // p x}}, elt_of a1 = elt_of a2 → a1 = a2 | ⟨x, h1⟩ ⟨.x, h2⟩ rfl := rfl end subtype diff --git a/library/init/timeit.lean b/library/init/timeit.lean index 0d44b5674b..6a0b49534b 100644 --- a/library/init/timeit.lean +++ b/library/init/timeit.lean @@ -5,5 +5,5 @@ prelude import init.string /- This function has a native implementation that tracks time. -/ -definition timeit {A : Type} (s : string) (f : unit → A) : A := +def timeit {A : Type} (s : string) (f : unit → A) : A := f () diff --git a/library/init/to_string.lean b/library/init/to_string.lean index 3b9d3ca6f8..ad5542a17d 100644 --- a/library/init/to_string.lean +++ b/library/init/to_string.lean @@ -10,7 +10,7 @@ universe variables u v class has_to_string (A : Type u) := (to_string : A → string) -definition to_string {A : Type u} [has_to_string A] : A → string := +def to_string {A : Type u} [has_to_string A] : A → string := has_to_string.to_string instance : has_to_string bool := @@ -20,12 +20,12 @@ instance {p : Prop} : has_to_string (decidable p) := -- Remark: type class inference will not consider local instance `b` in the new elaborator ⟨λ b : decidable p, @ite p b _ "tt" "ff"⟩ -definition list.to_string_aux {A : Type u} [has_to_string A] : bool → list A → string +def list.to_string_aux {A : Type u} [has_to_string A] : bool → list A → string | b [] := "" | tt (x::xs) := to_string x ++ list.to_string_aux ff xs | ff (x::xs) := ", " ++ to_string x ++ list.to_string_aux ff xs -definition list.to_string {A : Type u} [has_to_string A] : list A → string +def list.to_string {A : Type u} [has_to_string A] : list A → string | [] := "[]" | (x::xs) := "[" ++ list.to_string_aux tt (x::xs) ++ "]" @@ -50,7 +50,7 @@ instance {A : Type u} {B : A → Type v} [has_to_string A] [s : ∀ x, has_to_st instance {A : Type u} {P : A → Prop} [has_to_string A] : has_to_string (subtype P) := ⟨λ s, to_string (elt_of s)⟩ -definition char.quote_core (c : char) : string := +def char.quote_core (c : char) : string := if c = '\n' then "\\n" else if c = '\\' then "\\\\" else if c = '\"' then "\\\"" @@ -60,11 +60,11 @@ else c::nil instance : has_to_string char := ⟨λ c, "'" ++ char.quote_core c ++ "'"⟩ -definition string.quote_aux : string → string +def string.quote_aux : string → string | [] := "" | (x::xs) := string.quote_aux xs ++ char.quote_core x -definition string.quote : string → string +def string.quote : string → string | [] := "\"\"" | (x::xs) := "\"" ++ string.quote_aux (x::xs) ++ "\"" @@ -72,7 +72,7 @@ instance : has_to_string string := ⟨string.quote⟩ /- Remark: the code generator replaces this definition with one that display natural numbers in decimal notation -/ -definition nat.to_string : nat → string +def nat.to_string : nat → string | 0 := "zero" | (succ a) := "(succ " ++ nat.to_string a ++ ")" diff --git a/library/init/trace.lean b/library/init/trace.lean index 9519ec16e6..73cd110392 100644 --- a/library/init/trace.lean +++ b/library/init/trace.lean @@ -5,5 +5,5 @@ prelude import init.string /- This function has a native implementation that displays the given string in the regular output stream. -/ -definition trace {A : Type} (s : string) (f : unit → A) : A := +def trace {A : Type} (s : string) (f : unit → A) : A := f () diff --git a/library/init/unit.lean b/library/init/unit.lean index d12c5bbe2e..1024fd16ea 100644 --- a/library/init/unit.lean +++ b/library/init/unit.lean @@ -6,10 +6,10 @@ Author: Leonardo de Moura prelude import init.logic -theorem unit_eq (a b : unit) : a = b := +lemma unit_eq (a b : unit) : a = b := unit.rec_on a (unit.rec_on b rfl) -theorem unit_eq_unit (a : unit) : a = () := +lemma unit_eq_unit (a : unit) : a = () := unit_eq a () instance : subsingleton unit := diff --git a/library/init/unsigned.lean b/library/init/unsigned.lean index 3b527c8d5c..c724985289 100644 --- a/library/init/unsigned.lean +++ b/library/init/unsigned.lean @@ -7,20 +7,20 @@ prelude import init.fin open nat -definition unsigned_sz : nat := succ 4294967295 +def unsigned_sz : nat := succ 4294967295 attribute [reducible] -definition unsigned := fin unsigned_sz +def unsigned := fin unsigned_sz namespace unsigned /- We cannot use tactic dec_trivial here because the tactic framework has not been defined yet. -/ private lemma zero_lt_unsigned_sz : 0 < unsigned_sz := zero_lt_succ _ -definition of_nat (n : nat) : unsigned := +def of_nat (n : nat) : unsigned := if H : n < unsigned_sz then fin.mk n H else fin.mk 0 zero_lt_unsigned_sz -definition to_nat (c : unsigned) : nat := +def to_nat (c : unsigned) : nat := fin.val c end unsigned diff --git a/library/init/wf.lean b/library/init/wf.lean index 5604e1fb87..a25782703e 100644 --- a/library/init/wf.lean +++ b/library/init/wf.lean @@ -14,12 +14,12 @@ inductive acc {A : Type u} (r : A → A → Prop) : A → Prop namespace acc variables {A : Type u} {r : A → A → Prop} - definition inv {x y : A} (h₁ : acc r x) (h₂ : r y x) : acc r y := + def inv {x y : A} (h₁ : acc r x) (h₂ : r y x) : acc r y := acc.rec_on h₁ (λ x₁ ac₁ ih h₂, ac₁ y h₂) h₂ -- dependent elimination for acc attribute [recursor] - protected definition drec + protected def drec {C : Π (a : A), acc r a → Type v} (h₁ : Π (x : A) (acx : Π (y : A), r y x → acc r y), (Π (y : A) (ryx : r y x), C y (acx y ryx)) → C x (acc.intro x acx)) {a : A} (h₂ : acc r a) : C a h₂ := @@ -30,7 +30,7 @@ inductive well_founded {A : Type u} (r : A → A → Prop) : Prop | intro : (∀ a, acc r a) → well_founded namespace well_founded - definition apply {A : Type u} {r : A → A → Prop} (wf : well_founded r) : ∀ a, acc r a := + def apply {A : Type u} {r : A → A → Prop} (wf : well_founded r) : ∀ a, acc r a := take a, well_founded.rec_on wf (λ p, p) a section @@ -39,19 +39,19 @@ namespace well_founded hypothesis hwf : well_founded r - theorem recursion {C : A → Type v} (a : A) (h : Π x, (Π y, y ≺ x → C y) → C x) : C a := + lemma recursion {C : A → Type v} (a : A) (h : Π x, (Π y, y ≺ x → C y) → C x) : C a := acc.rec_on (apply hwf a) (λ x₁ ac₁ ih, h x₁ ih) - theorem induction {C : A → Prop} (a : A) (h : ∀ x, (∀ y, y ≺ x → C y) → C x) : C a := + lemma induction {C : A → Prop} (a : A) (h : ∀ x, (∀ y, y ≺ x → C y) → C x) : C a := recursion a h variable {C : A → Type v} variable F : Π x, (Π y, y ≺ x → C y) → C x - definition fix_F (x : A) (a : acc r x) : C x := + def fix_F (x : A) (a : acc r x) : C x := acc.rec_on a (λ x₁ ac₁ ih, F x₁ ih) - theorem fix_F_eq (x : A) (r : acc r x) : + lemma fix_F_eq (x : A) (r : acc r x) : fix_F F x r = F x (λ (y : A) (p : y ≺ x), fix_F F y (acc.inv r p)) := acc.drec (λ x r ih, rfl) r end @@ -59,11 +59,11 @@ namespace well_founded variables {A : Type u} {C : A → Type v} {r : A → A → Prop} -- Well-founded fixpoint - definition fix (hwf : well_founded r) (F : Π x, (Π y, r y x → C y) → C x) (x : A) : C x := + def fix (hwf : well_founded r) (F : Π x, (Π y, r y x → C y) → C x) (x : A) : C x := fix_F F x (apply hwf x) -- Well-founded fixpoint satisfies fixpoint equation - theorem fix_eq (hwf : well_founded r) (F : Π x, (Π y, r y x → C y) → C x) (x : A) : + lemma fix_eq (hwf : well_founded r) (F : Π x, (Π y, r y x → C y) → C x) (x : A) : fix hwf F x = F x (λ y h, fix hwf F y) := fix_F_eq F x (apply hwf x) end well_founded @@ -71,7 +71,7 @@ end well_founded open well_founded -- Empty relation is well-founded -definition empty_wf {A : Type u} : well_founded empty_relation := +def empty_wf {A : Type u} : well_founded empty_relation := well_founded.intro (λ (a : A), acc.intro a (λ (b : A) (lt : false), false.rec _ lt)) @@ -82,11 +82,11 @@ section parameters (h₁ : subrelation Q r) parameters (h₂ : well_founded r) - definition accessible {a : A} (ac : acc r a) : acc Q a := + def accessible {a : A} (ac : acc r a) : acc Q a := acc.rec_on ac (λ x ax ih, acc.intro x (λ (y : A) (lt : Q y x), ih y (h₁ lt))) - definition wf : well_founded Q := + def wf : well_founded Q := ⟨λ a, accessible (apply h₂ a)⟩ end end subrelation @@ -98,14 +98,14 @@ section parameters (f : A → B) parameters (h : well_founded r) - private definition acc_aux {b : B} (ac : acc r b) : ∀ (x : A), f x = b → acc (inv_image r f) x := + private def acc_aux {b : B} (ac : acc r b) : ∀ (x : A), f x = b → acc (inv_image r f) x := acc.rec_on ac (λ x acx ih z e, acc.intro z (λ y lt, eq.rec_on e (λ acx ih, ih (f y) lt y rfl) acx ih)) - definition accessible {a : A} (ac : acc r (f a)) : acc (inv_image r f) a := + def accessible {a : A} (ac : acc r (f a)) : acc (inv_image r f) a := acc_aux ac a rfl - definition wf : well_founded (inv_image r f) := + def wf : well_founded (inv_image r f) := ⟨λ a, accessible (apply h (f a))⟩ end end inv_image @@ -116,7 +116,7 @@ section parameters {A : Type u} {r : A → A → Prop} local notation `r⁺` := tc r - definition accessible {z : A} (ac : acc r z) : acc (tc r) z := + def accessible {z : A} (ac : acc r z) : acc (tc r) z := acc.rec_on ac (λ x acx ih, acc.intro x (λ y rel, tc.rec_on rel @@ -124,23 +124,23 @@ section (λ a b c rab rbc ih₁ ih₂ acx ih, acc.inv (ih₂ acx ih) rab) acx ih)) - definition wf (h : well_founded r) : well_founded r⁺ := + def wf (h : well_founded r) : well_founded r⁺ := ⟨λ a, accessible (apply h a)⟩ end end tc -- less-than is well-founded -definition nat.lt_wf : well_founded nat.lt := +def nat.lt_wf : well_founded nat.lt := ⟨nat.rec (acc.intro 0 (λ n h, absurd h (nat.not_lt_zero n))) (λ n ih, acc.intro (nat.succ n) (λ m h, or.elim (nat.eq_or_lt_of_le (nat.le_of_succ_le_succ h)) (λ e, eq.substr e ih) (acc.inv ih)))⟩ -definition measure {A : Type u} : (A → ℕ) → A → A → Prop := +def measure {A : Type u} : (A → ℕ) → A → A → Prop := inv_image lt -definition measure_wf {A : Type u} (f : A → ℕ) : well_founded (measure f) := +def measure_wf {A : Type u} (f : A → ℕ) : well_founded (measure f) := inv_image.wf f nat.lt_wf namespace prod @@ -166,7 +166,7 @@ namespace prod parameters {ra : A → A → Prop} {rb : B → B → Prop} local infix `≺`:50 := lex ra rb - definition lex_accessible {a} (aca : acc ra a) (acb : ∀ b, acc rb b): ∀ b, acc (lex ra rb) (a, b) := + def lex_accessible {a} (aca : acc ra a) (acb : ∀ b, acc rb b): ∀ b, acc (lex ra rb) (a, b) := acc.rec_on aca (λ xa aca iha b, acc.rec_on (acb b) (λ xb acb ihb, acc.intro (xa, xb) (λ p lt, @@ -178,15 +178,15 @@ namespace prod aux rfl rfl))) -- The lexicographical order of well founded relations is well-founded - definition lex_wf (ha : well_founded ra) (hb : well_founded rb) : well_founded (lex ra rb) := + def lex_wf (ha : well_founded ra) (hb : well_founded rb) : well_founded (lex ra rb) := ⟨λ p, destruct p (λ a b, lex_accessible (apply ha a) (well_founded.apply hb) b)⟩ -- relational product is a subrelation of the lex - definition rprod_sub_lex : ∀ a b, rprod ra rb a b → lex ra rb a b := + def rprod_sub_lex : ∀ a b, rprod ra rb a b → lex ra rb a b := λ a b h, prod.rprod.rec_on h (λ a₁ b₁ a₂ b₂ h₁ h₂, lex.left rb a₂ b₂ h₁) -- The relational product of well founded relations is well-founded - definition rprod_wf (ha : well_founded ra) (hb : well_founded rb) : well_founded (rprod ra rb) := + def rprod_wf (ha : well_founded ra) (hb : well_founded rb) : well_founded (rprod ra rb) := subrelation.wf (rprod_sub_lex) (lex_wf ha hb) end