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

chore(library/class): disable [trans_instance] attribute

Browse source 
Conflicts:
	src/library/class.cpp
This commit is contained in:
Leonardo de Moura 2016-07-29 14:29:31 -07:00
parent 03b1daa0bf
commit 264c23a24f
11 changed files with 23 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/algebra/field.lean
View file

@ -366,7 +366,7 @@ section discrete_field
or.inr (by rewrite [-one_mul, -(inv_mul_cancel this), mul.assoc, H, mul_zero]))
-/
definition discrete_field.to_integral_domain [trans_instance] :
definition discrete_field.to_integral_domain [instance] :
integral_domain A :=
⦃ integral_domain, s,
eq_zero_or_eq_zero_of_mul_eq_zero := discrete_field.eq_zero_or_eq_zero_of_mul_eq_zero⦄

8
library/algebra/group.lean
View file

@ -324,12 +324,12 @@ section group
end group
definition group.to_left_cancel_semigroup [trans_instance] [s : group A] :
definition group.to_left_cancel_semigroup [instance] [s : group A] :
left_cancel_semigroup A :=
⦃ left_cancel_semigroup, s,
mul_left_cancel := @mul_left_cancel A s ⦄
definition group.to_right_cancel_semigroup [trans_instance] [s : group A] :
definition group.to_right_cancel_semigroup [instance] [s : group A] :
right_cancel_semigroup A :=
⦃ right_cancel_semigroup, s,
mul_right_cancel := @mul_right_cancel A s ⦄
@ -466,11 +466,11 @@ section add_group
by inst_simp
-/
definition add_group.to_left_cancel_semigroup [trans_instance] : add_left_cancel_semigroup A :=
definition add_group.to_left_cancel_semigroup [instance] : add_left_cancel_semigroup A :=
⦃ add_left_cancel_semigroup, s,
add_left_cancel := @add_left_cancel A s ⦄
definition add_group.to_add_right_cancel_semigroup [trans_instance] :
definition add_group.to_add_right_cancel_semigroup [instance] :
add_right_cancel_semigroup A :=
⦃ add_right_cancel_semigroup, s,
add_right_cancel := @add_right_cancel A s ⦄

6
library/algebra/order.lean
View file

