michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library): use anonymous instance implicit arguments

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-13 11:15:10 -08:00
parent d26a83da02
commit ef546c5c5b
17 changed files with 182 additions and 187 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

92
library/algebra/group.lean
View file

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

8
library/algebra/group_set_bigops.lean
View file

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

4
library/algebra/ordered_group.lean
View file

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

56
library/algebra/ring.lean
View file

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

14
library/data/finset/basic.lean
View file

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

4
library/data/finset/bigops.lean
View file

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

6
library/data/list/basic.lean
View file

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

6
library/data/list/perm.lean
View file

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

28
library/data/list/set.lean
View file

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

4
library/data/list/sort.lean
View file

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

4
library/data/nat/bquant.lean
View file

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

28
library/data/set/card.lean
View file

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

45
library/data/set/finite.lean
View file

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

44
library/init/logic.lean
View file

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

6
library/init/measurable.lean
View file

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

2
library/init/quot.lean
View file

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

18
tests/lean/run/blast_cc8.lean
View file

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