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

refactor(library/algebra/group): avoid abuse of rewrite tactic

Browse source 
The two instances are relying on the fact that (a - b) reduces to (a + -b)
This commit is contained in:
Leonardo de Moura 2015-06-22 15:11:14 -07:00
parent a2389fb664
commit 7ffabeb245
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/algebra/group.lean
View file

@ -439,7 +439,7 @@ section add_group
theorem neg_sub (a b : A) : -(a - b) = b - a := theorem neg_sub (a b : A) : -(a - b) = b - a :=
neg_eq_of_add_eq_zero neg_eq_of_add_eq_zero
(calc (calc
a - b + (b - a) = a - b + b - a : by rewrite -add.assoc a - b + (b - a) = a - b + b - a : by krewrite -add.assoc
... = a - a : sub_add_cancel ... = a - a : sub_add_cancel
... = 0 : sub_self) ... = 0 : sub_self)
@ -448,7 +448,7 @@ section add_group
theorem sub_add_eq_sub_sub_swap (a b c : A) : a - (b + c) = a - c - b := theorem sub_add_eq_sub_sub_swap (a b c : A) : a - (b + c) = a - c - b :=
calc calc
a - (b + c) = a + (-c - b) : neg_add_rev a - (b + c) = a + (-c - b) : neg_add_rev
... = a - c - b : by rewrite add.assoc ... = a - c - b : by krewrite -add.assoc
theorem sub_eq_iff_eq_add (a b c : A) : a - b = c ↔ a = c + b := theorem sub_eq_iff_eq_add (a b c : A) : a - b = c ↔ a = c + b :=
iff.intro (assume H, eq_add_of_add_neg_eq H) (assume H, add_neg_eq_of_eq_add H) iff.intro (assume H, eq_add_of_add_neg_eq H) (assume H, add_neg_eq_of_eq_add H)