max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init): cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-24 16:38:39 -07:00
parent 49cffc0b20
commit e304d778a1
34 changed files with 304 additions and 336 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
library/init/alternative.lean
View file

@ -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

6
library/init/applicative.lean
View file

@ -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

3
library/init/char.lean
View file

@ -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 :=

16
library/init/classical.lean
View file

@ -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

1
library/init/coe.lean
View file

@ -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

6
library/init/combinator.lean
View file

@ -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

12
library/init/datatypes.lean
View file

@ -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}

3
library/init/functor.lean
View file

@ -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

7
library/init/funext.lean
View file

@ -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))⟩

15
library/init/list.lean
View file

@ -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

15
library/init/list_classes.lean
View file

@ -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⟩

4
library/init/logic.lean
View file

@ -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₂,

13
library/init/monad.lean
View file

@ -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

32
library/init/monad_combinators.lean
View file

@ -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₅)

166
library/init/nat.lean
View file

@ -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)

14
library/init/nat_div.lean
View file

@ -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

18
library/init/num.lean
View file

@ -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

34
library/init/option.lean
View file

@ -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 _}

8
library/init/ordering.lean
View file

@ -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

38
library/init/quot.lean
View file

@ -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₁

26
library/init/relation.lean
View file

@ -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

28
library/init/set.lean
View file

@ -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

6
library/init/setoid.lean
View file

@ -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

2
library/init/sigma.lean
View file

@ -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

25
library/init/sigma_lex.lean
View file

@ -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

30
library/init/state.lean
View file

@ -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

19
library/init/string.lean
View file

@ -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)

6
library/init/subtype.lean
View file

@ -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

2
library/init/timeit.lean
View file

@ -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 ()

14
library/init/to_string.lean
View file

@ -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 ++ ")"

2
library/init/trace.lean
View file

@ -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 ()

4
library/init/unit.lean
View file

@ -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 :=

8
library/init/unsigned.lean
View file

@ -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

48
library/init/wf.lean
View file

@ -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