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

fix(algebra/simplifier): update numeral simp rules

Browse source
This commit is contained in:
Daniel Selsam 2015-11-13 10:50:35 -08:00
parent db59c6829c
commit 30b1b79c4e
2 changed files with 45 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

60
library/algebra/simplifier.lean
View file

@ -37,45 +37,63 @@ end units
-- TODO(dhs): remove `add1` from the original lemmas and delete this -- TODO(dhs): remove `add1` from the original lemmas and delete this
namespace numeral_helper namespace numeral_helper
open algebra norm_num open algebra
theorem bit1_add_bit1 {A : Type} [s : algebra.add_comm_semigroup A] theorem bit1_add_bit1 {A : Type} [s : add_comm_semigroup A]
[s' : has_one A] (a b : A) : bit1 a + bit1 b = bit0 ((a + b) + 1) [s' : has_one A] (a b : A) : bit1 a + bit1 b = bit0 ((a + b) + 1)
:= bit1_add_bit1 a b := norm_num.bit1_add_bit1 a b
theorem one_add_bit1 {A : Type} [s : add_comm_semigroup A] [s' : has_one A] (a : A)
: one + bit1 a = (bit1 a) + 1 := !add.comm
theorem bit1_add_one {A : Type} [s : add_comm_semigroup A] [s' : has_one A] (a : A) theorem bit1_add_one {A : Type} [s : add_comm_semigroup A] [s' : has_one A] (a : A)
: bit1 a + one = bit0 (a + 1) := add1_bit1 a : bit1 a + one = bit0 (a + 1) := norm_num.add1_bit1 a
theorem one_add_bit1 {A : Type} [s : add_comm_semigroup A] [s' : has_one A] (a : A)
: one + bit1 a = bit0 (a + 1) := by rewrite [!add.comm, bit1_add_one]
lemma one_add_bit0 [simp] {A : Type} [s : add_comm_semigroup A] [s' : has_one A] (a : A)
: 1 + bit0 a = bit1 a := norm_num.one_add_bit0 a
lemma bit0_add_one [simp] {A : Type} [s : add_comm_semigroup A] [s' : has_one A] (a : A)
: bit0 a + 1 = bit1 a := norm_num.bit0_add_one a
lemma mul_bit0_helper0 [simp] {A : Type} [s : comm_ring A] (a b : A)
: bit0 a * bit0 b = bit0 (bit0 a * b) := norm_num.mul_bit0_helper (bit0 a) b (bit0 a * b) rfl
lemma mul_bit0_helper1 [simp] {A : Type} [s : comm_ring A] (a b : A)
: bit1 a * bit0 b = bit0 (bit1 a * b) := norm_num.mul_bit0_helper (bit1 a) b (bit1 a * b) rfl
lemma mul_bit1_helper0 [simp] {A : Type} [s : comm_ring A] (a b : A)
: bit0 a * bit1 b = bit0 (bit0 a * b) + bit0 a := norm_num.mul_bit1_helper (bit0 a) b (bit0 a * b) (bit0 (bit0 a * b) + bit0 a) rfl rfl
lemma mul_bit1_helper1 [simp] {A : Type} [s : comm_ring A] (a b : A)
: bit1 a * bit1 b = bit0 (bit1 a * b) + bit1 a := norm_num.mul_bit1_helper (bit1 a) b (bit1 a * b) (bit0 (bit1 a * b) + bit1 a) rfl rfl
end numeral_helper end numeral_helper
namespace numeral namespace numeral
attribute norm_num.one_add_bit0 [simp]
attribute norm_num.bit0_add_one [simp]
attribute numeral_helper.one_add_bit1 [simp]
attribute numeral_helper.bit1_add_one [simp]
attribute norm_num.one_add_one [simp]
attribute norm_num.bit0_add_bit0 [simp] attribute norm_num.bit0_add_bit0 [simp]
attribute norm_num.bit0_add_bit1 [simp] attribute numeral_helper.bit1_add_one [simp]
attribute norm_num.bit1_add_bit0 [simp] attribute norm_num.bit1_add_bit0 [simp]
attribute numeral_helper.bit1_add_bit1 [simp] attribute numeral_helper.bit1_add_bit1 [simp]
attribute norm_num.bit0_add_bit1 [simp]
attribute algebra.one_mul [simp] attribute numeral_helper.one_add_bit1 [simp]
attribute algebra.mul_one [simp]
attribute norm_num.mul_bit0 [simp]
attribute norm_num.mul_bit1 [simp]
attribute algebra.zero_add [simp] attribute algebra.zero_add [simp]
attribute algebra.add_zero [simp] attribute algebra.add_zero [simp]
attribute norm_num.one_add_one [simp]
attribute numeral_helper.one_add_bit0 [simp]
attribute numeral_helper.bit0_add_one [simp]
attribute numeral_helper.mul_bit0_helper0 [simp]
attribute numeral_helper.mul_bit0_helper1 [simp]
attribute numeral_helper.mul_bit1_helper0 [simp]
attribute numeral_helper.mul_bit1_helper1 [simp]
attribute algebra.zero_mul [simp] attribute algebra.zero_mul [simp]
attribute algebra.mul_zero [simp] attribute algebra.mul_zero [simp]
attribute algebra.one_mul [simp]
attribute algebra.mul_one [simp]
end numeral end numeral

9
tests/lean/simplifier_norm_num.lean
View file

@ -1,9 +1,11 @@
import algebra.simplifier import algebra.simplifier
open simplifier.numeral
open algebra open algebra
set_option simplify.max_steps 500000 open simplifier.numeral
constants (A : Type.{1}) (A_comm_ring : algebra.comm_ring A)
set_option simplify.max_steps 5000000
universe l
constants (A : Type.{l}) (A_comm_ring : comm_ring A)
attribute A_comm_ring [instance] attribute A_comm_ring [instance]
#simplify eq 0 (0:A) + 1 #simplify eq 0 (0:A) + 1
@ -27,6 +29,7 @@ attribute A_comm_ring [instance]
#simplify eq 0 (5:A) + 28 #simplify eq 0 (5:A) + 28
#simplify eq 0 (0 : A) + (2 + 3) + 7 #simplify eq 0 (0 : A) + (2 + 3) + 7
#simplify eq 0 (70 : A) + (33 + 2) #simplify eq 0 (70 : A) + (33 + 2)
#simplify eq 0 (23000000000 : A) + 22000000000 #simplify eq 0 (23000000000 : A) + 22000000000
#simplify eq 0 (0 : A) * 0 #simplify eq 0 (0 : A) * 0