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

chore(*): don't use upper case letter for type variables, and camelCase for declarations

Browse source
This commit is contained in:
Leonardo de Moura 2016-11-17 14:46:22 -08:00
parent d59bf05f20
commit c816b80855
69 changed files with 1201 additions and 1207 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
library/algebra/order.lean
View file

@ -7,16 +7,15 @@ This ports just the min function and theorems from the lean2 library; additional
functions will be ported in the future.
-/
/- min -/
definition min {A : Type} [has_le A] (a b : A) [decidable (a ≤ b)] : A :=
definition min {α : Type} [has_le α] (a b : α) [decidable (a ≤ b)] : α :=
if a ≤ b then a else b
theorem min_eq_left {A : Type} [has_le A] {a b : A} [decidable (a ≤ b)]
theorem min_eq_left {α : Type} [has_le α] {a b : α} [decidable (a ≤ b)]
(H : a ≤ b) : min a b = a := if_pos H
theorem min_eq_right {A : Type} [weak_order A] {x y : A}
theorem min_eq_right {α : Type} [weak_order α] {x y : α}
[p : decidable (x ≤ y)] (H : (y ≤ x)) : min x y = y :=
let q : decidable (x ≤ y) := p in
match q with
@ -26,7 +25,7 @@ theorem min_eq_right {A : Type} [weak_order A] {x y : A}
| is_false h := if_neg h
end
theorem min_self {A : Type} [has_le A] (x : A) [p : decidable (x ≤ x)] : min x x = x :=
theorem min_self {α : Type} [has_le α] (x : α) [p : decidable (x ≤ x)] : min x x = x :=
let q : decidable (x ≤ x) := p in
match q with
| is_true h := if_pos h

14
library/data/bitvec.lean
View file

@ -80,13 +80,13 @@ section arith
definition neg : bitvec n → bitvec n
| x :=
let f := λy c, (y || c, bxor y c) in
prod.snd (mapAccumR f x ff)
prod.snd (map_accumr f x ff)
-- Add with carry (no overflow)
definition adc : bitvec n → bitvec n → bool → bitvec (n+1)
| x y c :=
let f := λx y c, (bitvec.carry x y c, bitvec.xor3 x y c) in
let z := tuple.mapAccumR₂ f x y c in
let z := tuple.map_accumr₂ f x y c in
prod.fst z :: prod.snd z
definition add : bitvec n → bitvec n → bitvec n
@ -99,7 +99,7 @@ section arith
definition sbb : bitvec n → bitvec n → bool → bool × bitvec n
| x y b :=
let f := λx y c, (bitvec.borrow x y c, bitvec.xor3 x y c) in
tuple.mapAccumR₂ f x y b
tuple.map_accumr₂ f x y b
definition sub : bitvec n → bitvec n → bitvec n
| x y := prod.snd (sbb x y ff)
@ -145,12 +145,12 @@ section comparison
end comparison
section from_bitvec
variable {A : Type}
variable {α : Type}
-- Convert a bitvector to another number.
definition from_bitvec [p : has_add A] [q0 : has_zero A] [q1 : has_one A] {n:nat} (v:bitvec n) : A :=
let f : A → bool → A := λr b, cond b (r + r + 1) (r + r) in
list.foldl f (0 : A) (to_list v)
definition from_bitvec [p : has_add α] [q0 : has_zero α] [q1 : has_one α] {n:nat} (v:bitvec n) : α :=
let f : α → bool → α := λr b, cond b (r + r + 1) (r + r) in
list.foldl f (0 : α) (to_list v)
end from_bitvec

62
library/data/list.lean
View file

@ -15,27 +15,27 @@ namespace list
open nat
variables {A : Type u} { B : Type v } { C : Type w }
variables {α : Type u} {β : Type v} {φ : Type w}
/- length theorems -/
theorem length_append : ∀ (x y : list A), length (x ++ y) = length x + length y
theorem length_append : ∀ (x y : list α), length (x ++ y) = length x + length y
| [] l := eq.symm (nat.zero_add (length l))
| (a::s) l :=
calc nat.succ (length (s ++ l))
= nat.succ (length s + length l) : congr_arg nat.succ (length_append s l)
... = nat.succ (length s) + length l : eq.symm (nat.succ_add (length s) (length l))
theorem length_repeat (a : A) : ∀ (n : ℕ), length (repeat a n) = n
theorem length_repeat (a : α) : ∀ (n : ℕ), length (repeat a n) = n
| 0 := eq.refl 0
| (succ i) := congr_arg succ (length_repeat i)
theorem length_map (f : A → B) : ∀ (a : list A), length (map f a) = length a
theorem length_map (f : α → β) : ∀ (a : list α), length (map f a) = length a
| [] := rfl
| (a :: l) := congr_arg succ (length_map l)
theorem length_dropn
: ∀ (i : ℕ) (l : list A), length (dropn i l) = length l - i
: ∀ (i : ℕ) (l : list α), length (dropn i l) = length l - i
| 0 l := rfl
| (succ i) [] := eq.symm (nat.zero_sub_eq_zero (succ i))
| (succ i) (x::l) := calc
@ -45,13 +45,13 @@ theorem length_dropn
/- firstn -/
def firstn : ℕ → list A → list A
def firstn : ℕ → list α → list α
| 0 l := []
| (succ n) [] := []
| (succ n) (a::l) := a :: firstn n l
theorem length_firstn
: ∀ (i : ℕ) (l : list A), length (firstn i l) = min i (length l)
: ∀ (i : ℕ) (l : list α), length (firstn i l) = min i (length l)
| 0 l := eq.symm (nat.min_zero_left (length l))
| (succ n) [] := eq.symm (nat.min_zero_right (succ n))
| (succ n) (a::l) :=
@ -61,22 +61,22 @@ theorem length_firstn
/- map₂ -/
definition map₂ {A : Type u} {B : Type v} {C : Type w} (f : A → B → C) : list A → list B → list C
definition map₂ {α : Type u} {β : Type v} {φ : Type w} (f : α → β → φ) : list α → list β → list φ
| [] l := []
| l [] := []
| (a::s) (b::t) := f a b :: map₂ s t
theorem map₂_nil_1 {A : Type u} {B : Type v} {C : Type w} (f : A → B → C)
theorem map₂_nil_1 {α : Type u} {β : Type v} {φ : Type w} (f : α → β → φ)
: Π y, map₂ f nil y = nil
| [] := eq.refl nil
| (b::t) := eq.refl nil
theorem map₂_nil_2 {A B C : Type} (f : A → B → C)
: Π (x : list A), map₂ f x nil = nil
theorem map₂_nil_2 {α β φ : Type} (f : α → β → φ)
: Π (x : list α), map₂ f x nil = nil
| [] := eq.refl nil
| (b::t) := eq.refl nil
theorem length_map₂ {A B C : Type} (f : A → B → C)
theorem length_map₂ {α β φ : Type} (f : α → β → φ)
: Π x y, length (map₂ f x y) = min (length x) (length y)
| [] y :=
calc length (map₂ f nil y) = 0 : congr_arg length (map₂_nil_1 f y)
@ -91,51 +91,51 @@ theorem length_map₂ {A B C : Type} (f : A → B → C)
... = min (succ (length x)) (succ (length y))
: eq.symm (min_succ_succ (length x) (length y))
section mapAccumR
variable {S : Type}
section map_accumr
variable {σ : Type}
-- This runs a function over a list returning the intermediate results and a
-- a final result.
definition mapAccumR (f : A → S → S × B) : list A → S → (S × list B)
definition map_accumr (f : α → σ → σ × β) : list α → σ → (σ × list β)
| [] c := (c, [])
| (y::yr) c :=
let r := mapAccumR yr c in
let r := map_accumr yr c in
let z := f y (prod.fst r) in
(prod.fst z, prod.snd z :: prod.snd r)
theorem length_mapAccumR
: ∀ (f : A → S → S × B) (x : list A) (s : S),
length (prod.snd (mapAccumR f x s)) = length x
| f (a::x) s := congr_arg succ (length_mapAccumR f x s)
theorem length_map_accumr
: ∀ (f : α → σ → σ × β) (x : list α) (s : σ),
length (prod.snd (map_accumr f x s)) = length x
| f (a::x) s := congr_arg succ (length_map_accumr f x s)
| f [] s := rfl
end mapAccumR
end map_accumr
section mapAccumR₂
section map_accumr₂
-- This runs a function over two lists returning the intermediate results and a
-- a final result.
definition mapAccumR₂ { A B S C : Type} (f : A → B → S → S × C)
: list A → list B → S → S × list C
definition map_accumr₂ {α β σ φ : Type} (f : α → β → σ → σ × φ)
: list α → list β → σ → σ × list φ
| [] _ c := (c,[])
| _ [] c := (c,[])
| (x::xr) (y::yr) c :=
let r := mapAccumR₂ xr yr c in
let r := map_accumr₂ xr yr c in
let q := f x y (prod.fst r) in
(prod.fst q, prod.snd q :: (prod.snd r))
theorem length_mapAccumR₂ {A B S C : Type }
: ∀ (f : A → B → S → S × C) x y c,
length (prod.snd (mapAccumR₂ f x y c)) = min (length x) (length y)
theorem length_map_accumr₂ {α β σ φ : Type}
: ∀ (f : α → β → σ → σ × φ) x y c,
length (prod.snd (map_accumr₂ f x y c)) = min (length x) (length y)
| f (a::x) (b::y) c := calc
succ (length (prod.snd (mapAccumR₂ f x y c)))
succ (length (prod.snd (map_accumr₂ f x y c)))
= succ (min (length x) (length y))
: congr_arg succ (length_mapAccumR₂ f x y c)
: congr_arg succ (length_map_accumr₂ f x y c)
... = min (succ (length x)) (succ (length y))
: eq.symm (min_succ_succ (length x) (length y))
| f (a::x) [] c := rfl
| f [] (b::y) c := rfl
| f [] [] c := rfl
end mapAccumR₂
end map_accumr₂
end list

62
library/data/tuple.lean
View file