@ -114,7 +114,7 @@ section
private theorem lt_trans (s' : order_pair A) (a b c: A) (lt_ab : a < b) (lt_bc : b < c) : a < c :=
lt_of_lt_of_le lt_ab (le_of_lt lt_bc)
definition order_pair.to_strict_order [trans_instance] : strict_order A :=
definition order_pair.to_strict_order [instance] : strict_order A :=
⦃ strict_order, s, lt_irrefl := lt_irrefl s, lt_trans := lt_trans s ⦄
theorem gt_of_gt_of_ge [trans] (H1 : a > b) (H2 : b ≥ c) : a > c := lt_of_le_of_lt H2 H1
@ -188,7 +188,7 @@ section strong_order_pair
show a < c, from iff.mpr (lt_iff_le_and_ne) (and.intro le_ac ne_ac)
end strong_order_pair
definition strong_order_pair.to_order_pair [trans_instance]
definition strong_order_pair.to_order_pair [instance]
[s : strong_order_pair A] : order_pair A :=
⦃ order_pair, s,
lt_irrefl := lt_irrefl',
@ -203,7 +203,7 @@ structure linear_order_pair [class] (A : Type) extends order_pair A, linear_weak
structure linear_strong_order_pair [class] (A : Type) extends strong_order_pair A,
linear_weak_order A
definition linear_strong_order_pair.to_linear_order_pair [trans_instance]
definition linear_strong_order_pair.to_linear_order_pair [instance]
[s : linear_strong_order_pair A] : linear_order_pair A :=
⦃ linear_order_pair, s, strong_order_pair.to_order_pair ⦄

2
library/algebra/ordered_field.lean
View file

@ -469,7 +469,7 @@ section discrete_linear_ordered_field
(assume H' : ¬ y < x,
decidable.tt (le.antisymm (le_of_not_gt H') (le_of_not_gt H))))
definition discrete_linear_ordered_field.to_discrete_field [trans_instance] : discrete_field A :=
definition discrete_linear_ordered_field.to_discrete_field [instance] : discrete_field A :=
⦃ discrete_field, s, has_decidable_eq := dec_eq_of_dec_lt⦄
theorem pos_of_one_div_pos (H : 0 < 1 / a) : 0 < a :=

6
library/algebra/ordered_group.lean
View file

@ -276,7 +276,7 @@ theorem ordered_comm_group.lt_of_add_lt_add_left [ordered_comm_group A] {a b c :
have H' : -a + (a + b) < -a + (a + c), from ordered_comm_group.add_lt_add_left _ _ H _,
sorry -- by rewrite *neg_add_cancel_left at H'; exact H'
definition ordered_comm_group.to_ordered_cancel_comm_monoid [trans_instance] [s : ordered_comm_group A] : ordered_cancel_comm_monoid A :=
definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] [s : ordered_comm_group A] : ordered_cancel_comm_monoid A :=
⦃ ordered_cancel_comm_monoid, s,
add_left_cancel := @add.left_cancel A _,
add_right_cancel := @add.right_cancel A _,
@ -781,7 +781,7 @@ structure decidable_linear_ordered_comm_group [class] (A : Type)
(add_lt_add_left : ∀ a b, lt a b → ∀ c, lt (add c a) (add c b))
definition decidable_linear_ordered_comm_group.to_ordered_comm_group
[trans_instance]
[instance]
(A : Type) [s : decidable_linear_ordered_comm_group A] : ordered_comm_group A :=
⦃ ordered_comm_group, s,
le_of_lt := @le_of_lt A _,
@ -789,7 +789,7 @@ definition decidable_linear_ordered_comm_group.to_ordered_comm_group
lt_of_lt_of_le := @lt_of_lt_of_le A _ ⦄
definition decidable_linear_ordered_comm_group.to_decidable_linear_ordered_cancel_comm_monoid
[trans_instance] (A : Type) [s : decidable_linear_ordered_comm_group A] :
[instance] (A : Type) [s : decidable_linear_ordered_comm_group A] :
decidable_linear_ordered_cancel_comm_monoid A :=
⦃ decidable_linear_ordered_cancel_comm_monoid, s,
@ordered_comm_group.to_ordered_cancel_comm_monoid A _ ⦄

8
library/algebra/ordered_ring.lean
View file

@ -271,7 +271,7 @@ begin
end
-/
definition ordered_ring.to_ordered_semiring [trans_instance]
definition ordered_ring.to_ordered_semiring [instance]
[s : ordered_ring A] :
ordered_semiring A :=
⦃ ordered_semiring, s,
@ -371,7 +371,7 @@ structure linear_ordered_ring [class] (A : Type)
extends ordered_ring A, linear_strong_order_pair A :=
(zero_lt_one : lt zero one)
definition linear_ordered_ring.to_linear_ordered_semiring [trans_instance]
definition linear_ordered_ring.to_linear_ordered_semiring [instance]
[s : linear_ordered_ring A] :
linear_ordered_semiring A :=
⦃ linear_ordered_semiring, s,
@ -428,7 +428,7 @@ lt.by_cases
-/
-- Linearity implies no zero divisors. Doesn't need commutativity.
definition linear_ordered_comm_ring.to_integral_domain [trans_instance]
definition linear_ordered_comm_ring.to_integral_domain [instance]
[s: linear_ordered_comm_ring A] : integral_domain A :=
⦃ integral_domain, s,
eq_zero_or_eq_zero_of_mul_eq_zero :=
@ -535,7 +535,7 @@ structure decidable_linear_ordered_comm_ring [class] (A : Type) extends linear_o
decidable_linear_ordered_comm_group A
definition decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_semiring
[trans_instance] [s : decidable_linear_ordered_comm_ring A] :
[instance] [s : decidable_linear_ordered_comm_ring A] :
decidable_linear_ordered_semiring A :=
⦃decidable_linear_ordered_semiring, s, @linear_ordered_ring.to_linear_ordered_semiring A _⦄

4
library/algebra/ring.lean
View file

@ -196,7 +196,7 @@ have 0 * a + 0 = 0 * a + 0 * a, from calc
show 0 * a = 0, from (add.left_cancel this)⁻¹
-/
definition ring.to_semiring [trans_instance] [s : ring A] : semiring A :=
definition ring.to_semiring [instance] [s : ring A] : semiring A :=
⦃ semiring, s,
mul_zero := ring.mul_zero,
zero_mul := ring.zero_mul ⦄
@ -289,7 +289,7 @@ end
structure comm_ring [class] (A : Type) extends ring A, comm_semigroup A
definition comm_ring.to_comm_semiring [trans_instance] [s : comm_ring A] : comm_semiring A :=
definition comm_ring.to_comm_semiring [instance] [s : comm_ring A] : comm_semiring A :=
⦃ comm_semiring, s,
mul_zero := mul_zero,
zero_mul := zero_mul ⦄

2
library/data/nat/basic.lean
View file

@ -252,7 +252,7 @@ nat.cases_on n (by simp)
!succ_ne_zero))
-/
protected definition comm_semiring [trans_instance] : comm_semiring nat :=
protected definition comm_semiring [instance] : comm_semiring nat :=
⦃comm_semiring,
add := nat.add,
add_assoc := nat.add_assoc,

2
library/data/nat/order.lean
View file

@ -93,7 +93,7 @@ mul.comm k m ▸ mul.comm k n ▸ nat.mul_lt_mul_of_pos_left H Hk
/- nat is an instance of a linearly ordered semiring and a lattice -/
protected definition decidable_linear_ordered_semiring [trans_instance] :
protected definition decidable_linear_ordered_semiring [instance] :
decidable_linear_ordered_semiring nat :=
⦃ decidable_linear_ordered_semiring, nat.comm_semiring,
add_left_cancel := @nat.add_left_cancel,

4
src/library/class.cpp
View file

@ -429,10 +429,6 @@ void initialize_class() {
register_attribute(prio_attribute("instance", "type class instance", [](environment const & env, io_state const &, name const & d, unsigned prio, bool persistent) {
return add_instance(env, d, prio, persistent);
}));
register_attribute(prio_attribute("trans_instance", "transitive type class instance", [](environment const & env, io_state const &, name const & d, unsigned prio, bool persistent) {
return add_trans_instance(env, d, prio, persistent);
}));
}
void finalize_class() {

9
tests/lean/pp_all.lean.expected.out
View file

@ -1,9 +1,6 @@
a + of_num b = 10 : Prop
@eq.{1} nat
(@add.{1} nat nat._trans_of_decidable_linear_ordered_semiring_2 ((λ (x : nat), x) a)
(nat.of_num (@bit0.{1} num num_has_add (@one.{1} num num_has_one))))
(@bit0.{1} nat nat._trans_of_decidable_linear_ordered_semiring_2
(@bit1.{1} nat nat._trans_of_decidable_linear_ordered_semiring_22 nat._trans_of_decidable_linear_ordered_semiring_2
(@bit0.{1} nat nat._trans_of_decidable_linear_ordered_semiring_2
(@one.{1} nat nat._trans_of_decidable_linear_ordered_semiring_22)))) :
(@add.{1} nat nat_has_add ((λ (x : nat), x) a) (nat.of_num (@bit0.{1} num num_has_add (@one.{1} num num_has_one))))
(@bit0.{1} nat nat_has_add
(@bit1.{1} nat nat_has_one nat_has_add (@bit0.{1} nat nat_has_add (@one.{1} nat nat_has_one)))) :
Prop