From ef546c5c5b88a7c39436bd3796a4762b341f0b22 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 13 Dec 2015 11:15:10 -0800 Subject: [PATCH] refactor(library): use anonymous instance implicit arguments --- library/algebra/group.lean | 92 +++++++++++++-------------- library/algebra/group_set_bigops.lean | 8 +-- library/algebra/ordered_group.lean | 4 +- library/algebra/ring.lean | 56 ++++++++-------- library/data/finset/basic.lean | 14 ++-- library/data/finset/bigops.lean | 4 +- library/data/list/basic.lean | 6 +- library/data/list/perm.lean | 6 +- library/data/list/set.lean | 28 ++++---- library/data/list/sort.lean | 4 +- library/data/nat/bquant.lean | 4 +- library/data/set/card.lean | 28 ++++---- library/data/set/finite.lean | 45 ++++++------- library/init/logic.lean | 44 ++++++------- library/init/measurable.lean | 6 +- library/init/quot.lean | 2 +- tests/lean/run/blast_cc8.lean | 18 +++--- 17 files changed, 182 insertions(+), 187 deletions(-) diff --git a/library/algebra/group.lean b/library/algebra/group.lean index c9d933813..183a4c660 100644 --- a/library/algebra/group.lean +++ b/library/algebra/group.lean @@ -19,25 +19,25 @@ variable {A : Type} structure semigroup [class] (A : Type) extends has_mul A := (mul_assoc : ∀a b c, mul (mul a b) c = mul a (mul b c)) -theorem mul.assoc [s : semigroup A] (a b c : A) : a * b * c = a * (b * c) := +theorem mul.assoc [semigroup A] (a b c : A) : a * b * c = a * (b * c) := !semigroup.mul_assoc structure comm_semigroup [class] (A : Type) extends semigroup A := (mul_comm : ∀a b, mul a b = mul b a) -theorem mul.comm [s : comm_semigroup A] (a b : A) : a * b = b * a := +theorem mul.comm [comm_semigroup A] (a b : A) : a * b = b * a := !comm_semigroup.mul_comm -theorem mul.left_comm [s : comm_semigroup A] (a b c : A) : a * (b * c) = b * (a * c) := +theorem mul.left_comm [comm_semigroup A] (a b c : A) : a * (b * c) = b * (a * c) := binary.left_comm (@mul.comm A _) (@mul.assoc A _) a b c -theorem mul.right_comm [s : comm_semigroup A] (a b c : A) : (a * b) * c = (a * c) * b := +theorem mul.right_comm [comm_semigroup A] (a b c : A) : (a * b) * c = (a * c) * b := binary.right_comm (@mul.comm A _) (@mul.assoc A _) a b c structure left_cancel_semigroup [class] (A : Type) extends semigroup A := (mul_left_cancel : ∀a b c, mul a b = mul a c → b = c) -theorem mul.left_cancel [s : left_cancel_semigroup A] {a b c : A} : +theorem mul.left_cancel [left_cancel_semigroup A] {a b c : A} : a * b = a * c → b = c := !left_cancel_semigroup.mul_left_cancel @@ -46,7 +46,7 @@ abbreviation eq_of_mul_eq_mul_left' := @mul.left_cancel structure right_cancel_semigroup [class] (A : Type) extends semigroup A := (mul_right_cancel : ∀a b c, mul a b = mul c b → a = c) -theorem mul.right_cancel [s : right_cancel_semigroup A] {a b c : A} : +theorem mul.right_cancel [right_cancel_semigroup A] {a b c : A} : a * b = c * b → a = c := !right_cancel_semigroup.mul_right_cancel @@ -57,26 +57,26 @@ abbreviation eq_of_mul_eq_mul_right' := @mul.right_cancel structure add_semigroup [class] (A : Type) extends has_add A := (add_assoc : ∀a b c, add (add a b) c = add a (add b c)) -theorem add.assoc [s : add_semigroup A] (a b c : A) : a + b + c = a + (b + c) := +theorem add.assoc [add_semigroup A] (a b c : A) : a + b + c = a + (b + c) := !add_semigroup.add_assoc structure add_comm_semigroup [class] (A : Type) extends add_semigroup A := (add_comm : ∀a b, add a b = add b a) -theorem add.comm [s : add_comm_semigroup A] (a b : A) : a + b = b + a := +theorem add.comm [add_comm_semigroup A] (a b : A) : a + b = b + a := !add_comm_semigroup.add_comm -theorem add.left_comm [s : add_comm_semigroup A] (a b c : A) : +theorem add.left_comm [add_comm_semigroup A] (a b c : A) : a + (b + c) = b + (a + c) := binary.left_comm (@add.comm A _) (@add.assoc A _) a b c -theorem add.right_comm [s : add_comm_semigroup A] (a b c : A) : (a + b) + c = (a + c) + b := +theorem add.right_comm [add_comm_semigroup A] (a b c : A) : (a + b) + c = (a + c) + b := binary.right_comm (@add.comm A _) (@add.assoc A _) a b c structure add_left_cancel_semigroup [class] (A : Type) extends add_semigroup A := (add_left_cancel : ∀a b c, add a b = add a c → b = c) -theorem add.left_cancel [s : add_left_cancel_semigroup A] {a b c : A} : +theorem add.left_cancel [add_left_cancel_semigroup A] {a b c : A} : a + b = a + c → b = c := !add_left_cancel_semigroup.add_left_cancel @@ -85,7 +85,7 @@ abbreviation eq_of_add_eq_add_left := @add.left_cancel structure add_right_cancel_semigroup [class] (A : Type) extends add_semigroup A := (add_right_cancel : ∀a b c, add a b = add c b → a = c) -theorem add.right_cancel [s : add_right_cancel_semigroup A] {a b c : A} : +theorem add.right_cancel [add_right_cancel_semigroup A] {a b c : A} : a + b = c + b → a = c := !add_right_cancel_semigroup.add_right_cancel @@ -96,9 +96,9 @@ abbreviation eq_of_add_eq_add_right := @add.right_cancel structure monoid [class] (A : Type) extends semigroup A, has_one A := (one_mul : ∀a, mul one a = a) (mul_one : ∀a, mul a one = a) -theorem one_mul [s : monoid A] (a : A) : 1 * a = a := !monoid.one_mul +theorem one_mul [monoid A] (a : A) : 1 * a = a := !monoid.one_mul -theorem mul_one [s : monoid A] (a : A) : a * 1 = a := !monoid.mul_one +theorem mul_one [monoid A] (a : A) : a * 1 = a := !monoid.mul_one structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A @@ -107,13 +107,13 @@ structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A structure add_monoid [class] (A : Type) extends add_semigroup A, has_zero A := (zero_add : ∀a, add zero a = a) (add_zero : ∀a, add a zero = a) -theorem zero_add [s : add_monoid A] (a : A) : 0 + a = a := !add_monoid.zero_add +theorem zero_add [add_monoid A] (a : A) : 0 + a = a := !add_monoid.zero_add -theorem add_zero [s : add_monoid A] (a : A) : a + 0 = a := !add_monoid.add_zero +theorem add_zero [add_monoid A] (a : A) : a + 0 = a := !add_monoid.add_zero structure add_comm_monoid [class] (A : Type) extends add_monoid A, add_comm_semigroup A -definition add_monoid.to_monoid {A : Type} [s : add_monoid A] : monoid A := +definition add_monoid.to_monoid {A : Type} [add_monoid A] : monoid A := ⦃ monoid, mul := add_monoid.add, mul_assoc := add_monoid.add_assoc, @@ -122,7 +122,7 @@ definition add_monoid.to_monoid {A : Type} [s : add_monoid A] : monoid A := one_mul := add_monoid.zero_add ⦄ -definition add_comm_monoid.to_comm_monoid {A : Type} [s : add_comm_monoid A] : comm_monoid A := +definition add_comm_monoid.to_comm_monoid {A : Type} [add_comm_monoid A] : comm_monoid A := ⦃ comm_monoid, add_monoid.to_monoid, mul_comm := add_comm_monoid.add_comm @@ -326,7 +326,7 @@ structure comm_group [class] (A : Type) extends group A, comm_monoid A structure add_group [class] (A : Type) extends add_monoid A, has_neg A := (add_left_inv : ∀a, add (neg a) a = zero) -definition add_group.to_group {A : Type} [s : add_group A] : group A := +definition add_group.to_group {A : Type} [add_group A] : group A := ⦃ group, add_monoid.to_monoid, mul_left_inv := add_group.add_left_inv ⦄ @@ -580,40 +580,40 @@ definition group_of_add_group (A : Type) [G : add_group A] : group A := namespace norm_num reveal add.assoc -definition add1 [s : has_add A] [s' : has_one A] (a : A) : A := add a one +definition add1 [has_add A] [has_one A] (a : A) : A := add a one -theorem add_comm_four [s : add_comm_semigroup A] (a b : A) : a + a + (b + b) = (a + b) + (a + b) := +theorem add_comm_four [add_comm_semigroup A] (a b : A) : a + a + (b + b) = (a + b) + (a + b) := by rewrite [-add.assoc at {1}, add.comm, {a + b}add.comm at {1}, *add.assoc] -theorem add_comm_middle [s : add_comm_semigroup A] (a b c : A) : a + b + c = a + c + b := +theorem add_comm_middle [add_comm_semigroup A] (a b c : A) : a + b + c = a + c + b := by rewrite [add.assoc, add.comm b, -add.assoc] -theorem bit0_add_bit0 [s : add_comm_semigroup A] (a b : A) : bit0 a + bit0 b = bit0 (a + b) := +theorem bit0_add_bit0 [add_comm_semigroup A] (a b : A) : bit0 a + bit0 b = bit0 (a + b) := !add_comm_four -theorem bit0_add_bit0_helper [s : add_comm_semigroup A] (a b t : A) (H : a + b = t) : +theorem bit0_add_bit0_helper [add_comm_semigroup A] (a b t : A) (H : a + b = t) : bit0 a + bit0 b = bit0 t := by rewrite -H; apply bit0_add_bit0 -theorem bit1_add_bit0 [s : add_comm_semigroup A] [s' : has_one A] (a b : A) : +theorem bit1_add_bit0 [add_comm_semigroup A] [has_one A] (a b : A) : bit1 a + bit0 b = bit1 (a + b) := begin rewrite [↑bit0, ↑bit1, add_comm_middle], congruence, apply add_comm_four end -theorem bit1_add_bit0_helper [s : add_comm_semigroup A] [s' : has_one A] (a b t : A) +theorem bit1_add_bit0_helper [add_comm_semigroup A] [has_one A] (a b t : A) (H : a + b = t) : bit1 a + bit0 b = bit1 t := by rewrite -H; apply bit1_add_bit0 -theorem bit0_add_bit1 [s : add_comm_semigroup A] [s' : has_one A] (a b : A) : +theorem bit0_add_bit1 [add_comm_semigroup A] [has_one A] (a b : A) : bit0 a + bit1 b = bit1 (a + b) := by rewrite [{bit0 a + _}add.comm, {a + _}add.comm]; apply bit1_add_bit0 -theorem bit0_add_bit1_helper [s : add_comm_semigroup A] [s' : has_one A] (a b t : A) +theorem bit0_add_bit1_helper [add_comm_semigroup A] [has_one A] (a b t : A) (H : a + b = t) : bit0 a + bit1 b = bit1 t := by rewrite -H; apply bit0_add_bit1 -theorem bit1_add_bit1 [s : add_comm_semigroup A] [s' : has_one A] (a b : A) : +theorem bit1_add_bit1 [add_comm_semigroup A] [has_one A] (a b : A) : bit1 a + bit1 b = bit0 (add1 (a + b)) := begin rewrite ↑[bit0, bit1, add1, add.assoc], @@ -622,64 +622,64 @@ theorem bit1_add_bit1 [s : add_comm_semigroup A] [s' : has_one A] (a b : A) : {b + a}add.comm, *add.assoc] end -theorem bit1_add_bit1_helper [s : add_comm_semigroup A] [s' : has_one A] (a b t s: A) +theorem bit1_add_bit1_helper [add_comm_semigroup A] [has_one A] (a b t s: A) (H : (a + b) = t) (H2 : add1 t = s) : bit1 a + bit1 b = bit0 s := begin rewrite [-H2, -H], apply bit1_add_bit1 end -theorem bin_add_zero [s : add_monoid A] (a : A) : a + zero = a := !add_zero +theorem bin_add_zero [add_monoid A] (a : A) : a + zero = a := !add_zero -theorem bin_zero_add [s : add_monoid A] (a : A) : zero + a = a := !zero_add +theorem bin_zero_add [add_monoid A] (a : A) : zero + a = a := !zero_add -theorem one_add_bit0 [s : add_comm_semigroup A] [s' : has_one A] (a : A) : one + bit0 a = bit1 a := +theorem one_add_bit0 [add_comm_semigroup A] [has_one A] (a : A) : one + bit0 a = bit1 a := begin rewrite ↑[bit0, bit1], rewrite add.comm end -theorem bit0_add_one [s : has_add A] [s' : has_one A] (a : A) : bit0 a + one = bit1 a := +theorem bit0_add_one [has_add A] [has_one A] (a : A) : bit0 a + one = bit1 a := rfl -theorem bit1_add_one [s : has_add A] [s' : has_one A] (a : A) : bit1 a + one = add1 (bit1 a) := +theorem bit1_add_one [has_add A] [has_one A] (a : A) : bit1 a + one = add1 (bit1 a) := rfl -theorem bit1_add_one_helper [s : has_add A] [s' : has_one A] (a t : A) (H : add1 (bit1 a) = t) : +theorem bit1_add_one_helper [has_add A] [has_one A] (a t : A) (H : add1 (bit1 a) = t) : bit1 a + one = t := by rewrite -H -theorem one_add_bit1 [s : add_comm_semigroup A] [s' : has_one A] (a : A) : +theorem one_add_bit1 [add_comm_semigroup A] [has_one A] (a : A) : one + bit1 a = add1 (bit1 a) := !add.comm -theorem one_add_bit1_helper [s : add_comm_semigroup A] [s' : has_one A] (a t : A) +theorem one_add_bit1_helper [add_comm_semigroup A] [has_one A] (a t : A) (H : add1 (bit1 a) = t) : one + bit1 a = t := by rewrite -H; apply one_add_bit1 -theorem add1_bit0 [s : has_add A] [s' : has_one A] (a : A) : add1 (bit0 a) = bit1 a := +theorem add1_bit0 [has_add A] [has_one A] (a : A) : add1 (bit0 a) = bit1 a := rfl -theorem add1_bit1 [s : add_comm_semigroup A] [s' : has_one A] (a : A) : +theorem add1_bit1 [add_comm_semigroup A] [has_one A] (a : A) : add1 (bit1 a) = bit0 (add1 a) := begin rewrite ↑[add1, bit1, bit0], rewrite [add.assoc, add_comm_four] end -theorem add1_bit1_helper [s : add_comm_semigroup A] [s' : has_one A] (a t : A) (H : add1 a = t) : +theorem add1_bit1_helper [add_comm_semigroup A] [has_one A] (a t : A) (H : add1 a = t) : add1 (bit1 a) = bit0 t := by rewrite -H; apply add1_bit1 -theorem add1_one [s : has_add A] [s' : has_one A] : add1 (one : A) = bit0 one := +theorem add1_one [has_add A] [has_one A] : add1 (one : A) = bit0 one := rfl -theorem add1_zero [s : add_monoid A] [s' : has_one A] : add1 (zero : A) = one := +theorem add1_zero [add_monoid A] [has_one A] : add1 (zero : A) = one := begin rewrite [↑add1, zero_add] end -theorem one_add_one [s : has_add A] [s' : has_one A] : (one : A) + one = bit0 one := +theorem one_add_one [has_add A] [has_one A] : (one : A) + one = bit0 one := rfl -theorem subst_into_sum [s : has_add A] (l r tl tr t : A) (prl : l = tl) (prr : r = tr) +theorem subst_into_sum [has_add A] (l r tl tr t : A) (prl : l = tl) (prr : r = tr) (prt : tl + tr = t) : l + r = t := by rewrite [prl, prr, prt] -theorem neg_zero_helper [s : add_group A] (a : A) (H : a = 0) : - a = 0 := +theorem neg_zero_helper [add_group A] (a : A) (H : a = 0) : - a = 0 := by rewrite [H, neg_zero] end norm_num diff --git a/library/algebra/group_set_bigops.lean b/library/algebra/group_set_bigops.lean index 6f836df0c..a3065a685 100644 --- a/library/algebra/group_set_bigops.lean +++ b/library/algebra/group_set_bigops.lean @@ -42,12 +42,12 @@ section Prod assert ¬ finite (insert a s), from assume H, nfs (finite_of_finite_insert H), by rewrite [Prod_of_not_finite nfs, Prod_of_not_finite this]) - theorem Prod_insert_of_not_mem (f : A → B) {a : A} {s : set A} [fins : finite s] (H : a ∉ s) : + theorem Prod_insert_of_not_mem (f : A → B) {a : A} {s : set A} [finite s] (H : a ∉ s) : Prod (insert a s) f = f a * Prod s f := assert (#finset a ∉ set.to_finset s), by rewrite mem_to_finset_eq; apply H, by rewrite [↑Prod, to_finset_insert, finset.Prod_insert_of_not_mem f this] - theorem Prod_union (f : A → B) {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] + theorem Prod_union (f : A → B) {s₁ s₂ : set A} [finite s₁] [finite s₂] (disj : s₁ ∩ s₂ = ∅) : Prod (s₁ ∪ s₂) f = Prod s₁ f * Prod s₂ f := begin @@ -88,9 +88,9 @@ section Sum theorem Sum_insert_of_mem (f : A → B) {a : A} {s : set A} (H : a ∈ s) : Sum (insert a s) f = Sum s f := Prod_insert_of_mem f H - theorem Sum_insert_of_not_mem (f : A → B) {a : A} {s : set A} [fins : finite s] (H : a ∉ s) : + theorem Sum_insert_of_not_mem (f : A → B) {a : A} {s : set A} [finite s] (H : a ∉ s) : Sum (insert a s) f = f a + Sum s f := Prod_insert_of_not_mem f H - theorem Sum_union (f : A → B) {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] + theorem Sum_union (f : A → B) {s₁ s₂ : set A} [finite s₁] [finite s₂] (disj : s₁ ∩ s₂ = ∅) : Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := Prod_union f disj theorem Sum_ext {s : set A} {f g : A → B} (H : ∀x, x ∈ s → f x = g x) : diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean index 505c1e485..43f51d5c0 100644 --- a/library/algebra/ordered_group.lean +++ b/library/algebra/ordered_group.lean @@ -198,12 +198,12 @@ structure ordered_comm_group [class] (A : Type) extends add_comm_group A, order_ (add_le_add_left : ∀a b, le a b → ∀c, le (add c a) (add c b)) (add_lt_add_left : ∀a b, lt a b → ∀ c, lt (add c a) (add c b)) -theorem ordered_comm_group.le_of_add_le_add_left [s : ordered_comm_group A] {a b c : A} +theorem ordered_comm_group.le_of_add_le_add_left [ordered_comm_group A] {a b c : A} (H : a + b ≤ a + c) : b ≤ c := assert H' : -a + (a + b) ≤ -a + (a + c), from ordered_comm_group.add_le_add_left _ _ H _, by rewrite *neg_add_cancel_left at H'; exact H' -theorem ordered_comm_group.lt_of_add_lt_add_left [s : ordered_comm_group A] {a b c : A} +theorem ordered_comm_group.lt_of_add_lt_add_left [ordered_comm_group A] {a b c : A} (H : a + b < a + c) : b < c := assert H' : -a + (a + b) < -a + (a + c), from ordered_comm_group.add_lt_add_left _ _ H _, by rewrite *neg_add_cancel_left at H'; exact H' diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 89c99a82f..5332f4085 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -19,18 +19,18 @@ structure distrib [class] (A : Type) extends has_mul A, has_add A := (left_distrib : ∀a b c, mul a (add b c) = add (mul a b) (mul a c)) (right_distrib : ∀a b c, mul (add a b) c = add (mul a c) (mul b c)) -theorem left_distrib [s : distrib A] (a b c : A) : a * (b + c) = a * b + a * c := +theorem left_distrib [distrib A] (a b c : A) : a * (b + c) = a * b + a * c := !distrib.left_distrib -theorem right_distrib [s: distrib A] (a b c : A) : (a + b) * c = a * c + b * c := +theorem right_distrib [distrib A] (a b c : A) : (a + b) * c = a * c + b * c := !distrib.right_distrib structure mul_zero_class [class] (A : Type) extends has_mul A, has_zero A := (zero_mul : ∀a, mul zero a = zero) (mul_zero : ∀a, mul a zero = zero) -theorem zero_mul [s : mul_zero_class A] (a : A) : 0 * a = 0 := !mul_zero_class.zero_mul -theorem mul_zero [s : mul_zero_class A] (a : A) : a * 0 = 0 := !mul_zero_class.mul_zero +theorem zero_mul [mul_zero_class A] (a : A) : 0 * a = 0 := !mul_zero_class.zero_mul +theorem mul_zero [mul_zero_class A] (a : A) : a * 0 = 0 := !mul_zero_class.mul_zero structure zero_ne_one_class [class] (A : Type) extends has_zero A, has_one A := (zero_ne_one : zero ≠ one) @@ -158,14 +158,14 @@ end comm_semiring structure ring [class] (A : Type) extends add_comm_group A, monoid A, distrib A -theorem ring.mul_zero [s : ring A] (a : A) : a * 0 = 0 := +theorem ring.mul_zero [ring A] (a : A) : a * 0 = 0 := have a * 0 + 0 = a * 0 + a * 0, from calc a * 0 + 0 = a * 0 : by rewrite add_zero ... = a * (0 + 0) : by rewrite add_zero ... = a * 0 + a * 0 : by rewrite {a*_}ring.left_distrib, show a * 0 = 0, from (add.left_cancel this)⁻¹ -theorem ring.zero_mul [s : ring A] (a : A) : 0 * a = 0 := +theorem ring.zero_mul [ring A] (a : A) : 0 * a = 0 := have 0 * a + 0 = 0 * a + 0 * a, from calc 0 * a + 0 = 0 * a : by rewrite add_zero ... = (0 + 0) * a : by rewrite add_zero @@ -328,7 +328,7 @@ end structure no_zero_divisors [class] (A : Type) extends has_mul A, has_zero A := (eq_zero_or_eq_zero_of_mul_eq_zero : ∀a b, mul a b = zero → a = zero ∨ b = zero) -theorem eq_zero_or_eq_zero_of_mul_eq_zero {A : Type} [s : no_zero_divisors A] {a b : A} +theorem eq_zero_or_eq_zero_of_mul_eq_zero {A : Type} [no_zero_divisors A] {a b : A} (H : a * b = 0) : a = 0 ∨ b = 0 := !no_zero_divisors.eq_zero_or_eq_zero_of_mul_eq_zero H @@ -404,29 +404,29 @@ end namespace norm_num -theorem mul_zero [s : mul_zero_class A] (a : A) : a * zero = zero := +theorem mul_zero [mul_zero_class A] (a : A) : a * zero = zero := by rewrite [↑zero, mul_zero] -theorem zero_mul [s : mul_zero_class A] (a : A) : zero * a = zero := +theorem zero_mul [mul_zero_class A] (a : A) : zero * a = zero := by rewrite [↑zero, zero_mul] -theorem mul_one [s : monoid A] (a : A) : a * one = a := +theorem mul_one [monoid A] (a : A) : a * one = a := by rewrite [↑one, mul_one] -theorem mul_bit0 [s : distrib A] (a b : A) : a * (bit0 b) = bit0 (a * b) := +theorem mul_bit0 [distrib A] (a b : A) : a * (bit0 b) = bit0 (a * b) := by rewrite [↑bit0, left_distrib] -theorem mul_bit0_helper [s : distrib A] (a b t : A) (H : a * b = t) : a * (bit0 b) = bit0 t := +theorem mul_bit0_helper [distrib A] (a b t : A) (H : a * b = t) : a * (bit0 b) = bit0 t := by rewrite -H; apply mul_bit0 -theorem mul_bit1 [s : semiring A] (a b : A) : a * (bit1 b) = bit0 (a * b) + a := +theorem mul_bit1 [semiring A] (a b : A) : a * (bit1 b) = bit0 (a * b) + a := by rewrite [↑bit1, ↑bit0, +left_distrib, ↑one, mul_one] -theorem mul_bit1_helper [s : semiring A] (a b s t : A) (Hs : a * b = s) (Ht : bit0 s + a = t) : +theorem mul_bit1_helper [semiring A] (a b s t : A) (Hs : a * b = s) (Ht : bit0 s + a = t) : a * (bit1 b) = t := begin rewrite [-Ht, -Hs, mul_bit1] end -theorem subst_into_prod [s : has_mul A] (l r tl tr t : A) (prl : l = tl) (prr : r = tr) +theorem subst_into_prod [has_mul A] (l r tl tr t : A) (prl : l = tl) (prr : r = tr) (prt : tl * tr = t) : l * r = t := by rewrite [prl, prr, prt] @@ -436,7 +436,7 @@ theorem mk_cong (op : A → A) (a b : A) (H : a = b) : op a = op b := theorem mk_eq (a : A) : a = a := rfl -theorem neg_add_neg_eq_of_add_add_eq_zero [s : add_comm_group A] (a b c : A) (H : c + a + b = 0) : +theorem neg_add_neg_eq_of_add_add_eq_zero [add_comm_group A] (a b c : A) (H : c + a + b = 0) : -a + -b = c := begin apply add_neg_eq_of_eq_add, @@ -444,42 +444,42 @@ theorem neg_add_neg_eq_of_add_add_eq_zero [s : add_comm_group A] (a b c : A) (H rewrite [add.comm, add.assoc, add.comm b, -add.assoc, H] end -theorem neg_add_neg_helper [s : add_comm_group A] (a b c : A) (H : a + b = c) : -a + -b = -c := +theorem neg_add_neg_helper [add_comm_group A] (a b c : A) (H : a + b = c) : -a + -b = -c := begin apply iff.mp !neg_eq_neg_iff_eq, rewrite [neg_add, *neg_neg, H] end -theorem neg_add_pos_eq_of_eq_add [s : add_comm_group A] (a b c : A) (H : b = c + a) : -a + b = c := +theorem neg_add_pos_eq_of_eq_add [add_comm_group A] (a b c : A) (H : b = c + a) : -a + b = c := begin apply neg_add_eq_of_eq_add, rewrite add.comm, exact H end -theorem neg_add_pos_helper1 [s : add_comm_group A] (a b c : A) (H : b + c = a) : -a + b = -c := +theorem neg_add_pos_helper1 [add_comm_group A] (a b c : A) (H : b + c = a) : -a + b = -c := begin apply neg_add_eq_of_eq_add, apply eq_add_neg_of_add_eq H end -theorem neg_add_pos_helper2 [s : add_comm_group A] (a b c : A) (H : a + c = b) : -a + b = c := +theorem neg_add_pos_helper2 [add_comm_group A] (a b c : A) (H : a + c = b) : -a + b = c := begin apply neg_add_eq_of_eq_add, rewrite H end -theorem pos_add_neg_helper [s : add_comm_group A] (a b c : A) (H : b + a = c) : a + b = c := +theorem pos_add_neg_helper [add_comm_group A] (a b c : A) (H : b + a = c) : a + b = c := by rewrite [add.comm, H] -theorem sub_eq_add_neg_helper [s : add_comm_group A] (t₁ t₂ e w₁ w₂: A) (H₁ : t₁ = w₁) +theorem sub_eq_add_neg_helper [add_comm_group A] (t₁ t₂ e w₁ w₂: A) (H₁ : t₁ = w₁) (H₂ : t₂ = w₂) (H : w₁ + -w₂ = e) : t₁ - t₂ = e := by rewrite [sub_eq_add_neg, H₁, H₂, H] -theorem pos_add_pos_helper [s : add_comm_group A] (a b c h₁ h₂ : A) (H₁ : a = h₁) (H₂ : b = h₂) +theorem pos_add_pos_helper [add_comm_group A] (a b c h₁ h₂ : A) (H₁ : a = h₁) (H₂ : b = h₂) (H : h₁ + h₂ = c) : a + b = c := by rewrite [H₁, H₂, H] -theorem subst_into_subtr [s : add_group A] (l r t : A) (prt : l + -r = t) : l - r = t := +theorem subst_into_subtr [add_group A] (l r t : A) (prt : l + -r = t) : l - r = t := by rewrite [sub_eq_add_neg, prt] -theorem neg_neg_helper [s : add_group A] (a b : A) (H : a = -b) : -a = b := +theorem neg_neg_helper [add_group A] (a b : A) (H : a = -b) : -a = b := by rewrite [H, neg_neg] -theorem neg_mul_neg_helper [s : ring A] (a b c : A) (H : a * b = c) : (-a) * (-b) = c := +theorem neg_mul_neg_helper [ring A] (a b c : A) (H : a * b = c) : (-a) * (-b) = c := begin rewrite [neg_mul_neg, H] end -theorem neg_mul_pos_helper [s : ring A] (a b c : A) (H : a * b = c) : (-a) * b = -c := +theorem neg_mul_pos_helper [ring A] (a b c : A) (H : a * b = c) : (-a) * b = -c := begin rewrite [-neg_mul_eq_neg_mul, H] end -theorem pos_mul_neg_helper [s : ring A] (a b c : A) (H : a * b = c) : a * (-b) = -c := +theorem pos_mul_neg_helper [ring A] (a b c : A) (H : a * b = c) : a * (-b) = -c := begin rewrite [-neg_mul_comm, -neg_mul_eq_neg_mul, H] end end norm_num diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean index bb186173f..7a789a321 100644 --- a/library/data/finset/basic.lean +++ b/library/data/finset/basic.lean @@ -16,7 +16,7 @@ variable {A : Type} definition to_nodup_list_of_nodup {l : list A} (n : nodup l) : nodup_list A := tag l n -definition to_nodup_list [h : decidable_eq A] (l : list A) : nodup_list A := +definition to_nodup_list [decidable_eq A] (l : list A) : nodup_list A := @to_nodup_list_of_nodup A (erase_dup l) (nodup_erase_dup l) private definition eqv (l₁ l₂ : nodup_list A) := @@ -47,10 +47,10 @@ protected definition prio : num := num.succ std.priority.default definition to_finset_of_nodup (l : list A) (n : nodup l) : finset A := ⟦to_nodup_list_of_nodup n⟧ -definition to_finset [h : decidable_eq A] (l : list A) : finset A := +definition to_finset [decidable_eq A] (l : list A) : finset A := ⟦to_nodup_list l⟧ -lemma to_finset_eq_of_nodup [h : decidable_eq A] {l : list A} (n : nodup l) : +lemma to_finset_eq_of_nodup [decidable_eq A] {l : list A} (n : nodup l) : to_finset_of_nodup l n = to_finset l := assert P : to_nodup_list_of_nodup n = to_nodup_list l, from begin @@ -60,7 +60,7 @@ assert P : to_nodup_list_of_nodup n = to_nodup_list l, from end, quot.sound (eq.subst P !setoid.refl) -definition has_decidable_eq [instance] [h : decidable_eq A] : decidable_eq (finset A) := +definition has_decidable_eq [instance] [decidable_eq A] : decidable_eq (finset A) := λ s₁ s₂, quot.rec_on_subsingleton₂ s₁ s₂ (λ l₁ l₂, match decidable_perm (elt_of l₁) (elt_of l₂) with @@ -106,7 +106,7 @@ definition decidable_mem [instance] [h : decidable_eq A] : ∀ (a : A) (s : fins | decidable.inr n := decidable.inr (λ p, absurd (mem_list_of_mem p) n) end) -theorem mem_to_finset [h : decidable_eq A] {a : A} {l : list A} : a ∈ l → a ∈ to_finset l := +theorem mem_to_finset [decidable_eq A] {a : A} {l : list A} : a ∈ l → a ∈ to_finset l := λ ainl, mem_erase_dup ainl theorem mem_to_finset_of_nodup {a : A} {l : list A} (n : nodup l) : a ∈ l → a ∈ to_finset_of_nodup l n := @@ -138,10 +138,10 @@ ext (take x, iff_false_intro (H x)) definition univ [h : fintype A] : finset A := to_finset_of_nodup (@fintype.elems A h) (@fintype.unique A h) -theorem mem_univ [h : fintype A] (x : A) : x ∈ univ := +theorem mem_univ [fintype A] (x : A) : x ∈ univ := fintype.complete x -theorem mem_univ_eq [h : fintype A] (x : A) : x ∈ univ = true := propext (iff_true_intro !mem_univ) +theorem mem_univ_eq [fintype A] (x : A) : x ∈ univ = true := propext (iff_true_intro !mem_univ) /- card -/ definition card (s : finset A) : nat := diff --git a/library/data/finset/bigops.lean b/library/data/finset/bigops.lean index 51407a0d5..3f456368a 100644 --- a/library/data/finset/bigops.lean +++ b/library/data/finset/bigops.lean @@ -18,7 +18,7 @@ variables {A B : Type} [deceqA : decidable_eq A] [deceqB : decidable_eq B] section union -definition to_comm_monoid_Union (B : Type) [deceqB : decidable_eq B] : +definition to_comm_monoid_Union (B : Type) [decidable_eq B] : comm_monoid (finset B) := ⦃ comm_monoid, mul := union, @@ -117,7 +117,7 @@ section deceqA (by rewrite Union_empty) (take s1 a Pa IH, by rewrite [image_insert, *Union_insert, IH]) - lemma Union_const [deceqB : decidable_eq B] {f : A → finset B} {s : finset A} {t : finset B} : + lemma Union_const [decidable_eq B] {f : A → finset B} {s : finset A} {t : finset B} : s ≠ ∅ → (∀ x, x ∈ s → f x = t) → Union s f = t := begin induction s with a' s' H IH, diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 1ce63e229..9dc12cc8a 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -496,7 +496,7 @@ theorem nth_eq_some : ∀ {l : list T} {n : nat}, n < length l → Σ a : T, nth ⟨r, by rewrite [nth_succ, req]⟩ open decidable -theorem find_nth [h : decidable_eq T] {a : T} : ∀ {l}, a ∈ l → nth l (find a l) = some a +theorem find_nth [decidable_eq T] {a : T} : ∀ {l}, a ∈ l → nth l (find a l) = some a | [] ain := absurd ain !not_mem_nil | (b::l) ainbl := by_cases (λ aeqb : a = b, by rewrite [find_cons_of_eq _ aeqb, nth_zero, aeqb]) @@ -510,9 +510,9 @@ match nth l n with | none := arbitrary T end -theorem inth_zero [h : inhabited T] (a : T) (l : list T) : inth (a :: l) 0 = a +theorem inth_zero [inhabited T] (a : T) (l : list T) : inth (a :: l) 0 = a -theorem inth_succ [h : inhabited T] (a : T) (l : list T) (n : nat) : inth (a::l) (n+1) = inth l n +theorem inth_succ [inhabited T] (a : T) (l : list T) (n : nat) : inth (a::l) (n+1) = inth l n end nth section ith diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean index 8cb4f5691..970917de4 100644 --- a/library/data/list/perm.lean +++ b/library/data/list/perm.lean @@ -169,7 +169,7 @@ assume p, calc ... ~ l₁++(a::l₂) : perm_app_right l₁ (perm.symm (perm_cons_app a l₂)) open decidable -theorem perm_erase [H : decidable_eq A] {a : A} : ∀ {l : list A}, a ∈ l → l ~ a::(erase a l) +theorem perm_erase [decidable_eq A] {a : A} : ∀ {l : list A}, a ∈ l → l ~ a::(erase a l) | [] h := absurd h !not_mem_nil | (x::t) h := by_cases @@ -181,7 +181,7 @@ theorem perm_erase [H : decidable_eq A] {a : A} : ∀ {l : list A}, a ∈ l → ... ~ a::x::(erase a t) : swap ... = a::(erase a (x::t)) : by rewrite [!erase_cons_tail naeqx]) -theorem erase_perm_erase_of_perm [congr] [H : decidable_eq A] (a : A) {l₁ l₂ : list A} : l₁ ~ l₂ → erase a l₁ ~ erase a l₂ := +theorem erase_perm_erase_of_perm [congr] [decidable_eq A] (a : A) {l₁ l₂ : list A} : l₁ ~ l₂ → erase a l₁ ~ erase a l₂ := assume p, perm.induction_on p nil (λ x t₁ t₂ p r, @@ -786,7 +786,7 @@ assume p₁ p₂, trans (perm_product_left t₁ p₁) (perm_product_right l₂ p end product /- filter -/ -theorem perm_filter [congr] {l₁ l₂ : list A} {p : A → Prop} [decp : decidable_pred p] : +theorem perm_filter [congr] {l₁ l₂ : list A} {p : A → Prop} [decidable_pred p] : l₁ ~ l₂ → (filter p l₁) ~ (filter p l₂) := assume u, perm.induction_on u perm.nil diff --git a/library/data/list/set.lean b/library/data/list/set.lean index 6d45bd3de..aa3a0e2d8 100644 --- a/library/data/list/set.lean +++ b/library/data/list/set.lean @@ -290,7 +290,7 @@ theorem nodup_map {f : A → B} (inj : injective f) : ∀ {l : list A}, nodup l by subst y; contradiction, nodup_cons nfxinm ndmfxs -theorem nodup_erase_of_nodup [h : decidable_eq A] (a : A) : ∀ {l}, nodup l → nodup (erase a l) +theorem nodup_erase_of_nodup [decidable_eq A] (a : A) : ∀ {l}, nodup l → nodup (erase a l) | [] n := nodup_nil | (b::l) n := by_cases (λ aeqb : a = b, by rewrite [aeqb, erase_cons_head]; exact (nodup_of_nodup_cons n)) @@ -302,7 +302,7 @@ theorem nodup_erase_of_nodup [h : decidable_eq A] (a : A) : ∀ {l}, nodup l → assert aux : nodup (b :: erase a l), from nodup_cons nbineal ndeal, by rewrite [erase_cons_tail _ aneb]; exact aux) -theorem mem_erase_of_nodup [h : decidable_eq A] (a : A) : ∀ {l}, nodup l → a ∉ erase a l +theorem mem_erase_of_nodup [decidable_eq A] (a : A) : ∀ {l}, nodup l → a ∉ erase a l | [] n := !not_mem_nil | (b::l) n := have ndl : nodup l, from nodup_of_nodup_cons n, @@ -317,23 +317,23 @@ theorem mem_erase_of_nodup [h : decidable_eq A] (a : A) : ∀ {l}, nodup l → a (λ aineal : a ∈ erase a l, absurd aineal naineal), by rewrite [erase_cons_tail _ aneb]; exact aux) -definition erase_dup [H : decidable_eq A] : list A → list A +definition erase_dup [decidable_eq A] : list A → list A | [] := [] | (x :: xs) := if x ∈ xs then erase_dup xs else x :: erase_dup xs -theorem erase_dup_nil [H : decidable_eq A] : erase_dup [] = ([] : list A) +theorem erase_dup_nil [decidable_eq A] : erase_dup [] = ([] : list A) -theorem erase_dup_cons_of_mem [H : decidable_eq A] {a : A} {l : list A} : a ∈ l → erase_dup (a::l) = erase_dup l := +theorem erase_dup_cons_of_mem [decidable_eq A] {a : A} {l : list A} : a ∈ l → erase_dup (a::l) = erase_dup l := assume ainl, calc erase_dup (a::l) = if a ∈ l then erase_dup l else a :: erase_dup l : rfl ... = erase_dup l : if_pos ainl -theorem erase_dup_cons_of_not_mem [H : decidable_eq A] {a : A} {l : list A} : a ∉ l → erase_dup (a::l) = a :: erase_dup l := +theorem erase_dup_cons_of_not_mem [decidable_eq A] {a : A} {l : list A} : a ∉ l → erase_dup (a::l) = a :: erase_dup l := assume nainl, calc erase_dup (a::l) = if a ∈ l then erase_dup l else a :: erase_dup l : rfl ... = a :: erase_dup l : if_neg nainl -theorem mem_erase_dup [H : decidable_eq A] {a : A} : ∀ {l}, a ∈ l → a ∈ erase_dup l +theorem mem_erase_dup [decidable_eq A] {a : A} : ∀ {l}, a ∈ l → a ∈ erase_dup l | [] h := absurd h !not_mem_nil | (b::l) h := by_cases (λ binl : b ∈ l, or.elim (eq_or_mem_of_mem_cons h) @@ -343,7 +343,7 @@ theorem mem_erase_dup [H : decidable_eq A] {a : A} : ∀ {l}, a ∈ l → a ∈ (λ aeqb : a = b, by rewrite [erase_dup_cons_of_not_mem nbinl, aeqb]; exact !mem_cons) (λ ainl : a ∈ l, by rewrite [erase_dup_cons_of_not_mem nbinl]; exact (or.inr (mem_erase_dup ainl)))) -theorem mem_of_mem_erase_dup [H : decidable_eq A] {a : A} : ∀ {l}, a ∈ erase_dup l → a ∈ l +theorem mem_of_mem_erase_dup [decidable_eq A] {a : A} : ∀ {l}, a ∈ erase_dup l → a ∈ l | [] h := by rewrite [erase_dup_nil at h]; exact h | (b::l) h := by_cases (λ binl : b ∈ l, @@ -355,13 +355,13 @@ theorem mem_of_mem_erase_dup [H : decidable_eq A] {a : A} : ∀ {l}, a ∈ erase (λ aeqb : a = b, by rewrite aeqb; exact !mem_cons) (λ ainel : a ∈ erase_dup l, or.inr (mem_of_mem_erase_dup ainel))) -theorem erase_dup_sub [H : decidable_eq A] (l : list A) : erase_dup l ⊆ l := +theorem erase_dup_sub [decidable_eq A] (l : list A) : erase_dup l ⊆ l := λ a i, mem_of_mem_erase_dup i -theorem sub_erase_dup [H : decidable_eq A] (l : list A) : l ⊆ erase_dup l := +theorem sub_erase_dup [decidable_eq A] (l : list A) : l ⊆ erase_dup l := λ a i, mem_erase_dup i -theorem nodup_erase_dup [H : decidable_eq A] : ∀ l : list A, nodup (erase_dup l) +theorem nodup_erase_dup [decidable_eq A] : ∀ l : list A, nodup (erase_dup l) | [] := by rewrite erase_dup_nil; exact nodup_nil | (a::l) := by_cases (λ ainl : a ∈ l, by rewrite [erase_dup_cons_of_mem ainl]; exact (nodup_erase_dup l)) @@ -371,14 +371,14 @@ theorem nodup_erase_dup [H : decidable_eq A] : ∀ l : list A, nodup (erase_dup assume ab : a ∈ erase_dup l, absurd (mem_of_mem_erase_dup ab) nainl, by rewrite [erase_dup_cons_of_not_mem nainl]; exact (nodup_cons nin r)) -theorem erase_dup_eq_of_nodup [H : decidable_eq A] : ∀ {l : list A}, nodup l → erase_dup l = l +theorem erase_dup_eq_of_nodup [decidable_eq A] : ∀ {l : list A}, nodup l → erase_dup l = l | [] d := rfl | (a::l) d := assert nainl : a ∉ l, from not_mem_of_nodup_cons d, assert dl : nodup l, from nodup_of_nodup_cons d, by rewrite [erase_dup_cons_of_not_mem nainl, erase_dup_eq_of_nodup dl] -definition decidable_nodup [instance] [h : decidable_eq A] : ∀ (l : list A), decidable (nodup l) +definition decidable_nodup [instance] [decidable_eq A] : ∀ (l : list A), decidable (nodup l) | [] := inl nodup_nil | (a::l) := match decidable_mem a l with @@ -416,7 +416,7 @@ theorem nodup_product : ∀ {l₁ : list A} {l₂ : list B}, nodup l₁ → nodu end, nodup_append_of_nodup_of_nodup_of_disjoint dm n₄ dsj -theorem nodup_filter (p : A → Prop) [h : decidable_pred p] : ∀ {l : list A}, nodup l → nodup (filter p l) +theorem nodup_filter (p : A → Prop) [decidable_pred p] : ∀ {l : list A}, nodup l → nodup (filter p l) | [] nd := nodup_nil | (a::l) nd := have nainl : a ∉ l, from not_mem_of_nodup_cons nd, diff --git a/library/data/list/sort.lean b/library/data/list/sort.lean index 3f3708490..0584a8fe9 100644 --- a/library/data/list/sort.lean +++ b/library/data/list/sort.lean @@ -177,10 +177,10 @@ eq_of_sorted_of_perm tr asy p s₁ s₂ section omit decR -lemma strongly_sorted_sort [ord : decidable_linear_order A] (l : list A) : strongly_sorted le (sort le l) := +lemma strongly_sorted_sort [decidable_linear_order A] (l : list A) : strongly_sorted le (sort le l) := strongly_sorted_sort_core le.total (@le.trans A _) le.refl l -lemma sort_eq_of_perm {l₁ l₂ : list A} [ord : decidable_linear_order A] (h : l₁ ~ l₂) : sort le l₁ = sort le l₂ := +lemma sort_eq_of_perm {l₁ l₂ : list A} [decidable_linear_order A] (h : l₁ ~ l₂) : sort le l₁ = sort le l₂ := sort_eq_of_perm_core le.total (@le.trans A _) le.refl (@le.antisymm A _) h end end list diff --git a/library/data/nat/bquant.lean b/library/data/nat/bquant.lean index e16dd5f7c..9ce3b3ba5 100644 --- a/library/data/nat/bquant.lean +++ b/library/data/nat/bquant.lean @@ -100,13 +100,13 @@ section (λ p_neg, inr (not_ball_of_not p_neg))) (λ ih_neg, inr (not_ball_succ_of_not_ball ih_neg))) - definition decidable_bex_le [instance] (n : nat) (P : nat → Prop) [H : decidable_pred P] + definition decidable_bex_le [instance] (n : nat) (P : nat → Prop) [decidable_pred P] : decidable (∃ x, x ≤ n ∧ P x) := decidable_of_decidable_of_iff (decidable_bex (succ n) P) (exists_congr (λn, and_congr !lt_succ_iff_le !iff.refl)) - definition decidable_ball_le [instance] (n : nat) (P : nat → Prop) [H : decidable_pred P] + definition decidable_ball_le [instance] (n : nat) (P : nat → Prop) [decidable_pred P] : decidable (∀ x, x ≤ n → P x) := decidable_of_decidable_of_iff (decidable_ball (succ n) P) diff --git a/library/data/set/card.lean b/library/data/set/card.lean index 9dc5fed31..aa735489c 100644 --- a/library/data/set/card.lean +++ b/library/data/set/card.lean @@ -30,11 +30,11 @@ else (assert ¬ finite (insert a s), from suppose _, absurd (!finite_of_finite_insert this) fins, by rewrite [card_of_not_finite fins, card_of_not_finite this]) -theorem card_insert_of_not_mem {a : A} {s : set A} [fins : finite s] (H : a ∉ s) : +theorem card_insert_of_not_mem {a : A} {s : set A} [finite s] (H : a ∉ s) : card (insert a s) = card s + 1 := by rewrite [↑card, to_finset_insert, -mem_to_finset_eq at H, finset.card_insert_of_not_mem H] -theorem card_insert_le (a : A) (s : set A) [fins : finite s] : +theorem card_insert_le (a : A) (s : set A) [finite s] : card (insert a s) ≤ card s + 1 := if H : a ∈ s then by rewrite [card_insert_of_mem H]; apply le_succ else by rewrite [card_insert_of_not_mem H] @@ -44,7 +44,7 @@ by rewrite [card_insert_of_not_mem !not_mem_empty, card_empty] /- Note: the induction tactic does not work well with the set induction principle with the extra predicate "finite". -/ -theorem eq_empty_of_card_eq_zero {s : set A} [fins : finite s] : card s = 0 → s = ∅ := +theorem eq_empty_of_card_eq_zero {s : set A} [finite s] : card s = 0 → s = ∅ := induction_on_finite s (by intro H; exact rfl) (begin @@ -56,7 +56,7 @@ induction_on_finite s theorem card_upto (n : ℕ) : card {i | i < n} = n := by rewrite [↑card, to_finset_upto, finset.card_upto] -theorem card_add_card (s₁ s₂ : set A) [fins₁ : finite s₁] [fins₂ : finite s₂] : +theorem card_add_card (s₁ s₂ : set A) [finite s₁] [finite s₂] : card s₁ + card s₂ = card (s₁ ∪ s₂) + card (s₁ ∩ s₂) := begin rewrite [-to_set_to_finset s₁, -to_set_to_finset s₂], @@ -64,17 +64,17 @@ begin apply finset.card_add_card end -theorem card_union (s₁ s₂ : set A) [fins₁ : finite s₁] [fins₂ : finite s₂] : +theorem card_union (s₁ s₂ : set A) [finite s₁] [finite s₂] : card (s₁ ∪ s₂) = card s₁ + card s₂ - card (s₁ ∩ s₂) := calc card (s₁ ∪ s₂) = card (s₁ ∪ s₂) + card (s₁ ∩ s₂) - card (s₁ ∩ s₂) : nat.add_sub_cancel ... = card s₁ + card s₂ - card (s₁ ∩ s₂) : card_add_card s₁ s₂ -theorem card_union_of_disjoint {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] (H : s₁ ∩ s₂ = ∅) : +theorem card_union_of_disjoint {s₁ s₂ : set A} [finite s₁] [finite s₂] (H : s₁ ∩ s₂ = ∅) : card (s₁ ∪ s₂) = card s₁ + card s₂ := by rewrite [card_union, H, card_empty] -theorem card_eq_card_add_card_diff {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] (H : s₁ ⊆ s₂) : +theorem card_eq_card_add_card_diff {s₁ s₂ : set A} [finite s₁] [finite s₂] (H : s₁ ⊆ s₂) : card s₂ = card s₁ + card (s₂ \ s₁) := have H1 : s₁ ∩ (s₂ \ s₁) = ∅, from eq_empty_of_forall_not_mem (take x, assume H, (and.right (and.right H)) (and.left H)), @@ -83,7 +83,7 @@ calc card s₂ = card (s₁ ∪ (s₂ \ s₁)) : {this} ... = card s₁ + card (s₂ \ s₁) : card_union_of_disjoint H1 -theorem card_le_card_of_subset {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] (H : s₁ ⊆ s₂) : +theorem card_le_card_of_subset {s₁ s₂ : set A} [finite s₁] [finite s₂] (H : s₁ ⊆ s₂) : card s₁ ≤ card s₂ := calc card s₂ = card s₁ + card (s₂ \ s₁) : card_eq_card_add_card_diff H @@ -91,7 +91,7 @@ calc variable {B : Type} -theorem card_image_eq_of_inj_on {f : A → B} {s : set A} [fins : finite s] (injfs : inj_on f s) : +theorem card_image_eq_of_inj_on {f : A → B} {s : set A} [finite s] (injfs : inj_on f s) : card (image f s) = card s := begin rewrite [↑card, to_finset_image]; @@ -100,7 +100,7 @@ begin apply injfs end -theorem card_le_of_inj_on (a : set A) (b : set B) [finb : finite b] +theorem card_le_of_inj_on (a : set A) (b : set B) [finite b] (Pex : ∃ f : A → B, inj_on f a ∧ (image f a ⊆ b)) : card a ≤ card b := by_cases @@ -115,10 +115,10 @@ by_cases (assume nfina : ¬ finite a, by rewrite [card_of_not_finite nfina]; exact !zero_le) -theorem card_image_le (f : A → B) (s : set A) [fins : finite s] : card (image f s) ≤ card s := +theorem card_image_le (f : A → B) (s : set A) [finite s] : card (image f s) ≤ card s := by rewrite [↑card, to_finset_image]; apply finset.card_image_le -theorem inj_on_of_card_image_eq {f : A → B} {s : set A} [fins : finite s] +theorem inj_on_of_card_image_eq {f : A → B} {s : set A} [finite s] (H : card (image f s) = card s) : inj_on f s := begin rewrite -to_set_to_finset, @@ -127,11 +127,11 @@ begin exact H end -theorem card_pos_of_mem {a : A} {s : set A} [fins : finite s] (H : a ∈ s) : card s > 0 := +theorem card_pos_of_mem {a : A} {s : set A} [finite s] (H : a ∈ s) : card s > 0 := have (#finset a ∈ to_finset s), by rewrite [finset.mem_eq_mem_to_set, to_set_to_finset]; apply H, finset.card_pos_of_mem this -theorem eq_of_card_eq_of_subset {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] +theorem eq_of_card_eq_of_subset {s₁ s₂ : set A} [finite s₁] [finite s₂] (Hcard : card s₁ = card s₂) (Hsub : s₁ ⊆ s₂) : s₁ = s₂ := begin diff --git a/library/data/set/finite.lean b/library/data/set/finite.lean index dbfb8a66c..b5a791cff 100644 --- a/library/data/set/finite.lean +++ b/library/data/set/finite.lean @@ -30,7 +30,7 @@ by rewrite [↑to_finset, dif_neg nfins] theorem to_set_to_finset (s : set A) [fins : finite s] : finset.to_set (to_finset s) = s := by rewrite [↑to_finset, dif_pos fins]; exact eq.symm (some_spec fins) -theorem mem_to_finset_eq (a : A) (s : set A) [fins : finite s] : +theorem mem_to_finset_eq (a : A) (s : set A) [finite s] : (#finset a ∈ to_finset s) = (a ∈ s) := by rewrite [-to_set_to_finset at {2}] @@ -57,64 +57,61 @@ by rewrite [-finset.to_set_empty]; apply finite_finset theorem to_finset_empty : to_finset (∅ : set A) = (#finset ∅) := to_finset_eq_of_to_set_eq !finset.to_set_empty -theorem finite_insert [instance] (a : A) (s : set A) [fins : finite s] : finite (insert a s) := +theorem finite_insert [instance] (a : A) (s : set A) [finite s] : finite (insert a s) := exists.intro (finset.insert a (to_finset s)) (by rewrite [finset.to_set_insert, to_set_to_finset]) -theorem to_finset_insert (a : A) (s : set A) [fins : finite s] : +theorem to_finset_insert (a : A) (s : set A) [finite s] : to_finset (insert a s) = finset.insert a (to_finset s) := by apply to_finset_eq_of_to_set_eq; rewrite [finset.to_set_insert, to_set_to_finset] -theorem finite_union [instance] (s t : set A) [fins : finite s] [fint : finite t] : +theorem finite_union [instance] (s t : set A) [finite s] [finite t] : finite (s ∪ t) := exists.intro (#finset to_finset s ∪ to_finset t) (by rewrite [finset.to_set_union, *to_set_to_finset]) -theorem to_finset_union (s t : set A) [fins : finite s] [fint : finite t] : +theorem to_finset_union (s t : set A) [finite s] [finite t] : to_finset (s ∪ t) = (#finset to_finset s ∪ to_finset t) := by apply to_finset_eq_of_to_set_eq; rewrite [finset.to_set_union, *to_set_to_finset] -theorem finite_inter [instance] (s t : set A) [fins : finite s] [fint : finite t] : +theorem finite_inter [instance] (s t : set A) [finite s] [finite t] : finite (s ∩ t) := exists.intro (#finset to_finset s ∩ to_finset t) (by rewrite [finset.to_set_inter, *to_set_to_finset]) -theorem to_finset_inter (s t : set A) [fins : finite s] [fint : finite t] : +theorem to_finset_inter (s t : set A) [finite s] [finite t] : to_finset (s ∩ t) = (#finset to_finset s ∩ to_finset t) := by apply to_finset_eq_of_to_set_eq; rewrite [finset.to_set_inter, *to_set_to_finset] -theorem finite_sep [instance] (s : set A) (p : A → Prop) [h : decidable_pred p] - [fins : finite s] : +theorem finite_sep [instance] (s : set A) (p : A → Prop) [decidable_pred p] [finite s] : finite {x ∈ s | p x} := exists.intro (finset.sep p (to_finset s)) (by rewrite [finset.to_set_sep, *to_set_to_finset]) -theorem to_finset_sep (s : set A) (p : A → Prop) [h : decidable_pred p] [fins : finite s] : +theorem to_finset_sep (s : set A) (p : A → Prop) [decidable_pred p] [finite s] : to_finset {x ∈ s | p x} = (#finset {x ∈ to_finset s | p x}) := by apply to_finset_eq_of_to_set_eq; rewrite [finset.to_set_sep, to_set_to_finset] -theorem finite_image [instance] {B : Type} [h : decidable_eq B] (f : A → B) (s : set A) - [fins : finite s] : +theorem finite_image [instance] {B : Type} [decidable_eq B] (f : A → B) (s : set A) [finite s] : finite (f '[s]) := exists.intro (finset.image f (to_finset s)) (by rewrite [finset.to_set_image, *to_set_to_finset]) -theorem to_finset_image {B : Type} [h : decidable_eq B] (f : A → B) (s : set A) +theorem to_finset_image {B : Type} [decidable_eq B] (f : A → B) (s : set A) [fins : finite s] : to_finset (f '[s]) = (#finset f '[to_finset s]) := by apply to_finset_eq_of_to_set_eq; rewrite [finset.to_set_image, to_set_to_finset] -theorem finite_diff [instance] (s t : set A) [fins : finite s] : finite (s \ t) := +theorem finite_diff [instance] (s t : set A) [finite s] : finite (s \ t) := !finite_sep -theorem to_finset_diff (s t : set A) [fins : finite s] [fint : finite t] : - to_finset (s \ t) = (#finset to_finset s \ to_finset t) := +theorem to_finset_diff (s t : set A) [finite s] [finite t] : to_finset (s \ t) = (#finset to_finset s \ to_finset t) := by apply to_finset_eq_of_to_set_eq; rewrite [finset.to_set_diff, *to_set_to_finset] -theorem finite_subset {s t : set A} [fint : finite t] (ssubt : s ⊆ t) : finite s := +theorem finite_subset {s t : set A} [finite t] (ssubt : s ⊆ t) : finite s := by rewrite (eq_sep_of_subset ssubt); apply finite_sep -theorem to_finset_subset_to_finset_eq (s t : set A) [fins : finite s] [fint : finite t] : +theorem to_finset_subset_to_finset_eq (s t : set A) [finite s] [finite t] : (#finset to_finset s ⊆ to_finset t) = (s ⊆ t) := by rewrite [finset.subset_eq_to_set_subset, *to_set_to_finset] @@ -127,7 +124,7 @@ by rewrite [-finset.to_set_upto n]; apply finite_finset theorem to_finset_upto (n : ℕ) : to_finset {i | i < n} = finset.upto n := by apply (to_finset_eq_of_to_set_eq !finset.to_set_upto) -theorem finite_powerset (s : set A) [fins : finite s] : finite 𝒫 s := +theorem finite_powerset (s : set A) [finite s] : finite 𝒫 s := assert H : 𝒫 s = finset.to_set '[finset.to_set (#finset 𝒫 (to_finset s))], from ext (take t, iff.intro (suppose t ∈ 𝒫 s, @@ -150,9 +147,8 @@ by rewrite H; apply finite_image /- induction for finite sets -/ theorem induction_finite [recursor 6] {P : set A → Prop} - (H1 : P ∅) - (H2 : ∀ ⦃a : A⦄, ∀ {s : set A} [fins : finite s], a ∉ s → P s → P (insert a s)) : - ∀ (s : set A) [fins : finite s], P s := + (H1 : P ∅) (H2 : ∀ ⦃a : A⦄, ∀ {s : set A} [finite s], a ∉ s → P s → P (insert a s)) : + ∀ (s : set A) [finite s], P s := begin intro s fins, rewrite [-to_set_to_finset s], @@ -166,9 +162,8 @@ begin exact ih end -theorem induction_on_finite {P : set A → Prop} (s : set A) [fins : finite s] - (H1 : P ∅) - (H2 : ∀ ⦃a : A⦄, ∀ {s : set A} [fins : finite s], a ∉ s → P s → P (insert a s)) : +theorem induction_on_finite {P : set A → Prop} (s : set A) [finite s] + (H1 : P ∅) (H2 : ∀ ⦃a : A⦄, ∀ {s : set A} [finite s], a ∉ s → P s → P (insert a s)) : P s := induction_finite H1 H2 s diff --git a/library/init/logic.lean b/library/init/logic.lean index 4426285bf..7cdc23c15 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -604,9 +604,9 @@ namespace decidable definition by_cases {q : Type} [C : decidable p] : (p → q) → (¬p → q) → q := !dite - theorem em (p : Prop) [H : decidable p] : p ∨ ¬p := by_cases or.inl or.inr + theorem em (p : Prop) [decidable p] : p ∨ ¬p := by_cases or.inl or.inr - theorem by_contradiction [Hp : decidable p] (H : ¬p → false) : p := + theorem by_contradiction [decidable p] (H : ¬p → false) : p := if H1 : p then H1 else false.rec _ (H H1) end decidable @@ -620,7 +620,7 @@ section definition decidable_of_decidable_of_eq (Hp : decidable p) (H : p = q) : decidable q := decidable_of_decidable_of_iff Hp (iff.of_eq H) - protected definition or.by_cases [Hp : decidable p] [Hq : decidable q] {A : Type} + protected definition or.by_cases [decidable p] [decidable q] {A : Type} (h : p ∨ q) (h₁ : p → A) (h₂ : q → A) : A := if hp : p then h₁ hp else if hq : q then h₂ hq else @@ -631,27 +631,27 @@ section variables {p q : Prop} open decidable (rec_on inl inr) - definition decidable_and [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p ∧ q) := + definition decidable_and [instance] [decidable p] [decidable q] : decidable (p ∧ q) := if hp : p then if hq : q then inl (and.intro hp hq) else inr (assume H : p ∧ q, hq (and.right H)) else inr (assume H : p ∧ q, hp (and.left H)) - definition decidable_or [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p ∨ q) := + definition decidable_or [instance] [decidable p] [decidable q] : decidable (p ∨ q) := if hp : p then inl (or.inl hp) else if hq : q then inl (or.inr hq) else inr (or.rec hp hq) - definition decidable_not [instance] [Hp : decidable p] : decidable (¬p) := + definition decidable_not [instance] [decidable p] : decidable (¬p) := if hp : p then inr (absurd hp) else inl hp - definition decidable_implies [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p → q) := + definition decidable_implies [instance] [decidable p] [decidable q] : decidable (p → q) := if hp : p then if hq : q then inl (assume H, hq) else inr (assume H : p → q, absurd (H hp) hq) else inl (assume Hp, absurd Hp hp) - definition decidable_iff [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p ↔ q) := + definition decidable_iff [instance] [decidable p] [decidable q] : decidable (p ↔ q) := decidable_and end @@ -659,7 +659,7 @@ end definition decidable_pred [reducible] {A : Type} (R : A → Prop) := Π (a : A), decidable (R a) definition decidable_rel [reducible] {A : Type} (R : A → A → Prop) := Π (a b : A), decidable (R a b) definition decidable_eq [reducible] (A : Type) := decidable_rel (@eq A) -definition decidable_ne [instance] {A : Type} [H : decidable_eq A] (a b : A) : decidable (a ≠ b) := +definition decidable_ne [instance] {A : Type} [decidable_eq A] (a b : A) : decidable (a ≠ b) := decidable_implies namespace bool @@ -719,7 +719,7 @@ inhabited.mk true definition inhabited_fun [instance] (A : Type) {B : Type} [H : inhabited B] : inhabited (A → B) := inhabited.rec_on H (λb, inhabited.mk (λa, b)) -definition inhabited_Pi [instance] (A : Type) {B : A → Type} [H : Πx, inhabited (B x)] : +definition inhabited_Pi [instance] (A : Type) {B : A → Type} [Πx, inhabited (B x)] : inhabited (Πx, B x) := inhabited.mk (λa, !default) @@ -738,7 +738,7 @@ intro : A → nonempty A protected definition nonempty.elim {A : Type} {B : Prop} (H1 : nonempty A) (H2 : A → B) : B := nonempty.rec H2 H1 -theorem nonempty_of_inhabited [instance] {A : Type} [H : inhabited A] : nonempty A := +theorem nonempty_of_inhabited [instance] {A : Type} [inhabited A] : nonempty A := nonempty.intro !default theorem nonempty_of_exists {A : Type} {P : A → Prop} : (∃x, P x) → nonempty A := @@ -794,10 +794,10 @@ decidable.rec (λ Hnc : ¬c, eq.refl (@ite c (decidable.inr Hnc) A t t)) H -theorem implies_of_if_pos {c t e : Prop} [H : decidable c] (h : ite c t e) : c → t := +theorem implies_of_if_pos {c t e : Prop} [decidable c] (h : ite c t e) : c → t := assume Hc, eq.rec_on (if_pos Hc) h -theorem implies_of_if_neg {c t e : Prop} [H : decidable c] (h : ite c t e) : ¬c → e := +theorem 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) h theorem if_ctx_congr {A : Type} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c] @@ -903,13 +903,13 @@ theorem dif_ctx_simp_congr {A : Type} {b c : Prop} [dec_b : decidable b] @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 -- Remark: dite and ite are "definitionally equal" when we ignore the proofs. -theorem dite_ite_eq (c : Prop) [H : decidable c] {A : Type} (t : A) (e : A) : dite c (λh, t) (λh, e) = ite c t e := +theorem dite_ite_eq (c : Prop) [decidable c] {A : Type} (t : A) (e : A) : dite c (λh, t) (λh, e) = ite c t e := rfl -definition is_true (c : Prop) [H : decidable c] : Prop := +definition is_true (c : Prop) [decidable c] : Prop := if c then true else false -definition is_false (c : Prop) [H : decidable c] : Prop := +definition is_false (c : Prop) [decidable c] : Prop := if c then false else true definition of_is_true {c : Prop} [H₁ : decidable c] (H₂ : is_true c) : c := @@ -917,14 +917,14 @@ decidable.rec_on H₁ (λ Hc, Hc) (λ Hnc, !false.rec (if_neg Hnc ▸ H₂)) notation `dec_trivial` := of_is_true trivial -theorem not_of_not_is_true {c : Prop} [H₁ : decidable c] (H₂ : ¬ is_true c) : ¬ c := -if Hc : c then absurd trivial (if_pos Hc ▸ H₂) else Hc +theorem not_of_not_is_true {c : Prop} [decidable c] (H : ¬ is_true c) : ¬ c := +if Hc : c then absurd trivial (if_pos Hc ▸ H) else Hc -theorem not_of_is_false {c : Prop} [H₁ : decidable c] (H₂ : is_false c) : ¬ c := -if Hc : c then !false.rec (if_pos Hc ▸ H₂) else Hc +theorem not_of_is_false {c : Prop} [decidable c] (H : is_false c) : ¬ c := +if Hc : c then !false.rec (if_pos Hc ▸ H) else Hc -theorem of_not_is_false {c : Prop} [H₁ : decidable c] (H₂ : ¬ is_false c) : c := -if Hc : c then Hc else absurd trivial (if_neg Hc ▸ H₂) +theorem of_not_is_false {c : Prop} [decidable c] (H : ¬ is_false c) : c := +if Hc : c then Hc else absurd trivial (if_neg Hc ▸ H) -- The following symbols should not be considered in the pattern inference procedure used by -- heuristic instantiation. diff --git a/library/init/measurable.lean b/library/init/measurable.lean index 017f2ad36..0352c6458 100644 --- a/library/init/measurable.lean +++ b/library/init/measurable.lean @@ -18,13 +18,13 @@ measurable.rec_on s (λ f, f) definition nat.measurable [instance] : measurable nat := measurable.mk (λ a, a) -definition option.measurable [instance] (A : Type) [s : measurable A] : measurable (option A) := +definition option.measurable [instance] (A : Type) [measurable A] : measurable (option A) := measurable.mk (λ a, option.cases_on a zero size_of) -definition prod.measurable [instance] (A B : Type) [sa : measurable A] [sb : measurable B] : measurable (prod A B) := +definition prod.measurable [instance] (A B : Type) [measurable A] [measurable B] : measurable (prod A B) := measurable.mk (λ p, prod.cases_on p (λ a b, size_of a + size_of b)) -definition sum.measurable [instance] (A B : Type) [sa : measurable A] [sb : measurable B] : measurable (sum A B) := +definition sum.measurable [instance] (A B : Type) [measurable A] [measurable B] : measurable (sum A B) := measurable.mk (λ s, sum.cases_on s (λ a, size_of a) (λ b, size_of b)) definition bool.measurable [instance] : measurable bool := diff --git a/library/init/quot.lean b/library/init/quot.lean index 97055225e..f353844f8 100644 --- a/library/init/quot.lean +++ b/library/init/quot.lean @@ -27,7 +27,7 @@ namespace quot init_quotient - protected theorem lift_beta {A B : Type} [s : setoid A] (f : A → B) (c : ∀ a b, a ≈ b → f a = f b) (a : A) : lift f c ⟦a⟧ = f a := + protected theorem lift_beta {A B : Type} [setoid A] (f : A → B) (c : ∀ a b, a ≈ b → f a = f b) (a : A) : lift f c ⟦a⟧ = f a := rfl protected theorem ind_beta {A : Type} [s : setoid A] {B : quot s → Prop} (p : ∀ a, B ⟦a⟧) (a : A) : ind p ⟦a⟧ = p a := diff --git a/tests/lean/run/blast_cc8.lean b/tests/lean/run/blast_cc8.lean index 3f155ad7a..b9afafe9b 100644 --- a/tests/lean/run/blast_cc8.lean +++ b/tests/lean/run/blast_cc8.lean @@ -19,22 +19,22 @@ end variable {A : Type} definition finite_set_empty [instance] : finite_set (∅:set A) := sorry definition finite_set_finset [instance] (fxs : finset A) : finite_set (to_set fxs) := sorry -definition finite_set_insert [instance] (xs : set A) [fxs : finite_set xs] (x : A) : finite_set (insert x xs) := sorry -definition finite_set_union [instance] (xs : set A) [fxs : finite_set xs] (ys : set A) [fys : finite_set ys] : finite_set (xs ∪ ys) := sorry -definition finite_set_inter1 [instance] (xs : set A) [fxs : finite_set xs] (ys : set A) [ys_dec : decidable_pred ys] : finite_set (xs ∩ ys) := sorry -definition finite_set_inter2 [instance] (xs : set A) [fxs : finite_set xs] (ys : set A) [ys_dec : decidable_pred ys] : finite_set (ys ∩ xs) := sorry -definition finite_set_set_of [instance] (xs : set A) [fxs : finite_set xs] : finite_set (set.set_of xs) := sorry +definition finite_set_insert [instance] (xs : set A) [finite_set xs] (x : A) : finite_set (insert x xs) := sorry +definition finite_set_union [instance] (xs : set A) [finite_set xs] (ys : set A) [finite_set ys] : finite_set (xs ∪ ys) := sorry +definition finite_set_inter1 [instance] (xs : set A) [finite_set xs] (ys : set A) [decidable_pred ys] : finite_set (xs ∩ ys) := sorry +definition finite_set_inter2 [instance] (xs : set A) [finite_set xs] (ys : set A) [decidable_pred ys] : finite_set (ys ∩ xs) := sorry +definition finite_set_set_of [instance] (xs : set A) [finite_set xs] : finite_set (set.set_of xs) := sorry /- Defined cardinality using finite_set type class -/ -noncomputable definition mycard {T : Type} (xs : set T) [fxs : finite_set xs] := +noncomputable definition mycard {T : Type} (xs : set T) [finite_set xs] := finset.card (to_finset xs) /- Congruence closure still works :-) -/ definition tst (A : Type) (s₁ s₂ s₃ s₄ s₅ s₆ : set A) - [fxs₁ : finite_set s₁] [fxs₂ : finite_set s₂] - [fxs₁ : finite_set s₃] [fxs₂ : finite_set s₄] - [d₁ : decidable_pred s₅] [d₂ : decidable_pred s₆] : + [finite_set s₁] [finite_set s₂] + [finite_set s₃] [finite_set s₄] + [decidable_pred s₅] [decidable_pred s₆] : s₁ = s₂ → s₃ = s₄ → s₆ = s₅ → mycard ((s₁ ∪ s₃) ∩ s₅) = mycard ((s₂ ∪ s₄) ∩ s₆) := by blast