@ -9,15 +9,15 @@ It is implemented as a subtype.
import data.list
import init.subtype
def tuple (A : Type) (n : ℕ) := {l : list A // list.length l = n}
def tuple (α : Type) (n : ℕ) := {l : list α // list.length l = n}
namespace tuple
variables {A B C : Type}
variables {α β φ : Type}
variable {n : ℕ}
definition nil : tuple A 0 := ⟨ [], rfl ⟩
definition nil : tuple α 0 := ⟨ [], rfl ⟩
definition cons : A → tuple A n → tuple A (nat.succ n)
definition cons : α → tuple α n → tuple α (nat.succ n)
| a ⟨ v, h ⟩ := ⟨ a::v, congr_arg nat.succ h ⟩
notation a :: b := cons a b
@ -25,25 +25,25 @@ namespace tuple
open nat
definition head : tuple A (nat.succ n) → A
definition head : tuple α (nat.succ n) → α
| ⟨list.nil, h ⟩ := let q : 0 = succ n := h in by contradiction
| ⟨list.cons a v, h ⟩ := a
theorem head_cons (a : A) : Π (v : tuple A n), head (a :: v) = a
theorem head_cons (a : α) : Π (v : tuple α n), head (a :: v) = a
| ⟨ l, h ⟩ := rfl
definition tail : tuple A (succ n) → tuple A n
definition tail : tuple α (succ n) → tuple α n
| ⟨ list.nil, h ⟩ := let q : 0 = succ n := h in by contradiction
| ⟨ list.cons a v, h ⟩ := ⟨ v, congr_arg pred h ⟩
theorem tail_cons (a : A) : Π (v : tuple A n), tail (a :: v) = v
theorem tail_cons (a : α) : Π (v : tuple α n), tail (a :: v) = v
| ⟨ l, h ⟩ := rfl
definition to_list : tuple A n → list A | ⟨ l, h ⟩ := l
definition to_list : tuple α n → list α | ⟨ l, h ⟩ := l
/- append -/
definition append {n m : nat} : tuple A n → tuple A m → tuple A (n + m)
definition append {n m : nat} : tuple α n → tuple α m → tuple α (n + m)
| ⟨ l₁, h₁ ⟩ ⟨ l₂, h₂ ⟩ :=
let p := calc
list.length (l₁ ++ l₂)
@ -54,21 +54,21 @@ namespace tuple
/- map -/
definition map (f : A → B) : tuple A n → tuple B n
definition map (f : α → β) : tuple α n → tuple β n
| ⟨ l, h ⟩ :=
let q := calc list.length (list.map f l) = list.length l : list.length_map f l
... = n : h in
⟨ list.map f l, q ⟩
theorem map_nil (f : A → B) : map f nil = nil := rfl
theorem map_nil (f : α → β) : map f nil = nil := rfl
theorem map_cons (f : A → B) (a : A)
: Π (v : tuple A n), map f (a::v) = f a :: map f v
theorem map_cons (f : α → β) (a : α)
: Π (v : tuple α n), map f (a::v) = f a :: map f v
| ⟨ l, h ⟩ := rfl
definition map₂ (f : A → B → C) : tuple A n → tuple B n → tuple C n
definition map₂ (f : α → β → φ) : tuple α n → tuple β n → tuple φ n
| ⟨ x, px ⟩ ⟨ y, py ⟩ :=
let z : list C := list.map₂ f x y in
let z : list φ := list.map₂ f x y in
let pxx : list.length x = n := px in
let pyy : list.length y = n := py in
let p : list.length z = n := calc
@ -77,40 +77,40 @@ namespace tuple
... = n : min_self n in
⟨ z, p ⟩
definition repeat (a : A) : tuple A n
definition repeat (a : α) : tuple α n
:= ⟨ list.repeat a n, list.length_repeat a n ⟩
definition dropn : Π (i:ℕ), tuple A n → tuple A (n - i)
definition dropn : Π (i:ℕ), tuple α n → tuple α (n - i)
| i ⟨ l, p ⟩ := ⟨ list.dropn i l, p ▸ list.length_dropn i l ⟩
definition firstn : Π (i:ℕ) {p:i ≤ n}, tuple A n → tuple A i
| i isLe ⟨ l, p ⟩ :=
definition firstn : Π (i:ℕ) {p:i ≤ n}, tuple α n → tuple α i
| i is_le ⟨ l, p ⟩ :=
let q := calc list.length (list.firstn i l)
= min i (list.length l) : list.length_firstn i l
... = min i n : congr_arg (λ v, min i v) p
... = i : min_eq_left isLe in
... = i : min_eq_left is_le in
⟨ list.firstn i l, q ⟩
section accum
open prod
variable {S : Type}
variable {σ : Type}
definition mapAccumR
: (A → S → S × B) → tuple A n → S → S × tuple B n
definition map_accumr
: (α → σ → σ × β) → tuple α n → σ → σ × tuple β n
| f ⟨ x, px ⟩ c :=
let z := list.mapAccumR f x c in
let p := eq.trans (list.length_mapAccumR f x c) px in
let z := list.map_accumr f x c in
let p := eq.trans (list.length_map_accumr f x c) px in
(prod.fst z, ⟨ prod.snd z, p ⟩)
definition mapAccumR₂
: (A → B → S → S × C) → tuple A n → tuple B n → S → S × tuple C n
definition map_accumr₂
: (α → β → σ → σ × φ) → tuple α n → tuple β n → σ → σ × tuple φ n
| f ⟨ x, px ⟩ ⟨ y, py ⟩ c :=
let z := list.mapAccumR₂ f x y c in
let z := list.map_accumr₂ f x y c in
let pxx : list.length x = n := px in
let pyy : list.length y = n := py in
let p := calc
list.length (prod.snd (list.mapAccumR₂ f x y c))
= min (list.length x) (list.length y) : list.length_mapAccumR₂ f x y c
list.length (prod.snd (list.map_accumr₂ f x y c))
= min (list.length x) (list.length y) : list.length_map_accumr₂ f x y c
... = n : by rewrite [ pxx, pyy, min_self ] in
(prod.fst z, ⟨prod.snd z, p ⟩)

64
library/init/algebra.lean
View file

@ -11,55 +11,55 @@ import init.logic init.binary init.combinator init.meta.interactive init.meta.de
set_option default_priority 100
universe variable u
variables {A : Type u}
variables {α : Type u}
class semigroup (A : Type u) extends has_mul A :=
(mul_assoc : ∀ a b c : A, a * b * c = a * (b * c))
class semigroup (α : Type u) extends has_mul α :=
(mul_assoc : ∀ a b c : α, a * b * c = a * (b * c))
class comm_semigroup (A : Type u) extends semigroup A :=
(mul_comm : ∀ a b : A, a * b = b * a)
class comm_semigroup (α : Type u) extends semigroup α :=
(mul_comm : ∀ a b : α, a * b = b * a)
class left_cancel_semigroup (A : Type u) extends semigroup A :=
(mul_left_cancel : ∀ a b c : A, a * b = a * c → b = c)
class left_cancel_semigroup (α : Type u) extends semigroup α :=
(mul_left_cancel : ∀ a b c : α, a * b = a * c → b = c)
class right_cancel_semigroup (A : Type u) extends semigroup A :=
(mul_right_cancel : ∀ a b c : A, a * b = c * b → a = c)
class right_cancel_semigroup (α : Type u) extends semigroup α :=
(mul_right_cancel : ∀ a b c : α, a * b = c * b → a = c)
class monoid (A : Type u) extends semigroup A, has_one A :=
(one_mul : ∀ a : A, 1 * a = a) (mul_one : ∀ a : A, a * 1 = a)
class monoid (α : Type u) extends semigroup α, has_one α :=
(one_mul : ∀ a : α, 1 * a = a) (mul_one : ∀ a : α, a * 1 = a)
class comm_monoid (A : Type u) extends monoid A, comm_semigroup A
class comm_monoid (α : Type u) extends monoid α, comm_semigroup α
class group (A : Type u) extends monoid A, has_inv A :=
(mul_left_inv : ∀ a : A, a⁻¹ * a = 1)
class group (α : Type u) extends monoid α, has_inv α :=
(mul_left_inv : ∀ a : α, a⁻¹ * a = 1)
class comm_group (A : Type u) extends group A, comm_monoid A
class comm_group (α : Type u) extends group α, comm_monoid α
@[simp] lemma mul_assoc [semigroup A] : ∀ a b c : A, a * b * c = a * (b * c) :=
@[simp] lemma mul_assoc [semigroup α] : ∀ a b c : α, a * b * c = a * (b * c) :=
semigroup.mul_assoc
@[simp] lemma mul_comm [comm_semigroup A] : ∀ a b : A, a * b = b * a :=
@[simp] lemma mul_comm [comm_semigroup α] : ∀ a b : α, a * b = b * a :=
comm_semigroup.mul_comm
@[simp] lemma mul_left_comm [comm_semigroup A] : ∀ a b c : A, a * (b * c) = b * (a * c) :=
@[simp] lemma mul_left_comm [comm_semigroup α] : ∀ a b c : α, a * (b * c) = b * (a * c) :=
left_comm mul mul_comm mul_assoc
lemma mul_left_cancel [left_cancel_semigroup A] {a b c : A} : a * b = a * c → b = c :=
lemma mul_left_cancel [left_cancel_semigroup α] {a b c : α} : a * b = a * c → b = c :=
left_cancel_semigroup.mul_left_cancel a b c
lemma mul_right_cancel [right_cancel_semigroup A] {a b c : A} : a * b = c * b → a = c :=
lemma mul_right_cancel [right_cancel_semigroup α] {a b c : α} : a * b = c * b → a = c :=
right_cancel_semigroup.mul_right_cancel a b c
@[simp] lemma one_mul [monoid A] : ∀ a : A, 1 * a = a :=
@[simp] lemma one_mul [monoid α] : ∀ a : α, 1 * a = a :=
monoid.one_mul
@[simp] lemma mul_one [monoid A] : ∀ a : A, a * 1 = a :=
@[simp] lemma mul_one [monoid α] : ∀ a : α, a * 1 = a :=
monoid.mul_one
@[simp] lemma mul_left_inv [group A] : ∀ a : A, a⁻¹ * a = 1 :=
@[simp] lemma mul_left_inv [group α] : ∀ a : α, a⁻¹ * a = 1 :=
group.mul_left_inv
/- Additive "sister" structures.
/- αdditive "sister" structures.
Example, add_semigroup mirrors semigroup.
These structures exist just to help automation.
In an alternative design, we could have the binary operation as an
@ -67,8 +67,8 @@ group.mul_left_inv
would be hard to index since they would not contain any constant.
For example, mul_assoc would be
lemma mul_assoc {A : Type u} {op : A → A → A} [semigroup A op] :
∀ a b c : A, op (op a b) c = op a (op b c) :=
lemma mul_assoc {α : Type u} {op : α → α → α} [semigroup α op] :
∀ a b c : α, op (op a b) c = op a (op b c) :=
semigroup.mul_assoc
The simplifier cannot effectively use this lemma since the pattern for
@ -87,12 +87,12 @@ group.mul_left_inv
@[class] def add_comm_monoid := comm_monoid
@[class] def add_comm_group := comm_group
instance add_semigroup.to_has_add {A : Type u} [s : add_semigroup A] : has_add A :=
⟨@semigroup.mul A s⟩
instance add_monoid.to_has_zero {A : Type u} [s : add_monoid A] : has_zero A :=
⟨@monoid.one A s⟩
instance add_group.to_has_neg {A : Type u} [s : add_group A] : has_neg A :=
⟨@group.inv A s⟩
instance add_semigroup.to_has_add {α : Type u} [s : add_semigroup α] : has_add α :=
⟨@semigroup.mul α s⟩
instance add_monoid.to_has_zero {α : Type u} [s : add_monoid α] : has_zero α :=
⟨@monoid.one α s⟩
instance add_group.to_has_neg {α : Type u} [s : add_group α] : has_neg α :=
⟨@group.inv α s⟩
meta def multiplicative_to_additive : name_map name :=
rb_map.of_list $

16
library/init/alternative.lean
View file

@ -7,17 +7,17 @@ prelude
import init.logic init.applicative
universe variables u v
class alternative (F : Type u → Type v) extends applicative F : Type (max u+1 v) :=
(failure : Π {A : Type u}, F A)
(orelse : Π {A : Type u}, F A → F A → F A)
class alternative (f : Type u → Type v) extends applicative f : Type (max u+1 v) :=
(failure : Π {a : Type u}, f a)
(orelse : Π {a : Type u}, f a → f a → f a)
@[inline] def failure {F : Type u → Type v} [alternative F] {A : Type u} : F A :=
alternative.failure F
@[inline] def failure {f : Type u → Type v} [alternative f] {a : Type u} : f a :=
alternative.failure f
@[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
@[inline] def guard {F : Type → Type v} [alternative F] (P : Prop) [decidable P] : F unit :=
if P then pure () else failure
@[inline] def guard {f : Type → Type v} [alternative f] (p : Prop) [decidable p] : f unit :=
if p then pure () else failure

12
library/init/applicative.lean
View file

@ -7,14 +7,14 @@ prelude
import init.functor
universe variables u v
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)
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)
@[inline] def pure {F : Type u → Type v} [applicative F] {A : Type u} : A → F A :=
applicative.pure F
@[inline] def pure {f : Type u → Type v} [applicative f] {a : Type u} : a → f a :=
applicative.pure f
@[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

18
library/init/binary.lean
View file

@ -1,7 +1,7 @@
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Jeremy Avigad
αuthors: Leonardo de Moura, Jeremy αvigad
General properties of binary operations.
-/
@ -9,14 +9,14 @@ prelude
import init.logic
universe variables u v
variable {A : Type u}
variable {B : Type v}
variable f : A → A → A
variable inv : A → A
variable one : A
variable {α : Type u}
variable {β : Type v}
variable f : α → α → α
variable inv : α → α
variable one : α
local notation a * b := f a b
local notation a ⁻¹ := inv a
variable g : A → A → A
variable g : α → α → α
local notation a + b := g a b
def commutative := ∀ a b, a * b = b * a
@ -28,8 +28,8 @@ def left_cancelative := ∀ a b c, a * b = a * c → b = c
def right_cancelative := ∀ a b c, a * b = c * b → a = c
def left_distributive := ∀ a b c, a * (b + c) = a * b + a * c
def right_distributive := ∀ a b c, (a + b) * c = a * c + b * c
def right_commutative (h : B → A → B) := ∀ b a₁ a₂, h (h b a₁) a₂ = h (h b a₂) a₁
def left_commutative (h : A → B → B) := ∀ a₁ a₂ b, h a₁ (h a₂ b) = h a₂ (h a₁ b)
def right_commutative (h : β → α → β) := ∀ b a₁ a₂, h (h b a₁) a₂ = h (h b a₂) a₁
def left_commutative (h : α → β → β) := ∀ a₁ a₂ b, h a₁ (h a₂ b) = h a₂ (h a₁ b)
lemma left_comm : commutative f → associative f → left_commutative f :=
assume hcomm hassoc, take a b c, calc

10
library/init/bool.lean
View file

@ -4,9 +4,9 @@
prelude
import init.core
@[inline] def {u} cond {A : Type u} : bool → A → A → A
| tt a b := a
| ff a b := b
@[inline] def {u} cond {a : Type u} : bool → a → a → a
| tt x y := x
| ff x y := y
@[inline] def bor : bool → bool → bool
| tt _ := tt
@ -27,5 +27,5 @@ import init.core
| ff tt := tt
| _ _ := ff
notation a || b := bor a b
notation a && b := band a b
notation x || y := bor x y
notation x && y := band x y

2
library/init/char.lean
View file

@ -17,7 +17,7 @@ private lemma zero_lt_char_sz : 0 < char_sz :=
zero_lt_succ _
@[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
if h : n < char_sz then fin.mk n h else fin.mk 0 zero_lt_char_sz
def to_nat (c : char) : nat :=
fin.val c

60
library/init/classical.lean
View file

@ -12,54 +12,54 @@ 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 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}
theorem exists_true_of_nonempty {A : Type u} (h : nonempty A) : ∃ x : A, true :=
theorem exists_true_of_nonempty {a : Type u} (h : nonempty a) : ∃ x : a, true :=
nonempty.elim h (take x, ⟨x, trivial⟩)
noncomputable def inhabited_of_nonempty {A : Type u} (h : nonempty A) : inhabited A :=
noncomputable def inhabited_of_nonempty {a : Type u} (h : nonempty a) : inhabited a :=
⟨elt_of (strong_indefinite_description (λ a, true) h)⟩
noncomputable def inhabited_of_exists {A : Type u} {p : A → Prop} (H : ∃ x, p x) : inhabited A :=
inhabited_of_nonempty (exists.elim H (λ w Hw, ⟨w⟩))
noncomputable def inhabited_of_exists {a : Type u} {p : a → Prop} (h : ∃ x, p x) : inhabited a :=
inhabited_of_nonempty (exists.elim h (λ w hw, ⟨w⟩))
/- the Hilbert epsilon function -/
noncomputable def epsilon {A : Type u} [h : nonempty A] (p : A → Prop) : A :=
noncomputable def epsilon {a : Type u} [h : nonempty a] (p : a → Prop) : a :=
elt_of (strong_indefinite_description p h)
theorem epsilon_spec_aux {A : Type u} (h : nonempty A) (p : A → Prop) (hex : ∃ y, p y) :
p (@epsilon A h p) :=
theorem epsilon_spec_aux {a : Type u} (h : nonempty a) (p : a → Prop) (hex : ∃ y, p y) :
p (@epsilon a h p) :=
have aux : (∃ y, p y) → p (elt_of (strong_indefinite_description p h)), from has_property (strong_indefinite_description p h),
aux hex
theorem epsilon_spec {A : Type u} {p : A → Prop} (hex : ∃ y, p y) :
p (@epsilon A (nonempty_of_exists hex) p) :=
theorem epsilon_spec {a : Type u} {p : a → Prop} (hex : ∃ y, p y) :
p (@epsilon a (nonempty_of_exists hex) p) :=
epsilon_spec_aux (nonempty_of_exists hex) p hex
theorem epsilon_singleton {A : Type u} (a : A) : @epsilon A ⟨a⟩ (λ x, x = a) = a :=
@epsilon_spec A (λ x, x = a) ⟨a, rfl⟩
theorem epsilon_singleton {a : Type u} (x : a) : @epsilon a ⟨x⟩ (λ y, y = x) = x :=
@epsilon_spec a (λ y, y = x) ⟨x, rfl⟩
noncomputable def some {A : Type u} {p : A → Prop} (h : ∃ x, p x) : A :=
@epsilon A (nonempty_of_exists h) p
noncomputable def some {a : Type u} {p : a → Prop} (h : ∃ x, p x) : a :=
@epsilon a (nonempty_of_exists h) p
theorem some_spec {A : Type u} {p : A → Prop} (h : ∃ x, p x) : p (some h) :=
theorem some_spec {a : Type u} {p : a → Prop} (h : ∃ x, p x) : p (some h) :=
epsilon_spec h
/- the axiom of choice -/
theorem axiom_of_choice {A : Type u} {B : A → Type v} {R : Π x, B x → Prop} (h : ∀ x, ∃ y, R x y) :
∃ (f : Π x, B x), ∀ x, R x (f x) :=
have h : ∀ x, R x (some (h x)), from take x, some_spec (h x),
theorem axiom_of_choice {a : Type u} {b : a → Type v} {r : Π x, b x → Prop} (h : ∀ x, ∃ y, r x y) :
∃ (f : Π x, b x), ∀ x, r x (f x) :=
have h : ∀ x, r x (some (h x)), from take x, some_spec (h x),
⟨_, h⟩
theorem skolem {A : Type u} {B : A → Type v} {p : Π x, B x → Prop} :
(∀ x, ∃ y, p x y) ↔ ∃ (f : Π x, B x) , (∀ x, p x (f x)) :=
theorem skolem {a : Type u} {b : a → Type v} {p : Π x, b x → Prop} :
(∀ x, ∃ y, p x y) ↔ ∃ (f : Π x, b x) , (∀ x, p x (f x)) :=
iff.intro
(assume h : (∀ x, ∃ y, p x y), axiom_of_choice h)
(assume h : (∃ (f : Π x, B x), (∀ x, p x (f x))),
take x, exists.elim h (λ (fw : ∀ x, B x) (hw : ∀ x, p x (fw x)),
(assume h : (∃ (f : Π x, b x), (∀ x, p x (f x))),
take x, exists.elim h (λ (fw : ∀ x, b x) (hw : ∀ x, p x (fw x)),
⟨fw x, hw x⟩))
/-
Prove excluded middle using hilbert's choice
@ -95,9 +95,9 @@ assume hp : p,
have hpred : U = V, from
funext (take x : Prop,
have hl : (x = true ∨ p) → (x = false ∨ p), from
assume A, or.inr hp,
assume a, or.inr hp,
have hr : (x = false ∨ p) → (x = true ∨ p), from
assume A, or.inr hp,
assume a, or.inr hp,
show (x = true ∨ p) = (x = false ∨ p), from
propext (iff.intro hl hr)),
have h' : epsilon U = epsilon V, from hpred ▸ rfl,
@ -160,7 +160,7 @@ have (a ↔ true) = a, from propext (iff_true a),
eq.subst (@iff_eq_eq a true) this
end aux
/- All propositions are decidable -/
/- αll propositions are decidable -/
noncomputable def decidable_inhabited (a : Prop) : inhabited (decidable a) :=
inhabited_of_nonempty
(or.elim (em a)
@ -172,11 +172,11 @@ noncomputable def prop_decidable (a : Prop) : decidable a :=
arbitrary (decidable a)
local attribute [instance] prop_decidable
noncomputable def type_decidable_eq (A : Type u) : decidable_eq A :=
λ a b, prop_decidable (a = b)
noncomputable def type_decidable_eq (a : Type u) : decidable_eq a :=
λ x y, prop_decidable (x = y)
noncomputable def type_decidable (A : Type u) : sum A (A → false) :=
match (prop_decidable (nonempty A)) with
noncomputable def type_decidable (a : Type u) : sum a (a → false) :=
match (prop_decidable (nonempty a)) with
| (is_true hp) := sum.inl (@inhabited.default _ (inhabited_of_nonempty hp))
| (is_false hn) := sum.inr (λ a, absurd (nonempty.intro a) hn)
end

126
library/init/coe.lean
View file

@ -27,123 +27,123 @@ prelude
import init.list init.subtype init.prod
universe variables u v
class has_lift (A : Type u) (B : Type v) :=
(lift : A → B)
class has_lift (a : Type u) (b : Type v) :=
(lift : a → b)
/- Auxiliary class that contains the transitive closure of has_lift. -/
class has_lift_t (A : Type u) (B : Type v) :=
(lift : A → B)
/- auxiliary class that contains the transitive closure of has_lift. -/
class has_lift_t (a : Type u) (b : Type v) :=
(lift : a → b)
class has_coe (A : Type u) (B : Type v) :=
(coe : A → B)
class has_coe (a : Type u) (b : Type v) :=
(coe : a → b)
/- Auxiliary class that contains the transitive closure of has_coe. -/
class has_coe_t (A : Type u) (B : Type v) :=
(coe : A → B)
/- auxiliary class that contains the transitive closure of has_coe. -/
class has_coe_t (a : Type u) (b : Type v) :=
(coe : a → b)
class has_coe_to_fun (A : Type u) : Type (max u (v+1)) :=
(F : A → Type v) (coe : Π a, F a)
class has_coe_to_fun (a : Type u) : Type (max u (v+1)) :=
(F : a → Type v) (coe : Π x, F x)
class has_coe_to_sort (A : Type u) : Type (max u (v+1)) :=
(S : Type v) (coe : A → S)
class has_coe_to_sort (a : Type u) : Type (max u (v+1)) :=
(S : Type v) (coe : a → S)
def lift {A : Type u} {B : Type v} [has_lift A B] : A → B :=
@has_lift.lift A B _
def lift {a : Type u} {b : Type v} [has_lift a b] : a → b :=
@has_lift.lift a b _
def lift_t {A : Type u} {B : Type v} [has_lift_t A B] : A → B :=
@has_lift_t.lift A B _
def lift_t {a : Type u} {b : Type v} [has_lift_t a b] : a → b :=
@has_lift_t.lift a b _
def coe_b {A : Type u} {B : Type v} [has_coe A B] : A → B :=
@has_coe.coe A B _
def coe_b {a : Type u} {b : Type v} [has_coe a b] : a → b :=
@has_coe.coe a b _
def coe_t {A : Type u} {B : Type v} [has_coe_t A B] : A → B :=
@has_coe_t.coe A B _
def coe_t {a : Type u} {b : Type v} [has_coe_t a b] : a → b :=
@has_coe_t.coe a b _
def coe_fn_b {A : Type u} [has_coe_to_fun.{u v} A] : Π a : A, has_coe_to_fun.F.{u v} a :=
def coe_fn_b {a : Type u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x :=
has_coe_to_fun.coe
/- User level coercion operators -/
def coe {A : Type u} {B : Type v} [has_lift_t A B] : A → B :=
def coe {a : Type u} {b : Type v} [has_lift_t a b] : a → b :=
lift_t
def coe_fn {A : Type u} [has_coe_to_fun.{u v} A] : Π a : A, has_coe_to_fun.F.{u v} a :=
def coe_fn {a : Type u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x :=
has_coe_to_fun.coe
def coe_sort {A : Type u} [has_coe_to_sort.{u v} A] : A → has_coe_to_sort.S.{u v} A :=
def coe_sort {a : Type u} [has_coe_to_sort.{u v} a] : a → has_coe_to_sort.S.{u v} a :=
has_coe_to_sort.coe
/- Notation -/
notation `↑`:max a:max := coe a
notation `↑`:max x:max := coe x
notation `⇑`:max a:max := coe_fn a
notation `⇑`:max x:max := coe_fn x
notation `↥`:max a:max := coe_sort a
notation `↥`:max x:max := coe_sort x
universe variables u₁ u₂ u₃
/- Transitive closure for has_lift, has_coe, has_coe_to_fun -/
instance lift_trans {A : Type u₁} {B : Type u₂} {C : Type u₃} [has_lift A B] [has_lift_t B C] : has_lift_t A C :=
⟨λ a, lift_t (lift a : B)⟩
instance lift_trans {a : Type u₁} {b : Type u₂} {c : Type u₃} [has_lift a b] [has_lift_t b c] : has_lift_t a c :=
⟨λ x, lift_t (lift x : b)⟩
instance lift_base {A : Type u} {B : Type v} [has_lift A B] : has_lift_t A B :=
instance lift_base {a : Type u} {b : Type v} [has_lift a b] : has_lift_t a b :=
⟨lift⟩
instance coe_trans {A : Type u₁} {B : Type u₂} {C : Type u₃} [has_coe A B] [has_coe_t B C] : has_coe_t A C :=
⟨λ a, coe_t (coe_b a : B)⟩
instance coe_trans {a : Type u₁} {b : Type u₂} {c : Type u₃} [has_coe a b] [has_coe_t b c] : has_coe_t a c :=
⟨λ x, coe_t (coe_b x : b)⟩
instance coe_base {A : Type u} {B : Type v} [has_coe A B] : has_coe_t A B :=
instance coe_base {a : Type u} {b : Type v} [has_coe a b] : has_coe_t a b :=
⟨coe_b⟩
instance coe_fn_trans {A : Type u₁} {B : Type u₂} [has_lift_t A B] [has_coe_to_fun.{u₂ u₃} B] : has_coe_to_fun.{u₁ u₃} A :=
{ F := λ a, @has_coe_to_fun.F.{u₂ u₃} B _ (coe a),
coe := λ a, coe_fn (coe a) }
instance coe_fn_trans {a : Type u₁} {b : Type u₂} [has_lift_t a b] [has_coe_to_fun.{u₂ u₃} b] : has_coe_to_fun.{u₁ u₃} a :=
{ F := λ x, @has_coe_to_fun.F.{u₂ u₃} b _ (coe x),
coe := λ x, coe_fn (coe x) }
instance coe_sort_trans {A : Type u₁} {B : Type u₂} [has_lift_t A B] [has_coe_to_sort.{u₂ u₃} B] : has_coe_to_sort.{u₁ u₃} A :=
{ S := has_coe_to_sort.S.{u₂ u₃} B,
coe := λ a, coe_sort (coe a) }
instance coe_sort_trans {a : Type u₁} {b : Type u₂} [has_lift_t a b] [has_coe_to_sort.{u₂ u₃} b] : has_coe_to_sort.{u₁ u₃} a :=
{ S := has_coe_to_sort.S.{u₂ u₃} b,
coe := λ x, coe_sort (coe x) }
/- Every coercion is also a lift -/
instance coe_to_lift {A : Type u} {B : Type v} [has_coe_t A B] : has_lift_t A B :=
instance coe_to_lift {a : Type u} {b : Type v} [has_coe_t a b] : has_lift_t a b :=
⟨coe_t⟩
/- Basic coercions -/
/- basic coercions -/
instance coe_bool_to_Prop : has_coe bool Prop :=
⟨λ b, b = tt⟩
⟨λ y, y = tt⟩
instance coe_decidable_eq (b : bool) : decidable (coe b) :=
show decidable (b = tt), from bool.decidable_eq b tt
instance coe_decidable_eq (x : bool) : decidable (coe x) :=
show decidable (x = tt), from bool.decidable_eq x tt
instance coe_subtype {A : Type u} {p : A → Prop} : has_coe {a // p a} A :=
instance coe_subtype {a : Type u} {p : a → Prop} : has_coe {x // p x} a :=
⟨λ s, subtype.elt_of s⟩
/- Basic lifts -/
/- basic lifts -/
universe variables ua ua₁ ua₂ ub ub₁ ub₂
/- Remark: we can't use [has_lift_t A₂ A₁] since it will produce non-termination whenever a type class resolution
/- Remark: we cant use [has_lift_t a₂ a₁] since it will produce non-termination whenever a type class resolution
problem does not have a solution. -/
instance lift_fn {A₁ : Type ua₁} {A₂ : Type ua₂} {B₁ : Type ub₁} {B₂ : Type ub₂} [has_lift A₂ A₁] [has_lift_t B₁ B₂] : has_lift (A₁ → B₁) (A₂ → B₂) :=
⟨λ f a, ↑(f ↑a)⟩
instance lift_fn {a₁ : Type ua₁} {a₂ : Type ua₂} {b₁ : Type ub₁} {b₂ : Type ub₂} [has_lift a₂ a₁] [has_lift_t b₁ b₂] : has_lift (a₁ → b₁) (a₂ → b₂) :=
⟨λ f x, ↑(f ↑x)⟩
instance lift_fn_range {A : Type ua} {B₁ : Type ub₁} {B₂ : Type ub₂} [has_lift_t B₁ B₂] : has_lift (A → B₁) (A → B₂) :=
⟨λ f a, ↑(f a)⟩
instance lift_fn_range {a : Type ua} {b₁ : Type ub₁} {b₂ : Type ub₂} [has_lift_t b₁ b₂] : has_lift (a → b₁) (a → b₂) :=
⟨λ f x, ↑(f x)⟩
instance lift_fn_dom {A₁ : Type ua₁} {A₂ : Type ua₂} {B : Type ub} [has_lift A₂ A₁] : has_lift (A₁ → B) (A₂ → B) :=
⟨λ f a, f ↑a⟩
instance lift_fn_dom {a₁ : Type ua₁} {a₂ : Type ua₂} {b : Type ub} [has_lift a₂ a₁] : has_lift (a₁ → b) (a₂ → b) :=
⟨λ f x, f ↑x⟩
instance lift_pair {A₁ : Type ua₁} {A₂ : Type ub₂} {B₁ : Type ub₁} {B₂ : Type ub₂} [has_lift_t A₁ A₂] [has_lift_t B₁ B₂] : has_lift (A₁ × B₁) (A₂ × B₂) :=
⟨λ p, prod.cases_on p (λ a b, (↑a, ↑b))⟩
instance lift_pair {a₁ : Type ua₁} {a₂ : Type ub₂} {b₁ : Type ub₁} {b₂ : Type ub₂} [has_lift_t a₁ a₂] [has_lift_t b₁ b₂] : has_lift (a₁ × b₁) (a₂ × b₂) :=
⟨λ p, prod.cases_on p (λ x y, (↑x, ↑y))⟩
instance lift_pair₁ {A₁ : Type ua₁} {A₂ : Type ua₂} {B : Type ub} [has_lift_t A₁ A₂] : has_lift (A₁ × B) (A₂ × B) :=
⟨λ p, prod.cases_on p (λ a b, (↑a, b))⟩
instance lift_pair₁ {a₁ : Type ua₁} {a₂ : Type ua₂} {b : Type ub} [has_lift_t a₁ a₂] : has_lift (a₁ × b) (a₂ × b) :=
⟨λ p, prod.cases_on p (λ x y, (↑x, y))⟩
instance lift_pair₂ {A : Type ua} {B₁ : Type ub₁} {B₂ : Type ub₂} [has_lift_t B₁ B₂] : has_lift (A × B₁) (A × B₂) :=
⟨λ p, prod.cases_on p (λ a b, (a, ↑b))⟩
instance lift_pair₂ {a : Type ua} {b₁ : Type ub₁} {b₂ : Type ub₂} [has_lift_t b₁ b₂] : has_lift (a × b₁) (a × b₂) :=
⟨λ p, prod.cases_on p (λ x y, (x, ↑y))⟩
instance lift_list {A : Type u} {B : Type v} [has_lift_t A B] : has_lift (list A) (list B) :=
⟨λ l, list.map (@coe A B _) l⟩
instance lift_list {a : Type u} {b : Type v} [has_lift_t a b] : has_lift (list a) (list b) :=
⟨λ l, list.map (@coe a b _) l⟩

6
library/init/combinator.lean
View file

@ -7,7 +7,7 @@ prelude
/- Combinator calculus -/
namespace combinator
universe variables u₁ u₂ u₃
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)
def I {α : Type u₁} (a : α) := a
def K {α : Type u₁} {β : Type u₂} (a : α) (b : β) := a
def S {α : Type u₁} {β : Type u₂} {γ : Type u₃} (x : α → β → γ) (y : α → β) (z : α) := x z (y z)
end combinator

2
library/init/congr.lean
View file

@ -9,7 +9,7 @@ prelude
import init.quot
universe variables u v
lemma forall_congr_eq {A : Type u} {p q : A → Prop} (h : ∀ a, p a = q a) : (∀ a, p a) = ∀ a, q a :=
lemma forall_congr_eq {a : Type u} {p q : a → Prop} (h : ∀ x, p x = q x) : (∀ x, p x) = ∀ x, q x :=
propext (forall_congr (λ a, (h a)^.to_iff))
lemma imp_congr_eq {a b c d : Prop} (h₁ : a = c) (h₂ : b = d) : (a → b) = (c → d) :=

222
library/init/core.lean
View file

@ -97,44 +97,44 @@ inductive empty : Type
def not (a : Prop) := a → false
prefix `¬` := not
inductive eq {A : Type u} (a : A) : A → Prop
inductive eq {α : Type u} (a : α) : α → Prop
| refl : eq a
inductive heq {A : Type u} (a : A) : Π {B : Type u}, B → Prop
inductive heq {α : Type u} (a : α) : Π {β : Type u}, β → Prop
| refl : heq a
structure prod (A : Type u) (B : Type v) :=
(fst : A) (snd : B)
structure prod (α : Type u) (β : Type v) :=
(fst : α) (snd : β)
inductive and (a b : Prop) : Prop
| intro : a → b → and
def and.elim_left {a b : Prop} (H : and a b) : a :=
and.rec (λ Ha Hb, Ha) H
def and.elim_left {a b : Prop} (h : and a b) : a :=
and.rec (λ ha hb, ha) h
def and.left := @and.elim_left
def and.elim_right {a b : Prop} (H : and a b) : b :=
and.rec (λ Ha Hb, Hb) H
def and.elim_right {a b : Prop} (h : and a b) : b :=
and.rec (λ ha hb, hb) h
def and.right := @and.elim_right
inductive sum (A : Type u) (B : Type v)
| inl {} : A → sum
| inr {} : B → sum
inductive sum (α : Type u) (β : Type v)
| inl {} : α → sum
| inr {} : β → sum
inductive or (a b : Prop) : Prop
| inl {} : a → or
| inr {} : b → or
def or.intro_left {a : Prop} (b : Prop) (Ha : a) : or a b :=
or.inl Ha
def or.intro_left {a : Prop} (b : Prop) (ha : a) : or a b :=
or.inl ha
def or.intro_right (a : Prop) {b : Prop} (Hb : b) : or a b :=
or.inr Hb
def or.intro_right (a : Prop) {b : Prop} (hb : b) : or a b :=
or.inr hb
structure sigma {A : Type u} (B : A → Type v) :=
mk :: (fst : A) (snd : B fst)
structure sigma {α : Type u} (β : α → Type v) :=
mk :: (fst : α) (snd : β fst)
inductive pos_num : Type
| one : pos_num
@ -168,20 +168,20 @@ class inductive decidable (p : Prop)
| is_true : p → decidable
@[reducible]
def decidable_pred {A : Type u} (r : A → Prop) :=
Π (a : A), decidable (r a)
def decidable_pred {α : Type u} (r : α → Prop) :=
Π (a : α), decidable (r a)
@[reducible]
def decidable_rel {A : Type u} (r : A → A → Prop) :=
Π (a b : A), decidable (r a b)
def decidable_rel {α : Type u} (r : α → α → Prop) :=
Π (a b : α), decidable (r a b)
@[reducible]
def decidable_eq (A : Type u) :=
decidable_rel (@eq A)
def decidable_eq (α : Type u) :=
decidable_rel (@eq α)
inductive option (A : Type u)
inductive option (α : Type u)
| none {} : option
| some : A → option
| some : α → option
export option (none some)
export bool (ff tt)
@ -195,7 +195,7 @@ inductive nat
| succ : nat → nat
structure unification_constraint :=
{A : Type u} (lhs : A) (rhs : A)
{α : Type u} (lhs : α) (rhs : α)
infix ` ≟ `:50 := unification_constraint.mk
infix ` =?= `:50 := unification_constraint.mk
@ -206,82 +206,82 @@ structure unification_hint :=
/- Declare builtin and reserved notation -/
class has_zero (A : Type u) := (zero : A)
class has_one (A : Type u) := (one : A)
class has_add (A : Type u) := (add : A → A → A)
class has_mul (A : Type u) := (mul : A → A → A)
class has_inv (A : Type u) := (inv : A → A)
class has_neg (A : Type u) := (neg : A → A)
class has_sub (A : Type u) := (sub : A → A → A)
class has_div (A : Type u) := (div : A → A → A)
class has_dvd (A : Type u) := (dvd : A → A → Prop)
class has_mod (A : Type u) := (mod : A → A → A)
class has_le (A : Type u) := (le : A → A → Prop)
class has_lt (A : Type u) := (lt : A → A → Prop)
class has_append (A : Type u) := (append : A → A → A)
class has_andthen (A : Type u) := (andthen : A → A → A)
class has_union (A : Type u) := (union : A → A → A)
class has_inter (A : Type u) := (inter : A → A → A)
class has_sdiff (A : Type u) := (sdiff : A → A → A)
class has_subset (A : Type u) := (subset : A → A → Prop)
class has_ssubset (A : Type u) := (ssubset : A → A → Prop)
class has_zero (α : Type u) := (zero : α)
class has_one (α : Type u) := (one : α)
class has_add (α : Type u) := (add : α → α → α)
class has_mul (α : Type u) := (mul : α → α → α)
class has_inv (α : Type u) := (inv : α → α)
class has_neg (α : Type u) := (neg : α → α)
class has_sub (α : Type u) := (sub : α → α → α)
class has_div (α : Type u) := (div : α → α → α)
class has_dvd (α : Type u) := (dvd : α → α → Prop)
class has_mod (α : Type u) := (mod : α → α → α)
class has_le (α : Type u) := (le : α → α → Prop)
class has_lt (α : Type u) := (lt : α → α → Prop)
class has_append (α : Type u) := (append : α → α → α)
class has_andthen (α : Type u) := (andthen : α → α → α)
class has_union (α : Type u) := (union : α → α → α)
class has_inter (α : Type u) := (inter : α → α → α)
class has_sdiff (α : Type u) := (sdiff : α → α → α)
class has_subset (α : Type u) := (subset : α → α → Prop)
class has_ssubset (α : Type u) := (ssubset : α → α → Prop)
/- Type classes has_emptyc and has_insert are
used to implement polymorphic notation for collections.
Example: {a, b, c}. -/
class has_emptyc (A : Type u) := (emptyc : A)
class has_insert (A : Type u) (C : Type u → Type v) := (insert : A → C A → C A)
class has_emptyc (α : Type u) := (emptyc : α)
class has_insert (α : Type u) (γ : Type u → Type v) := (insert : α → γ α → γ α)
/- Type class used to implement the notation { a ∈ c | p a } -/
class has_sep (A : Type u) (C : Type u → Type v) :=
(sep : (A → Prop) → C A → C A)
class has_sep (α : Type u) (γ : Type u → Type v) :=
(sep : (α → Prop) → γ α → γ α)
/- Type class for set-like membership -/
class has_mem (A : Type u) (C : Type u → Type v) := (mem : A → C A → Prop)
class has_mem (α : Type u) (γ : Type u → Type v) := (mem : α → γ α → Prop)
def zero {A : Type u} [has_zero A] : A := has_zero.zero A
def one {A : Type u} [has_one A] : A := has_one.one A
def add {A : Type u} [has_add A] : A → A → A := has_add.add
def mul {A : Type u} [has_mul A] : A → A → A := has_mul.mul
def sub {A : Type u} [has_sub A] : A → A → A := has_sub.sub
def div {A : Type u} [has_div A] : A → A → A := has_div.div
def dvd {A : Type u} [has_dvd A] : A → A → Prop := has_dvd.dvd
def mod {A : Type u} [has_mod A] : A → A → A := has_mod.mod
def neg {A : Type u} [has_neg A] : A → A := has_neg.neg
def inv {A : Type u} [has_inv A] : A → A := has_inv.inv
def le {A : Type u} [has_le A] : A → A → Prop := has_le.le
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
def union {A : Type u} [has_union A] : A → A → A := has_union.union
def inter {A : Type u} [has_inter A] : A → A → A := has_inter.inter
def sdiff {A : Type u} [has_sdiff A] : A → A → A := has_sdiff.sdiff
def subset {A : Type u} [has_subset A] : A → A → Prop := has_subset.subset
def ssubset {A : Type u} [has_ssubset A] : A → A → Prop := has_ssubset.ssubset
def zero {α : Type u} [has_zero α] : α := has_zero.zero α
def one {α : Type u} [has_one α] : α := has_one.one α
def add {α : Type u} [has_add α] : α → α → α := has_add.add
def mul {α : Type u} [has_mul α] : α → α → α := has_mul.mul
def sub {α : Type u} [has_sub α] : α → α → α := has_sub.sub
def div {α : Type u} [has_div α] : α → α → α := has_div.div
def dvd {α : Type u} [has_dvd α] : α → α → Prop := has_dvd.dvd
def mod {α : Type u} [has_mod α] : α → α → α := has_mod.mod
def neg {α : Type u} [has_neg α] : α → α := has_neg.neg
def inv {α : Type u} [has_inv α] : α → α := has_inv.inv
def le {α : Type u} [has_le α] : α → α → Prop := has_le.le
def lt {α : Type u} [has_lt α] : α → α → Prop := has_lt.lt
def append {α : Type u} [has_append α] : α → α → α := has_append.append
def andthen {α : Type u} [has_andthen α] : α → α → α := has_andthen.andthen
def union {α : Type u} [has_union α] : α → α → α := has_union.union
def inter {α : Type u} [has_inter α] : α → α → α := has_inter.inter
def sdiff {α : Type u} [has_sdiff α] : α → α → α := has_sdiff.sdiff
def subset {α : Type u} [has_subset α] : α → α → Prop := has_subset.subset
def ssubset {α : Type u} [has_ssubset α] : α → α → Prop := has_ssubset.ssubset
@[reducible]
def ge {A : Type u} [has_le A] (a b : A) : Prop := le b a
def ge {α : Type u} [has_le α] (a b : α) : Prop := le b a
@[reducible]
def gt {A : Type u} [has_lt A] (a b : A) : Prop := lt b a
def gt {α : Type u} [has_lt α] (a b : α) : Prop := lt b a
@[reducible]
def superset {A : Type u} [has_subset A] (a b : A) : Prop := subset b a
def superset {α : Type u} [has_subset α] (a b : α) : Prop := subset b a
@[reducible]
def ssuperset {A : Type u} [has_ssubset A] (a b : A) : Prop := ssubset 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
def ssuperset {α : Type u} [has_ssubset α] (a b : α) : Prop := ssubset b a
def bit0 {α : Type u} [s : has_add α] (a : α) : α := add a a
def bit1 {α : Type u} [s₁ : has_one α] [s₂ : has_add α] (a : α) : α := add (bit0 a) one
attribute [pattern] zero one bit0 bit1 add
def insert {A : Type u} {C : Type u → Type v} [has_insert A C] : A → C A → C A :=
def insert {α : Type u} {γ : Type u → Type v} [has_insert α γ] : α → γ α → γ α :=
has_insert.insert
/- The empty collection -/
def emptyc {A : Type u} [has_emptyc A] : A :=
has_emptyc.emptyc A
def emptyc {α : Type u} [has_emptyc α] : α :=
has_emptyc.emptyc α
def singleton {A : Type u} {C : Type u → Type v} [has_emptyc (C A)] [has_insert A C] (a : A) : C A :=
def singleton {α : Type u} {γ : Type u → Type v} [has_emptyc (γ α)] [has_insert α γ] (a : α) : γ α :=
insert a emptyc
def sep {A : Type u} {C : Type u → Type v} [has_sep A C] : (A → Prop) → C A → C A :=
def sep {α : Type u} {γ : Type u → Type v} [has_sep α γ] : (α → Prop) → γ α → γ α :=
has_sep.sep
def mem {A : Type u} {C : Type u → Type v} [has_mem A C] : A → C A → Prop :=
def mem {α : Type u} {γ : Type u → Type v} [has_mem α γ] : α → γ α → Prop :=
has_mem.mem
/- num, pos_num instances -/
@ -418,26 +418,26 @@ infix \ := sdiff
attribute [refl] eq.refl
@[pattern] def rfl {A : Type u} {a : A} : a = a := eq.refl a
@[pattern] def rfl {α : Type u} {a : α} : a = a := eq.refl a
@[elab_as_eliminator, subst]
lemma eq.subst {A : Type u} {P : A → Prop} {a b : A} (H₁ : a = b) (H₂ : P a) : P b :=
eq.rec H₂ H₁
lemma eq.subst {α : Type u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b :=
eq.rec h₂ h₁
notation H1 ▸ H2 := eq.subst H1 H2
notation h1 ▸ h2 := eq.subst h1 h2
@[trans] lemma eq.trans {A : Type u} {a b c : A} (h₁ : a = b) (h₂ : b = c) : a = c :=
@[trans] lemma eq.trans {α : Type u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c :=
h₂ ▸ h₁
@[symm] lemma eq.symm {A : Type u} {a b : A} (h : a = b) : b = a :=
@[symm] lemma eq.symm {α : Type u} {a b : α} (h : a = b) : b = a :=
h ▸ rfl
/- sizeof -/
class has_sizeof (A : Type u) :=
(sizeof : A → nat)
class has_sizeof (α : Type u) :=
(sizeof : α → nat)
def sizeof {A : Type u} [s : has_sizeof A] : A → nat :=
def sizeof {α : Type u} [s : has_sizeof α] : α → nat :=
has_sizeof.sizeof
/-
@ -445,14 +445,14 @@ Declare sizeof instances and lemmas for types declared before has_sizeof.
From now on, the inductive compiler will automatically generate sizeof instances and lemmas.
-/
/- Every type `A` has a default has_sizeof instance that just returns 0 for every element of `A` -/
instance default_has_sizeof (A : Type u) : has_sizeof A :=
/- Every type `α` has a default has_sizeof instance that just returns 0 for every element of `α` -/
instance default_has_sizeof (α : Type u) : has_sizeof α :=
⟨λ a, nat.zero⟩
/- TODO(Leo): the [simp.sizeof] annotations are not really necessary.
What we need is a robust way of unfolding sizeof definitions. -/
attribute [simp.sizeof]
def default_has_sizeof_eq (A : Type u) (a : A) : @sizeof A (default_has_sizeof A) a = 0 :=
def default_has_sizeof_eq (α : Type u) (a : α) : @sizeof α (default_has_sizeof α) a = 0 :=
rfl
instance : has_sizeof nat :=
@ -462,39 +462,39 @@ attribute [simp.sizeof]
def sizeof_nat_eq (a : nat) : sizeof a = a :=
rfl
protected def prod.sizeof {A : Type u} {B : Type v} [has_sizeof A] [has_sizeof B] : (prod A B) → nat
protected def prod.sizeof {α : Type u} {β : Type v} [has_sizeof α] [has_sizeof β] : (prod α β) → nat
| ⟨a, b⟩ := 1 + sizeof a + sizeof b
instance (A : Type u) (B : Type v) [has_sizeof A] [has_sizeof B] : has_sizeof (prod A B) :=
instance (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] : has_sizeof (prod α β) :=
⟨prod.sizeof⟩
attribute [simp.sizeof]
def sizeof_prod_eq {A : Type u} {B : Type v} [has_sizeof A] [has_sizeof B] (a : A) (b : B) : sizeof (prod.mk a b) = 1 + sizeof a + sizeof b :=
def sizeof_prod_eq {α : Type u} {β : Type v} [has_sizeof α] [has_sizeof β] (a : α) (b : β) : sizeof (prod.mk a b) = 1 + sizeof a + sizeof b :=
rfl
protected def sum.sizeof {A : Type u} {B : Type v} [has_sizeof A] [has_sizeof B] : (sum A B) → nat
protected def sum.sizeof {α : Type u} {β : Type v} [has_sizeof α] [has_sizeof β] : (sum α β) → nat
| (sum.inl a) := 1 + sizeof a
| (sum.inr b) := 1 + sizeof b
instance (A : Type u) (B : Type v) [has_sizeof A] [has_sizeof B] : has_sizeof (sum A B) :=
instance (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] : has_sizeof (sum α β) :=
⟨sum.sizeof⟩
attribute [simp.sizeof]
def sizeof_sum_eq_left {A : Type u} {B : Type v} [has_sizeof A] [has_sizeof B] (a : A) : sizeof (@sum.inl A B a) = 1 + sizeof a :=
def sizeof_sum_eq_left {α : Type u} {β : Type v} [has_sizeof α] [has_sizeof β] (a : α) : sizeof (@sum.inl α β a) = 1 + sizeof a :=
rfl
attribute [simp.sizeof]
def sizeof_sum_eq_right {A : Type u} {B : Type v} [has_sizeof A] [has_sizeof B] (b : B) : sizeof (@sum.inr A B b) = 1 + sizeof b :=
def sizeof_sum_eq_right {α : Type u} {β : Type v} [has_sizeof α] [has_sizeof β] (b : β) : sizeof (@sum.inr α β b) = 1 + sizeof b :=
rfl
protected def sigma.sizeof {A : Type u} {B : A → Type v} [has_sizeof A] [∀ a, has_sizeof (B a)] : sigma B → nat
protected def sigma.sizeof {α : Type u} {β : α → Type v} [has_sizeof α] [∀ a, has_sizeof (β a)] : sigma β → nat
| ⟨a, b⟩ := 1 + sizeof a + sizeof b
instance (A : Type u) (B : A → Type v) [has_sizeof A] [∀ a, has_sizeof (B a)] : has_sizeof (sigma B) :=
instance (α : Type u) (β : α → Type v) [has_sizeof α] [∀ a, has_sizeof (β a)] : has_sizeof (sigma β) :=
⟨sigma.sizeof⟩
attribute [simp.sizeof]
def sizeof_sigma_eq {A : Type u} {B : A → Type v} [has_sizeof A] [∀ a, has_sizeof (B a)] (a : A) (b : B a) : sizeof (@sigma.mk A B a b) = 1 + sizeof a + sizeof b :=
def sizeof_sigma_eq {α : Type u} {β : α → Type v} [has_sizeof α] [∀ a, has_sizeof (β a)] (a : α) (b : β a) : sizeof (@sigma.mk α β a b) = 1 + sizeof a + sizeof b :=
rfl
instance : has_sizeof unit := ⟨λ u, 1⟩
@ -529,34 +529,34 @@ attribute [simp.sizeof]
def sizeof_num_eq (n : num) : sizeof n = nat.of_num n :=
rfl
protected def option.sizeof {A : Type u} [has_sizeof A] : option A → nat
protected def option.sizeof {α : Type u} [has_sizeof α] : option α → nat
| none := 1
| (some a) := 1 + sizeof a
instance (A : Type u) [has_sizeof A] : has_sizeof (option A) :=
instance (α : Type u) [has_sizeof α] : has_sizeof (option α) :=
⟨option.sizeof⟩
attribute [simp.sizeof]
def sizeof_option_none_eq (A : Type u) [has_sizeof A] : sizeof (@none A) = 1 :=
def sizeof_option_none_eq (α : Type u) [has_sizeof α] : sizeof (@none α) = 1 :=
rfl
attribute [simp.sizeof]
def sizeof_option_some_eq {A : Type u} [has_sizeof A] (a : A) : sizeof (some a) = 1 + sizeof a :=
def sizeof_option_some_eq {α : Type u} [has_sizeof α] (a : α) : sizeof (some a) = 1 + sizeof a :=
rfl
protected def list.sizeof {A : Type u} [has_sizeof A] : list A → nat
protected def list.sizeof {α : Type u} [has_sizeof α] : list α → nat
| list.nil := 1
| (list.cons a l) := 1 + sizeof a + list.sizeof l
instance (A : Type u) [has_sizeof A] : has_sizeof (list A) :=
instance (α : Type u) [has_sizeof α] : has_sizeof (list α) :=
⟨list.sizeof⟩
attribute [simp.sizeof]
def sizeof_list_nil_eq (A : Type u) [has_sizeof A] : sizeof (@list.nil A) = 1 :=
def sizeof_list_nil_eq (α : Type u) [has_sizeof α] : sizeof (@list.nil α) = 1 :=
rfl
attribute [simp.sizeof]
def sizeof_list_cons_eq {A : Type u} [has_sizeof A] (a : A) (l : list A) : sizeof (list.cons a l) = 1 + sizeof a + sizeof l :=
def sizeof_list_cons_eq {α : Type u} [has_sizeof α] (a : α) (l : list α) : sizeof (list.cons a l) = 1 + sizeof a + sizeof l :=
rfl
attribute [simp.sizeof]

98
library/init/function.lean
View file

@ -8,14 +8,14 @@ General operations on functions.
prelude
import init.prod init.funext init.logic
notation f ` $ `:1 a:0 := f a
universe variables u_a u_b u_c u_d u_e
variables {A : Type u_a} {B : Type u_b} {C : Type u_c} {D : Type u_d} {E : Type u_a}
universe variables u₁ u₂ u₃ u₄
variables {α : Type u₁} {β : Type u₂} {φ : Type u₃} {δ : Type u₄} {ζ : Type u₁}
@[inline, reducible] def function.comp (f : B → C) (g : A → B) : A → C :=
@[inline, reducible] def function.comp (f : β → φ) (g : α → β) : α → φ :=
λ x, f (g x)
@[inline, reducible] def function.dcomp {B : A → Type u_b} {C : Π {x : A}, B x → Type u_c}
(f : Π {x : A} (y : B x), C y) (g : Π x, B x) : Π x, C (g x) :=
@[inline, reducible] def function.dcomp {β : α → Type u₂} {φ : Π {x : α}, β x → Type u₃}
(f : Π {x : α} (y : β x), φ y) (g : Π x, β x) : Π x, φ (g x) :=
λ x, f (g x)
infixr ` ∘ ` := function.comp
@ -23,119 +23,119 @@ infixr ` ∘' `:80 := function.dcomp
namespace function
@[reducible] def comp_right (f : B → B → B) (g : A → B) : B → A → B :=
@[reducible] def comp_right (f : β → β → β) (g : α → β) : β → α → β :=
λ b a, f b (g a)
@[reducible] def comp_left (f : B → B → B) (g : A → B) : A → B → B :=
@[reducible] def comp_left (f : β → β → β) (g : α → β) : α → β → β :=
λ a b, f (g a) b
@[reducible] def on_fun (f : B → B → C) (g : A → B) : A → A → C :=
@[reducible] def on_fun (f : β → β → φ) (g : α → β) : α → α → φ :=
λ x y, f (g x) (g y)
@[reducible] def combine (f : A → B → C) (op : C → D → E) (g : A → B → D)
: A → B → E :=
@[reducible] def combine (f : α → β → φ) (op : φ → δ → ζ) (g : α → β → δ)
: α → β → ζ :=
λ x y, op (f x y) (g x y)
@[reducible] def const (B : Type u_b) (a : A) : B → A :=
@[reducible] def const (β : Type u₂) (a : α) : β → α :=
λ x, a
@[reducible] def swap {C : A → B → Type u_c} (f : Π x y, C x y) : Π y x, C x y :=
@[reducible] def swap {φ : α → β → Type u₃} (f : Π x y, φ x y) : Π y x, φ x y :=
λ y x, f x y
@[reducible] def app {B : A → Type u_b} (f : Π x, B x) (x : A) : B x :=
@[reducible] def app {β : α → Type u₂} (f : Π x, β x) (x : α) : β x :=
f x
@[reducible] def curry : (A × B → C) → A → B → C :=
@[reducible] def curry : (α × β → φ) → α → β → φ :=
λ f a b, f (a, b)
@[reducible] def uncurry : (A → B → C) → A × B → C :=
@[reducible] def uncurry : (α → β → φ) → α × β → φ :=
λ f ⟨a, b⟩, f a b
lemma curry_uncurry (f : A → B → C) : curry (uncurry f) = f :=
lemma curry_uncurry (f : α → β → φ) : curry (uncurry f) = f :=
rfl
lemma uncurry_curry (f : A × B → C) : uncurry (curry f) = f :=
lemma uncurry_curry (f : α × β → φ) : uncurry (curry f) = f :=
funext (λ ⟨a, b⟩, rfl)
infixl ` on `:1 := on_fun
notation f ` -[` op `]- ` g := combine f op g
lemma left_id (f : A → B) : id ∘ f = f := rfl
lemma left_id (f : α → β) : id ∘ f = f := rfl
lemma right_id (f : A → B) : f ∘ id = f := rfl
lemma right_id (f : α → β) : f ∘ id = f := rfl
lemma comp.assoc (f : C → D) (g : B → C) (h : A → B) : (f ∘ g) ∘ h = f ∘ (g ∘ h) := rfl
lemma comp.assoc (f : φ → δ) (g : β → φ) (h : α → β) : (f ∘ g) ∘ h = f ∘ (g ∘ h) := rfl
lemma comp.left_id (f : A → B) : id ∘ f = f := rfl
lemma comp.left_id (f : α → β) : id ∘ f = f := rfl
lemma comp.right_id (f : A → B) : f ∘ id = f := rfl
lemma comp.right_id (f : α → β) : f ∘ id = f := rfl
lemma comp_const_right (f : B → C) (b : B) : f ∘ (const A b) = const A (f b) := rfl
lemma comp_const_right (f : β → φ) (b : β) : f ∘ (const α b) = const α (f b) := rfl
@[reducible] def injective (f : A → B) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂
@[reducible] def injective (f : α → β) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂
lemma injective_comp {g : B → C} {f : A → B} (hg : injective g) (hf : injective f) : injective (g ∘ f) :=
lemma injective_comp {g : β → φ} {f : α → β} (hg : injective g) (hf : injective f) : injective (g ∘ f) :=
take a₁ a₂, assume h, hf (hg h)
@[reducible] def surjective (f : A → B) : Prop := ∀ b, ∃ a, f a = b
@[reducible] def surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b
lemma surjective_comp {g : B → C} {f : A → B} (hg : surjective g) (hf : surjective f) : surjective (g ∘ f) :=
λ (c : C), exists.elim (hg c) (λ b hb, exists.elim (hf b) (λ a ha,
lemma surjective_comp {g : β → φ} {f : α → β} (hg : surjective g) (hf : surjective f) : surjective (g ∘ f) :=
λ (c : φ), exists.elim (hg c) (λ b hb, exists.elim (hf b) (λ a ha,
exists.intro a (show g (f a) = c, from (eq.trans (congr_arg g ha) hb))))
def bijective (f : A → B) := injective f ∧ surjective f
def bijective (f : α → β) := injective f ∧ surjective f
lemma bijective_comp {g : B → C} {f : A → B} : bijective g → bijective f → bijective (g ∘ f)
lemma bijective_comp {g : β → φ} {f : α → β} : bijective g → bijective f → bijective (g ∘ f)
| ⟨h_ginj, h_gsurj⟩ ⟨h_finj, h_fsurj⟩ := ⟨injective_comp h_ginj h_finj, surjective_comp h_gsurj h_fsurj⟩
-- g is a left inverse to f
def left_inverse (g : B → A) (f : A → B) : Prop := ∀ x, g (f x) = x
def left_inverse (g : β → α) (f : α → β) : Prop := ∀ x, g (f x) = x
def id_of_left_inverse {g : B → A} {f : A → B} : left_inverse g f → g ∘ f = id :=
def id_of_left_inverse {g : β → α} {f : α → β} : left_inverse g f → g ∘ f = id :=
assume h, funext h
def has_left_inverse (f : A → B) : Prop := ∃ finv : B → A, left_inverse finv f
def has_left_inverse (f : α → β) : Prop := ∃ finv : β → α, left_inverse finv f
-- g is a right inverse to f
def right_inverse (g : B → A) (f : A → B) : Prop := left_inverse f g
def right_inverse (g : β → α) (f : α → β) : Prop := left_inverse f g
def id_of_right_inverse {g : B → A} {f : A → B} : right_inverse g f → f ∘ g = id :=
def id_of_right_inverse {g : β → α} {f : α → β} : right_inverse g f → f ∘ g = id :=
assume h, funext h
def has_right_inverse (f : A → B) : Prop := ∃ finv : B → A, right_inverse finv f
def has_right_inverse (f : α → β) : Prop := ∃ finv : β → α, right_inverse finv f
lemma injective_of_left_inverse {g : B → A} {f : A → B} : left_inverse g f → injective f :=
lemma injective_of_left_inverse {g : β → α} {f : α → β} : left_inverse g f → injective f :=
assume h, take a b, assume faeqfb,
have h₁ : a = g (f a), from eq.symm (h a),
have h₂ : g (f b) = b, from h b,
have h₃ : g (f a) = g (f b), from congr_arg g faeqfb,
eq.trans h₁ (eq.trans h₃ h₂)
lemma injective_of_has_left_inverse {f : A → B} : has_left_inverse f → injective f :=
lemma injective_of_has_left_inverse {f : α → β} : has_left_inverse f → injective f :=
assume h, exists.elim h (λ finv inv, injective_of_left_inverse inv)
lemma right_inverse_of_injective_of_left_inverse {f : A → B} {g : B → A}
lemma right_inverse_of_injective_of_left_inverse {f : α → β} {g : β → α}
(injf : injective f) (lfg : left_inverse f g) :
right_inverse f g :=
take x,
have H : f (g (f x)) = f x, from lfg (f x),
injf H
have h : f (g (f x)) = f x, from lfg (f x),
injf h
lemma surjective_of_has_right_inverse {f : A → B} : has_right_inverse f → surjective f
lemma surjective_of_has_right_inverse {f : α → β} : has_right_inverse f → surjective f
| ⟨finv, inv⟩ b := ⟨finv b, inv b⟩
lemma left_inverse_of_surjective_of_right_inverse {f : A → B} {g : B → A}
lemma left_inverse_of_surjective_of_right_inverse {f : α → β} {g : β → α}
(surjf : surjective f) (rfg : right_inverse f g) :
left_inverse f g :=
take y, exists.elim (surjf y) (λ x Hx, calc
f (g y) = f (g (f x)) : Hx ▸ rfl
take y, exists.elim (surjf y) (λ x hx, calc
f (g y) = f (g (f x)) : hx ▸ rfl
... = f x : eq.symm (rfg x) ▸ rfl
... = y : Hx)
... = y : hx)
lemma injective_id : injective (@id A) := take a₁ a₂ h, h
lemma injective_id : injective (@id α) := take a₁ a₂ h, h
lemma surjective_id : surjective (@id A) := take a, ⟨a, rfl⟩
lemma surjective_id : surjective (@id α) := take a, ⟨a, rfl⟩
lemma bijective_id : bijective (@id A) := ⟨injective_id, surjective_id⟩
lemma bijective_id : bijective (@id α) := ⟨injective_id, surjective_id⟩
end function

6
library/init/functor.lean
View file

@ -6,10 +6,10 @@ Authors: Luke Nelson and Jared Roesch
prelude
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)
class functor (f : Type u → Type v) : Type (max u+1 v) :=
(map : Π {a b : Type u}, (a → b) → f a → f b)
@[inline] def fmap {F : Type u → Type v} [functor F] {A B : Type u} : (A → B) → F A → F B :=
@[inline] def fmap {f : Type u → Type v} [functor f] {a b : Type u} : (a → b) → f a → f b :=
functor.map
infixr ` <$> `:100 := fmap

45
library/init/funext.lean
View file

@ -11,47 +11,47 @@ import init.quot init.logic
universe variables u v
namespace function
variables {A : Type u} {B : A → Type v}
variables {α : Type u} {β : α → Type v}
protected def equiv (f₁ f₂ : Π x : A, B x) : Prop := ∀ x, f₁ x = f₂ x
protected def equiv (f₁ f₂ : Π x : α, β x) : Prop := ∀ x, f₁ x = f₂ x
local infix `~` := function.equiv
protected theorem equiv.refl (f : Π x : A, B x) : f ~ f := take x, rfl
protected theorem equiv.refl (f : Π x : α, β x) : f ~ f := take x, rfl
protected theorem equiv.symm {f₁ f₂ : Π x: A, B x} : f₁ ~ f₂ → f₂ ~ f₁ :=
λ H x, eq.symm (H x)
protected theorem equiv.symm {f₁ f₂ : Π x: α, β x} : f₁ ~ f₂ → f₂ ~ f₁ :=
λ h x, eq.symm (h x)
protected theorem equiv.trans {f₁ f₂ f₃ : Π x: A, B x} : f₁ ~ f₂ → f₂ ~ f₃ → f₁ ~ f₃ :=
λ H₁ H₂ x, eq.trans (H₁ x) (H₂ x)
protected theorem equiv.trans {f₁ f₂ f₃ : Π x: α, β x} : f₁ ~ f₂ → f₂ ~ f₃ → f₁ ~ f₃ :=
λ h₁ h₂ x, eq.trans (h₁ x) (h₂ x)
protected theorem equiv.is_equivalence (A : Type u) (B : A → Type v) : equivalence (@function.equiv A B) :=
mk_equivalence (@function.equiv A B) (@equiv.refl A B) (@equiv.symm A B) (@equiv.trans A B)
protected theorem equiv.is_equivalence (α : Type u) (β : α → Type v) : equivalence (@function.equiv α β) :=
mk_equivalence (@function.equiv α β) (@equiv.refl α β) (@equiv.symm α β) (@equiv.trans α β)
end function
section
open quot
variables {A : Type u} {B : A → Type v}
variables {α : Type u} {β : α → Type v}
@[instance]
private def fun_setoid (A : Type u) (B : A → Type v) : setoid (Π x : A, B x) :=
setoid.mk (@function.equiv A B) (function.equiv.is_equivalence A B)
private def fun_setoid (α : Type u) (β : α → Type v) : setoid (Π x : α, β x) :=
setoid.mk (@function.equiv α β) (function.equiv.is_equivalence α β)
private def extfun (A : Type u) (B : A → Type v) : Type (imax u v) :=
quot (fun_setoid A B)
private def extfun (α : Type u) (β : α → Type v) : Type (imax u v) :=
quot (fun_setoid α β)
private def fun_to_extfun (f : Π x : A, B x) : extfun A B :=
private def fun_to_extfun (f : Π x : α, β x) : extfun α β :=
⟦f⟧
private def extfun_app (f : extfun A B) : Π x : A, B x :=
private def extfun_app (f : extfun α β) : Π x : α, β x :=
take x,
quot.lift_on f
(λ f : Π x : A, B x, f x)
(λ f₁ f₂ H, H x)
(λ f : Π x : α, β x, f x)
(λ f₁ f₂ h, h x)
theorem funext {f₁ f₂ : Π x : A, B x} : (∀ x, f₁ x = f₂ x) → f₁ = f₂ :=
assume H, calc
theorem funext {f₁ f₂ : Π x : α, β x} : (∀ x, f₁ x = f₂ x) → f₁ = f₂ :=
assume h, calc
f₁ = extfun_app ⟦f₁⟧ : rfl
... = extfun_app ⟦f₂⟧ : @sound _ _ f₁ f₂ H ▸ rfl
... = extfun_app ⟦f₂⟧ : @sound _ _ f₁ f₂ h ▸ rfl
... = f₂ : rfl
end
@ -59,6 +59,5 @@ attribute [intro!] funext
local infix `~` := function.equiv
instance pi.subsingleton {A : Type u} {B : A → Type v} (H : ∀ a, subsingleton (B a)) :
subsingleton (Π a, B a) :=
instance pi.subsingleton {α : Type u} {β : α → Type v} [∀ a, subsingleton (β a)] : subsingleton (Π a, β a) :=
⟨λ f₁ f₂, funext (λ a, subsingleton.elim (f₁ a) (f₂ a))⟩

6
library/init/id_locked.lean
View file

@ -15,9 +15,9 @@ open tactic
run_command do
l ← return $ level.param `l,
Ty ← return $ expr.sort l,
type ← to_expr `(Π {A : %%Ty}, A → A),
val ← to_expr `(λ {A : %%Ty} (a : A), a),
type ← to_expr `(Π {α : %%Ty}, α → α),
val ← to_expr `(λ {α : %%Ty} (a : α), a),
add_decl (declaration.defn `id_locked [`l] type val reducibility_hints.opaque tt)
lemma {u} id_locked_eq {A : Type u} (a : A) : id_locked a = a :=
lemma {u} id_locked_eq {α : Type u} (a : α) : id_locked a = a :=
rfl

6
library/init/instances.lean
View file

@ -8,10 +8,10 @@ import init.meta.mk_dec_eq_instance init.subtype init.meta.occurrences init.sum
open tactic subtype
universe variables u v
instance {A : Type u} {p : A → Prop} [decidable_eq A] : decidable_eq {x : A // p x} :=
instance {α : Type u} {p : α → Prop} [decidable_eq α] : decidable_eq {x : α // p x} :=
by mk_dec_eq_instance
instance {A : Type u} [decidable_eq A] : decidable_eq (list A) :=
instance {α : Type u} [decidable_eq α] : decidable_eq (list α) :=
by mk_dec_eq_instance
instance : decidable_eq occurrences :=
@ -20,5 +20,5 @@ by mk_dec_eq_instance
instance : decidable_eq unit :=
by mk_dec_eq_instance
instance {A : Type u} {B : Type v} [decidable_eq A] [decidable_eq B] : decidable_eq (A ⊕ B) :=
instance {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] : decidable_eq (α ⊕ β) :=
by mk_dec_eq_instance

64
library/init/list.lean
View file

@ -12,27 +12,27 @@ notation `[` l:(foldr `, ` (h t, cons h t) nil `]`) := l
universe variables u v
instance (A : Type u) : inhabited (list A) :=
instance (α : Type u) : inhabited (list α) :=
⟨list.nil⟩
variables {A : Type u} {B : Type v}
variables {α : Type u} {β : Type v}
namespace list
protected def append : list A → list A → list A
protected def append : list α → list α → list α
| [] l := l
| (h :: s) t := h :: (append s t)
instance : has_append (list A) :=
instance : has_append (list α) :=
⟨list.append⟩
protected def mem : A → list A → Prop
protected def mem : α → list α → Prop
| a [] := false
| a (b :: l) := a = b ∨ mem a l
instance : has_mem A list :=
instance : has_mem α list :=
⟨list.mem⟩
instance decidable_mem [decidable_eq A] (a : A) : ∀ (l : list A), decidable (a ∈ l)
instance decidable_mem [decidable_eq α] (a : α) : ∀ (l : list α), decidable (a ∈ l)
| [] := is_false not_false
| (b::l) :=
if h₁ : a = b then is_true (or.inl h₁)
@ -41,96 +41,96 @@ instance decidable_mem [decidable_eq A] (a : A) : ∀ (l : list A), decidable (a
| is_false h₂ := is_false (not_or h₁ h₂)
end
def concat : list A → A → list A
def concat : list α → α → list α
| [] a := [a]
| (b::l) a := b :: concat l a
instance : has_emptyc (list A) :=
instance : has_emptyc (list α) :=
⟨list.nil⟩
protected def insert [decidable_eq A] (a : A) (l : list A) : list A :=
protected def insert [decidable_eq α] (a : α) (l : list α) : list α :=
if a ∈ l then l else concat l a
instance [decidable_eq A] : has_insert A list :=
instance [decidable_eq α] : has_insert α list :=
⟨list.insert⟩
protected def union [decidable_eq A] : list A → list A → list A
protected def union [decidable_eq α] : list α → list α → list α
| l₁ [] := l₁
| l₁ (a::l₂) := union (insert a l₁) l₂
instance [decidable_eq A] : has_union (list A) :=
instance [decidable_eq α] : has_union (list α) :=
⟨list.union⟩
protected def inter [decidable_eq A] : list A → list A → list A
protected def inter [decidable_eq α] : list α → list α → list α
| [] l₂ := []
| (a::l₁) l₂ := if a ∈ l₂ then a :: inter l₁ l₂ else inter l₁ l₂
instance [decidable_eq A] : has_inter (list A) :=
instance [decidable_eq α] : has_inter (list α) :=
⟨list.inter⟩
def length : list A → nat
def length : list α → nat
| [] := 0
| (a :: l) := length l + 1
open option nat
def nth : list A → nat → option A
def nth : list α → nat → option α
| [] n := none
| (a :: l) 0 := some a
| (a :: l) (n+1) := nth l n
def head [inhabited A] : list A → A
| [] := default A
def head [inhabited α] : list α → α
| [] := default α
| (a :: l) := a
def tail : list A → list A
def tail : list α → list α
| [] := []
| (a :: l) := l
def reverse : list A → list A
def reverse : list α → list α
| [] := []
| (a :: l) := concat (reverse l) a
def map (f : A → B) : list A → list B
def map (f : α → β) : list α → list β
| [] := []
| (a :: l) := f a :: map l
def for : list A → (A → B) → list B :=
def for : list α → (α → β) → list β :=
flip map
def join : list (list A) → list A
def join : list (list α) → list α
| [] := []
| (l :: ls) := append l (join ls)
def filter (p : A → Prop) [h : decidable_pred p] : list A → list A
def filter (p : α → Prop) [decidable_pred p] : list α → list α
| [] := []
| (a::l) := if p a then a :: filter l else filter l
def dropn : ℕ → list A → list A
def dropn : ℕ → list α → list α
| 0 a := a
| (succ n) [] := []
| (succ n) (x::r) := dropn n r
definition foldl (f : A → B → A) : A → list B → A
definition foldl (f : α → β → α) : α → list β → α
| a [] := a
| a (b :: l) := foldl (f a b) l
definition foldr (f : A → B → B) : B → list A → B
definition foldr (f : α → β → β) : β → list α → β
| b [] := b
| b (a :: l) := f a (foldr b l)
definition any (l : list A) (p : A → bool) : bool :=
definition any (l : list α) (p : α → bool) : bool :=
foldr (λ a r, p a || r) ff l
definition all (l : list A) (p : A → bool) : bool :=
definition all (l : list α) (p : α → bool) : bool :=
foldr (λ a r, p a && r) tt l
def zip : list A → list B → list (prod A B)
def zip : list α → list β → list (prod α β)
| [] _ := []
| _ [] := []
| (x::xs) (y::ys) := (prod.mk x y) :: zip xs ys
def repeat (a : A) : ℕ → list A
def repeat (a : α) : ℕ → list α
| 0 := []
| (succ n) := a :: repeat n

4
library/init/list_classes.lean
View file

@ -9,10 +9,10 @@ open list
universe variables u v
@[inline] def list.bind {A : Type u} {B : Type v} (a : list A) (b : A → list B) : list B :=
@[inline] def list.bind {α : Type u} {β : Type v} (a : list α) (b : α → list β) : list β :=
join (map b a)
@[inline] def list.ret {A : Type u} (a : A) : list A :=
@[inline] def list.ret {α : Type u} (a : α) : list α :=
[a]
instance : monad list :=

264
library/init/logic.lean
View file

@ -8,9 +8,9 @@ import init.core
universe variables u v w
@[reducible] def id {A : Type u} (a : A) : A := a
@[reducible] def id {α : Type u} (a : α) : α := a
def flip {A : Type u} {B : Type v} {C : Type w} (f : A → B → C) : B → A → C :=
def flip {α : Type u} {β : Type v} {φ : Type w} (f : α → β → φ) : β → α → φ :=
λ b a, f a b
/- implication -/
@ -54,39 +54,39 @@ false.rec c h
lemma proof_irrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ :=
rfl
@[simp] lemma id.def {A : Type u} (a : A) : id a = a := rfl
@[simp] lemma id.def {α : Type u} (a : α) : id a = a := rfl
-- Remark: we provide the universe levels explicitly to make sure `eq.drec` has the same type of `eq.rec` in the hoTT library
attribute [elab_as_eliminator]
protected lemma {u₁ u₂} eq.drec {A : Type u₂} {a : A} {C : Π (x : A), a = x → Type u₁} (h₁ : C a (eq.refl a)) {b : A} (h₂ : a = b) : C b h₂ :=
eq.rec (λ h₂ : a = a, show C a h₂, from h₁) h₂ h₂
protected lemma {u₁ u₂} eq.drec {α : Type u₂} {a : α} {φ : Π (x : α), a = x → Type u₁} (h₁ : φ a (eq.refl a)) {b : α} (h₂ : a = b) : φ b h₂ :=
eq.rec (λ h₂ : a = a, show φ a h₂, from h₁) h₂ h₂
attribute [elab_as_eliminator]
protected lemma drec_on {A : Type u} {a : A} {C : Π (x : A), a = x → Type v} {b : A} (h₂ : a = b) (h₁ : C a (eq.refl a)) : C b h₂ :=
protected lemma drec_on {α : Type u} {a : α} {φ : Π (x : α), a = x → Type v} {b : α} (h₂ : a = b) (h₁ : φ a (eq.refl a)) : φ b h₂ :=
eq.drec h₁ h₂
lemma eq.mp {A B : Type u} : (A = B) → A → B :=
lemma eq.mp {α β : Type u} : (α = β) → α → β :=
eq.rec_on
lemma eq.mpr {A B : Type u} : (A = B) → B → A :=
lemma eq.mpr {α β : Type u} : (α = β) → β → α :=
λ h₁ h₂, eq.rec_on (eq.symm h₁) h₂
lemma eq.substr {A : Type u} {p : A → Prop} {a b : A} (h₁ : b = a) : p a → p b :=
lemma eq.substr {α : Type u} {p : α → Prop} {a b : α} (h₁ : b = a) : p a → p b :=
eq.subst (eq.symm h₁)
lemma congr {A : Type u} {B : Type v} {f₁ f₂ : A → B} {a₁ a₂ : A} (h₁ : f₁ = f₂) (h₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=
lemma congr {α : Type u} {β : Type v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : f₁ = f₂) (h₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=
eq.subst h₁ (eq.subst h₂ rfl)
lemma congr_fun {A : Type u} {B : A → Type v} {f g : Π x, B x} (h : f = g) (a : A) : f a = g a :=
lemma congr_fun {α : Type u} {β : α → Type v} {f g : Π x, β x} (h : f = g) (a : α) : f a = g a :=
eq.subst h (eq.refl (f a))
lemma congr_arg {A : Type u} {B : Type v} {a₁ a₂ : A} (f : A → B) : a₁ = a₂ → f a₁ = f a₂ :=
lemma congr_arg {α : Type u} {β : Type v} {a₁ a₂ : α} (f : α → β) : a₁ = a₂ → f a₁ = f a₂ :=
congr rfl
lemma trans_rel_left {A : Type u} {a b c : A} (r : A → A → Prop) (h₁ : r a b) (h₂ : b = c) : r a c :=
lemma trans_rel_left {α : Type u} {a b c : α} (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c :=
h₂ ▸ h₁
lemma trans_rel_right {A : Type u} {a b c : A} (r : A → A → Prop) (h₁ : a = b) (h₂ : r b c) : r a c :=
lemma trans_rel_right {α : Type u} {a b c : α} (r : α → α → Prop) (h₁ : a = b) (h₂ : r b c) : r a c :=
h₁^.symm ▸ h₂
lemma of_eq_true {p : Prop} (h : p = true) : p :=
@ -95,26 +95,26 @@ h^.symm ▸ trivial
lemma not_of_eq_false {p : Prop} (h : p = false) : ¬p :=
assume hp, h ▸ hp
@[inline] def cast {A B : Type u} (h : A = B) (a : A) : B :=
@[inline] def cast {α β : Type u} (h : α = β) (a : α) : β :=
eq.rec a h
lemma cast_proof_irrel {A B : Type u} (h₁ h₂ : A = B) (a : A) : cast h₁ a = cast h₂ a :=
lemma cast_proof_irrel {α β : Type u} (h₁ h₂ : α = β) (a : α) : cast h₁ a = cast h₂ a :=
rfl
lemma cast_eq {A : Type u} (h : A = A) (a : A) : cast h a = a :=
lemma cast_eq {α : Type u} (h : α = α) (a : α) : cast h a = a :=
rfl
/- ne -/
@[reducible] def ne {A : Type u} (a b : A) := ¬(a = b)
@[reducible] def ne {α : Type u} (a b : α) := ¬(a = b)
notation a ≠ b := ne a b
@[simp] lemma ne.def {A : Type u} (a b : A) : a ≠ b = ¬ (a = b) :=
@[simp] lemma ne.def {α : Type u} (a b : α) : a ≠ b = ¬ (a = b) :=
rfl
namespace ne
variable {A : Type u}
variables {a b : A}
variable {α : Type u}
variables {a b : α}
lemma intro (h : a = b → false) : a ≠ b := h
@ -126,7 +126,7 @@ namespace ne
assume (h₁ : b = a), h (h₁^.symm)
end ne
lemma false_of_ne {A : Type u} {a : A} : a ≠ a → false := ne.irrefl
lemma false_of_ne {α : Type u} {a : α} : a ≠ a → false := ne.irrefl
section
variables {p : Prop}
@ -144,18 +144,18 @@ end
attribute [refl] heq.refl
section
variables {A B C : Type u} {a a' : A} {b b' : B} {c : C}
variables {α β φ : Type u} {a a' : α} {b b' : β} {c : φ}
lemma eq_of_heq (h : a == a') : a = a' :=
have ∀ (A' : Type u) (a' : A') (h₁ : @heq A a A' a') (h₂ : A = A'), (eq.rec_on h₂ a : A') = a', from
λ (A' : Type u) (a' : A') (h₁ : @heq A a A' a'), heq.rec_on h₁ (λ h₂ : A = A, rfl),
show (eq.rec_on (eq.refl A) a : A) = a', from
this A a' h (eq.refl A)
have ∀ (α' : Type u) (a' : α') (h₁ : @heq α a α' a') (h₂ : α = α'), (eq.rec_on h₂ a : α') = a', from
λ (α' : Type u) (a' : α') (h₁ : @heq α a α' a'), heq.rec_on h₁ (λ h₂ : α = α, rfl),
show (eq.rec_on (eq.refl α) a : α) = a', from
this α a' h (eq.refl α)
lemma heq.elim {A : Type u} {a : A} {p : A → Type v} {b : A} (h₁ : a == b)
lemma heq.elim {α : Type u} {a : α} {p : α → Type v} {b : α} (h₁ : a == b)
: p a → p b := eq.rec_on (eq_of_heq h₁)
lemma heq.subst {p : ∀ T : Type u, T → Prop} : a == b → p A a → p B b :=
lemma heq.subst {p : ∀ T : Type u, T → Prop} : a == b → p α a → p β b :=
heq.rec_on
@[symm] lemma heq.symm (h : a == b) : b == a :=
@ -173,17 +173,17 @@ heq.trans h₁ (heq_of_eq h₂)
@[trans] lemma heq_of_eq_of_heq (h₁ : a = a') (h₂ : a' == b) : a == b :=
heq.trans (heq_of_eq h₁) h₂
def type_eq_of_heq (h : a == b) : A = B :=
heq.rec_on h (eq.refl A)
def type_eq_of_heq (h : a == b) : α = β :=
heq.rec_on h (eq.refl α)
end
lemma eq_rec_heq {A : Type u} {C : A → Type v} : ∀ {a a' : A} (h : a = a') (p : C a), (eq.rec_on h p : C a') == p
lemma eq_rec_heq {α : Type u} {φ : α → Type v} : ∀ {a a' : α} (h : a = a') (p : φ a), (eq.rec_on h p : φ a') == p
| a .a rfl p := heq.refl p
lemma heq_of_eq_rec_left {A : Type u} {C : A → Type v} : ∀ {a a' : A} {p₁ : C a} {p₂ : C a'} (e : a = a') (h₂ : (eq.rec_on e p₁ : C a') = p₂), p₁ == p₂
lemma heq_of_eq_rec_left {α : Type u} {φ : α → Type v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a = a') (h₂ : (eq.rec_on e p₁ : φ a') = p₂), p₁ == p₂
| a .a p₁ p₂ (eq.refl .a) h := eq.rec_on h (heq.refl p₁)
lemma heq_of_eq_rec_right {A : Type u} {C : A → Type v} : ∀ {a a' : A} {p₁ : C a} {p₂ : C a'} (e : a' = a) (h₂ : p₁ = eq.rec_on e p₂), p₁ == p₂
lemma heq_of_eq_rec_right {α : Type u} {φ : α → Type v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a' = a) (h₂ : p₁ = eq.rec_on e p₂), p₁ == p₂
| a .a p₁ p₂ (eq.refl .a) h :=
have p₁ = p₂, from h,
this ▸ heq.refl p₁
@ -191,20 +191,20 @@ lemma heq_of_eq_rec_right {A : Type u} {C : A → Type v} : ∀ {a a' : A} {p₁
lemma of_heq_true {a : Prop} (h : a == true) : a :=
of_eq_true (eq_of_heq h)
lemma eq_rec_compose : ∀ {A B C : Type u} (p₁ : B = C) (p₂ : A = B) (a : A), (eq.rec_on p₁ (eq.rec_on p₂ a : B) : C) = eq.rec_on (eq.trans p₂ p₁) a
| A .A .A (eq.refl .A) (eq.refl .A) a := rfl
lemma eq_rec_compose : ∀ {α β φ : Type u} (p₁ : β = φ) (p₂ : α = β) (a : α), (eq.rec_on p₁ (eq.rec_on p₂ a : β) : φ) = eq.rec_on (eq.trans p₂ p₁) a
| α .α .α (eq.refl .α) (eq.refl .α) a := rfl
lemma eq_rec_eq_eq_rec : ∀ {A₁ A₂ : Type u} {p : A₁ = A₂} {a₁ : A₁} {a₂ : A₂}, (eq.rec_on p a₁ : A₂) = a₂ → a₁ = eq.rec_on (eq.symm p) a₂
| A .A rfl a .a rfl := rfl
lemma eq_rec_eq_eq_rec : ∀ {α₁ α₂ : Type u} {p : α₁ = α₂} {a₁ : α₁} {a₂ : α₂}, (eq.rec_on p a₁ : α₂) = a₂ → a₁ = eq.rec_on (eq.symm p) a₂
| α .α rfl a .a rfl := rfl
lemma eq_rec_of_heq_left : ∀ {A₁ A₂ : Type u} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂), (eq.rec_on (type_eq_of_heq h) a₁ : A₂) = a₂
| A .A a .a (heq.refl .a) := rfl
lemma eq_rec_of_heq_left : ∀ {α₁ α₂ : Type u} {a₁ : α₁} {a₂ : α₂} (h : a₁ == a₂), (eq.rec_on (type_eq_of_heq h) a₁ : α₂) = a₂
| α .α a .a (heq.refl .a) := rfl
lemma eq_rec_of_heq_right {A₁ A₂ : Type u} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂) : a₁ = eq.rec_on (eq.symm (type_eq_of_heq h)) a₂ :=
lemma eq_rec_of_heq_right {α₁ α₂ : Type u} {a₁ : α₁} {a₂ : α₂} (h : a₁ == a₂) : a₁ = eq.rec_on (eq.symm (type_eq_of_heq h)) a₂ :=
eq_rec_eq_eq_rec (eq_rec_of_heq_left h)
lemma cast_heq : ∀ {A B : Type u} (h : A = B) (a : A), cast h a == a
| A .A (eq.refl .A) a := heq.refl a
lemma cast_heq : ∀ {α β : Type u} (h : α = β) (a : α), cast h a == a
| α .α (eq.refl .α) a := heq.refl a
/- and -/
@ -341,13 +341,13 @@ iff_true_intro not_false
@[congr] lemma not_congr (h : a ↔ b) : ¬a ↔ ¬b :=
iff.intro (λ h₁ h₂, h₁ (iff.mpr h h₂)) (λ h₁ h₂, h₁ (iff.mp h h₂))
@[simp] lemma ne_self_iff_false {A : Type u} (a : A) : (not (a = a)) ↔ false :=
@[simp] lemma ne_self_iff_false {α : Type u} (a : α) : (not (a = a)) ↔ false :=
iff.intro false_of_ne false.elim
@[simp] lemma eq_self_iff_true {A : Type u} (a : A) : (a = a) ↔ true :=
@[simp] lemma eq_self_iff_true {α : Type u} (a : α) : (a = a) ↔ true :=
iff_true_intro rfl
@[simp] lemma heq_self_iff_true {A : Type u} (a : A) : (a == a) ↔ true :=
@[simp] lemma heq_self_iff_true {α : Type u} (a : α) : (a == a) ↔ true :=
iff_true_intro (heq.refl a)
@[simp] lemma iff_not_self (a : Prop) : (a ↔ ¬a) ↔ false :=
@ -505,8 +505,8 @@ iff.intro (λ h, trivial) (λ ha h, false.elim h)
/- exists -/
inductive Exists {A : Type u} (p : A → Prop) : Prop
| intro : ∀ (a : A), p a → Exists
inductive Exists {α : Type u} (p : α → Prop) : Prop
| intro : ∀ (a : α), p a → Exists
attribute [intro] Exists.intro
@ -515,54 +515,54 @@ def exists.intro := @Exists.intro
notation `exists` binders `, ` r:(scoped P, Exists P) := r
notation `∃` binders `, ` r:(scoped P, Exists P) := r
lemma exists.elim {A : Type u} {p : A → Prop} {b : Prop}
(h₁ : ∃ x, p x) (h₂ : ∀ (a : A), p a → b) : b :=
lemma exists.elim {α : Type u} {p : α → Prop} {b : Prop}
(h₁ : ∃ x, p x) (h₂ : ∀ (a : α), p a → b) : b :=
Exists.rec h₂ h₁
/- exists unique -/
def exists_unique {A : Type u} (p : A → Prop) :=
def exists_unique {α : Type u} (p : α → Prop) :=
∃ x, p x ∧ ∀ y, p y → y = x
notation `∃!` binders `, ` r:(scoped P, exists_unique P) := r
attribute [intro]
lemma exists_unique.intro {A : Type u} {p : A → Prop} (w : A) (h₁ : p w) (h₂ : ∀ y, p y → y = w) :
lemma exists_unique.intro {α : Type u} {p : α → Prop} (w : α) (h₁ : p w) (h₂ : ∀ y, p y → y = w) :
∃! x, p x :=
exists.intro w ⟨h₁, h₂⟩
attribute [recursor 4]
lemma exists_unique.elim {A : Type u} {p : A → Prop} {b : Prop}
lemma exists_unique.elim {α : Type u} {p : α → Prop} {b : Prop}
(h₂ : ∃! x, p x) (h₁ : ∀ x, p x → (∀ y, p y → y = x) → b) : b :=
exists.elim h₂ (λ w hw, h₁ w (and.left hw) (and.right hw))
lemma exists_unique_of_exists_of_unique {A : Type u} {p : A → Prop}
lemma exists_unique_of_exists_of_unique {α : Type u} {p : α → Prop}
(hex : ∃ x, p x) (hunique : ∀ y₁ y₂, p y₁ → p y₂ → y₁ = y₂) : ∃! x, p x :=
exists.elim hex (λ x px, exists_unique.intro x px (take y, suppose p y, hunique y x this px))
lemma exists_of_exists_unique {A : Type u} {p : A → Prop} (h : ∃! x, p x) : ∃ x, p x :=
lemma exists_of_exists_unique {α : Type u} {p : α → Prop} (h : ∃! x, p x) : ∃ x, p x :=
exists.elim h (λ x hx, ⟨x, and.left hx⟩)
lemma unique_of_exists_unique {A : Type u} {p : A → Prop}
(h : ∃! x, p x) {y₁ y₂ : A} (py₁ : p y₁) (py₂ : p y₂) : y₁ = y₂ :=
lemma unique_of_exists_unique {α : Type u} {p : α → Prop}
(h : ∃! x, p x) {y₁ y₂ : α} (py₁ : p y₁) (py₂ : p y₂) : y₁ = y₂ :=
exists_unique.elim h
(take x, suppose p x,
assume unique : ∀ y, p y → y = x,
show y₁ = y₂, from eq.trans (unique _ py₁) (eq.symm (unique _ py₂)))
/- exists, forall, exists unique congruences -/
@[congr] lemma forall_congr {A : Type u} {p q : A → Prop} (h : ∀ a, (p a ↔ q a)) : (∀ a, p a) ↔ ∀ a, q a :=
@[congr] lemma forall_congr {α : Type u} {p q : α → Prop} (h : ∀ a, (p a ↔ q a)) : (∀ a, p a) ↔ ∀ a, q a :=
iff.intro (λ p a, iff.mp (h a) (p a)) (λ q a, iff.mpr (h a) (q a))
lemma exists_imp_exists {A : Type u} {p q : A → Prop} (h : ∀ a, (p a → q a)) (p : ∃ a, p a) : ∃ a, q a :=
lemma exists_imp_exists {α : Type u} {p q : α → Prop} (h : ∀ a, (p a → q a)) (p : ∃ a, p a) : ∃ a, q a :=
exists.elim p (λ a hp, ⟨a, h a hp⟩)
@[congr] lemma exists_congr {A : Type u} {p q : A → Prop} (h : ∀ a, (p a ↔ q a)) : (Exists p) ↔ ∃ a, q a :=
@[congr] lemma exists_congr {α : Type u} {p q : α → Prop} (h : ∀ a, (p a ↔ q a)) : (Exists p) ↔ ∃ a, q a :=
iff.intro
(exists_imp_exists (λ a, iff.mp (h a)))
(exists_imp_exists (λ a, iff.mpr (h a)))
@[congr] lemma exists_unique_congr {A : Type u} {p₁ p₂ : A → Prop} (h : ∀ x, p₁ x ↔ p₂ x) : (exists_unique p₁) ↔ (∃! x, p₂ x) := --
@[congr] lemma exists_unique_congr {α : Type u} {p₁ p₂ : α → Prop} (h : ∀ x, p₁ x ↔ p₂ x) : (exists_unique p₁) ↔ (∃! x, p₂ x) := --
exists_congr (λ x, and_congr (h x) (forall_congr (λ y, imp_congr (h y) iff.rfl)))
/- decidable -/
@ -580,12 +580,12 @@ is_false not_false
-- We use "dependent" if-then-else to be able to communicate the if-then-else condition
-- to the branches
@[inline] def dite (c : Prop) [h : decidable c] {A : Type u} : (c → A) → (¬ c → A) → A :=
@[inline] def dite (c : Prop) [h : decidable c] {α : Type u} : (c → α) → (¬ c → α) → α :=
λ t e, decidable.rec_on h e t
/- if-then-else -/
@[inline] def ite (c : Prop) [h : decidable c] {A : Type u} (t e : A) : A :=
@[inline] def ite (c : Prop) [h : decidable c] {α : Type u} (t e : α) : α :=
decidable.rec_on h (λ hnc, e) (λ hc, t)
namespace decidable
@ -599,7 +599,7 @@ namespace decidable
: decidable.rec_on h h₂ h₁ :=
decidable.rec_on h (λ h, h₄) (λ h, false.rec _ (h₃ h))
def by_cases {q : Type u} [C : decidable p] : (p → q) → (¬p → q) → q := dite _
def by_cases {q : Type u} [φ : decidable p] : (p → q) → (¬p → q) → q := dite _
lemma em (p : Prop) [decidable p] : p ∨ ¬p := by_cases or.inl or.inr
@ -616,8 +616,8 @@ section
def decidable_of_decidable_of_eq (hp : decidable p) (h : p = q) : decidable q :=
decidable_of_decidable_of_iff hp h^.to_iff
protected def or.by_cases [decidable p] [decidable q] {A : Type u}
(h : p ∨ q) (h₁ : p → A) (h₂ : q → A) : A :=
protected def or.by_cases [decidable p] [decidable q] {α : Type u}
(h : p ∨ q) (h₁ : p → α) (h₂ : q → α) : α :=
if hp : p then h₁ hp else
if hq : q then h₂ hq else
false.rec _ (or.elim h hp hq)
@ -650,14 +650,14 @@ section
and.decidable
end
instance {A : Type u} [decidable_eq A] (a b : A) : decidable (a ≠ b) :=
instance {α : Type u} [decidable_eq α] (a b : α) : decidable (a ≠ b) :=
implies.decidable
lemma bool.ff_ne_tt : ff = tt → false
.
def is_dec_eq {A : Type u} (p : A → A → bool) : Prop := ∀ ⦃x y : A⦄, p x y = tt → x = y
def is_dec_refl {A : Type u} (p : A → A → bool) : Prop := ∀ x, p x x = tt
def is_dec_eq {α : Type u} (p : α → α → bool) : Prop := ∀ ⦃x y : α⦄, p x y = tt → x = y
def is_dec_refl {α : Type u} (p : α → α → bool) : Prop := ∀ x, p x x = tt
open decidable
instance : decidable_eq bool
@ -666,18 +666,18 @@ instance : decidable_eq bool
| tt ff := is_false (ne.symm bool.ff_ne_tt)
| tt tt := is_true rfl
def decidable_eq_of_bool_pred {A : Type u} {p : A → A → bool} (h₁ : is_dec_eq p) (h₂ : is_dec_refl p) : decidable_eq A :=
take x y : A,
def decidable_eq_of_bool_pred {α : Type u} {p : α → α → bool} (h₁ : is_dec_eq p) (h₂ : is_dec_refl p) : decidable_eq α :=
take x y : α,
if hp : p x y = tt then is_true (h₁ hp)
else is_false (assume hxy : x = y, absurd (h₂ y) (@eq.rec_on _ _ (λ z, ¬p z y = tt) _ hxy hp))
lemma decidable_eq_inl_refl {A : Type u} [h : decidable_eq A] (a : A) : h a a = is_true (eq.refl a) :=
lemma decidable_eq_inl_refl {α : Type u} [h : decidable_eq α] (a : α) : h a a = is_true (eq.refl a) :=
match (h a a) with
| (is_true e) := rfl
| (is_false n) := absurd rfl n
end
lemma decidable_eq_inr_neg {A : Type u} [h : decidable_eq A] {a b : A} : Π n : a ≠ b, h a b = is_false n :=
lemma decidable_eq_inr_neg {α : Type u} [h : decidable_eq α] {a b : α} : Π n : a ≠ b, h a b = is_false n :=
assume n,
match (h a b) with
| (is_true e) := absurd e n
@ -686,23 +686,23 @@ end
/- inhabited -/
class inhabited (A : Type u) :=
(default : A)
class inhabited (α : Type u) :=
(default : α)
def default (A : Type u) [inhabited A] : A :=
inhabited.default A
def default (α : Type u) [inhabited α] : α :=
inhabited.default α
@[inline, irreducible] def arbitrary (A : Type u) [inhabited A] : A :=
default A
@[inline, irreducible] def arbitrary (α : Type u) [inhabited α] : α :=
default α
instance prop.inhabited : inhabited Prop :=
⟨true⟩
instance fun.inhabited (A : Type u) {B : Type v} [h : inhabited B] : inhabited (A → B) :=
instance fun.inhabited (α : Type u) {β : Type v} [h : inhabited β] : inhabited (α → β) :=
inhabited.rec_on h (λ b, ⟨λ a, b⟩)
instance pi.inhabited (A : Type u) {B : A → Type v} [Π x, inhabited (B x)] : inhabited (Π x, B x) :=
⟨λ a, default (B a)⟩
instance pi.inhabited (α : Type u) {β : α → Type v} [Π x, inhabited (β x)] : inhabited (Π x, β x) :=
⟨λ a, default (β a)⟩
instance : inhabited bool :=
⟨ff⟩
@ -713,28 +713,28 @@ instance : inhabited pos_num :=
instance : inhabited num :=
⟨num.zero⟩
class inductive nonempty (A : Type u) : Prop
| intro : A → nonempty
class inductive nonempty (α : Type u) : Prop
| intro : α → nonempty
protected def nonempty.elim {A : Type u} {p : Prop} (h₁ : nonempty A) (h₂ : A → p) : p :=
protected def nonempty.elim {α : Type u} {p : Prop} (h₁ : nonempty α) (h₂ : α → p) : p :=
nonempty.rec h₂ h₁
instance nonempty_of_inhabited {A : Type u} [inhabited A] : nonempty A :=
⟨default A⟩
instance nonempty_of_inhabited {α : Type u} [inhabited α] : nonempty α :=
⟨default α⟩
lemma nonempty_of_exists {A : Type u} {p : A → Prop} : (∃ x, p x) → nonempty A
lemma nonempty_of_exists {α : Type u} {p : α → Prop} : (∃ x, p x) → nonempty α
| ⟨w, h⟩ := ⟨w⟩
/- subsingleton -/
class inductive subsingleton (A : Type u) : Prop
| intro : (∀ a b : A, a = b) → subsingleton
class inductive subsingleton (α : Type u) : Prop
| intro : (∀ a b : α, a = b) → subsingleton
protected def subsingleton.elim {A : Type u} [h : subsingleton A] : ∀ (a b : A), a = b :=
protected def subsingleton.elim {α : Type u} [h : subsingleton α] : ∀ (a b : α), a = b :=
subsingleton.rec (λ p, p) h
protected def subsingleton.helim {A B : Type u} [h : subsingleton A] (h : A = B) : ∀ (a : A) (b : B), a == b :=
eq.rec_on h (λ a b : A, heq_of_eq (subsingleton.elim a b))
protected def subsingleton.helim {α β : Type u} [h : subsingleton α] (h : α = β) : ∀ (a : α) (b : β), a == b :=
eq.rec_on h (λ a b : α, heq_of_eq (subsingleton.elim a b))
instance subsingleton_prop (p : Prop) : subsingleton p :=
⟨λ a b, proof_irrel a b⟩
@ -762,20 +762,20 @@ match h with
| (is_false h) := h₄ h
end
lemma if_pos {c : Prop} [h : decidable c] (hc : c) {A : Type u} {t e : A} : (ite c t e) = t :=
lemma if_pos {c : Prop} [h : decidable c] (hc : c) {α : Type u} {t e : α} : (ite c t e) = t :=
match h with
| (is_true hc) := rfl
| (is_false hnc) := absurd hc hnc
end
lemma if_neg {c : Prop} [h : decidable c] (hnc : ¬c) {A : Type u} {t e : A} : (ite c t e) = e :=
lemma if_neg {c : Prop} [h : decidable c] (hnc : ¬c) {α : Type u} {t e : α} : (ite c t e) = e :=
match h with
| (is_true hc) := absurd hc hnc
| (is_false hnc) := rfl
end
attribute [simp]
lemma if_t_t (c : Prop) [h : decidable c] {A : Type u} (t : A) : (ite c t t) = t :=
lemma if_t_t (c : Prop) [h : decidable c] {α : Type u} (t : α) : (ite c t t) = t :=
match h with
| (is_true hc) := rfl
| (is_false hnc) := rfl
@ -787,8 +787,8 @@ assume hc, eq.rec_on (if_pos hc : ite c t e = t) h
lemma implies_of_if_neg {c t e : Prop} [decidable c] (h : ite c t e) : ¬c → e :=
assume hnc, eq.rec_on (if_neg hnc : ite c t e = e) h
lemma if_ctx_congr {A : Type u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c]
{x y u v : A}
lemma if_ctx_congr {α : Type u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c]
{x y u v : α}
(h_c : b ↔ c) (h_t : c → x = u) (h_e : ¬c → y = v) :
ite b x y = ite c u v :=
match dec_b, dec_c with
@ -799,29 +799,29 @@ match dec_b, dec_c with
end
@[congr]
lemma if_congr {A : Type u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c]
{x y u v : A}
lemma if_congr {α : Type u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c]
{x y u v : α}
(h_c : b ↔ c) (h_t : x = u) (h_e : y = v) :
ite b x y = ite c u v :=
@if_ctx_congr A b c dec_b dec_c x y u v h_c (λ h, h_t) (λ h, h_e)
@if_ctx_congr α b c dec_b dec_c x y u v h_c (λ h, h_t) (λ h, h_e)
lemma if_ctx_simp_congr {A : Type u} {b c : Prop} [dec_b : decidable b] {x y u v : A}
lemma if_ctx_simp_congr {α : Type u} {b c : Prop} [dec_b : decidable b] {x y u v : α}
(h_c : b ↔ c) (h_t : c → x = u) (h_e : ¬c → y = v) :
ite b x y = (@ite c (decidable_of_decidable_of_iff dec_b h_c) A u v) :=
@if_ctx_congr A b c dec_b (decidable_of_decidable_of_iff dec_b h_c) x y u v h_c h_t h_e
ite b x y = (@ite c (decidable_of_decidable_of_iff dec_b h_c) α u v) :=
@if_ctx_congr α b c dec_b (decidable_of_decidable_of_iff dec_b h_c) x y u v h_c h_t h_e
@[congr]
lemma if_simp_congr {A : Type u} {b c : Prop} [dec_b : decidable b] {x y u v : A}
lemma if_simp_congr {α : Type u} {b c : Prop} [dec_b : decidable b] {x y u v : α}
(h_c : b ↔ c) (h_t : x = u) (h_e : y = v) :
ite b x y = (@ite c (decidable_of_decidable_of_iff dec_b h_c) A u v) :=
@if_ctx_simp_congr A b c dec_b x y u v h_c (λ h, h_t) (λ h, h_e)
ite b x y = (@ite c (decidable_of_decidable_of_iff dec_b h_c) α u v) :=
@if_ctx_simp_congr α b c dec_b x y u v h_c (λ h, h_t) (λ h, h_e)
@[simp]
def if_true {A : Type u} (t e : A) : (if true then t else e) = t :=
def if_true {α : Type u} (t e : α) : (if true then t else e) = t :=
if_pos trivial
@[simp]
def if_false {A : Type u} (t e : A) : (if false then t else e) = e :=
def if_false {α : Type u} (t e : α) : (if false then t else e) = e :=
if_neg not_false
lemma if_ctx_congr_prop {b c x y u v : Prop} [dec_b : decidable b] [dec_c : decidable c]
@ -851,24 +851,24 @@ lemma if_simp_congr_prop {b c x y u v : Prop} [dec_b : decidable b]
ite b x y ↔ (@ite c (decidable_of_decidable_of_iff dec_b h_c) Prop u v) :=
@if_ctx_simp_congr_prop b c x y u v dec_b h_c (λ h, h_t) (λ h, h_e)
lemma dif_pos {c : Prop} [h : decidable c] (hc : c) {A : Type u} {t : c → A} {e : ¬ c → A} : dite c t e = t hc :=
lemma dif_pos {c : Prop} [h : decidable c] (hc : c) {α : Type u} {t : c → α} {e : ¬ c → α} : dite c t e = t hc :=
match h with
| (is_true hc) := rfl
| (is_false hnc) := absurd hc hnc
end
lemma dif_neg {c : Prop} [h : decidable c] (hnc : ¬c) {A : Type u} {t : c → A} {e : ¬ c → A} : dite c t e = e hnc :=
lemma dif_neg {c : Prop} [h : decidable c] (hnc : ¬c) {α : Type u} {t : c → α} {e : ¬ c → α} : dite c t e = e hnc :=
match h with
| (is_true hc) := absurd hc hnc
| (is_false hnc) := rfl
end
lemma dif_ctx_congr {A : Type u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c]
{x : b → A} {u : c → A} {y : ¬b → A} {v : ¬c → A}
lemma dif_ctx_congr {α : Type u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c]
{x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
(h_c : b ↔ c)
(h_t : ∀ (h : c), x (iff.mpr h_c h) = u h)
(h_e : ∀ (h : ¬c), y (iff.mpr (not_iff_not_of_iff h_c) h) = v h) :
(@dite b dec_b A x y) = (@dite c dec_c A u v) :=
(@dite b dec_b α x y) = (@dite c dec_c α u v) :=
match dec_b, dec_c with
| (is_false h₁), (is_false h₂) := h_e h₂
| (is_true h₁), (is_true h₂) := h_t h₂
@ -876,16 +876,16 @@ match dec_b, dec_c with
| (is_true h₁), (is_false h₂) := absurd h₁ (iff.mpr (not_iff_not_of_iff h_c) h₂)
end
lemma dif_ctx_simp_congr {A : Type u} {b c : Prop} [dec_b : decidable b]
{x : b → A} {u : c → A} {y : ¬b → A} {v : ¬c → A}
lemma dif_ctx_simp_congr {α : Type u} {b c : Prop} [dec_b : decidable b]
{x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
(h_c : b ↔ c)
(h_t : ∀ (h : c), x (iff.mpr h_c h) = u h)
(h_e : ∀ (h : ¬c), y (iff.mpr (not_iff_not_of_iff h_c) h) = v h) :
(@dite b dec_b A x y) = (@dite c (decidable_of_decidable_of_iff dec_b h_c) A u v) :=
@dif_ctx_congr A b c dec_b (decidable_of_decidable_of_iff dec_b h_c) x u y v h_c h_t h_e
(@dite b dec_b α x y) = (@dite c (decidable_of_decidable_of_iff dec_b h_c) α u v) :=
@dif_ctx_congr α b c dec_b (decidable_of_decidable_of_iff dec_b h_c) x u y v h_c h_t h_e
-- Remark: dite and ite are "defally equal" when we ignore the proofs.
lemma dite_ite_eq (c : Prop) [h : decidable c] {A : Type u} (t : A) (e : A) : dite c (λ h, t) (λ h, e) = ite c t e :=
lemma dite_ite_eq (c : Prop) [h : decidable c] {α : Type u} (t : α) (e : α) : dite c (λ h, t) (λ h, e) = ite c t e :=
match h with
| (is_true hc) := rfl
| (is_false hnc) := rfl
@ -904,31 +904,31 @@ match h₁, h₂ with
end
/- Universe lifting operation -/
structure {r s} ulift (A : Type s) : Type (max 1 s r) :=
up :: (down : A)
structure {r s} ulift (α : Type s) : Type (max 1 s r) :=
up :: (down : α)
namespace ulift
/- Bijection between A and ulift.{v} A -/
lemma up_down {A : Type u} : ∀ (b : ulift.{v} A), up (down b) = b
/- βijection between α and ulift.{v} α -/
lemma up_down {α : Type u} : ∀ (b : ulift.{v} α), up (down b) = b
| (up a) := rfl
lemma down_up {A : Type u} (a : A) : down (up.{v} a) = a :=
lemma down_up {α : Type u} (a : α) : down (up.{v} a) = a :=
rfl
end ulift
/- Equalities for rewriting let-expressions -/
lemma let_value_eq {A : Type u} {B : Type v} {a₁ a₂ : A} (b : A → B) :
a₁ = a₂ → (let x : A := a₁ in b x) = (let x : A := a₂ in b x) :=
lemma let_value_eq {α : Type u} {β : Type v} {a₁ a₂ : α} (b : α → β) :
a₁ = a₂ → (let x : α := a₁ in b x) = (let x : α := a₂ in b x) :=
λ h, eq.rec_on h rfl
lemma let_value_heq {A : Type v} {B : A → Type u} {a₁ a₂ : A} (b : Π x : A, B x) :
a₁ = a₂ → (let x : A := a₁ in b x) == (let x : A := a₂ in b x) :=
lemma let_value_heq {α : Type v} {β : α → Type u} {a₁ a₂ : α} (b : Π x : α, β x) :
a₁ = a₂ → (let x : α := a₁ in b x) == (let x : α := a₂ in b x) :=
λ h, eq.rec_on h (heq.refl (b a₁))
lemma let_body_eq {A : Type v} {B : A → Type u} (a : A) {b₁ b₂ : Π x : A, B x} :
(∀ x, b₁ x = b₂ x) → (let x : A := a in b₁ x) = (let x : A := a in b₂ x) :=
lemma let_body_eq {α : Type v} {β : α → Type u} (a : α) {b₁ b₂ : Π x : α, β x} :
(∀ x, b₁ x = b₂ x) → (let x : α := a in b₁ x) = (let x : α := a in b₂ x) :=
λ h, h a
lemma let_eq {A : Type v} {B : Type u} {a₁ a₂ : A} {b₁ b₂ : A → B} :
a₁ = a₂ → (∀ x, b₁ x = b₂ x) → (let x : A := a₁ in b₁ x) = (let x : A := a₂ in b₂ x) :=
lemma let_eq {α : Type v} {β : Type u} {a₁ a₂ : α} {b₁ b₂ : α → β} :
a₁ = a₂ → (∀ x, b₁ x = b₂ x) → (let x : α := a₁ in b₁ x) = (let x : α := a₂ in b₂ x) :=
λ h₁ h₂, eq.rec_on h₁ (h₂ a₁)

6
library/init/meta/attribute.lean
View file

@ -17,8 +17,8 @@ structure user_attribute :=
`user_attribute` or a sub-structure. -/
meta constant attribute.register : name → command
meta structure caching_user_attribute (A : Type) extends user_attribute :=
(mk_cache : list _root_.name → tactic A)
meta structure caching_user_attribute (α : Type) extends user_attribute :=
(mk_cache : list _root_.name → tactic α)
(dependencies : list _root_.name)
meta constant caching_user_attribute.get_cache : Π {A : Type}, caching_user_attribute A → tactic A
meta constant caching_user_attribute.get_cache : Π {α : Type}, caching_user_attribute α → tactic α

6
library/init/meta/contradiction_tactic.lean
View file

@ -10,7 +10,7 @@ namespace tactic
open expr tactic decidable environment
private meta def contra_A_not_A : list expr → list expr → tactic unit
private meta def contra_p_not_p : list expr → list expr → tactic unit
| [] Hs := failed
| (H1 :: Rs) Hs :=
do t_0 ← infer_type H1,
@ -20,7 +20,7 @@ private meta def contra_A_not_A : list expr → list expr → tactic unit
tgt ← target,
pr ← mk_app `absurd [tgt, H2, H1],
exact pr)
<|> contra_A_not_A Rs Hs
<|> contra_p_not_p Rs Hs
private meta def contra_false : list expr → tactic unit
| [] := failed
@ -75,7 +75,7 @@ meta def contradiction : tactic unit :=
do ctx ← local_context,
(contra_false ctx <|>
contra_not_a_refl_rel_a ctx <|>
contra_A_not_A ctx ctx <|>
contra_p_not_p ctx ctx <|>
contra_constructor_eq ctx <|>
fail "contradiction tactic failed")

28
library/init/meta/converter.lean
View file

@ -10,11 +10,11 @@ import init.meta.tactic init.meta.simp_tactic
import init.meta.congr_lemma init.meta.match_tactic
open tactic
meta structure conv_result (A : Type) :=
(val : A) (rhs : expr) (proof : option expr)
meta structure conv_result (α : Type) :=
(val : α) (rhs : expr) (proof : option expr)
meta def conv (A : Type) : Type :=
name → expr → tactic (conv_result A)
meta def conv (α : Type) : Type :=
name → expr → tactic (conv_result α)
namespace conv
@ -27,7 +27,7 @@ meta def change (new_p : pexpr) : conv unit :=
unify e new_e,
return ⟨(), new_e, none⟩
protected meta def pure {A : Type} : A → conv A :=
protected meta def pure {α : Type} : α → conv α :=
λ a r e, return ⟨a, e, none⟩
private meta def join_proofs (r : name) (o₁ o₂ : option expr) : tactic (option expr) :=
@ -42,25 +42,25 @@ match o₁, o₂ with
end
end
protected meta def seq {A B : Type} (c₁ : conv (A → B)) (c₂ : conv A) : conv B :=
protected meta def seq {α β : Type} (c₁ : conv (α → β)) (c₂ : conv α) : conv β :=
λ r e, do
⟨fn, e₁, pr₁⟩ ← c₁ r e,
⟨a, e₂, pr₂⟩ ← c₂ r e₁,
pr ← join_proofs r pr₁ pr₂,
return ⟨fn a, e₂, pr⟩
protected meta def fail {A : Type} : conv A :=
protected meta def fail {α : Type} : conv α :=
λ r e, failed
protected meta def orelse {A : Type} (c₁ : conv A) (c₂ : conv A) : conv A :=
protected meta def orelse {α : Type} (c₁ : conv α) (c₂ : conv α) : conv α :=
λ r e, c₁ r e <|> c₂ r e
protected meta def map {A B : Type} (f : A → B) (c : conv A) : conv B :=
protected meta def map {α β : Type} (f : α → β) (c : conv α) : conv β :=
λ r e, do
⟨a, e₁, pr⟩ ← c r e,
return ⟨f a, e₁, pr⟩
protected meta def bind {A B : Type} (c₁ : conv A) (c₂ : A → conv B) : conv B :=
protected meta def bind {α β : Type} (c₁ : conv α) (c₂ : α → conv β) : conv β :=
λ r e, do
⟨a, e₁, pr₁⟩ ← c₁ r e,
⟨b, e₂, pr₂⟩ ← c₂ a r e₁,
@ -94,7 +94,7 @@ c <|> return ()
meta def tryb (c : conv unit) : conv bool :=
(c >> return tt) <|> return ff
meta def trace {A : Type} [has_to_tactic_format A] (a : A) : conv unit :=
meta def trace {α : Type} [has_to_tactic_format α] (a : α) : conv unit :=
λ r e, tactic.trace a >> return ⟨(), e, none⟩
meta def trace_lhs : conv unit :=
@ -108,7 +108,7 @@ meta def apply_lemmas_core (s : simp_lemmas) (prove : tactic unit) : conv unit :
meta def apply_lemmas (s : simp_lemmas) : conv unit :=
apply_lemmas_core s failed
/- Adapter for using iff-lemmas as eq-lemmas -/
/- αdapter for using iff-lemmas as eq-lemmas -/
meta def apply_propext_lemmas_core (s : simp_lemmas) (prove : tactic unit) : conv unit :=
λ r e, do
guard (r = `eq),
@ -134,7 +134,7 @@ meta def to_tactic (c : conv unit) : name → expr → tactic (expr × expr) :=
| some p := return (e₁, p)
end
meta def lift_tactic {A : Type} (t : tactic A) : conv A :=
meta def lift_tactic {α : Type} (t : tactic α) : conv α :=
λ r e, do a ← t, return ⟨a, e, none⟩
meta def apply_simp_set (attr_name : name) : conv unit :=
@ -156,7 +156,7 @@ meta def repeat : conv unit → conv unit
return ⟨(), rhs₂, pr⟩)
<|> return ⟨(), lhs, none⟩
meta def first {A : Type} : list (conv A) → conv A
meta def first {α : Type} : list (conv α) → conv α
| [] := conv.fail
| (c::cs) := c <|> first cs

2
library/init/meta/environment.lean
View file

@ -49,7 +49,7 @@ meta constant inductive_dep_elim : environment → name → bool
/- Return tt iff the given name is a generalized inductive datatype -/
meta constant is_ginductive : environment → name → bool
/- Fold over declarations in the environment -/
meta constant fold {A :Type} : environment → A → (declaration → A → A) → A
meta constant fold {α :Type} : environment → α → (declaration → α → α) → α
/- (relation_info env n) returns some value if n is marked as a relation in the given environment.
the tuple contains: total number of arguments of the relation, lhs position and rhs position. -/
meta constant relation_info : environment → name → option (nat × nat × nat)

38
library/init/meta/exceptional.lean
View file

@ -9,49 +9,49 @@ import init.monad init.meta.format
Remark: we use a function that produces a format object as the exception information.
Motivation: the formatting object may be big, and we may create it on demand.
-/
meta inductive exceptional (A : Type)
| success : A → exceptional
meta inductive exceptional (α : Type)
| success : α → exceptional
| exception : (options → format) → exceptional
section
open exceptional
variables {A : Type}
variables [has_to_string A]
variables {α : Type}
variables [has_to_string α]
protected meta def exceptional.to_string : exceptional A → string
protected meta def exceptional.to_string : exceptional α → string
| (success a) := to_string a
| (exception .A e) := "Exception: " ++ to_string (e options.mk)
| (exception .α e) := "Exception: " ++ to_string (e options.mk)
meta instance : has_to_string (exceptional A) :=
meta instance : has_to_string (exceptional α) :=
has_to_string.mk exceptional.to_string
end
namespace exceptional
variables {A B : Type}
variables {α β : Type}
protected meta def to_bool : exceptional A → bool
protected meta def to_bool : exceptional α → bool
| (success _) := tt
| (exception .A _) := ff
| (exception .α _) := ff
protected meta def to_option : exceptional A → option A
protected meta def to_option : exceptional α → option α
| (success a) := some a
| (exception .A _) := none
| (exception .α _) := none
@[inline] protected meta def fmap (f : A → B) (e : exceptional A) : exceptional B :=
@[inline] protected meta def fmap (f : α → β) (e : exceptional α) : exceptional β :=
exceptional.cases_on e
(λ a, success (f a))
(λ f, exception B f)
(λ f, exception β f)
@[inline] protected meta def bind (e₁ : exceptional A) (e₂ : A → exceptional B) : exceptional B :=
@[inline] protected meta def bind (e₁ : exceptional α) (e₂ : α → exceptional β) : exceptional β :=
exceptional.cases_on e₁
(λ a, e₂ a)
(λ f, exception B f)
(λ f, exception β f)
@[inline] protected meta def return (a : A) : exceptional A :=
@[inline] protected meta def return (a : α) : exceptional α :=
success a
@[inline] meta def fail (f : format) : exceptional A :=
exception A (λ u, f)
@[inline] meta def fail (f : format) : exceptional α :=
exception α (λ u, f)
end exceptional
meta instance : monad exceptional :=

2
library/init/meta/expr.lean
View file

@ -60,7 +60,7 @@ if expr.lt a b then ordering.lt
else if a =ₐ b then ordering.eq
else ordering.gt
meta constant expr.fold {A : Type} : expr → A → (expr → nat → A → A) → A
meta constant expr.fold {α : Type} : expr → α → (expr → nat → α → α) → α
meta constant expr.replace : expr → (expr → nat → option expr) → expr
meta constant expr.abstract_local : expr → name → expr

32
library/init/meta/format.lean
View file

@ -25,7 +25,7 @@ meta constant format.flatten : format → format
meta constant format.to_string : format → options → string
meta constant format.of_options : options → format
meta constant format.is_nil : format → bool
meta constant trace_fmt {A : Type u} : format → (unit → A) → A
meta constant trace_fmt {α : Type u} : format → (unit → α) → α
meta instance : inhabited format :=
⟨format.space⟩
@ -36,13 +36,13 @@ meta instance : has_append format :=
meta instance : has_to_string format :=
⟨λ f, format.to_string f options.mk⟩
meta class has_to_format (A : Type u) :=
(to_format : A → format)
meta class has_to_format (α : Type u) :=
(to_format : α → format)
meta instance : has_to_format format :=
⟨id⟩
meta def to_fmt {A : Type u} [has_to_format A] : A → format :=
meta def to_fmt {α : Type u} [has_to_format α] : α → format :=
has_to_format.to_format
meta instance nat_to_format : has_coe nat format :=
@ -56,7 +56,7 @@ open format list
meta def format.indent (f : format) (n : nat) : format :=
nest n (line ++ f)
meta def format.when {A : Type u} [has_to_format A] : bool → A → format
meta def format.when {α : Type u} [has_to_format α] : bool → α → format
| tt a := to_fmt a
| ff a := nil
@ -78,16 +78,16 @@ meta instance : has_to_format nat :=
meta instance : has_to_format char :=
⟨λ c : char, format.of_string [c]⟩
meta def list.to_format_aux {A : Type u} [has_to_format A] : bool → list A → format
meta def list.to_format_aux {α : Type u} [has_to_format α] : bool → list α → format
| b [] := to_fmt ""
| tt (x::xs) := to_fmt x ++ list.to_format_aux ff xs
| ff (x::xs) := to_fmt "," ++ line ++ to_fmt x ++ list.to_format_aux ff xs
meta def list.to_format {A : Type u} [has_to_format A] : list A → format
meta def list.to_format {α : Type u} [has_to_format α] : list α → format
| [] := to_fmt "[]"
| (x::xs) := to_fmt "[" ++ group (nest 1 (list.to_format_aux tt (x::xs))) ++ to_fmt "]"
meta instance {A : Type u} [has_to_format A] : has_to_format (list A) :=
meta instance {α : Type u} [has_to_format α] : has_to_format (list α) :=
⟨list.to_format⟩
attribute [instance] string.has_to_format
@ -98,30 +98,30 @@ meta instance : has_to_format name :=
meta instance : has_to_format unit :=
⟨λ u, to_fmt "()"⟩
meta instance {A : Type u} [has_to_format A] : has_to_format (option A) :=
meta instance {α : Type u} [has_to_format α] : has_to_format (option α) :=
⟨λ o, option.cases_on o
(to_fmt "none")
(λ a, to_fmt "(some " ++ nest 6 (to_fmt a) ++ to_fmt ")")⟩
meta instance {A : Type u} {B : Type v} [has_to_format A] [has_to_format B] : has_to_format (sum A B) :=
meta instance {α : Type u} {β : Type v} [has_to_format α] [has_to_format β] : has_to_format (sum α β) :=
⟨λ s, sum.cases_on s
(λ a, to_fmt "(inl " ++ nest 5 (to_fmt a) ++ to_fmt ")")
(λ b, to_fmt "(inr " ++ nest 5 (to_fmt b) ++ to_fmt ")")⟩
open prod
meta instance {A : Type u} {B : Type v} [has_to_format A] [has_to_format B] : has_to_format (prod A B) :=
⟨λ p, group (nest 1 (to_fmt "(" ++ to_fmt (fst p) ++ to_fmt "," ++ line ++ to_fmt (snd p) ++ to_fmt ")"))⟩
meta instance {α : Type u} {β : Type v} [has_to_format α] [has_to_format β] : has_to_format (prod α β) :=
⟨λ p, group (nest 1 (to_fmt "(" ++ to_fmt p.1 ++ to_fmt "," ++ line ++ to_fmt p.2 ++ to_fmt ")"))⟩
open sigma
meta instance {A : Type u} {B : A → Type v} [has_to_format A] [s : ∀ x, has_to_format (B x)]
: has_to_format (sigma B) :=
⟨λ p, group (nest 1 (to_fmt "⟨" ++ to_fmt (fst p) ++ to_fmt "," ++ line ++ to_fmt (snd p) ++ to_fmt "⟩"))⟩
meta instance {α : Type u} {β : α → Type v} [has_to_format α] [s : ∀ x, has_to_format (β x)]
: has_to_format (sigma β) :=
⟨λ p, group (nest 1 (to_fmt "⟨" ++ to_fmt p.1 ++ to_fmt "," ++ line ++ to_fmt p.2 ++ to_fmt "⟩"))⟩
open subtype
meta instance {A : Type u} {P : A → Prop} [has_to_format A] : has_to_format (subtype P) :=
meta instance {α : Type u} {p : α → Prop} [has_to_format α] : has_to_format (subtype p) :=
⟨λ s, to_fmt (elt_of s)⟩
meta def format.bracket : string → string → format → format

6
library/init/meta/fun_info.lean
View file

@ -15,7 +15,7 @@ structure param_info :=
open format list decidable
private meta def ppfield {A : Type} [has_to_format A] (fname : string) (v : A) : format :=
private meta def ppfield {α : Type} [has_to_format α] (fname : string) (v : α) : format :=
group $ to_fmt fname ++ space ++ to_fmt ":=" ++ space ++ nest (length fname + 4) (to_fmt v)
private meta def concat_fields (f₁ f₂ : format) : format :=
@ -55,7 +55,7 @@ has_to_format.mk fun_info_to_format
using this argument.
For example, consider the function
f : Pi (A : Type), A -> A
f : Pi (α : Type), α -> α
Now, suppse we request get_specialize fun_info for the application
@ -99,7 +99,7 @@ meta constant get_subsingleton_info_n_core : transparency → expr → nat → t
(f a_1 ... a_n).
This tactic is more precise than (get_subsingleton_info f) and (get_subsingleton_info_n f n)
Example: given (f : Pi (A : Type), A -> A), \c get_spec_subsingleton_info for
Example: given (f : Pi (α : Type), α -> α), \c get_spec_subsingleton_info for
f unit b

34
library/init/meta/injection_tactic.lean
View file

@ -11,37 +11,37 @@ open nat tactic environment expr list
private meta def mk_intro_name : name → list name → name
| n₁ (n₂ :: ns) := n₂
| n [] := if n = `a then `H else n
| n [] := if n = `a then `h else n
-- Auxiliary function for introducing the new equalities produced by the
-- injection tactic
private meta def injection_intro : expr → list name → tactic unit
| (pi n bi b d) ns := do
Hname ← return $ mk_intro_name n ns,
H ← intro Hname,
Ht ← infer_type H,
hname ← return $ mk_intro_name n ns,
h ← intro hname,
ht ← infer_type h,
-- Clear new hypothesis if it is of the form (a = a)
@try unit $ do {
(lhs, rhs) ← match_eq Ht,
(lhs, rhs) ← match_eq ht,
unify lhs rhs,
clear H },
clear h },
-- If new hypothesis is of the form (@heq A a B b) where
-- A and B can be unified then convert it into (a = b) using
-- the eq_of_heq lemma
@try unit $ do {
(A, lhs, B, rhs) ← match_heq Ht,
(A, lhs, B, rhs) ← match_heq ht,
unify A B,
Heq ← mk_app `eq [lhs, rhs],
pr ← mk_app `eq_of_heq [H],
assertv Hname Heq pr,
clear H },
heq ← mk_app `eq [lhs, rhs],
pr ← mk_app `eq_of_heq [h],
assertv hname heq pr,
clear h },
injection_intro d (tail ns)
| e ns := skip
meta def injection_with (H : expr) (ns : list name) : tactic unit :=
meta def injection_with (h : expr) (ns : list name) : tactic unit :=
do
Ht ← infer_type H,
(lhs, rhs) ← match_eq Ht,
ht ← infer_type h,
(lhs, rhs) ← match_eq ht,
env ← get_env,
if is_constructor_app env lhs ∧
is_constructor_app env rhs ∧
@ -49,14 +49,14 @@ do
then do
tgt ← target,
I_name ← return $ name.get_prefix (const_name (get_app_fn lhs)),
pr ← mk_app (I_name <.> "no_confusion") [tgt, lhs, rhs, H],
pr ← mk_app (I_name <.> "no_confusion") [tgt, lhs, rhs, h],
pr_type ← infer_type pr,
pr_type ← whnf pr_type,
apply pr,
injection_intro (binding_domain pr_type) ns
else fail "injection tactic failed, argument must be an equality proof where lhs and rhs are of the form (c ...), where c is a constructor"
meta def injection (H : expr) : tactic unit :=
injection_with H []
meta def injection (h : expr) : tactic unit :=
injection_with h []
end tactic

2
library/init/meta/level.lean
View file

@ -24,7 +24,7 @@ meta constant level.has_decidable_eq : decidable_eq level
attribute [instance] level.has_decidable_eq
meta constant level.lt : level → level → bool
meta constant level.lex_lt : level → level → bool
meta constant level.fold {A :Type} : level → A → (level → A → A) → A
meta constant level.fold {α :Type} : level → α → (level → α → α) → α
/- Return the given level expression normal form -/
meta constant level.normalize : level → level
/- Return tt iff lhs and rhs denote the same level.

2
library/init/meta/options.lean
View file

@ -17,7 +17,7 @@ meta constant options.get_bool : options → name → bool → bool
meta constant options.get_nat : options → name → nat → nat
meta constant options.get_string : options → name → string → string
meta constant options.join : options → options → options
meta constant options.fold {A : Type u} : options → A → (name → A → A) → A
meta constant options.fold {α : Type u} : options → α → (name → α → α) → α
meta constant options.has_decidable_eq : decidable_eq options
attribute [instance] options.has_decidable_eq

6
library/init/meta/pexpr.lean
View file

@ -20,10 +20,10 @@ meta constant pexpr.to_string : pexpr → string
meta instance : has_to_string pexpr :=
⟨pexpr.to_string⟩
meta class has_to_pexpr (A : Type u) :=
(to_pexpr : A → pexpr)
meta class has_to_pexpr (α : Type u) :=
(to_pexpr : α → pexpr)
meta def to_pexpr {A : Type u} [has_to_pexpr A] : A → pexpr :=
meta def to_pexpr {α : Type u} [has_to_pexpr α] : α → pexpr :=
has_to_pexpr.to_pexpr
meta instance : has_to_pexpr pexpr :=

2
library/init/meta/rb_map.lean
View file

@ -17,7 +17,7 @@ meta constant contains {key : Type} {data : Type} : rb_map key data → ke
meta constant find {key : Type} {data : Type} : rb_map key data → key → option data
meta constant min {key : Type} {data : Type} : rb_map key data → option data
meta constant max {key : Type} {data : Type} : rb_map key data → option data
meta constant fold {key : Type} {data : Type} {A :Type} : rb_map key data → A → (key → data → A → A) → A
meta constant fold {key : Type} {data : Type} {α :Type} : rb_map key data → α → (key → data → α → α) → α
attribute [inline]
meta def mk (key : Type) [has_ordering key] (data : Type) : rb_map key data :=

80
library/init/meta/simp_tactic.lean
View file

@ -66,9 +66,9 @@ simp_lemmas.dsimplify_core default_max_steps ff
namespace tactic
meta constant dsimplify_core
/- The user state type. -/
{A : Type}
{α : Type}
/- Initial user data -/
(a : A)
(a : α)
(max_steps : nat)
/- If visit_instances = ff, then instance implicit arguments are not visited, but
tactic will canonize them. -/
@ -78,12 +78,12 @@ meta constant dsimplify_core
- 'new_a' is the new value for the user data
- 'new_e' is a new expression that must be definitionally equal to 'e',
- 'flag' if tt 'new_e' children should be visited, and 'post' invoked. -/
(pre : A → expr → tactic (A × expr × bool))
(pre : α → expr → tactic (α × expr × bool))
/- (post a e) is invoked after visiting the children of subterm 'e',
The output is similar to (pre a e), but the 'flag' indicates whether
the new expression should be revisited or not. -/
(post : A → expr → tactic (A × expr × bool))
: expr → tactic (A × expr)
(post : α → expr → tactic (α × expr × bool))
: expr → tactic (α × expr)
meta def dsimplify
(pre : expr → tactic (expr × bool))
@ -166,17 +166,17 @@ meta constant simplify_core
meta constant ext_simplify_core
/- The user state type. -/
{A : Type}
{α : Type}
/- Initial user data -/
(a : A)
(a : α)
(c : simplify_config)
/- Congruence and simplification lemmas.
Remark: the simplification lemmas at not applied automatically like in the simplify_core tactic.
the caller must use them at pre/post. -/
(s : simp_lemmas)
/- Tactic for dischaging hypothesis in conditional rewriting rules.
The argument 'A' is the current user state. -/
(prove : A → tactic A)
The argument 'α' is the current user state. -/
(prove : α → tactic α)
/- (pre a r s p e) is invoked before visiting the children of subterm 'e',
'r' is the simplification relation being used, 's' is the updated set of lemmas if 'contextual' is tt,
'p' is the "parent" expression (if there is one).
@ -185,14 +185,14 @@ meta constant ext_simplify_core
- 'new_e' is a new expression s.t. 'e r new_e'
- 'new_pr' is a proof for 'e r new_e', If it is none, the proof is assumed to be by reflexivity
- 'flag' if tt 'new_e' children should be visited, and 'post' invoked. -/
(pre : A → simp_lemmas → name → option expr → expr → tactic (A × expr × option expr × bool))
(pre : α → simp_lemmas → name → option expr → expr → tactic (α × expr × option expr × bool))
/- (post a r s p e) is invoked after visiting the children of subterm 'e',
The output is similar to (pre a r s p e), but the 'flag' indicates whether
the new expression should be revisited or not. -/
(post : A → simp_lemmas → name → option expr → expr → tactic (A × expr × option expr × bool))
(post : α → simp_lemmas → name → option expr → expr → tactic (α × expr × option expr × bool))
/- simplification relation -/
(r : name) :
expr → tactic (A × expr × expr)
expr → tactic (α × expr × expr)
meta def simplify (cfg : simplify_config) (extra_lemmas : list expr) (e : expr) : tactic (expr × expr) :=
do lemmas ← simp_lemmas.mk_default,
@ -201,16 +201,16 @@ do lemmas ← simp_lemmas.mk_default,
simplify_core cfg new_lemmas `eq e
meta def simplify_goal (cfg : simplify_config) (extra_lemmas : list expr) : tactic unit :=
do (new_target, Heq) ← target >>= simplify cfg extra_lemmas,
assert `Htarget new_target, swap,
Ht ← get_local `Htarget,
mk_app `eq.mpr [Heq, Ht] >>= exact
do (new_target, heq) ← target >>= simplify cfg extra_lemmas,
assert `htarget new_target, swap,
ht ← get_local `htarget,
mk_app `eq.mpr [heq, ht] >>= exact
meta def simp : tactic unit :=
simplify_goal default_simplify_config [] >> try triv >> try reflexivity
meta def simp_using (Hs : list expr) : tactic unit :=
simplify_goal default_simplify_config Hs >> try triv
meta def simp_using (hs : list expr) : tactic unit :=
simplify_goal default_simplify_config hs >> try triv
meta def ctx_simp : tactic unit :=
simplify_goal {default_simplify_config with contextual := tt} [] >> try triv >> try reflexivity
@ -219,12 +219,12 @@ meta def dsimp : tactic unit :=
do S ← simp_lemmas.mk_default,
target >>= S^.dsimplify >>= change
meta def dsimp_at (H : expr) : tactic unit :=
do num_reverted : ℕ ← revert H,
meta def dsimp_at (h : expr) : tactic unit :=
do num_reverted : ℕ ← revert h,
(expr.pi n bi d b : expr) ← target | failed,
S ← simp_lemmas.mk_default,
H_simp ← S^.dsimplify d,
change $ expr.pi n bi H_simp b,
h_simp ← S^.dsimplify d,
change $ expr.pi n bi h_simp b,
intron num_reverted
private meta def is_equation : expr → bool
@ -233,38 +233,38 @@ private meta def is_equation : expr → bool
private meta def collect_eqs : list expr → tactic (list expr)
| [] := return []
| (H :: Hs) := do
Eqs ← collect_eqs Hs,
Htype ← infer_type H >>= whnf,
return $ if is_equation Htype then H :: Eqs else Eqs
| (h :: hs) := do
Eqs ← collect_eqs hs,
htype ← infer_type h >>= whnf,
return $ if is_equation htype then h :: Eqs else Eqs
/- Simplify target using all hypotheses in the local context. -/
meta def simp_using_hs : tactic unit :=
local_context >>= collect_eqs >>= simp_using
meta def simp_core_at (extra_lemmas : list expr) (H : expr) : tactic unit :=
do when (expr.is_local_constant H = ff) (fail "tactic simp_at failed, the given expression is not a hypothesis"),
Htype ← infer_type H,
(new_Htype, Heq) ← simplify default_simplify_config extra_lemmas Htype,
assert (expr.local_pp_name H) new_Htype,
mk_app `eq.mp [Heq, H] >>= exact,
try $ clear H
meta def simp_core_at (extra_lemmas : list expr) (h : expr) : tactic unit :=
do when (expr.is_local_constant h = ff) (fail "tactic simp_at failed, the given expression is not a hypothesis"),
htype ← infer_type h,
(new_htype, heq) ← simplify default_simplify_config extra_lemmas htype,
assert (expr.local_pp_name h) new_htype,
mk_app `eq.mp [heq, h] >>= exact,
try $ clear h
meta def simp_at : expr → tactic unit :=
simp_core_at []
meta def simp_at_using (Hs : list expr) : expr → tactic unit :=
simp_core_at Hs
meta def simp_at_using (hs : list expr) : expr → tactic unit :=
simp_core_at hs
meta def simp_at_using_hs (H : expr) : tactic unit :=
do Hs ← local_context >>= collect_eqs,
simp_core_at (list.filter (ne H) Hs) H
meta def simp_at_using_hs (h : expr) : tactic unit :=
do hs ← local_context >>= collect_eqs,
simp_core_at (list.filter (ne h) hs) h
meta def mk_eq_simp_ext (simp_ext : expr → tactic (expr × expr)) : tactic unit :=
do (lhs, rhs) ← target >>= match_eq,
(new_rhs, Heq) ← simp_ext lhs,
(new_rhs, heq) ← simp_ext lhs,
unify rhs new_rhs,
exact Heq
exact heq
/- Simp attribute support -/

106
library/init/meta/tactic.lean
View file

@ -25,52 +25,52 @@ end tactic_state
meta instance : has_to_format tactic_state :=
⟨tactic_state.to_format⟩
meta inductive tactic_result (A : Type u)
| success : A → tactic_state → tactic_result
meta inductive tactic_result (α : Type u)
| success : α → tactic_state → tactic_result
| exception : (unit → format) → option expr → tactic_state → tactic_result
open tactic_result
section
variables {A : Type u}
variables [has_to_string A]
variables {α : Type u}
variables [has_to_string α]
meta def tactic_result_to_string : tactic_result A → string
meta def tactic_result_to_string : tactic_result α → string
| (success a s) := to_string a
| (exception .A t ref s) := "Exception: " ++ to_string (t ())
| (exception .α t ref s) := "Exception: " ++ to_string (t ())
meta instance : has_to_string (tactic_result A) :=
meta instance : has_to_string (tactic_result α) :=
⟨tactic_result_to_string⟩
end
attribute [reducible]
meta def tactic (A : Type u) :=
tactic_state → tactic_result A
meta def tactic (α : Type u) :=
tactic_state → tactic_result α
section
variables {A : Type u} {B : Type v}
variables {α : Type u} {β : Type v}
@[inline] meta def tactic_fmap (f : A → B) (t : tactic A) : tactic B :=
@[inline] meta def tactic_fmap (f : α → β) (t : tactic α) : tactic β :=
λ s, tactic_result.cases_on (t s)
(λ a s', success (f a) s')
(λ e s', exception B e s')
(λ e s', exception β e s')
@[inline] meta def tactic_bind (t₁ : tactic A) (t₂ : A → tactic B) : tactic B :=
@[inline] meta def tactic_bind (t₁ : tactic α) (t₂ : α → tactic β) : tactic β :=
λ s, tactic_result.cases_on (t₁ s)
(λ a s', t₂ a s')
(λ e s', exception B e s')
(λ e s', exception β e s')
@[inline] meta def tactic_return (a : A) : tactic A :=
@[inline] meta def tactic_return (a : α) : tactic α :=
λ s, success a s
meta def tactic_orelse {A : Type u} (t₁ t₂ : tactic A) : tactic A :=
meta def tactic_orelse {α : Type u} (t₁ t₂ : tactic α) : tactic α :=
λ s, tactic_result.cases_on (t₁ s)
success
(λ e₁ ref₁ s', tactic_result.cases_on (t₂ s)
success
(exception A))
(exception α))
@[inline] meta def tactic_seq (t₁ : tactic A) (t₂ : tactic B) : tactic B :=
@[inline] meta def tactic_seq (t₁ : tactic α) (t₂ : tactic β) : tactic β :=
tactic_bind t₁ (λ a, t₂)
infixl ` >>=[tactic] `:2 := tactic_bind
@ -80,31 +80,31 @@ end
meta instance : monad tactic :=
⟨@tactic_fmap, @tactic_return, @tactic_bind⟩
meta def tactic.fail {A : Type u} {B : Type v} [has_to_format B] (msg : B) : tactic A :=
λ s, exception A (λ u, to_fmt msg) none s
meta def tactic.fail {α : Type u} {β : Type v} [has_to_format β] (msg : β) : tactic α :=
λ s, exception α (λ u, to_fmt msg) none s
meta def tactic.failed {A : Type u} : tactic A :=
meta def tactic.failed {α : Type u} : tactic α :=
tactic.fail "failed"
meta instance : alternative tactic :=
⟨@tactic_fmap, (λ A a s, success a s), (@fapp _ _), @tactic.failed, @tactic_orelse⟩
⟨@tactic_fmap, (λ α a s, success a s), (@fapp _ _), @tactic.failed, @tactic_orelse⟩
meta def {u₁ u₂} tactic.up {A : Type u₂} (t : tactic A) : tactic (ulift.{u₁} A) :=
meta def {u₁ u₂} tactic.up {α : Type u₂} (t : tactic α) : tactic (ulift.{u₁} α) :=
λ s, match t s with
| success a s' := success (ulift.up a) s'
| exception .A t ref s := exception (ulift A) t ref s
| exception .α t ref s := exception (ulift α) t ref s
end
meta def {u₁ u₂} tactic.down {A : Type u₂} (t : tactic (ulift.{u₁} A)) : tactic A :=
meta def {u₁ u₂} tactic.down {α : Type u₂} (t : tactic (ulift.{u₁} α)) : tactic α :=
λ s, match t s with
| success (ulift.up a) s' := success a s'
| exception .(ulift A) t ref s := exception A t ref s
| exception .(ulift α) t ref s := exception α t ref s
end
namespace tactic
variables {A : Type u}
variables {α : Type u}
meta def try (t : tactic A) : tactic unit :=
meta def try (t : tactic α) : tactic unit :=
λ s, tactic_result.cases_on (t s)
(λ a, success ())
(λ e ref s', success () s)
@ -113,7 +113,7 @@ meta def skip : tactic unit :=
success ()
open list
meta def foreach : list A → (A → tactic unit) → tactic unit
meta def foreach : list α → (α → tactic unit) → tactic unit
| [] fn := skip
| (e::es) fn := do fn e, foreach es fn
@ -131,23 +131,23 @@ meta def repeat_exactly : nat → tactic unit → tactic unit
meta def repeat : tactic unit → tactic unit :=
repeat_at_most 100000
meta def returnex {A : Type 1} (e : exceptional A) : tactic A :=
meta def returnex {α : Type 1} (e : exceptional α) : tactic α :=
λ s, match e with
| (exceptional.success a) := tactic_result.success a s
| (exceptional.exception .A f) := tactic_result.exception A (λ u, f options.mk) none s -- TODO(Leo): extract options from environment
| (exceptional.exception .α f) := tactic_result.exception α (λ u, f options.mk) none s -- TODO(Leo): extract options from environment
end
meta def returnopt (e : option A) : tactic A :=
meta def returnopt (e : option α) : tactic α :=
λ s, match e with
| (some a) := tactic_result.success a s
| none := tactic_result.exception A (λ u, to_fmt "failed") none s
| none := tactic_result.exception α (λ u, to_fmt "failed") none s
end
/- Decorate t's exceptions with msg -/
meta def decorate_ex (msg : format) (t : tactic A) : tactic A :=
meta def decorate_ex (msg : format) (t : tactic α) : tactic α :=
λ s, tactic_result.cases_on (t s)
success
(λ e, exception A (λ u, msg ++ format.nest 2 (format.line ++ e u)))
(λ e, exception α (λ u, msg ++ format.nest 2 (format.line ++ e u)))
attribute [inline]
meta def write (s' : tactic_state) : tactic unit :=
@ -161,34 +161,34 @@ end tactic
meta def tactic_format_expr (e : expr) : tactic format :=
do s ← tactic.read, return (tactic_state.format_expr s e)
meta class has_to_tactic_format (A : Type u) :=
(to_tactic_format : A → tactic format)
meta class has_to_tactic_format (α : Type u) :=
(to_tactic_format : α → tactic format)
meta instance : has_to_tactic_format expr :=
⟨tactic_format_expr⟩
meta def tactic.pp {A : Type u} [has_to_tactic_format A] : A → tactic format :=
meta def tactic.pp {α : Type u} [has_to_tactic_format α] : α → tactic format :=
has_to_tactic_format.to_tactic_format
open tactic format
meta def list_to_tactic_format_aux {A : Type u} [has_to_tactic_format A] : bool → list A → tactic format
meta def list_to_tactic_format_aux {α : Type u} [has_to_tactic_format α] : bool → list α → tactic format
| b [] := return $ to_fmt ""
| b (x::xs) := do
f₁ ← pp x,
f₂ ← list_to_tactic_format_aux ff xs,
return $ (if ¬ b then to_fmt "," ++ line else nil) ++ f₁ ++ f₂
meta def list_to_tactic_format {A : Type u} [has_to_tactic_format A] : list A → tactic format
meta def list_to_tactic_format {α : Type u} [has_to_tactic_format α] : list α → tactic format
| [] := return $ to_fmt "[]"
| (x::xs) := do
f ← list_to_tactic_format_aux tt (x::xs),
return $ to_fmt "[" ++ group (nest 1 f) ++ to_fmt "]"
meta instance {A : Type u} [has_to_tactic_format A] : has_to_tactic_format (list A) :=
meta instance {α : Type u} [has_to_tactic_format α] : has_to_tactic_format (list α) :=
⟨list_to_tactic_format⟩
meta instance has_to_format_to_has_to_tactic_format (A : Type) [has_to_format A] : has_to_tactic_format A :=
meta instance has_to_format_to_has_to_tactic_format (α : Type) [has_to_format α] : has_to_tactic_format α :=
⟨(λ x, return x) ∘ to_fmt⟩
namespace tactic
@ -202,7 +202,7 @@ meta def get_decl (n : name) : tactic declaration :=
do s ← read,
returnex $ environment.get (env s) n
meta def trace {A : Type u} [has_to_tactic_format A] (a : A) : tactic unit :=
meta def trace {α : Type u} [has_to_tactic_format α] (a : α) : tactic unit :=
do fmt ← pp a,
return $ _root_.trace_fmt fmt (λ u, ())
@ -218,11 +218,11 @@ inductive transparency
export transparency (reducible semireducible)
/- (eval_expr A A_as_expr e) evaluates 'e' IF 'e' has type 'A'.
'A' must be a closed term.
'A_as_expr' is synthesized by the code generator.
/- (eval_expr α α_as_expr e) evaluates 'e' IF 'e' has type 'α'.
'α' must be a closed term.
'α_as_expr' is synthesized by the code generator.
'e' must be a closed expression at runtime. -/
meta constant eval_expr (A : Type u) {A_expr : pexpr} : expr → tactic A
meta constant eval_expr (α : Type u) {α_expr : pexpr} : expr → tactic α
/- Return the partial term/proof constructed so far. Note that the resultant expression
may contain variables that are not declarate in the current main goal. -/
@ -261,10 +261,10 @@ meta constant get_unused_name : name → option nat → tactic name
type inference.
Example, given
rel.{l_1 l_2} : Pi (A : Type.{l_1}) (B : A -> Type.{l_2}), (Pi x : A, B x) -> (Pi x : A, B x) -> , Prop
rel.{l_1 l_2} : Pi (α : Type.{l_1}) (β : α -> Type.{l_2}), (Pi x : α, β x) -> (Pi x : α, β x) -> , Prop
nat : Type 1
real : Type 1
vec.{l} : Pi (A : Type l) (n : nat), Type.{l1}
vec.{l} : Pi (α : Type l) (n : nat), Type.{l1}
f g : Pi (n : nat), vec real n
then
mk_app_core semireducible "rel" [f, g]
@ -371,7 +371,7 @@ meta def cleanup : tactic unit :=
get_goals >>= set_goals
/- Auxiliary definition used to implement begin ... end blocks -/
meta def step {A : Type u} (t : tactic A) : tactic unit :=
meta def step {α : Type u} (t : tactic α) : tactic unit :=
t >>[tactic] cleanup
/- Add (H : T := pr) to the current goal -/
@ -459,7 +459,7 @@ end
meta def match_heq (e : expr) : tactic (expr × expr × expr × expr) :=
do match (expr.is_heq e) with
| (some (A, lhs, B, rhs)) := return (A, lhs, B, rhs)
| (some (α, lhs, β, rhs)) := return (α, lhs, β, rhs)
| none := fail "expression is not a heterogeneous equality"
end
@ -517,7 +517,7 @@ rotate_left
/- first [t_1, ..., t_n] applies the first tactic that doesn't fail.
The tactic fails if all t_i's fail. -/
meta def first {A : Type u} : list (tactic A) → tactic A
meta def first {α : Type u} : list (tactic α) → tactic α
| [] := fail "first tactic failed, no more alternatives"
| (t::ts) := t <|> first ts
@ -679,7 +679,7 @@ do tgt : expr ← target,
to_expr `((%%e : %%tgt)) >>= exact
/- (solve_aux type tac) synthesize an element of 'type' using tactic 'tac' -/
meta def solve_aux {A : Type} (type : expr) (tac : tactic A) : tactic (A × expr) :=
meta def solve_aux {α : Type} (type : expr) (tac : tactic α) : tactic (α × expr) :=
do m ← mk_meta_var type,
gs ← get_goals,
set_goals [m],

10
library/init/meta/vm.lean
View file

@ -68,14 +68,14 @@ meta constant args_info : vm_decl → list vm_local_info
end vm_decl
meta constant vm_core : Type → Type
meta constant vm_core.map {A B : Type} : (A → B) → vm_core A → vm_core B
meta constant vm_core.ret {A : Type} : A → vm_core A
meta constant vm_core.bind {A B : Type} : vm_core A → (A → vm_core B) → vm_core B
meta constant vm_core.map {α β : Type} : (α → β) → vm_core α → vm_core β
meta constant vm_core.ret {α : Type} : α → vm_core α
meta constant vm_core.bind {α β : Type} : vm_core α → (α → vm_core β) → vm_core β
meta instance : monad vm_core :=
⟨@vm_core.map, @vm_core.ret, @vm_core.bind⟩
@[reducible] meta def vm (A : Type) : Type := optionT.{1 1} vm_core A
@[reducible] meta def vm (α : Type) : Type := option_t.{1 1} vm_core α
namespace vm
meta constant get_env : vm environment
@ -120,7 +120,7 @@ meta constant eof : vm bool
/- Return the list of declarations tagged with the given attribute. -/
meta constant get_attribute : name → vm (list name)
meta def trace {A : Type} [has_to_format A] (a : A) : vm unit :=
meta def trace {α : Type} [has_to_format α] (a : α) : vm unit :=
do fmt ← return $ to_fmt a,
return $ _root_.trace_fmt fmt (λ u, ())

18
library/init/monad.lean
View file

@ -7,23 +7,23 @@ prelude
import init.applicative init.string init.trace
universe variables u v
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)
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)
@[inline] def return {M : Type u → Type v} [monad M] {A : Type u} : A → M A :=
monad.ret M
@[inline] def return {m : Type u → Type v} [monad m] {a : Type u} : a → m a :=
monad.ret m
def 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)
@[inline] instance monad_is_applicative (M : Type u → Type v) [monad M] : applicative M :=
@[inline] instance monad_is_applicative (m : Type u → Type v) [monad m] : applicative m :=
⟨@fmap _ _, @return _ _, @fapp _ _⟩
@[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
@[inline] def monad.and_then {a b : Type u} {m : Type u → Type v} [monad m] (x : m a) (y : m b) : m b :=
do x, y
infixl ` >>= `:2 := monad.bind
infixl ` >> `:2 := monad.and_then

40
library/init/monad_combinators.lean
View file

@ -10,27 +10,27 @@ import init.monad init.list
universe variables u v w
namespace monad
/- Remark: we use (u+1) to make sure B is not a proposition.
That is, we are making sure that B and (list B) inhabit the same universe -/
def mapm {m : Type (u+1) → Type v} [monad m] {A : Type w} {B : Type (u+1)} (f : A → m B) : list A → m (list B)
/- Remark: we use (u+1) to make sure β is not a proposition.
That is, we are making sure that β and (list β) inhabit the same universe -/
def mapm {m : Type (u+1) → Type v} [monad m] {α : Type w} {β : Type (u+1)} (f : α → m β) : list α → m (list β)
| [] := return []
| (h :: t) := do h' ← f h, t' ← mapm t, return (h' :: t')
def mapm' {m : Type → Type v} [monad m] {A : Type u} {B : Type} (f : A → m B) : list A → m unit
def mapm' {m : Type → Type v} [monad m] {α : Type u} {β : Type} (f : α → m β) : list α → m unit
| [] := return ()
| (h :: t) := f h >> mapm' t
def for {m : Type (u+1) → Type v} [monad m] {A : Type w} {B : Type (u+1)} (l : list A) (f : A → m B) : m (list B) :=
def for {m : Type (u+1) → Type v} [monad m] {α : Type w} {β : Type (u+1)} (l : list α) (f : α → m β) : m (list β) :=
mapm f l
def for' {m : Type → Type v} [monad m] {A : Type u} {B : Type} (l : list A) (f : A → m B) : m unit :=
def for' {m : Type → Type v} [monad m] {α : Type u} {β : Type} (l : list α) (f : α → m β) : m unit :=
mapm' f l
def sequence {m : Type (u+1) → Type v} [monad m] {A : Type (u+1)} : list (m A) → m (list A)
def sequence {m : Type (u+1) → Type v} [monad m] {α : Type (u+1)} : list (m α) → m (list α)
| [] := return []
| (h :: t) := do h' ← h, t' ← sequence t, return (h' :: t')
def sequence' {m : Type → Type u} [monad m] {A : Type} : list (m A) → m unit
def sequence' {m : Type → Type u} [monad m] {α : Type} : list (m α) → m unit
| [] := return ()
| (h :: t) := h >> sequence' t
@ -40,10 +40,10 @@ infix ` >=> `:2 := λ s t a, s a >>= t
infix ` <=< `:2 := λ t s a, s a >>= t
def join {m : Type u → Type u} [monad m] {A : Type u} (a : m (m A)) : m A :=
def join {m : Type u → Type u} [monad m] {α : Type u} (a : m (m α)) : m α :=
bind a id
def filter {m : Type → Type v} [monad m] {A : Type} (f : A → m bool) : list A → m (list A)
def filter {m : Type → Type v} [monad m] {α : Type} (f : α → m bool) : list α → m (list α)
| [] := return []
| (h :: t) := do b ← f h, t' ← filter t, cond b (return (h :: t')) (return t')
@ -53,26 +53,26 @@ cond b t (return ())
def unlessb {m : Type → Type} [monad m] (b : bool) (t : m unit) : m unit :=
cond b (return ()) t
def cond {m : Type → Type} [monad m] {A : Type} (mbool : m bool)
(tm fm : m A) : m A :=
def cond {m : Type → Type} [monad m] {α : Type} (mbool : m bool)
(tm fm : m α) : m α :=
do b ← mbool, cond b tm fm
def lift {m : Type u → Type v} [monad m] {A R : Type u} (f : A → R) (ma : m A) : m R :=
def lift {m : Type u → Type v} [monad m] {α φ : Type u} (f : α → φ) (ma : m α) : m φ :=
do a ← ma, return (f a)
def lift₂ {m : Type u → Type v} [monad m] {A R : Type u} (f : A → A → R) (ma₁ ma₂: m A) : m R :=
def lift₂ {m : Type u → Type v} [monad m] {α φ : Type u} (f : α → α → φ) (ma₁ ma₂: m α) : m φ :=
do a₁ ← ma₁, a₂ ← ma₂, return (f a₁ a₂)
def lift₃ {m : Type u → Type v} [monad m] {A R : Type u} (f : A → A → A → R)
(ma₁ ma₂ ma₃ : m A) : m R :=
def lift₃ {m : Type u → Type v} [monad m] {α φ : Type u} (f : α → α → α → φ)
(ma₁ ma₂ ma₃ : m α) : m φ :=
do a₁ ← ma₁, a₂ ← ma₂, a₃ ← ma₃, return (f a₁ a₂ a₃)
def lift₄ {m : Type u → Type v} [monad m] {A R : Type u} (f : A → A → A → A → R)
(ma₁ ma₂ ma₃ ma₄ : m A) : m R :=
def lift₄ {m : Type u → Type v} [monad m] {α φ : Type u} (f : α → α → α → α → φ)
(ma₁ ma₂ ma₃ ma₄ : m α) : m φ :=
do a₁ ← ma₁, a₂ ← ma₂, a₃ ← ma₃, a₄ ← ma₄, return (f a₁ a₂ a₃ a₄)
def lift₅ {m : Type u → Type v} [monad m] {A R : Type u} (f : A → A → A → A → A → R)
(ma₁ ma₂ ma₃ ma₄ ma₅ : m A) : m R :=
def lift₅ {m : Type u → Type v} [monad m] {α φ : Type u} (f : α → α → α → α → α → φ)
(ma₁ ma₂ ma₃ ma₄ ma₅ : m α) : m φ :=
do a₁ ← ma₁, a₂ ← ma₂, a₃ ← ma₃, a₄ ← ma₄, a₅ ← ma₅, return (f a₁ a₂ a₃ a₄ a₅)
end monad

2
library/init/nat.lean
View file

@ -362,7 +362,7 @@ namespace nat
lemma le_add_left (n m : ℕ): n ≤ m + n :=
nat.add_comm n m ▸ le_add_right n m
def {u} repeat {A : Type u} (f : ℕ → A → A) : ℕ → A → A
def {u} repeat {α : Type u} (f : ℕ → α → α) : ℕ → α → α
| 0 a := a
| (succ n) a := f n (repeat n a)

8
library/init/nat_div.lean
View file

@ -11,25 +11,25 @@ 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 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
if h : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma h) y + 1 else zero
protected def div := well_founded.fix lt_wf div.F
instance : has_div nat :=
⟨nat.div⟩
lemma 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 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
if h : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma h) y else x
protected def mod := well_founded.fix lt_wf mod.F
instance : has_mod nat :=
⟨nat.mod⟩
lemma 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

64
library/init/option.lean
View file

@ -9,80 +9,80 @@ open decidable
universe variables u v
instance (A : Type u) : inhabited (option A) :=
instance (α : Type u) : inhabited (option α) :=
⟨none⟩
instance {A : Type u} [H : decidable_eq A] : decidable_eq (option A)
instance {α : Type u} [d : decidable_eq α] : decidable_eq (option α)
| none none := is_true rfl
| none (some v₂) := is_false (λ H, option.no_confusion H)
| (some v₁) none := is_false (λ H, option.no_confusion H)
| none (some v₂) := is_false (λ h, option.no_confusion h)
| (some v₁) none := is_false (λ h, option.no_confusion h)
| (some v₁) (some v₂) :=
match (H v₁ v₂) with
| (is_true e) := is_true (congr_arg (@some A) e)
| (is_false n) := is_false (λ H, option.no_confusion H (λ e, absurd e n))
match (d v₁ v₂) with
| (is_true e) := is_true (congr_arg (@some α) e)
| (is_false n) := is_false (λ h, option.no_confusion h (λ e, absurd e n))
end
@[inline] def option_fmap {A : Type u} {B : Type v} (f : A → B) : option A → option B
@[inline] def option_fmap {α : Type u} {β : Type v} (f : α → β) : option α → option β
| none := none
| (some a) := some (f a)
@[inline] def option_bind {A : Type u} {B : Type v} : option A → (A → option B) → option B
@[inline] def option_bind {α : Type u} {β : Type v} : option α → (α → option β) → option β
| none b := none
| (some a) b := b a
instance : monad option :=
monad.mk @option_fmap @some @option_bind
def option_orelse {A : Type u} : option A → option A → option A
def option_orelse {α : Type u} : option α → option α → option α
| (some a) o := some a
| none (some a) := some a
| none none := none
instance {A : Type u} : alternative option :=
instance {α : Type u} : alternative option :=
alternative.mk @option_fmap @some (@fapp _ _) @none @option_orelse
def optionT (M : Type (max 1 u) → Type v) [monad M] (A : Type u) : Type v :=
M (option A)
def option_t (m : Type (max 1 u) → Type v) [monad m] (α : Type u) : Type v :=
m (option α)
@[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
@[inline] def option_t_fmap {m : Type (max 1 u) → Type v} [monad m] {α β : Type u} (f : α → β) (e : option_t m α) : option_t m β :=
show m (option β), from
do o ← e,
match o with
| none := return none
| (some a) := return (some (f a))
end
@[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
@[inline] def option_t_bind {m : Type (max 1 u) → Type v} [monad m] {α β : Type u} (a : option_t m α) (b : α → option_t m β)
: option_t m β :=
show m (option β), from
do o ← a,
match o with
| none := return none
| (some a) := b a
end
@[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
@[inline] def option_t_return {m : Type (max 1 u) → Type v} [monad m] {α : Type u} (a : α) : option_t m α :=
show m (option α), from
return (some a)
instance {M : Type (max 1 u) → Type v} [monad M] : monad (optionT M) :=
monad.mk (@optionT_fmap M _) (@optionT_return M _) (@optionT_bind M _)
instance {m : Type (max 1 u) → Type v} [monad m] : monad (option_t m) :=
monad.mk (@option_t_fmap m _) (@option_t_return m _) (@option_t_bind m _)
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
def option_t_orelse {m : Type (max 1 u) → Type v} [monad m] {α : Type u} (a : option_t m α) (b : option_t m α) : option_t m α :=
show m (option α), from
do o ← a,
match o with
| none := b
| (some v) := return (some v)
end
def optionT_fail {M : Type (max 1 u) → Type v} [monad M] {A : Type u} : optionT M A :=
show M (option A), from
def option_t_fail {m : Type (max 1 u) → Type v} [monad m] {α : Type u} : option_t m α :=
show m (option α), from
return none
instance {M : Type (max 1 u) → Type v} [monad M] : alternative (optionT M) :=
{map := @optionT_fmap M _,
pure := @optionT_return M _,
seq := @fapp (optionT M) (@optionT.monad M _),
failure := @optionT_fail M _,
orelse := @optionT_orelse M _}
instance {m : Type (max 1 u) → Type v} [monad m] : alternative (option_t m) :=
{map := @option_t_fmap m _,
pure := @option_t_return m _,
seq := @fapp (option_t m) (@option_t.monad m _),
failure := @option_t_fail m _,
orelse := @option_t_orelse m _}

130
library/init/order.lean
View file

@ -10,128 +10,128 @@ import init.logic
set_option default_priority 100
universe variable u
variables {A : Type u}
variables {α : Type u}
class weak_order (A : Type u) extends has_le A :=
(le_refl : ∀ a : A, a ≤ a)
(le_trans : ∀ a b c : A, a ≤ b → b ≤ c → a ≤ c)
(le_antisymm : ∀ a b : A, a ≤ b → b ≤ a → a = b)
class weak_order (α : Type u) extends has_le α :=
(le_refl : ∀ a : α, a ≤ a)
(le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
(le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b)
class linear_weak_order (A : Type u) extends weak_order A :=
(le_total : ∀ a b : A, a ≤ b ∨ b ≤ a)
class linear_weak_order (α : Type u) extends weak_order α :=
(le_total : ∀ a b : α, a ≤ b ∨ b ≤ a)
class strict_order (A : Type u) extends has_lt A :=
(lt_irrefl : ∀ a : A, ¬ a < a)
(lt_trans : ∀ a b c : A, a < b → b < c → a < c)
class strict_order (α : Type u) extends has_lt α :=
(lt_irrefl : ∀ a : α, ¬ a < a)
(lt_trans : ∀ a b c : α, a < b → b < c → a < c)
/- structures with a weak and a strict order -/
class order_pair (A : Type u) extends weak_order A, has_lt A :=
(le_of_lt : ∀ a b : A, a < b → a ≤ b)
(lt_of_lt_of_le : ∀ a b c : A, a < b → b ≤ c → a < c)
(lt_of_le_of_lt : ∀ a b c : A, a ≤ b → b < c → a < c)
(lt_irrefl : ∀ a : A, ¬ a < a)
class order_pair (α : Type u) extends weak_order α, has_lt α :=
(le_of_lt : ∀ a b : α, a < b → a ≤ b)
(lt_of_lt_of_le : ∀ a b c : α, a < b → b ≤ c → a < c)
(lt_of_le_of_lt : ∀ a b c : α, a ≤ b → b < c → a < c)
(lt_irrefl : ∀ a : α, ¬ a < a)
class strong_order_pair (A : Type u) extends weak_order A, has_lt A :=
(le_iff_lt_or_eq : ∀ a b : A, a ≤ b ↔ a < b ∨ a = b)
(lt_irrefl : ∀ a : A, ¬ a < a)
class strong_order_pair (α : Type u) extends weak_order α, has_lt α :=
(le_iff_lt_or_eq : ∀ a b : α, a ≤ b ↔ a < b ∨ a = b)
(lt_irrefl : ∀ a : α, ¬ a < a)
class linear_order_pair (A : Type u) extends order_pair A, linear_weak_order A
class linear_order_pair (α : Type u) extends order_pair α, linear_weak_order α
class linear_strong_order_pair (A : Type u) extends strong_order_pair A, linear_weak_order A
class linear_strong_order_pair (α : Type u) extends strong_order_pair α, linear_weak_order α
class decidable_linear_order (A : Type u) extends linear_strong_order_pair A :=
class decidable_linear_order (α : Type u) extends linear_strong_order_pair α :=
(decidable_lt : decidable_rel lt)
lemma le_refl [weak_order A] : ∀ a : A, a ≤ a :=
lemma le_refl [weak_order α] : ∀ a : α, a ≤ a :=
weak_order.le_refl
lemma le_trans [weak_order A] : ∀ {a b c : A}, a ≤ b → b ≤ c → a ≤ c :=
lemma le_trans [weak_order α] : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c :=
weak_order.le_trans
lemma le_antisymm [weak_order A] : ∀ {a b : A}, a ≤ b → b ≤ a → a = b :=
lemma le_antisymm [weak_order α] : ∀ {a b : α}, a ≤ b → b ≤ a → a = b :=
weak_order.le_antisymm
lemma le_of_eq [weak_order A] {a b : A} : a = b → a ≤ b :=
lemma le_of_eq [weak_order α] {a b : α} : a = b → a ≤ b :=
λ h, h ▸ le_refl a
lemma ge_trans [weak_order A] : ∀ {a b c : A}, a ≥ b → b ≥ c → a ≥ c :=
lemma ge_trans [weak_order α] : ∀ {a b c : α}, a ≥ b → b ≥ c → a ≥ c :=
λ a b c h₁ h₂, le_trans h₂ h₁
lemma le_total [linear_weak_order A] : ∀ a b : A, a ≤ b ∨ b ≤ a :=
lemma le_total [linear_weak_order α] : ∀ a b : α, a ≤ b ∨ b ≤ a :=
linear_weak_order.le_total
lemma le_of_not_ge [linear_weak_order A] {a b : A} : ¬ a ≥ b → a ≤ b :=
lemma le_of_not_ge [linear_weak_order α] {a b : α} : ¬ a ≥ b → a ≤ b :=
or.resolve_left (le_total b a)
lemma lt_irrefl [strict_order A] : ∀ a : A, ¬ a < a :=
lemma lt_irrefl [strict_order α] : ∀ a : α, ¬ a < a :=
strict_order.lt_irrefl
lemma gt_irrefl [strict_order A] : ∀ a : A, ¬ a > a :=
lemma gt_irrefl [strict_order α] : ∀ a : α, ¬ a > a :=
lt_irrefl
lemma lt_trans [strict_order A] : ∀ {a b c : A}, a < b → b < c → a < c :=
lemma lt_trans [strict_order α] : ∀ {a b c : α}, a < b → b < c → a < c :=
strict_order.lt_trans
lemma gt_trans [strict_order A] : ∀ {a b c : A}, a > b → b > c → a > c :=
lemma gt_trans [strict_order α] : ∀ {a b c : α}, a > b → b > c → a > c :=
λ a b c h₁ h₂, lt_trans h₂ h₁
lemma ne_of_lt [strict_order A] {a b : A} (h : a < b) : a ≠ b :=
lemma ne_of_lt [strict_order α] {a b : α} (h : a < b) : a ≠ b :=
λ he, absurd h (he ▸ lt_irrefl a)
lemma ne_of_gt [strict_order A] {a b : A} (h : a > b) : a ≠ b :=
lemma ne_of_gt [strict_order α] {a b : α} (h : a > b) : a ≠ b :=
λ he, absurd h (he ▸ lt_irrefl a)
lemma lt_asymm [strict_order A] {a b : A} (h : a < b) : ¬ b < a :=
lemma lt_asymm [strict_order α] {a b : α} (h : a < b) : ¬ b < a :=
λ h1 : b < a, lt_irrefl a (lt_trans h h1)
lemma not_lt_of_gt [strict_order A] {a b : A} (h : a > b) : ¬ a < b :=
lemma not_lt_of_gt [strict_order α] {a b : α} (h : a > b) : ¬ a < b :=
lt_asymm h
lemma le_of_lt [order_pair A] : ∀ {a b : A}, a < b → a ≤ b :=
lemma le_of_lt [order_pair α] : ∀ {a b : α}, a < b → a ≤ b :=
order_pair.le_of_lt
lemma lt_of_lt_of_le [order_pair A] : ∀ {a b c : A}, a < b → b ≤ c → a < c :=
lemma lt_of_lt_of_le [order_pair α] : ∀ {a b c : α}, a < b → b ≤ c → a < c :=
order_pair.lt_of_lt_of_le
lemma lt_of_le_of_lt [order_pair A] : ∀ {a b c : A}, a ≤ b → b < c → a < c :=
lemma lt_of_le_of_lt [order_pair α] : ∀ {a b c : α}, a ≤ b → b < c → a < c :=
order_pair.lt_of_le_of_lt
lemma gt_of_gt_of_ge [order_pair A] {a b c : A} (h₁ : a > b) (h₂ : b ≥ c) : a > c :=
lemma gt_of_gt_of_ge [order_pair α] {a b c : α} (h₁ : a > b) (h₂ : b ≥ c) : a > c :=
lt_of_le_of_lt h₂ h₁
lemma gt_of_ge_of_gt [order_pair A] {a b c : A} (h₁ : a ≥ b) (h₂ : b > c) : a > c :=
lemma gt_of_ge_of_gt [order_pair α] {a b c : α} (h₁ : a ≥ b) (h₂ : b > c) : a > c :=
lt_of_lt_of_le h₂ h₁
instance order_pair.to_strict_order [s : order_pair A] : strict_order A :=
instance order_pair.to_strict_order [s : order_pair α] : strict_order α :=
{ s with
lt_irrefl := order_pair.lt_irrefl,
lt_trans := λ a b c h₁ h₂, lt_of_lt_of_le h₁ (le_of_lt h₂) }
lemma not_le_of_gt [order_pair A] {a b : A} (h : a > b) : ¬ a ≤ b :=
lemma not_le_of_gt [order_pair α] {a b : α} (h : a > b) : ¬ a ≤ b :=
λ h₁, lt_irrefl b (lt_of_lt_of_le h h₁)
lemma not_lt_of_ge [order_pair A] {a b : A} (h : a ≥ b) : ¬ a < b :=
lemma not_lt_of_ge [order_pair α] {a b : α} (h : a ≥ b) : ¬ a < b :=
λ h₁, lt_irrefl b (lt_of_le_of_lt h h₁)
lemma le_iff_lt_or_eq [strong_order_pair A] : ∀ {a b : A}, a ≤ b ↔ a < b ∨ a = b :=
lemma le_iff_lt_or_eq [strong_order_pair α] : ∀ {a b : α}, a ≤ b ↔ a < b ∨ a = b :=
strong_order_pair.le_iff_lt_or_eq
lemma lt_or_eq_of_le [strong_order_pair A] : ∀ {a b : A}, a ≤ b → a < b ∨ a = b :=
lemma lt_or_eq_of_le [strong_order_pair α] : ∀ {a b : α}, a ≤ b → a < b ∨ a = b :=
λ a b h, iff.mp le_iff_lt_or_eq h
lemma le_of_lt_or_eq [strong_order_pair A] : ∀ {a b : A}, (a < b ∨ a = b) → a ≤ b :=
lemma le_of_lt_or_eq [strong_order_pair α] : ∀ {a b : α}, (a < b ∨ a = b) → a ≤ b :=
λ a b h, iff.mpr le_iff_lt_or_eq h
lemma lt_of_le_of_ne [strong_order_pair A] {a b : A} : a ≤ b → a ≠ b → a < b :=
lemma lt_of_le_of_ne [strong_order_pair α] {a b : α} : a ≤ b → a ≠ b → a < b :=
λ h₁ h₂, or.resolve_right (lt_or_eq_of_le h₁) h₂
private lemma lt_irrefl' [strong_order_pair A] : ∀ a : A, ¬ a < a :=
private lemma lt_irrefl' [strong_order_pair α] : ∀ a : α, ¬ a < a :=
strong_order_pair.lt_irrefl
private lemma le_of_lt' [strong_order_pair A] ⦃a b : A⦄ (h : a < b) : a ≤ b :=
private lemma le_of_lt' [strong_order_pair α] ⦃a b : α⦄ (h : a < b) : a ≤ b :=
le_of_lt_or_eq (or.inl h)
private lemma lt_of_lt_of_le' [strong_order_pair A] (a b c : A) (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
private lemma lt_of_lt_of_le' [strong_order_pair α] (a b c : α) (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
have a ≤ c, from le_trans (le_of_lt' h₁) h₂,
or.elim (lt_or_eq_of_le this)
(λ h : a < c, h)
@ -140,7 +140,7 @@ or.elim (lt_or_eq_of_le this)
have a = b, from le_antisymm (le_of_lt' h₁) this,
absurd h₁ (this ▸ lt_irrefl' a))
private lemma lt_of_le_of_lt' [strong_order_pair A] (a b c : A) (h₁ : a ≤ b) (h₂ : b < c) : a < c :=
private lemma lt_of_le_of_lt' [strong_order_pair α] (a b c : α) (h₁ : a ≤ b) (h₂ : b < c) : a < c :=
have a ≤ c, from le_trans h₁ (le_of_lt' h₂),
or.elim (lt_or_eq_of_le this)
(λ h : a < c, h)
@ -149,21 +149,21 @@ or.elim (lt_or_eq_of_le this)
have c = b, from le_antisymm this (le_of_lt' h₂),
absurd h₂ (this ▸ lt_irrefl' c))
instance strong_order_pair.to_order_pair [s : strong_order_pair A] : order_pair A :=
instance strong_order_pair.to_order_pair [s : strong_order_pair α] : order_pair α :=
{ s with
lt_irrefl := lt_irrefl',
le_of_lt := le_of_lt',
lt_of_le_of_lt := lt_of_le_of_lt',
lt_of_lt_of_le := lt_of_lt_of_le'}
instance linear_strong_order_pair.to_linear_order_pair [s : linear_strong_order_pair A] : linear_order_pair A :=
instance linear_strong_order_pair.to_linear_order_pair [s : linear_strong_order_pair α] : linear_order_pair α :=
{ s with
lt_irrefl := lt_irrefl',
le_of_lt := le_of_lt',
lt_of_le_of_lt := lt_of_le_of_lt',
lt_of_lt_of_le := lt_of_lt_of_le'}
lemma lt_trichotomy [linear_strong_order_pair A] (a b : A) : a < b ∨ a = b ∨ b < a :=
lemma lt_trichotomy [linear_strong_order_pair α] (a b : α) : a < b ∨ a = b ∨ b < a :=
or.elim (le_total a b)
(λ h : a ≤ b, or.elim (lt_or_eq_of_le h)
(λ h : a < b, or.inl h)
@ -172,52 +172,52 @@ or.elim (le_total a b)
(λ h : b < a, or.inr (or.inr h))
(λ h : b = a, or.inr (or.inl h^.symm)))
lemma le_of_not_gt [linear_strong_order_pair A] {a b : A} (h : ¬ a > b) : a ≤ b :=
lemma le_of_not_gt [linear_strong_order_pair α] {a b : α} (h : ¬ a > b) : a ≤ b :=
match lt_trichotomy a b with
| or.inl hlt := le_of_lt hlt
| or.inr (or.inl heq) := heq ▸ le_refl a
| or.inr (or.inr hgt) := absurd hgt h
end
lemma lt_of_not_ge [linear_strong_order_pair A] {a b : A} (h : ¬ a ≥ b) : a < b :=
lemma lt_of_not_ge [linear_strong_order_pair α] {a b : α} (h : ¬ a ≥ b) : a < b :=
match lt_trichotomy a b with
| or.inl hlt := hlt
| or.inr (or.inl heq) := absurd (heq ▸ le_refl a : a ≥ b) h
| or.inr (or.inr hgt) := absurd (le_of_lt hgt) h
end
lemma lt_or_ge [linear_strong_order_pair A] (a b : A) : a < b ∨ a ≥ b :=
lemma lt_or_ge [linear_strong_order_pair α] (a b : α) : a < b ∨ a ≥ b :=
match lt_trichotomy a b with
| or.inl hlt := or.inl hlt
| or.inr (or.inl heq) := or.inr (heq ▸ le_refl a)
| or.inr (or.inr hgt) := or.inr (le_of_lt hgt)
end
lemma le_or_gt [linear_strong_order_pair A] (a b : A) : a ≤ b ∨ a > b :=
lemma le_or_gt [linear_strong_order_pair α] (a b : α) : a ≤ b ∨ a > b :=
or.swap (lt_or_ge b a)
lemma lt_or_gt_of_ne [linear_strong_order_pair A] {a b : A} (h : a ≠ b) : a < b ∨ a > b :=
lemma lt_or_gt_of_ne [linear_strong_order_pair α] {a b : α} (h : a ≠ b) : a < b ∨ a > b :=
match lt_trichotomy a b with
| or.inl hlt := or.inl hlt
| or.inr (or.inl heq) := absurd heq h
| or.inr (or.inr hgt) := or.inr hgt
end
instance [decidable_linear_order A] (a b : A) : decidable (a < b) :=
decidable_linear_order.decidable_lt A a b
instance [decidable_linear_order α] (a b : α) : decidable (a < b) :=
decidable_linear_order.decidable_lt α a b
instance [decidable_linear_order A] (a b : A) : decidable (a ≤ b) :=
instance [decidable_linear_order α] (a b : α) : decidable (a ≤ b) :=
if h₁ : a < b then is_true (le_of_lt h₁)
else if h₂ : b < a then is_false (not_le_of_gt h₂)
else is_true (le_of_not_gt h₂)
instance [decidable_linear_order A] (a b : A) : decidable (a = b) :=
instance [decidable_linear_order α] (a b : α) : decidable (a = b) :=
if h₁ : a ≤ b then
if h₂ : b ≤ a
then is_true (le_antisymm h₁ h₂)
else is_false (λ he : a = b, h₂ (he ▸ le_refl a))
else is_false (λ he : a = b, h₁ (he ▸ le_refl a))
lemma eq_or_lt_of_not_lt [decidable_linear_order A] {a b : A} (h : ¬ a < b) : a = b ∨ b < a :=
lemma eq_or_lt_of_not_lt [decidable_linear_order α] {a b : α} (h : ¬ a < b) : a = b ∨ b < a :=
if h₁ : a = b then or.inl h₁
else or.inr (lt_of_not_ge (λ hge, h (lt_of_le_of_ne hge h₁)))

22
library/init/ordering.lean
View file

@ -14,8 +14,8 @@ open ordering
instance : has_to_string ordering :=
has_to_string.mk (λ s, match s with | ordering.lt := "lt" | ordering.eq := "eq" | ordering.gt := "gt" end)
class has_ordering (A : Type) :=
(cmp : A → A → ordering)
class has_ordering (α : Type) :=
(cmp : α → α → ordering)
def nat.cmp (a b : nat) : ordering :=
if a < b then ordering.lt
@ -28,9 +28,9 @@ instance : has_ordering nat :=
section
open prod
variables {A B : Type} [has_ordering A] [has_ordering B]
variables {α β : Type} [has_ordering α] [has_ordering β]
def prod.cmp : A × B → A × B → ordering
def prod.cmp : α × β → α × β → ordering
| (a₁, b₁) (a₂, b₂) :=
match (has_ordering.cmp a₁ a₂) with
| ordering.lt := lt
@ -38,36 +38,36 @@ def prod.cmp : A × B → A × B → ordering
| ordering.gt := gt
end
instance {A B : Type} [has_ordering A] [has_ordering B] : has_ordering (A × B) :=
instance {α β : Type} [has_ordering α] [has_ordering β] : has_ordering (α × β) :=
⟨prod.cmp⟩
end
section
open sum
variables {A B : Type} [has_ordering A] [has_ordering B]
variables {α β : Type} [has_ordering α] [has_ordering β]
def sum.cmp : A ⊕ B → A ⊕ B → ordering
def sum.cmp : α ⊕ β → α ⊕ β → ordering
| (inl a₁) (inl a₂) := has_ordering.cmp a₁ a₂
| (inr b₁) (inr b₂) := has_ordering.cmp b₁ b₂
| (inl a₁) (inr b₂) := lt
| (inr b₁) (inl a₂) := gt
instance {A B : Type} [has_ordering A] [has_ordering B] : has_ordering (A ⊕ B) :=
instance {α β : Type} [has_ordering α] [has_ordering β] : has_ordering (α ⊕ β) :=
⟨sum.cmp⟩
end
section
open option
variables {A : Type} [has_ordering A]
variables {α : Type} [has_ordering α]
def option.cmp : option A → option A → ordering
def option.cmp : option α → option α → ordering
| (some a₁) (some a₂) := has_ordering.cmp a₁ a₂
| (some a₁) none := gt
| none (some a₂) := lt
| none none := eq
instance {A : Type} [has_ordering A] : has_ordering (option A) :=
instance {α : Type} [has_ordering α] : has_ordering (option α) :=
⟨option.cmp⟩
end

8
library/init/prod.lean
View file

@ -5,16 +5,16 @@ Author: Leonardo de Moura, Jeremy Avigad
-/
prelude
import init.num init.relation
notation A × B := prod A B
notation α × β := prod α β
-- notation for n-ary tuples
notation `(` h `, ` t:(foldr `, ` (e r, prod.mk e r)) `)` := prod.mk h t
universe variables u v
instance {A : Type u} {B : Type v} [inhabited A] [inhabited B] : inhabited (prod A B) :=
⟨(default A, default B)⟩
instance {α : Type u} {β : Type v} [inhabited α] [inhabited β] : inhabited (prod α β) :=
⟨(default α, default β)⟩
instance {A : Type u} {B : Type v} [h₁ : decidable_eq A] [h₂ : decidable_eq B] : decidable_eq (A × B)
instance {α : Type u} {β : Type v} [h₁ : decidable_eq α] [h₂ : decidable_eq β] : decidable_eq (α × β)
| (a, b) (a', b') :=
match (h₁ a a') with
| (is_true e₁) :=

120
library/init/quot.lean
View file

@ -11,136 +11,136 @@ open setoid
universe variables u v
constant quot : Π {A : Type u}, setoid A → Type u
constant quot : Π {α : Type u}, setoid α → Type u
-- Remark: if we do not use propext here, then we would need a quot.lift for propositions.
constant propext {a b : Prop} : (a ↔ b) → a = b
-- iff can now be used to do substitutions in a calculation
attribute [subst]
lemma iff_subst {a b : Prop} {P : Prop → Prop} (H₁ : a ↔ b) (H₂ : P a) : P b :=
eq.subst (propext H₁) H₂
lemma iff_subst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) : p b :=
eq.subst (propext h₁) h₂
namespace quot
protected constant mk : Π {A : Type u} [s : setoid A], A → quot s
protected constant mk : Π {α : Type u} [s : setoid α], α → quot s
notation `⟦`:max a `⟧`:0 := quot.mk a
constant sound : Π {A : Type u} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧
constant lift : Π {A : Type u} {B : Type v} [s : setoid A] (f : A → B), (∀ a b, a ≈ b → f a = f b) → quot s → B
constant ind : ∀ {A : Type u} [s : setoid A] {B : quot s → Prop}, (∀ a, B ⟦a⟧) → ∀ q, B q
constant sound : Π {α : Type u} [s : setoid α] {a b : α}, a ≈ b → ⟦a⟧ = ⟦b⟧
constant lift : Π {α : Type u} {β : Type v} [s : setoid α] (f : α → β), (∀ a b, a ≈ b → f a = f b) → quot s → β
constant ind : ∀ {α : Type u} [s : setoid α] {β : quot s → Prop}, (∀ a, β ⟦a⟧) → ∀ q, β q
attribute [elab_as_eliminator] lift ind
init_quotient
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 :=
protected lemma lift_beta {α : Type u} {β : Type v} [setoid α] (f : α → β) (c : ∀ a b, a ≈ b → f a = f b) (a : α) : lift f c ⟦a⟧ = f a :=
rfl
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 :=
protected lemma ind_beta {α : Type u} [s : setoid α] {β : quot s → Prop} (p : ∀ a, β ⟦a⟧) (a : α) : (ind p ⟦a⟧ : β ⟦a⟧) = p a :=
rfl
attribute [reducible, elab_as_eliminator]
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 :=
protected def lift_on {α : Type u} {β : Type v} [s : setoid α] (q : quot s) (f : α → β) (c : ∀ a b, a ≈ b → f a = f b) : β :=
lift f c q
attribute [elab_as_eliminator]
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
protected lemma induction_on {α : Type u} [s : setoid α] {β : quot s → Prop} (q : quot s) (h : ∀ a, β ⟦a⟧) : β q :=
ind h q
lemma exists_rep {A : Type u} [s : setoid A] (q : quot s) : ∃ a : A, ⟦a⟧ = q :=
lemma exists_rep {α : Type u} [s : setoid α] (q : quot s) : ∃ a : α, ⟦a⟧ = q :=
quot.induction_on q (λ a, ⟨a, rfl⟩)
section
variable {A : Type u}
variable [s : setoid A]
variable {B : quot s → Type v}
variable {α : Type u}
variable [s : setoid α]
variable {β : quot s → Type v}
include s
attribute [reducible]
protected def indep (f : Π a, B ⟦a⟧) (a : A) : Σ q, B q :=
protected def indep (f : Π a, β ⟦a⟧) (a : α) : Σ q, β q :=
⟨⟦a⟧, f a⟩
protected lemma indep_coherent (f : Π a, B ⟦a⟧)
(H : ∀ (a b : A) (p : a ≈ b), (eq.rec (f a) (sound p) : B ⟦b⟧) = f b)
protected lemma indep_coherent (f : Π a, β ⟦a⟧)
(h : ∀ (a b : α) (p : a ≈ b), (eq.rec (f a) (sound p) : β ⟦b⟧) = f b)
: ∀ a b, a ≈ b → quot.indep f a = quot.indep f b :=
λ a b e, sigma.eq (sound e) (H a b e)
λ a b e, sigma.eq (sound e) (h a b e)
protected lemma lift_indep_pr1
(f : Π a, B ⟦a⟧) (H : ∀ (a b : A) (p : a ≈ b), (eq.rec (f a) (sound p) : B ⟦b⟧) = f b)
(q : quot s) : (lift (quot.indep f) (quot.indep_coherent f H) q).1 = q :=
quot.ind (λ (a : A), eq.refl (quot.indep f a).1) q
(f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : a ≈ b), (eq.rec (f a) (sound p) : β ⟦b⟧) = f b)
(q : quot s) : (lift (quot.indep f) (quot.indep_coherent f h) q).1 = q :=
quot.ind (λ (a : α), eq.refl (quot.indep f a).1) q
attribute [reducible, elab_as_eliminator]
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)
(f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : a ≈ b), (eq.rec (f a) (sound p) : β ⟦b⟧) = f b)
(q : quot s) : β 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 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
(q : quot s) (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : a ≈ b), (eq.rec (f a) (sound p) : β ⟦b⟧) = f b) : β q :=
quot.rec f h q
attribute [reducible, elab_as_eliminator]
protected def rec_on_subsingleton
[H : ∀ a, subsingleton (B ⟦a⟧)] (q : quot s) (f : Π a, B ⟦a⟧) : B q :=
[h : ∀ a, subsingleton (β ⟦a⟧)] (q : quot s) (f : Π a, β ⟦a⟧) : β q :=
quot.rec f (λ a b h, subsingleton.elim _ (f b)) q
attribute [reducible, elab_as_eliminator]
protected def hrec_on
(q : quot s) (f : Π a, B ⟦a⟧) (c : ∀ (a b : A) (p : a ≈ b), f a == f b) : B q :=
(q : quot s) (f : Π a, β ⟦a⟧) (c : ∀ (a b : α) (p : a ≈ b), f a == f b) : β q :=
quot.rec_on q f
(λ a b p, eq_of_heq (calc
(eq.rec (f a) (sound p) : B ⟦b⟧) == f a : eq_rec_heq (sound p) (f a)
(eq.rec (f a) (sound p) : β ⟦b⟧) == f a : eq_rec_heq (sound p) (f a)
... == f b : c a b p))
end
section
universe variables u_a u_b u_c
variables {A : Type u_a} {B : Type u_b} {C : Type u_c}
variables [s₁ : setoid A] [s₂ : setoid B]
variables {α : Type u_a} {β : Type u_b} {φ : Type u_c}
variables [s₁ : setoid α] [s₂ : setoid β]
include s₁ s₂
attribute [reducible, elab_as_eliminator]
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 :=
(f : α → β → φ)(c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂)
(q₁ : quot s₁) (q₂ : quot s₂) : φ :=
quot.lift
(λ (a₁ : A), quot.lift (f a₁) (λ (a b : B), c a₁ a a₁ b (setoid.refl a₁)) q₂)
(λ (a b : A) (H : a ≈ b),
@quot.ind B s₂
(λ (a₁ : α), quot.lift (f a₁) (λ (a b : β), c a₁ a a₁ b (setoid.refl a₁)) q₂)
(λ (a b : α) (h : a ≈ b),
@quot.ind β s₂
(λ (a_1 : quot s₂),
(quot.lift (f a) (λ (a_1 b : B), c a a_1 a b (setoid.refl a)) a_1)
(quot.lift (f a) (λ (a_1 b : β), c a a_1 a b (setoid.refl a)) a_1)
=
(quot.lift (f b) (λ (a b_1 : B), c b a b b_1 (setoid.refl b)) a_1))
(λ (a' : B), c a a' b a' H (setoid.refl a'))
(quot.lift (f b) (λ (a b_1 : β), c b a b b_1 (setoid.refl b)) a_1))
(λ (a' : β), c a a' b a' h (setoid.refl a'))
q₂)
q₁
attribute [reducible, elab_as_eliminator]
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 :=
(q₁ : quot s₁) (q₂ : quot s₂) (f : α → β → φ) (c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) : φ :=
quot.lift₂ f c q₁ q₂
attribute [elab_as_eliminator]
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₁
protected lemma ind₂ {φ : quot s₁ → quot s₂ → Prop} (h : ∀ a b, φ ⟦a⟧ ⟦b⟧) (q₁ : quot s₁) (q₂ : quot s₂) : φ q₁ q₂ :=
quot.ind (λ a₁, quot.ind (λ a₂, h a₁ a₂) q₂) q₁
attribute [elab_as_eliminator]
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₁
{φ : quot s₁ → quot s₂ → Prop} (q₁ : quot s₁) (q₂ : quot s₂) (h : ∀ a b, φ ⟦a⟧ ⟦b⟧) : φ q₁ q₂ :=
quot.ind (λ a₁, quot.ind (λ a₂, h a₁ a₂) q₂) q₁
attribute [elab_as_eliminator]
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₃ :=
quot.ind (λ a₁, quot.ind (λ a₂, quot.ind (λ a₃, H a₁ a₂ a₃) q₃) q₂) q₁
[s₃ : setoid φ]
{δ : quot s₁ → quot s₂ → quot s₃ → Prop} (q₁ : quot s₁) (q₂ : quot s₂) (q₃ : quot s₃) (h : ∀ a b c, δ ⟦a⟧ ⟦b⟧ ⟦c⟧)
: δ q₁ q₂ q₃ :=
quot.ind (λ a₁, quot.ind (λ a₂, quot.ind (λ a₃, h a₁ a₂ a₃) q₃) q₂) q₁
end
section exact
variable {A : Type u}
variable [s : setoid A]
variable {α : Type u}
variable [s : setoid α]
include s
private def rel (q₁ q₂ : quot s) : Prop :=
@ -159,32 +159,32 @@ namespace quot
private lemma eq_imp_rel {q₁ q₂ : quot s} : q₁ = q₂ → q₁ ~ q₂ :=
assume h, eq.rec_on h (rel.refl q₁)
lemma exact {a b : A} : ⟦a⟧ = ⟦b⟧ → a ≈ b :=
lemma exact {a b : α} : ⟦a⟧ = ⟦b⟧ → a ≈ b :=
assume h, eq_imp_rel h
end exact
section
universe variables u_a u_b u_c
variables {A : Type u_a} {B : Type u_b}
variables [s₁ : setoid A] [s₂ : setoid B]
variables {α : Type u_a} {β : Type u_b}
variables [s₁ : setoid α] [s₂ : setoid β]
include s₁ s₂
attribute [reducible, elab_as_eliminator]
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₁
{φ : quot s₁ → quot s₂ → Type u_c} [h : ∀ a b, subsingleton (φ ⟦a⟧ ⟦b⟧)]
(q₁ : quot s₁) (q₂ : quot s₂) (f : Π a b, φ ⟦a⟧ ⟦b⟧) : φ q₁ q₂:=
@quot.rec_on_subsingleton _ s₁ (λ q, φ q q₂) (λ a, quot.ind (λ b, h a b) q₂) q₁
(λ a, quot.rec_on_subsingleton q₂ (λ b, f a b))
end
end quot
open decidable
instance {A : Type u} {s : setoid A} [decR : ∀ a b : A, decidable (a ≈ b)] : decidable_eq (quot s) :=
instance {α : Type u} {s : setoid α} [d : ∀ a b : α, decidable (a ≈ b)] : decidable_eq (quot s) :=
λ q₁ q₂ : quot s,
quot.rec_on_subsingleton₂ q₁ q₂
(λ a₁ a₂,
match (decR a₁ a₂) with
match (d a₁ a₂) with
| (is_true h₁) := is_true (quot.sound h₁)
| (is_false h₂) := is_false (λ h, absurd (quot.exact h) h₂)
end)

28
library/init/relation.lean
View file

@ -11,8 +11,8 @@ import init.logic
-- TODO(Leo): remove duplication between this file and algebra/relation.lean
-- We need some of the following definitions asap when "initializing" Lean.
universe variables u v
variables {A : Type u} {B : Type v} (R : B → B → Prop)
local infix `≺`:50 := R
variables {α : Type u} {β : Type v} (r : β → β → Prop)
local infix `≺`:50 := r
def reflexive := ∀ x, x ≺ x
@ -20,30 +20,30 @@ def symmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x
def transitive := ∀ ⦃x y z⦄, x ≺ y → y ≺ z → x ≺ z
def equivalence := reflexive R ∧ symmetric R ∧ transitive R
def equivalence := reflexive r ∧ symmetric r ∧ transitive r
def total := ∀ x y, x ≺ y ∨ y ≺ x
def mk_equivalence (r : reflexive R) (s : symmetric R) (t : transitive R) : equivalence R :=
⟨r, s, t⟩
def mk_equivalence (rfl : reflexive r) (symm : symmetric r) (trans : transitive r) : equivalence r :=
⟨rfl, symm, trans⟩
def irreflexive := ∀ x, ¬ x ≺ x
def anti_symmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x → x = y
def empty_relation := λ a₁ a₂ : A, false
def empty_relation := λ a₁ a₂ : α, false
def subrelation (Q R : B → B → Prop) := ∀ ⦃x y⦄, Q x y → R x y
def subrelation (q r : β → β → Prop) := ∀ ⦃x y⦄, q x y → r x y
def inv_image (f : A → B) : A → A → Prop :=
def inv_image (f : α → β) : α → α → Prop :=
λ a₁ a₂, f a₁ ≺ f a₂
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₂
lemma inv_image.trans (f : α → β) (h : transitive r) : transitive (inv_image r f) :=
λ (a₁ a₂ a₃ : α) (h₁ : inv_image r f a₁ a₂) (h₂ : inv_image r f a₂ a₃), h h₁ h₂
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₁
lemma inv_image.irreflexive (f : α → β) (h : irreflexive r) : irreflexive (inv_image r f) :=
λ (a : α) (h₁ : inv_image r f a a), h (f a) h₁
inductive tc {A : Type u} (R : A → A → Prop) : A → A → Prop
| base : ∀ a b, R a b → tc a b
inductive tc {α : Type u} (r : α → α → Prop) : α → α → Prop
| base : ∀ a b, r a b → tc a b
| trans : ∀ a b c, tc a b → tc b c → tc a c

45
library/init/set.lean
View file

@ -7,71 +7,70 @@ prelude
import init.logic init.functor
universe variables u v
def set (α : Type u) := α → Prop
def set (A : Type u) := A → Prop
def set_of {A : Type u} (p : A → Prop) : set A :=
def set_of {α : Type u} (p : α → Prop) : set α :=
p
namespace set
variables {A : Type u} {B : Type v}
variables {α : Type u} {β : Type v}
protected def mem (a : A) (s : set A) :=
protected def mem (a : α) (s : set α) :=
s a
instance : has_mem A set :=
instance : has_mem α set :=
⟨set.mem⟩
protected def subset (s₁ s₂ : set A) :=
protected def subset (s₁ s₂ : set α) :=
∀ {a}, a ∈ s₁ → a ∈ s₂
instance : has_subset (set A) :=
instance : has_subset (set α) :=
⟨set.subset⟩
protected def sep (p : A → Prop) (s : set A) : set A :=
protected def sep (p : α → Prop) (s : set α) : set α :=
{a | a ∈ s ∧ p a}
instance : has_sep A set :=
instance : has_sep α set :=
⟨set.sep⟩
instance : has_emptyc (set A) :=
instance : has_emptyc (set α) :=
⟨λ a, false⟩
protected def insert (a : A) (s : set A) : set A :=
protected def insert (a : α) (s : set α) : set α :=
{b | b = a ∨ b ∈ s}
instance : has_insert A set :=
instance : has_insert α set :=
⟨set.insert⟩
protected def union (s₁ s₂ : set A) : set A :=
protected def union (s₁ s₂ : set α) : set α :=
{a | a ∈ s₁ ∨ a ∈ s₂}
instance : has_union (set A) :=
instance : has_union (set α) :=
⟨set.union⟩
protected def inter (s₁ s₂ : set A) : set A :=
protected def inter (s₁ s₂ : set α) : set α :=
{a | a ∈ s₁ ∧ a ∈ s₂}
instance : has_inter (set A) :=
instance : has_inter (set α) :=
⟨set.inter⟩
def compl (s : set A) : set A :=
def compl (s : set α) : set α :=
{a | a ∉ s}
instance : has_neg (set A) :=
instance : has_neg (set α) :=
⟨compl⟩
protected def diff (s t : set A) : set A :=
protected def diff (s t : set α) : set α :=
{a ∈ s | a ∉ t}
instance : has_sdiff (set A) :=
instance : has_sdiff (set α) :=
⟨set.diff⟩
def powerset (s : set A) : set (set A) :=
def powerset (s : set α) : set (set α) :=
{t | t ⊆ s}
prefix `𝒫`:100 := powerset
def image (f : A → B) (s : set A) : set B :=
def image (f : α → β) (s : set α) : set β :=
{b | ∃ a, a ∈ s ∧ f a = b}
instance : functor set :=

29
library/init/setoid.lean
View file

@ -7,31 +7,28 @@ Authors: Leonardo de Moura
prelude
import init.relation
universe variables u
class setoid (A : Type u) :=
(r : A → A → Prop) (iseqv : equivalence r)
class setoid (α : Type u) :=
(r : α → α → Prop) (iseqv : equivalence r)
namespace setoid
infix ` ≈ ` := setoid.r
variable {A : Type u}
variable [s : setoid A]
variable {α : Type u}
variable [s : setoid α]
include s
attribute [refl]
lemma refl (a : A) : a ≈ a :=
match setoid.iseqv A with
| ⟨H_refl, H_symm, H_trans⟩ := H_refl a
@[refl] lemma refl (a : α) : a ≈ a :=
match setoid.iseqv α with
| ⟨h_refl, h_symm, h_trans⟩ := h_refl a
end
attribute [symm]
lemma symm {a b : A} (Hab : a ≈ b) : b ≈ a :=
match setoid.iseqv A with
| ⟨H_refl, H_symm, H_trans⟩ := H_symm Hab
@[symm] lemma symm {a b : α} (hab : a ≈ b) : b ≈ a :=
match setoid.iseqv α with
| ⟨h_refl, h_symm, h_trans⟩ := h_symm hab
end
attribute [trans]
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
@[trans] lemma trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c :=
match setoid.iseqv α with
| ⟨h_refl, h_symm, h_trans⟩ := h_trans hab hbc
end
end setoid

8
library/init/sigma.lean
View file

@ -6,17 +6,17 @@ Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
prelude
import init.logic init.num init.wf
notation `Σ` binders `, ` r:(scoped P, sigma P) := r
notation `Σ` binders `, ` r:(scoped p, sigma p) := r
universe variables u v
lemma ex_of_sig {A : Type u} {P : A → Prop} : (Σ x, P x) → ∃ x, P x
lemma ex_of_sig {α : Type u} {p : α → Prop} : (Σ x, p x) → ∃ x, p x
| ⟨x, hx⟩ := ⟨x, hx⟩
namespace sigma
variables {A : Type u} {B : A → Type v}
variables {α : Type u} {β : α → Type v}
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₂
protected lemma eq : ∀ {p₁ p₂ : Σ a : α, β a} (h₁ : p₁.1 = p₂.1), (eq.rec_on h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂
| ⟨a, b⟩ ⟨.a, .b⟩ rfl rfl := rfl
end sigma

122
library/init/sigma_lex.lean
View file

@ -8,111 +8,111 @@ import init.sigma init.meta init.combinator
universe variables u v
namespace sigma
section
variables {A : Type u} {B : A → Type v}
variable (Ra : A → A → Prop)
variable (Rb : ∀ a, B a → B a → Prop)
variables {α : Type u} {β : α → Type v}
variable (r : α → α → Prop)
variable (s : ∀ a, β a → β a → Prop)
-- Lexicographical order based on Ra and Rb
inductive lex : sigma B → sigma B → Prop
| left : ∀ {a₁ : A} (b₁ : B a₁) {a₂ : A} (b₂ : B a₂), Ra a₁ a₂ → lex (sigma.mk a₁ b₁) (sigma.mk a₂ b₂)
| right : ∀ (a : A) {b₁ b₂ : B a}, Rb a b₁ b₂ → lex (sigma.mk a b₁) (sigma.mk a b₂)
-- Lexicographical order based on r and s
inductive lex : sigma β → sigma β → Prop
| left : ∀ {a₁ : α} (b₁ : β a₁) {a₂ : α} (b₂ : β a₂), r a₁ a₂ → lex (sigma.mk a₁ b₁) (sigma.mk a₂ b₂)
| right : ∀ (a : α) {b₁ b₂ : β a}, s 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
parameters {α : Type u} {β : α → Type v}
parameters {r : α → α → Prop} {s : Π a : α, β a → β a → Prop}
local infix `≺`:50 := lex r s
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) :=
def lex_accessible {a} (aca : acc r a) (acb : ∀ a, well_founded (s a))
: ∀ (b : β a), acc (lex r s) (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)
(λ xa aca (iha : ∀ y, r y xa → ∀ b : β y, acc (lex r s) (sigma.mk y b)),
λ b : β xa, acc.rec_on (well_founded.apply (acb xa) b)
(λ xb acb
(iHb : ∀ (y : B xa), Rb xa y xb → acc (lex Ra Rb) (sigma.mk xa y)),
(ihb : ∀ (y : β xa), s xa y xb → acc (lex r s) (sigma.mk xa y)),
acc.intro (sigma.mk xa xb) (λ p (lt : p ≺ (sigma.mk xa xb)),
have aux : xa = xa → xb == xb → acc (lex Ra Rb) p, from
@sigma.lex.rec_on A B Ra Rb (λ p₁ p₂, p₂.1 = xa → p₂.2 == xb → acc (lex Ra Rb) p₁)
have aux : xa = xa → xb == xb → acc (lex r s) p, from
@sigma.lex.rec_on α β r s (λ p₁ p₂, p₂.1 = xa → p₂.2 == xb → acc (lex r s) p₁)
p (sigma.mk xa xb) lt
(λ (a₁ : A) (b₁ : B a₁) (a₂ : A) (b₂ : B a₂) (H : Ra a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ == xb),
(λ (a₁ : α) (b₁ : β a₁) (a₂ : α) (b₂ : β a₂) (h : r a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ == xb),
by do
get_local `eq₂ >>= subst,
to_expr `(iHa a₁ H b₁) >>= exact)
(λ (a : A) (b₁ b₂ : B a) (H : Rb a b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ == xb),
to_expr `(iha a₁ h b₁) >>= exact)
(λ (a : α) (b₁ b₂ : β a) (h : s a b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ == xb),
by do
get_local `eq₂ >>= subst,
to_expr `(eq_of_heq eq₃) >>= note `new_eq₃,
get_local `new_eq₃ >>= subst,
to_expr `(iHb b₁ H) >>= exact),
to_expr `(ihb b₁ h) >>= exact),
aux rfl (heq.refl xb))))
-- The lexicographical order of well founded relations is well-founded
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))
def lex_wf (ha : well_founded r) (hb : ∀ x, well_founded (s x)) : well_founded (lex r s) :=
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}
parameters {α : Type u} {β : Type v}
def lex_ndep (Ra : A → A → Prop) (Rb : B → B → Prop) :=
lex Ra (λ a : A, Rb)
def lex_ndep (r : α → α → Prop) (s : β → β → Prop) :=
lex r (λ a : α, s)
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))
def lex_ndep_wf {r : α → α → Prop} {s : β → β → Prop} (ha : well_founded r) (hb : well_founded s)
: well_founded (lex_ndep r s) :=
well_founded.intro (λ p, destruct p (λ a b, lex_accessible (well_founded.apply ha a) (λ x, hb) b))
end
section
variables {A : Type u} {B : Type v}
variable (Ra : A → A → Prop)
variable (Rb : B → B → Prop)
variables {α : Type u} {β : Type v}
variable (r : α → α → Prop)
variable (s : β → β → Prop)
-- Reverse lexicographical order based on Ra and Rb
inductive rev_lex : @sigma A (λ a, B) → @sigma A (λ a, B) → Prop
| left : ∀ {a₁ a₂ : A} (b : B), Ra a₁ a₂ → rev_lex (sigma.mk a₁ b) (sigma.mk a₂ b)
| right : ∀ (a₁ : A) {b₁ : B} (a₂ : A) {b₂ : B}, Rb b₁ b₂ → rev_lex (sigma.mk a₁ b₁) (sigma.mk a₂ b₂)
-- Reverse lexicographical order based on r and s
inductive rev_lex : @sigma α (λ a, β) → @sigma α (λ a, β) → Prop
| left : ∀ {a₁ a₂ : α} (b : β), r a₁ a₂ → rev_lex (sigma.mk a₁ b) (sigma.mk a₂ b)
| right : ∀ (a₁ : α) {b₁ : β} (a₂ : α) {b₂ : β}, s b₁ b₂ → rev_lex (sigma.mk a₁ b₁) (sigma.mk a₂ b₂)
end
section
open well_founded tactic
parameters {A : Type u} {B : Type v}
parameters {Ra : A → A → Prop} {Rb : B → B → Prop}
local infix `≺`:50 := rev_lex Ra Rb
parameters {α : Type u} {β : Type v}
parameters {r : α → α → Prop} {s : β → β → Prop}
local infix `≺`:50 := rev_lex r s
def 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 s b) (aca : ∀ a, acc r a): ∀ a, acc (rev_lex r s) (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)),
(λ xb acb (ihb : ∀ y, s y xb → ∀ a, acc (rev_lex r s) (sigma.mk a y)),
λ a, acc.rec_on (aca a)
(λ xa aca (iHa : ∀ y, Ra y xa → acc (rev_lex Ra Rb) (mk y xb)),
(λ xa aca (iha : ∀ y, r y xa → acc (rev_lex r s) (mk y xb)),
acc.intro (sigma.mk xa xb) (λ p (lt : p ≺ (sigma.mk xa xb)),
have aux : xa = xa → xb = xb → acc (rev_lex Ra Rb) p, from
@rev_lex.rec_on A B Ra Rb (λ p₁ p₂, fst p₂ = xa → snd p₂ = xb → acc (rev_lex Ra Rb) p₁)
have aux : xa = xa → xb = xb → acc (rev_lex r s) p, from
@rev_lex.rec_on α β r s (λ p₁ p₂, fst p₂ = xa → snd p₂ = xb → acc (rev_lex r s) p₁)
p (sigma.mk xa xb) lt
(λ a₁ a₂ b (H : Ra a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b = xb),
show acc (rev_lex Ra Rb) (sigma.mk a₁ b), from
have Ra₁ : Ra a₁ xa, from eq.rec_on eq₂ H,
have aux : acc (rev_lex Ra Rb) (sigma.mk a₁ xb), from iHa a₁ Ra₁,
(λ a₁ a₂ b (h : r a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b = xb),
show acc (rev_lex r s) (sigma.mk a₁ b), from
have r₁ : r a₁ xa, from eq.rec_on eq₂ h,
have aux : acc (rev_lex r s) (sigma.mk a₁ xb), from iha a₁ r₁,
eq.rec_on (eq.symm eq₃) aux)
(λ a₁ b₁ a₂ b₂ (H : Rb b₁ b₂) (eq₂ : a₂ = xa) (eq₃ : b₂ = xb),
show acc (rev_lex Ra Rb) (mk a₁ b₁), from
have Rb₁ : Rb b₁ xb, from eq.rec_on eq₃ H,
iHb b₁ Rb₁ a₁),
(λ a₁ b₁ a₂ b₂ (h : s b₁ b₂) (eq₂ : a₂ = xa) (eq₃ : b₂ = xb),
show acc (rev_lex r s) (mk a₁ b₁), from
have s₁ : s b₁ xb, from eq.rec_on eq₃ h,
ihb b₁ s₁ a₁),
aux rfl rfl)))
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))
def rev_lex_wf (ha : well_founded r) (hb : well_founded s) : well_founded (rev_lex r s) :=
well_founded.intro (λ p, destruct p (λ a b, rev_lex_accessible (apply hb b) (well_founded.apply ha) a))
end
section
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
def skip_left (α : Type u) {β : Type v} (s : β → β → Prop) : @sigma α (λ a, β) → @sigma α (λ a, β) → Prop :=
rev_lex empty_relation s
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
def skip_left_wf (α : Type u) {β : Type v} {s : β → β → Prop} (hb : well_founded s) : well_founded (skip_left α s) :=
rev_lex_wf empty_wf hb
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
def mk_skip_left {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → Prop}
(a₁ a₂ : α) (h : s b₁ b₂) : skip_left α s (sigma.mk a₁ b₁) (sigma.mk a₂ b₂) :=
rev_lex.right _ _ _ h
end
end sigma

56
library/init/state.lean
View file

@ -6,64 +6,64 @@ Authors: Leonardo de Moura
prelude
import init.logic init.monad init.alternative init.prod
def state (S : Type) (A : Type) : Type :=
S → A × S
def state (σ : Type) (α : Type) : Type :=
σ → α × σ
section
variables {S : Type} {A B : Type}
variables {σ : Type} {α β : Type}
@[inline] def state_fmap (f : A → B) (a : state S A) : state S B :=
@[inline] def state_fmap (f : α → β) (a : state σ α) : state σ β :=
λ s, match (a s) with (a', s') := (f a', s') end
@[inline] def state_return (a : A) : state S A :=
@[inline] def state_return (a : α) : state σ α :=
λ s, (a, s)
@[inline] def state_bind (a : state S A) (b : A → state S B) : state S B :=
@[inline] def state_bind (a : state σ α) (b : α → state σ β) : state σ β :=
λ s, match (a s) with (a', s') := b a' s' end
instance (S : Type) : monad (state S) :=
⟨@state_fmap S, @state_return S, @state_bind S⟩
instance (σ : Type) : monad (state σ) :=
⟨@state_fmap σ, @state_return σ, @state_bind σ⟩
end
namespace state
@[inline] def read {S : Type} : state S S :=
@[inline] def read {σ : Type} : state σ σ :=
λ s, (s, s)
@[inline] def write {S : Type} : S → state S unit :=
@[inline] def write {σ : Type} : σ → state σ unit :=
λ s' s, ((), s')
end state
def stateT (S : Type) (M : Type → Type) [monad M] (A : Type) : Type :=
S → M (A × S)
def state_t (σ : Type) (m : Type → Type) [monad m] (α : Type) : Type :=
σ → m (α × σ)
section
variable {S : Type}
variable {M : Type → Type}
variable [monad M]
variables {A B : Type}
variable {σ : Type}
variable {m : Type → Type}
variable [monad m]
variables {α β : Type}
def stateT_fmap (f : A → B) (act : stateT S M A) : stateT S M B :=
λ s, show M (B × S), from
def state_t_fmap (f : α → β) (act : state_t σ m α) : state_t σ m β :=
λ s, show m (β × σ), from
do (a, new_s) ← act s,
return (f a, new_s)
def stateT_return (a : A) : stateT S M A :=
λ s, show M (A × S), from
def state_t_return (a : α) : state_t σ m α :=
λ s, show m (α × σ), from
return (a, s)
def stateT_bind (act₁ : stateT S M A) (act₂ : A → stateT S M B) : stateT S M B :=
λ s, show M (B × S), from
def state_t_bind (act₁ : state_t σ m α) (act₂ : α → state_t σ m β) : state_t σ m β :=
λ s, show m (β × σ), from
do (a, new_s) ← act₁ s,
act₂ a new_s
end
instance (S : Type) (M : Type → Type) [monad M] : monad (stateT S M) :=
⟨@stateT_fmap S M _, @stateT_return S M _, @stateT_bind S M _⟩
instance (σ : Type) (m : Type → Type) [monad m] : monad (state_t σ m) :=
⟨@state_t_fmap σ m _, @state_t_return σ m _, @state_t_bind σ m _⟩
namespace stateT
def read {S : Type} {M : Type → Type} [monad M] : stateT S M S :=
namespace state_t
def read {σ : Type} {m : Type → Type} [monad m] : state_t σ m σ :=
λ s, return (s, s)
def write {S : Type} {M : Type → Type} [monad M] : S → stateT S M unit :=
def write {σ : Type} {m : Type → Type} [monad m] : σ → state_t σ m unit :=
λ s' s, return ((), s')
end stateT
end state_t

