diff --git a/library/algebra/order.lean b/library/algebra/order.lean index 92d8fff832..51c3fd6f68 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -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 diff --git a/library/data/bitvec.lean b/library/data/bitvec.lean index 1b9f3f2ec9..36b4ecaa0b 100644 --- a/library/data/bitvec.lean +++ b/library/data/bitvec.lean @@ -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 diff --git a/library/data/list.lean b/library/data/list.lean index dd9c9f3c64..e264992ce9 100644 --- a/library/data/list.lean +++ b/library/data/list.lean @@ -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 diff --git a/library/data/tuple.lean b/library/data/tuple.lean index 51568bb23a..1e1e051d4e 100644 --- a/library/data/tuple.lean +++ b/library/data/tuple.lean @@ -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 ⟩) diff --git a/library/init/algebra.lean b/library/init/algebra.lean index fb45f13395..2d12f0ed1a 100644 --- a/library/init/algebra.lean +++ b/library/init/algebra.lean @@ -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 $ diff --git a/library/init/alternative.lean b/library/init/alternative.lean index c5cb7bf80f..2deba9b584 100644 --- a/library/init/alternative.lean +++ b/library/init/alternative.lean @@ -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 diff --git a/library/init/applicative.lean b/library/init/applicative.lean index af11f42e4d..ced999eb87 100644 --- a/library/init/applicative.lean +++ b/library/init/applicative.lean @@ -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 diff --git a/library/init/binary.lean b/library/init/binary.lean index 7eefa82b29..726a072a96 100644 --- a/library/init/binary.lean +++ b/library/init/binary.lean @@ -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 diff --git a/library/init/bool.lean b/library/init/bool.lean index ce421ea853..7099eabb19 100644 --- a/library/init/bool.lean +++ b/library/init/bool.lean @@ -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 diff --git a/library/init/char.lean b/library/init/char.lean index 1f336ad9c9..c5d5ff03d7 100644 --- a/library/init/char.lean +++ b/library/init/char.lean @@ -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 diff --git a/library/init/classical.lean b/library/init/classical.lean index c86d23f3ed..b6d04c97e4 100644 --- a/library/init/classical.lean +++ b/library/init/classical.lean @@ -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 diff --git a/library/init/coe.lean b/library/init/coe.lean index aab2079034..b45b7d72a4 100644 --- a/library/init/coe.lean +++ b/library/init/coe.lean @@ -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⟩ diff --git a/library/init/combinator.lean b/library/init/combinator.lean index 61b02eca49..030a37bb90 100644 --- a/library/init/combinator.lean +++ b/library/init/combinator.lean @@ -7,7 +7,7 @@ prelude /- Combinator calculus -/ namespace combinator universe variables u₁ u₂ u₃ -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 diff --git a/library/init/congr.lean b/library/init/congr.lean index 116b24ac5b..fd90b5bad2 100644 --- a/library/init/congr.lean +++ b/library/init/congr.lean @@ -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) := diff --git a/library/init/core.lean b/library/init/core.lean index 3dba49ef17..3f432beb8f 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -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] diff --git a/library/init/function.lean b/library/init/function.lean index f70a020648..3eb1c1bb05 100644 --- a/library/init/function.lean +++ b/library/init/function.lean @@ -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 diff --git a/library/init/functor.lean b/library/init/functor.lean index e7b9e81e86..d87680fc6d 100644 --- a/library/init/functor.lean +++ b/library/init/functor.lean @@ -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 diff --git a/library/init/funext.lean b/library/init/funext.lean index 409e7b1ac2..17d4c24f2b 100644 --- a/library/init/funext.lean +++ b/library/init/funext.lean @@ -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))⟩ diff --git a/library/init/id_locked.lean b/library/init/id_locked.lean index 8bdb06fe91..93b57c5081 100644 --- a/library/init/id_locked.lean +++ b/library/init/id_locked.lean @@ -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 diff --git a/library/init/instances.lean b/library/init/instances.lean index 17e27b05d1..bad511b45a 100644 --- a/library/init/instances.lean +++ b/library/init/instances.lean @@ -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 diff --git a/library/init/list.lean b/library/init/list.lean index d462d4d1dd..b1fbfca9fa 100644 --- a/library/init/list.lean +++ b/library/init/list.lean @@ -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 diff --git a/library/init/list_classes.lean b/library/init/list_classes.lean index 47517ef63b..eaa81322b8 100644 --- a/library/init/list_classes.lean +++ b/library/init/list_classes.lean @@ -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 := diff --git a/library/init/logic.lean b/library/init/logic.lean index 3ab886a6a4..f2bb257c8e 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -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₁) diff --git a/library/init/meta/attribute.lean b/library/init/meta/attribute.lean index 60ef76cdb3..55f1ce6968 100644 --- a/library/init/meta/attribute.lean +++ b/library/init/meta/attribute.lean @@ -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 α diff --git a/library/init/meta/contradiction_tactic.lean b/library/init/meta/contradiction_tactic.lean index 80a987610d..626a93fce8 100644 --- a/library/init/meta/contradiction_tactic.lean +++ b/library/init/meta/contradiction_tactic.lean @@ -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") diff --git a/library/init/meta/converter.lean b/library/init/meta/converter.lean index 4f01653955..997180c75e 100644 --- a/library/init/meta/converter.lean +++ b/library/init/meta/converter.lean @@ -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 diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean index e464e6171f..24a608d371 100644 --- a/library/init/meta/environment.lean +++ b/library/init/meta/environment.lean @@ -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) diff --git a/library/init/meta/exceptional.lean b/library/init/meta/exceptional.lean index fa632851b8..88e2655291 100644 --- a/library/init/meta/exceptional.lean +++ b/library/init/meta/exceptional.lean @@ -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 := diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index 4ae0a387fb..4d3f3c2510 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -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 diff --git a/library/init/meta/format.lean b/library/init/meta/format.lean index 6018b2e09c..a6d163e887 100644 --- a/library/init/meta/format.lean +++ b/library/init/meta/format.lean @@ -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 diff --git a/library/init/meta/fun_info.lean b/library/init/meta/fun_info.lean index 0f2024eb5f..371aa58d33 100644 --- a/library/init/meta/fun_info.lean +++ b/library/init/meta/fun_info.lean @@ -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 diff --git a/library/init/meta/injection_tactic.lean b/library/init/meta/injection_tactic.lean index 707a10b6d3..03103a8cf8 100644 --- a/library/init/meta/injection_tactic.lean +++ b/library/init/meta/injection_tactic.lean @@ -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 diff --git a/library/init/meta/level.lean b/library/init/meta/level.lean index 88702e2b5f..d47b992dc4 100644 --- a/library/init/meta/level.lean +++ b/library/init/meta/level.lean @@ -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. diff --git a/library/init/meta/options.lean b/library/init/meta/options.lean index c61af0e59d..e21c292413 100644 --- a/library/init/meta/options.lean +++ b/library/init/meta/options.lean @@ -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 diff --git a/library/init/meta/pexpr.lean b/library/init/meta/pexpr.lean index 99e3ad8ed2..1ba20621ef 100644 --- a/library/init/meta/pexpr.lean +++ b/library/init/meta/pexpr.lean @@ -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 := diff --git a/library/init/meta/rb_map.lean b/library/init/meta/rb_map.lean index 6941254465..192a4244f4 100644 --- a/library/init/meta/rb_map.lean +++ b/library/init/meta/rb_map.lean @@ -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 := diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index c3ec820269..f15481daf8 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -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 -/ diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index fa1199148d..1ed6970cac 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -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], diff --git a/library/init/meta/vm.lean b/library/init/meta/vm.lean index d1599c434d..88900a863b 100644 --- a/library/init/meta/vm.lean +++ b/library/init/meta/vm.lean @@ -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, ()) diff --git a/library/init/monad.lean b/library/init/monad.lean index ea813b92b3..07349b0b15 100644 --- a/library/init/monad.lean +++ b/library/init/monad.lean @@ -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 diff --git a/library/init/monad_combinators.lean b/library/init/monad_combinators.lean index ad8cb370fc..8b4791ed13 100644 --- a/library/init/monad_combinators.lean +++ b/library/init/monad_combinators.lean @@ -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 diff --git a/library/init/nat.lean b/library/init/nat.lean index 10a731a3f7..ac34d721f7 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -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) diff --git a/library/init/nat_div.lean b/library/init/nat_div.lean index 71c41540a5..07f76bc389 100644 --- a/library/init/nat_div.lean +++ b/library/init/nat_div.lean @@ -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 diff --git a/library/init/option.lean b/library/init/option.lean index 78cbb000e2..eb15ab6e93 100644 --- a/library/init/option.lean +++ b/library/init/option.lean @@ -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 _} diff --git a/library/init/order.lean b/library/init/order.lean index 80d524728c..26c7b72056 100644 --- a/library/init/order.lean +++ b/library/init/order.lean @@ -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₁))) diff --git a/library/init/ordering.lean b/library/init/ordering.lean index ea467499e9..ff13ecedbc 100644 --- a/library/init/ordering.lean +++ b/library/init/ordering.lean @@ -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 diff --git a/library/init/prod.lean b/library/init/prod.lean index f620ea4ea1..3f731cd779 100644 --- a/library/init/prod.lean +++ b/library/init/prod.lean @@ -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₁) := diff --git a/library/init/quot.lean b/library/init/quot.lean index 738b0f45fa..f2405a8422 100644 --- a/library/init/quot.lean +++ b/library/init/quot.lean @@ -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) diff --git a/library/init/relation.lean b/library/init/relation.lean index 32df527ffe..befac76cce 100644 --- a/library/init/relation.lean +++ b/library/init/relation.lean @@ -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 diff --git a/library/init/set.lean b/library/init/set.lean index 3cde3e76b3..2de87fb5d4 100644 --- a/library/init/set.lean +++ b/library/init/set.lean @@ -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 := diff --git a/library/init/setoid.lean b/library/init/setoid.lean index ab9eb01a31..43b4cc26a9 100644 --- a/library/init/setoid.lean +++ b/library/init/setoid.lean @@ -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 diff --git a/library/init/sigma.lean b/library/init/sigma.lean index 1c3edb413e..45beb11f40 100644 --- a/library/init/sigma.lean +++ b/library/init/sigma.lean @@ -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 diff --git a/library/init/sigma_lex.lean b/library/init/sigma_lex.lean index 22bddf90d8..d67343332c 100644 --- a/library/init/sigma_lex.lean +++ b/library/init/sigma_lex.lean @@ -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 diff --git a/library/init/state.lean b/library/init/state.lean index 10dd6aa758..c9f665bb49 100644 --- a/library/init/state.lean +++ b/library/init/state.lean @@ -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 diff --git a/library/init/subtype.lean b/library/init/subtype.lean index 98923bd255..f376225e48 100644 --- a/library/init/subtype.lean +++ b/library/init/subtype.lean @@ -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⟩⟩ diff --git a/library/init/sum.lean b/library/init/sum.lean index 93e07d188f..b21185edba 100644 --- a/library/init/sum.lean +++ b/library/init/sum.lean @@ -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 β)⟩ diff --git a/library/init/timeit.lean b/library/init/timeit.lean index 6a0b49534b..34e7f514c1 100644 --- a/library/init/timeit.lean +++ b/library/init/timeit.lean @@ -5,5 +5,5 @@ prelude import init.string /- This function has a native implementation that tracks time. -/ -def timeit {A : Type} (s : string) (f : unit → A) : A := +def timeit {α : Type} (s : string) (f : unit → α) : α := f () diff --git a/library/init/to_string.lean b/library/init/to_string.lean index 0272c206fb..fecae08be8 100644 --- a/library/init/to_string.lean +++ b/library/init/to_string.lean @@ -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 := diff --git a/library/init/trace.lean b/library/init/trace.lean index 73cd110392..78a405c38c 100644 --- a/library/init/trace.lean +++ b/library/init/trace.lean @@ -5,5 +5,5 @@ prelude import init.string /- This function has a native implementation that displays the given string in the regular output stream. -/ -def trace {A : Type} (s : string) (f : unit → A) : A := +def trace {α : Type} (s : string) (f : unit → α) : α := f () diff --git a/library/init/unsigned.lean b/library/init/unsigned.lean index c724985289..e36f13a449 100644 --- a/library/init/unsigned.lean +++ b/library/init/unsigned.lean @@ -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 diff --git a/library/init/wf.lean b/library/init/wf.lean index a25782703e..b9f076686b 100644 --- a/library/init/wf.lean +++ b/library/init/wf.lean @@ -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))), diff --git a/library/system/io.lean b/library/system/io.lean index 188e435071..0220dbf106 100644 --- a/library/system/io.lean +++ b/library/system/io.lean @@ -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) diff --git a/tests/lean/eta_tac.lean.expected.out b/tests/lean/eta_tac.lean.expected.out index bcf00aa6db..67e5376eb5 100644 --- a/tests/lean/eta_tac.lean.expected.out +++ b/tests/lean/eta_tac.lean.expected.out @@ -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 diff --git a/tests/lean/param_binder_update.lean.expected.out b/tests/lean/param_binder_update.lean.expected.out index 0a1180ba7d..72a93ed20b 100644 --- a/tests/lean/param_binder_update.lean.expected.out +++ b/tests/lean/param_binder_update.lean.expected.out @@ -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 diff --git a/tests/lean/print_ax1.lean.expected.out b/tests/lean/print_ax1.lean.expected.out index 4102ea6e7b..beaef00f18 100644 --- a/tests/lean/print_ax1.lean.expected.out +++ b/tests/lean/print_ax1.lean.expected.out @@ -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 diff --git a/tests/lean/print_ax2.lean.expected.out b/tests/lean/print_ax2.lean.expected.out index 4102ea6e7b..beaef00f18 100644 --- a/tests/lean/print_ax2.lean.expected.out +++ b/tests/lean/print_ax2.lean.expected.out @@ -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 diff --git a/tests/lean/print_ax3.lean.expected.out b/tests/lean/print_ax3.lean.expected.out index 4ff80260c2..101108c1cf 100644 --- a/tests/lean/print_ax3.lean.expected.out +++ b/tests/lean/print_ax3.lean.expected.out @@ -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 := diff --git a/tests/lean/run/stateT1.lean b/tests/lean/run/stateT1.lean index e5d84df52e..6653ede88b 100644 --- a/tests/lean/run/stateT1.lean +++ b/tests/lean/run/stateT1.lean @@ -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] diff --git a/tests/lean/user_attribute.lean.expected.out b/tests/lean/user_attribute.lean.expected.out index 52a84c3516..749e727d68 100644 --- a/tests/lean/user_attribute.lean.expected.out +++ b/tests/lean/user_attribute.lean.expected.out @@ -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: