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

refactor(library/data/nat,int): use nicer definitions of structure instances

Browse source
This commit is contained in:
Jeremy Avigad 2015-02-01 10:38:13 -05:00 committed by Leonardo de Moura
parent 95d79e7bda
commit e5c25ff7a3
3 changed files with 49 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
library/data/int/basic.lean
View file

@ -27,7 +27,6 @@ following:
padd_congr (p p' q q' : ℕ × ℕ) (H1 : p ≡ p') (H2 : q ≡ q') : padd p q ≡ p' q'
-/
import data.nat.basic data.nat.order data.nat.sub data.prod
import algebra.relation algebra.binary algebra.ordered_ring
import tools.fake_simplifier
@ -612,9 +611,25 @@ section
open [classes] algebra
protected definition integral_domain [instance] [reducible] : algebra.integral_domain int :=
algebra.integral_domain.mk add add.assoc zero zero_add add_zero neg add.left_inv
add.comm mul mul.assoc (of_num 1) one_mul mul_one mul.left_distrib mul.right_distrib
zero_ne_one mul.comm @eq_zero_or_eq_zero_of_mul_eq_zero
⦃algebra.integral_domain,
add := add,
add_assoc := add.assoc,
zero := zero,
zero_add := zero_add,
add_zero := add_zero,
neg := neg,
add_left_inv := add.left_inv,
add_comm := add.comm,
mul := mul,
mul_assoc := mul.assoc,
one := (of_num 1),
one_mul := one_mul,
mul_one := mul_one,
left_distrib := mul.left_distrib,
right_distrib := mul.right_distrib,
zero_ne_one := zero_ne_one,
mul_comm := mul.comm,
eq_zero_or_eq_zero_of_mul_eq_zero := @eq_zero_or_eq_zero_of_mul_eq_zero⦄
end
/- instantiate ring theorems to int -/

19
library/data/int/order.lean
View file

@ -8,9 +8,7 @@ Authors: Floris van Doorn, Jeremy Avigad
The order relation on the integers. We show that int is an instance of linear_comm_ordered_ring
and transfer the results.
-/
import .basic algebra.ordered_ring
open nat
open decidable
open fake_simplifier
@ -216,11 +214,18 @@ section
protected definition linear_ordered_comm_ring [instance] [reducible] :
algebra.linear_ordered_comm_ring int :=
algebra.linear_ordered_comm_ring.mk add add.assoc zero zero_add add_zero neg add.left_inv
add.comm mul mul.assoc (of_num 1) one_mul mul_one mul.left_distrib mul.right_distrib
zero_ne_one le le.refl @le.trans @le.antisymm lt lt_iff_le_and_ne @add_le_add_left
@mul_nonneg @mul_pos le_iff_lt_or_eq le.total mul.comm
⦃algebra.linear_ordered_comm_ring, int.integral_domain,
le := le,
le_refl := le.refl,
le_trans := @le.trans,
le_antisymm := @le.antisymm,
lt := lt,
lt_iff_le_ne := lt_iff_le_and_ne,
add_le_add_left := @add_le_add_left,
mul_nonneg := @mul_nonneg,
mul_pos := @mul_pos,
le_iff_lt_or_eq := le_iff_lt_or_eq,
le_total := le.total⦄
protected definition decidable_linear_ordered_comm_ring [instance] [reducible] :
algebra.decidable_linear_ordered_comm_ring int :=

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

@ -291,9 +291,24 @@ section
open [classes] algebra
protected definition comm_semiring [instance] [reducible] : algebra.comm_semiring nat :=
algebra.comm_semiring.mk add add.assoc zero zero_add add_zero add.comm
mul mul.assoc (succ zero) one_mul mul_one mul.left_distrib mul.right_distrib
zero_mul mul_zero (ne.symm (succ_ne_zero zero)) mul.comm
⦃algebra.comm_semiring,
add := add,
add_assoc := add.assoc,
zero := zero,
zero_add := zero_add,
add_zero := add_zero,
add_comm := add.comm,
mul := mul,
mul_assoc := mul.assoc,
one := succ zero,
one_mul := one_mul,
mul_one := mul_one,
left_distrib := mul.left_distrib,
right_distrib := mul.right_distrib,
zero_mul := zero_mul,
mul_zero := mul_zero,
zero_ne_one := ne.symm (succ_ne_zero zero),
mul_comm := mul.comm⦄
end
section port_algebra