12
library/init/subtype.lean
View file

@ -9,17 +9,17 @@ open decidable
universe variables u
structure subtype {A : Type u} (p : A → Prop) :=
tag :: (elt_of : A) (has_property : p elt_of)
structure subtype {α : Type u} (p : α → Prop) :=
tag :: (elt_of : α) (has_property : p elt_of)
namespace subtype
def exists_of_subtype {A : Type u} {p : A → Prop} : { x // p x } → ∃ x, p x
def exists_of_subtype {α : Type u} {p : α → Prop} : { x // p x } → ∃ x, p x
| ⟨a, h⟩ := ⟨a, h⟩
variables {A : Type u} {p : A → Prop}
variables {α : Type u} {p : α → Prop}
lemma tag_irrelevant {a : A} (h1 h2 : p a) : tag a h1 = tag a h2 :=
lemma tag_irrelevant {a : α} (h1 h2 : p a) : tag a h1 = tag a h2 :=
rfl
protected lemma eq : ∀ {a1 a2 : {x // p x}}, elt_of a1 = elt_of a2 → a1 = a2
@ -29,5 +29,5 @@ end subtype
open subtype
instance {A : Type u} {p : A → Prop} {a : A} (h : p a) : inhabited {x // p x} :=
instance {α : Type u} {p : α → Prop} {a : α} (h : p a) : inhabited {x // p x} :=
⟨⟨a, h⟩⟩

12
library/init/sum.lean
View file

@ -8,14 +8,14 @@ The sum type, aka disjoint union.
prelude
import init.logic
notation A ⊕ B := sum A B
notation α ⊕ β := sum α β
universe variables u v
variables {A : Type u} {B : Type v}
variables {α : Type u} {β : Type v}
instance sum.inhabited_left [h : inhabited A] : inhabited (A ⊕ B) :=
⟨sum.inl (default A)⟩
instance sum.inhabited_left [h : inhabited α] : inhabited (α ⊕ β) :=
⟨sum.inl (default α)⟩
instance sum.inhabited_right [h : inhabited B] : inhabited (A ⊕ B) :=
⟨sum.inr (default B)⟩
instance sum.inhabited_right [h : inhabited β] : inhabited (α ⊕ β) :=
⟨sum.inr (default β)⟩

2
library/init/timeit.lean
View file

@ -5,5 +5,5 @@ prelude
import init.string
/- This function has a native implementation that tracks time. -/
def timeit {A : Type} (s : string) (f : unit → A) : A :=
def timeit {α : Type} (s : string) (f : unit → α) : α :=
f ()

26
library/init/to_string.lean
View file

@ -7,10 +7,10 @@ open bool list sum prod sigma subtype nat
universe variables u v
class has_to_string (A : Type u) :=
(to_string : A → string)
class has_to_string (α : Type u) :=
(to_string : α → string)
def to_string {A : Type u} [has_to_string A] : A → string :=
def to_string {α : Type u} [has_to_string α] : α → string :=
has_to_string.to_string
instance : has_to_string bool :=
@ -20,34 +20,34 @@ 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"⟩
def list.to_string_aux {A : Type u} [has_to_string A] : bool → list A → string
def list.to_string_aux {α : Type u} [has_to_string α] : bool → list α → 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
def list.to_string {A : Type u} [has_to_string A] : list A → string
def list.to_string {α : Type u} [has_to_string α] : list α → string
| [] := "[]"
| (x::xs) := "[" ++ list.to_string_aux tt (x::xs) ++ "]"
instance {A : Type u} [has_to_string A] : has_to_string (list A) :=
instance {α : Type u} [has_to_string α] : has_to_string (list α) :=
⟨list.to_string⟩
instance : has_to_string unit :=
⟨λ u, "star"⟩
instance {A : Type u} [has_to_string A] : has_to_string (option A) :=
instance {α : Type u} [has_to_string α] : has_to_string (option α) :=
⟨λ o, match o with | none := "none" | (some a) := "(some " ++ to_string a ++ ")" end⟩
instance {A : Type u} {B : Type v} [has_to_string A] [has_to_string B] : has_to_string (A ⊕ B) :=
instance {α : Type u} {β : Type v} [has_to_string α] [has_to_string β] : has_to_string (α ⊕ β) :=
⟨λ s, match s with | (inl a) := "(inl " ++ to_string a ++ ")" | (inr b) := "(inr " ++ to_string b ++ ")" end⟩
instance {A : Type u} {B : Type v} [has_to_string A] [has_to_string B] : has_to_string (A × B) :=
⟨λ p, "(" ++ to_string (fst p) ++ ", " ++ to_string (snd p) ++ ")"⟩
instance {α : Type u} {β : Type v} [has_to_string α] [has_to_string β] : has_to_string (α × β) :=
⟨λ p, "(" ++ to_string p.1 ++ ", " ++ to_string p.2 ++ ")"⟩
instance {A : Type u} {B : A → Type v} [has_to_string A] [s : ∀ x, has_to_string (B x)] : has_to_string (sigma B) :=
⟨λ p, "⟨" ++ to_string (fst p) ++ ", " ++ to_string (snd p) ++ "⟩"⟩
instance {α : Type u} {β : α → Type v} [has_to_string α] [s : ∀ x, has_to_string (β x)] : has_to_string (sigma β) :=
⟨λ p, "⟨" ++ to_string p.1 ++ ", " ++ to_string p.2 ++ "⟩"⟩
instance {A : Type u} {P : A → Prop} [has_to_string A] : has_to_string (subtype P) :=
instance {α : Type u} {p : α → Prop} [has_to_string α] : has_to_string (subtype p) :=
⟨λ s, to_string (elt_of s)⟩
def char.quote_core (c : char) : string :=

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. -/
def trace {A : Type} (s : string) (f : unit → A) : A :=
def trace {α : Type} (s : string) (f : unit → α) : α :=
f ()

2
library/init/unsigned.lean
View file

@ -18,7 +18,7 @@ private lemma zero_lt_unsigned_sz : 0 < unsigned_sz :=
zero_lt_succ _
def of_nat (n : nat) : unsigned :=
if H : n < unsigned_sz then fin.mk n H else fin.mk 0 zero_lt_unsigned_sz
if h : n < unsigned_sz then fin.mk n h else fin.mk 0 zero_lt_unsigned_sz
def to_nat (c : unsigned) : nat :=
fin.val c

80
library/init/wf.lean
View file

@ -8,62 +8,62 @@ import init.relation init.nat init.prod
universe variables u v
inductive acc {A : Type u} (r : A → A → Prop) : A → Prop
inductive acc {α : Type u} (r : α → α → Prop) : α → Prop
| intro : ∀ x, (∀ y, r y x → acc y) → acc x
namespace acc
variables {A : Type u} {r : A → A → Prop}
variables {α : Type u} {r : α → α → Prop}
def inv {x y : A} (h₁ : acc r x) (h₂ : r y x) : acc r y :=
def inv {x y : α} (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 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₂ :=
{C : Π (a : α), acc r a → Type v}
(h₁ : Π (x : α) (acx : Π (y : α), r y x → acc r y), (Π (y : α) (ryx : r y x), C y (acx y ryx)) → C x (acc.intro x acx))
{a : α} (h₂ : acc r a) : C a h₂ :=
acc.rec (λ x acx ih h₂, h₁ x acx (λ y ryx, ih y ryx (acx y ryx))) h₂ h₂
end acc
inductive well_founded {A : Type u} (r : A → A → Prop) : Prop
inductive well_founded {α : Type u} (r : α → α → Prop) : Prop
| intro : (∀ a, acc r a) → well_founded
namespace well_founded
def apply {A : Type u} {r : A → A → Prop} (wf : well_founded r) : ∀ a, acc r a :=
def apply {α : Type u} {r : α → α → Prop} (wf : well_founded r) : ∀ a, acc r a :=
take a, well_founded.rec_on wf (λ p, p) a
section
parameters {A : Type u} {r : A → A → Prop}
parameters {α : Type u} {r : α → α → Prop}
local infix `≺`:50 := r
hypothesis hwf : well_founded r
lemma recursion {C : A → Type v} (a : A) (h : Π x, (Π y, y ≺ x → C y) → C x) : C a :=
lemma recursion {C : α → Type v} (a : α) (h : Π x, (Π y, y ≺ x → C y) → C x) : C a :=
acc.rec_on (apply hwf a) (λ x₁ ac₁ ih, h x₁ ih)
lemma induction {C : A → Prop} (a : A) (h : ∀ x, (∀ y, y ≺ x → C y) → C x) : C a :=
lemma induction {C : α → Prop} (a : α) (h : ∀ x, (∀ y, y ≺ x → C y) → C x) : C a :=
recursion a h
variable {C : A → Type v}
variable {C : α → Type v}
variable F : Π x, (Π y, y ≺ x → C y) → C x
def fix_F (x : A) (a : acc r x) : C x :=
def fix_F (x : α) (a : acc r x) : C x :=
acc.rec_on a (λ x₁ ac₁ ih, F x₁ ih)
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)) :=
lemma fix_F_eq (x : α) (r : acc r x) :
fix_F F x r = F x (λ (y : α) (p : y ≺ x), fix_F F y (acc.inv r p)) :=
acc.drec (λ x r ih, rfl) r
end
variables {A : Type u} {C : A → Type v} {r : A → A → Prop}
variables {α : Type u} {C : α → Type v} {r : α → α → Prop}
-- Well-founded fixpoint
def 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 : α) : C x :=
fix_F F x (apply hwf x)
-- Well-founded fixpoint satisfies fixpoint equation
lemma 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 : α) :
fix hwf F x = F x (λ y h, fix hwf F y) :=
fix_F_eq F x (apply hwf x)
end well_founded
@ -71,20 +71,20 @@ end well_founded
open well_founded
-- Empty relation is well-founded
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))
def empty_wf {α : Type u} : well_founded empty_relation :=
well_founded.intro (λ (a : α),
acc.intro a (λ (b : α) (lt : false), false.rec _ lt))
-- Subrelation of a well-founded relation is well-founded
namespace subrelation
section
parameters {A : Type u} {r Q : A → A → Prop}
parameters {α : Type u} {r Q : α → α → Prop}
parameters (h₁ : subrelation Q r)
parameters (h₂ : well_founded r)
def accessible {a : A} (ac : acc r a) : acc Q a :=
def accessible {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)))
acc.intro x (λ (y : α) (lt : Q y x), ih y (h₁ lt)))
def wf : well_founded Q :=
⟨λ a, accessible (apply h₂ a)⟩
@ -94,15 +94,15 @@ end subrelation
-- The inverse image of a well-founded relation is well-founded
namespace inv_image
section
parameters {A : Type u} {B : Type v} {r : B → B → Prop}
parameters (f : A → B)
parameters {α : Type u} {β : Type v} {r : β → β → Prop}
parameters (f : α → β)
parameters (h : well_founded r)
private def acc_aux {b : B} (ac : acc r b) : ∀ (x : A), f x = b → acc (inv_image r f) x :=
private def acc_aux {b : β} (ac : acc r b) : ∀ (x : α), 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))
def accessible {a : A} (ac : acc r (f a)) : acc (inv_image r f) a :=
def accessible {a : α} (ac : acc r (f a)) : acc (inv_image r f) a :=
acc_aux ac a rfl
def wf : well_founded (inv_image r f) :=
@ -113,10 +113,10 @@ end inv_image
-- The transitive closure of a well-founded relation is well-founded
namespace tc
section
parameters {A : Type u} {r : A → A → Prop}
parameters {α : Type u} {r : α → α → Prop}
local notation `r⁺` := tc r
def accessible {z : A} (ac : acc r z) : acc (tc r) z :=
def accessible {z : α} (ac : acc r z) : acc (tc r) z :=
acc.rec_on ac (λ x acx ih,
acc.intro x (λ y rel,
tc.rec_on rel
@ -137,33 +137,33 @@ def nat.lt_wf : well_founded nat.lt :=
or.elim (nat.eq_or_lt_of_le (nat.le_of_succ_le_succ h))
(λ e, eq.substr e ih) (acc.inv ih)))⟩
def measure {A : Type u} : (A → ℕ) → A → A → Prop :=
def measure {α : Type u} : (α → ℕ) → α → α → Prop :=
inv_image lt
def measure_wf {A : Type u} (f : A → ℕ) : well_founded (measure f) :=
def measure_wf {α : Type u} (f : α → ℕ) : well_founded (measure f) :=
inv_image.wf f nat.lt_wf
namespace prod
open well_founded
section
variables {A : Type u} {B : Type v}
variable (ra : A → A → Prop)
variable (rb : B → B → Prop)
variables {α : Type u} {β : Type v}
variable (ra : α → α → Prop)
variable (rb : β → β → Prop)
-- Lexicographical order based on ra and rb
inductive lex : A × B → A × B → Prop
inductive lex : α × β → α × β → Prop
| left : ∀ {a₁ b₁} a₂ b₂, ra a₁ a₂ → lex (a₁, b₁) (a₂, b₂)
| right : ∀ a {b₁ b₂}, rb b₁ b₂ → lex (a, b₁) (a, b₂)
-- relational product based on ra and rb
inductive rprod : A × B → A × B → Prop
inductive rprod : α × β → α × β → Prop
| intro : ∀ {a₁ b₁ a₂ b₂}, ra a₁ a₂ → rb b₁ b₂ → rprod (a₁, b₁) (a₂, b₂)
end
section
parameters {A : Type u} {B : Type v}
parameters {ra : A → A → Prop} {rb : B → B → Prop}
parameters {α : Type u} {β : Type v}
parameters {ra : α → α → Prop} {rb : β → β → Prop}
local infix `≺`:50 := lex ra rb
def lex_accessible {a} (aca : acc ra a) (acb : ∀ b, acc rb b): ∀ b, acc (lex ra rb) (a, b) :=
@ -171,7 +171,7 @@ namespace prod
acc.rec_on (acb b) (λ xb acb ihb,
acc.intro (xa, xb) (λ p lt,
have aux : xa = xa → xb = xb → acc (lex ra rb) p, from
@prod.lex.rec_on A B ra rb (λ p₁ p₂, fst p₂ = xa → snd p₂ = xb → acc (lex ra rb) p₁)
@prod.lex.rec_on α β ra rb (λ p₁ p₂, fst p₂ = xa → snd p₂ = xb → acc (lex ra rb) p₁)
p (xa, xb) lt
(λ a₁ b₁ a₂ b₂ h (eq₂ : a₂ = xa) (eq₃ : b₂ = xb), iha a₁ (eq.rec_on eq₂ h) b₁)
(λ a b₁ b₂ h (eq₂ : a = xa) (eq₃ : b₂ = xb), eq.rec_on eq₂~>symm (ihb b₁ (eq.rec_on eq₃ h))),

4
library/system/io.lean
View file

@ -18,8 +18,8 @@ meta constant format.print_using : format → options → io unit
meta definition format.print (fmt : format) : io unit :=
format.print_using fmt options.mk
meta definition pp_using {A : Type} [has_to_format A] (a : A) (o : options) : io unit :=
meta definition pp_using {α : Type} [has_to_format α] (a : α) (o : options) : io unit :=
format.print_using (to_fmt a) o
meta definition pp {A : Type} [has_to_format A] (a : A) : io unit :=
meta definition pp {α : Type} [has_to_format α] (a : α) : io unit :=
format.print (to_fmt a)

2
tests/lean/eta_tac.lean.expected.out
View file

@ -1,4 +1,4 @@
λ {A : Type ?} [_inst_1 : has_add A] (a a_1 : A), @add A _inst_1 a a_1
λ {α : Type ?} [_inst_1 : has_add α] (a a_1 : α), @add α _inst_1 a a_1
λ (a : nat), nat.succ a
λ (a_1 : nat), @add nat nat.has_add a a_1
λ (x a : nat), @add nat nat.has_add x a

2
tests/lean/param_binder_update.lean.expected.out
View file

@ -1,4 +1,4 @@
id : Π {A : Type u_1}, A → A
id : Π {α : Type u_1}, α → α
id₂ : Π {A : Type u_1}, A → A
foo1 : A → B → A
foo2 : A → B → A

4
tests/lean/print_ax1.lean.expected.out
View file

@ -1,3 +1,3 @@
quot.sound : ∀ {A : Type u} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧
classical.strong_indefinite_description : Π {A : Type u} (p : A → Prop), nonempty A → {x // (∃ (y : A), p y) → p x}
quot.sound : ∀ {α : Type u} [s : setoid α] {a b : α}, a ≈ b → ⟦a⟧ = ⟦b⟧
classical.strong_indefinite_description : Π {a : Type u} (p : a → Prop), nonempty a → {x // (∃ (y : a), p y) → p x}
propext : ∀ {a b : Prop}, (a ↔ b) → a = b

4
tests/lean/print_ax2.lean.expected.out
View file

@ -1,3 +1,3 @@
quot.sound : ∀ {A : Type u} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧
classical.strong_indefinite_description : Π {A : Type u} (p : A → Prop), nonempty A → {x // (∃ (y : A), p y) → p x}
quot.sound : ∀ {α : Type u} [s : setoid α] {a b : α}, a ≈ b → ⟦a⟧ = ⟦b⟧
classical.strong_indefinite_description : Π {a : Type u} (p : a → Prop), nonempty a → {x // (∃ (y : a), p y) → p x}
propext : ∀ {a b : Prop}, (a ↔ b) → a = b

4
tests/lean/print_ax3.lean.expected.out
View file

@ -1,7 +1,7 @@
no axioms
------
quot.sound : ∀ {A : Type u} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧
classical.strong_indefinite_description : Π {A : Type u} (p : A → Prop), nonempty A → {x // (∃ (y : A), p y) → p x}
quot.sound : ∀ {α : Type u} [s : setoid α] {a b : α}, a ≈ b → ⟦a⟧ = ⟦b⟧
classical.strong_indefinite_description : Π {a : Type u} (p : a → Prop), nonempty a → {x // (∃ (y : a), p y) → p x}
propext : ∀ {a b : Prop}, (a ↔ b) → a = b
------
theorem foo3 : 0 = 0 :=

8
tests/lean/run/stateT1.lean
View file

@ -1,14 +1,14 @@
meta definition mytactic (A : Type) := stateT (list nat) tactic A
meta definition mytactic (A : Type) := state_t (list nat) tactic A
attribute [instance]
meta definition mytactic_is_monad : monad mytactic :=
@stateT.monad _ _ _
@state_t.monad _ _ _
meta definition read_lst : mytactic (list nat) :=
stateT.read
state_t.read
meta definition write_lst : list nat → mytactic unit :=
stateT.write
state_t.write
meta definition foo : mytactic unit :=
write_lst [10, 20]

4
tests/lean/user_attribute.lean.expected.out
View file

@ -1,11 +1,11 @@
eq.refl
attribute [foo, refl]
constructor eq.refl : ∀ {A : Type u} (a : A), a = a
constructor eq.refl : ∀ {α : Type u} (a : α), a = a
[eq.refl]
---
eq.refl
attribute [foo, foo.baz, refl]
constructor eq.refl : ∀ {A : Type u} (a : A), a = a
constructor eq.refl : ∀ {α : Type u} (a : α), a = a
[eq.refl]
user_attribute.lean:24:0: error: an attribute named [reducible] has already been registered
state: