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

fix(tests/lean/simplifier_norm_num): adjust tests to recent changes

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-12 20:59:26 -08:00
parent 44a099f6f1
commit 182085b366
1 changed files with 38 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

75
tests/lean/simplifier_norm_num.lean
View file

@ -1,7 +1,7 @@
import algebra.numeral algebra.field import algebra.numeral algebra.field
open algebra open algebra
namespace norm_num namespace aux namespace norm_num
universe l universe l
constants (A : Type.{l}) (A_comm_ring : comm_ring A) constants (A : Type.{l}) (A_comm_ring : comm_ring A)
attribute A_comm_ring [instance] attribute A_comm_ring [instance]
@ -9,26 +9,26 @@ attribute A_comm_ring [instance]
set_option simplify.max_steps 5000000 set_option simplify.max_steps 5000000
set_option simplify.top_down false set_option simplify.top_down false
lemma bit0_add_bit0_helper [simp] (a b : A) : bit0 a + bit0 b = bit0 (a + b) := bit0_add_bit0_helper a b (a+b) rfl lemma bit0_add_bit0_helper [simp] (a b : A) : bit0 a + bit0 b = bit0 (a + b) := norm_num.bit0_add_bit0_helper a b (a+b) rfl
lemma add1_bit1_helper [simp] (a : A) : (bit1 a) + 1 = bit0 (a + 1) := add1_bit1_helper a (add1 a) rfl lemma add1_bit1_helper [simp] (a : A) : (bit1 a) + 1 = bit0 (a + 1) := norm_num.add1_bit1_helper a (norm_num.add1 a) rfl
lemma bit1_add_one_helper [simp] (a : A) : bit1 a + 1 = (bit1 a) + 1 := bit1_add_one_helper a (add1 (bit1 a)) rfl lemma bit1_add_one_helper [simp] (a : A) : bit1 a + 1 = (bit1 a) + 1 := norm_num.bit1_add_one_helper a (norm_num.add1 (bit1 a)) rfl
lemma bit1_add_bit0_helper [simp] (a b : A) : bit1 a + bit0 b = bit1 (a + b) := bit1_add_bit0_helper a b (a + b) rfl lemma bit1_add_bit0_helper [simp] (a b : A) : bit1 a + bit0 b = bit1 (a + b) := norm_num.bit1_add_bit0_helper a b (a + b) rfl
lemma bit1_add_bit1_helper [simp] (a b : A) : bit1 a + bit1 b = bit0 (a + b + 1) := bit1_add_bit1_helper a b (a + b) (a + b + 1) rfl rfl lemma bit1_add_bit1_helper [simp] (a b : A) : bit1 a + bit1 b = bit0 (a + b + 1) := norm_num.bit1_add_bit1_helper a b (a + b) (a + b + 1) rfl rfl
lemma bit0_add_bit1_helper [simp] (a b : A) : bit0 a + bit1 b = bit1 (a + b) := bit0_add_bit1_helper a b (a + b) rfl lemma bit0_add_bit1_helper [simp] (a b : A) : bit0 a + bit1 b = bit1 (a + b) := norm_num.bit0_add_bit1_helper a b (a + b) rfl
lemma one_add_bit1_helper [simp] (a : A) : 1 + bit1 a = bit1 a + 1 := one_add_bit1_helper a (bit1 a + 1) rfl lemma one_add_bit1_helper [simp] (a : A) : 1 + bit1 a = bit1 a + 1 := norm_num.one_add_bit1_helper a (bit1 a + 1) rfl
lemma bin_zero_add [simp] (a : A) : 0 + a = a := bin_zero_add a lemma bin_zero_add [simp] (a : A) : 0 + a = a := norm_num.bin_zero_add a
lemma bin_add_zero [simp] (a : A) : a + 0 = a := bin_add_zero a lemma bin_add_zero [simp] (a : A) : a + 0 = a := norm_num.bin_add_zero a
lemma one_add_one [simp] : (1:A) + 1 = 2 := one_add_one lemma one_add_one [simp] : (1:A) + 1 = 2 := norm_num.one_add_one
lemma one_add_bit0 [simp] (a : A) : 1 + bit0 a = bit1 a := one_add_bit0 a lemma one_add_bit0 [simp] (a : A) : 1 + bit0 a = bit1 a := norm_num.one_add_bit0 a
lemma bit0_add_one [simp] (a : A) : bit0 a + 1 = bit1 a := bit0_add_one a lemma bit0_add_one [simp] (a : A) : bit0 a + 1 = bit1 a := norm_num.bit0_add_one a
lemma mul_bit0_helper0 [simp] (a b : A) : bit0 a * bit0 b = bit0 (bit0 a * b) := mul_bit0_helper (bit0 a) b (bit0 a * b) rfl lemma mul_bit0_helper0 [simp] (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 b : A) : bit1 a * bit0 b = bit0 (bit1 a * b) := mul_bit0_helper (bit1 a) b (bit1 a * b) rfl lemma mul_bit0_helper1 [simp] (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 b : A) : bit0 a * bit1 b = bit0 (bit0 a * b) + bit0 a := mul_bit1_helper (bit0 a) b (bit0 a * b) (bit0 (bit0 a * b) + bit0 a) rfl rfl lemma mul_bit1_helper0 [simp] (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 b : A) : bit1 a * bit1 b = bit0 (bit1 a * b) + bit1 a := mul_bit1_helper (bit1 a) b (bit1 a * b) (bit0 (bit1 a * b) + bit1 a) rfl rfl lemma mul_bit1_helper1 [simp] (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
lemma mul_zero [simp] (a : A) : a * 0 = 0 := mul_zero a lemma mul_zero [simp] (a : A) : a * 0 = 0 := mul_zero a
lemma zero_mul [simp] (a : A) : 0 * a = 0 := zero_mul a lemma zero_mul [simp] (a : A) : 0 * a = 0 := zero_mul a
@ -36,27 +36,28 @@ lemma mul_one [simp] (a : A) : a * 1 = a := mul_one a
lemma one_mul [simp] (a : A) : 1 * a = a := one_mul a lemma one_mul [simp] (a : A) : 1 * a = a := one_mul a
end norm_num end norm_num
end aux
open norm_num open aux.norm_num
#simplify eq 0 (0:A) + 1 #simplify eq 0 (0:A) + 1
#simplify eq 0 (1:A) + 0 #simplify eq 0 (1:A) + 0
#simplify eq 0 (1:A) + 1 #simplify eq 0 (1:A) + 1
#simplify eq 0 (0:A) + 2 #simplify eq 0 (0:A) + 2
#simplify eq 0 (1:A) + 2 #simplify eq 0 (1:A) + 2
#simplify eq 0 (2:A) + 1 #simplify eq 0 (2:A) + 1
#simplify eq 0 (3:A) + 1 #simplify eq 0 (3:A) + 1
#simplify eq 0 (2:A) + 2 #simplify eq 0 (2:A) + 2
#simplify eq 0 (4:A) + 1 #simplify eq 0 (4:A) + 1
#simplify eq 0 (3:A) + 2 #simplify eq 0 (3:A) + 2
#simplify eq 0 (2:A) + 3 #simplify eq 0 (2:A) + 3
#simplify eq 0 (0:A) + 6 #simplify eq 0 (0:A) + 6
#simplify eq 0 (3:A) + 3 #simplify eq 0 (3:A) + 3
#simplify eq 0 (4:A) + 2 #simplify eq 0 (4:A) + 2
#simplify eq 0 (5:A) + 1 #simplify eq 0 (5:A) + 1
#simplify eq 0 (4:A) + 3 #simplify eq 0 (4:A) + 3
#simplify eq 0 (1:A) + 6 #simplify eq 0 (1:A) + 6
#simplify eq 0 (6:A) + 1 #simplify eq 0 (6:A) + 1
#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)