refactor(algebra/numeral): prove lemmas incrementally
This commit is contained in:
Daniel Selsam
Leonardo de Moura
parent
2e4765482b
commit
934b502c6f
11 changed files with 287 additions and 279 deletions
|
|
@ -470,3 +470,62 @@ section discrete_field
|
||||||
end discrete_field
|
end discrete_field
|
||||||
|
|
||||||
end algebra
|
end algebra
|
||||||
|
|
||||||
|
namespace norm_num
|
||||||
|
open algebra
|
||||||
|
variable {A : Type}
|
||||||
|
|
||||||
|
theorem div_add_helper [s : field A] (n d b c val : A) (Hd : d ≠ 0) (H : n + b * d = val)
|
||||||
|
(H2 : c * d = val) : n / d + b = c :=
|
||||||
|
begin
|
||||||
|
apply eq_of_mul_eq_mul_of_nonzero_right Hd,
|
||||||
|
rewrite [H2, -H, right_distrib, div_mul_cancel _ Hd]
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem add_div_helper [s : field A] (n d b c val : A) (Hd : d ≠ 0) (H : d * b + n = val)
|
||||||
|
(H2 : d * c = val) : b + n / d = c :=
|
||||||
|
begin
|
||||||
|
apply eq_of_mul_eq_mul_of_nonzero_left Hd,
|
||||||
|
rewrite [H2, -H, left_distrib, mul_div_cancel' Hd]
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem div_mul_helper [s : field A] (n d c v : A) (Hd : d ≠ 0) (H : (n * c) / d = v) :
|
||||||
|
(n / d) * c = v :=
|
||||||
|
by rewrite [-H, field.div_mul_eq_mul_div_comm _ _ Hd, mul_div_assoc]
|
||||||
|
|
||||||
|
theorem mul_div_helper [s : field A] (a n d v : A) (Hd : d ≠ 0) (H : (a * n) / d = v) :
|
||||||
|
a * (n / d) = v :=
|
||||||
|
by rewrite [-H, mul_div_assoc]
|
||||||
|
|
||||||
|
theorem nonzero_of_div_helper [s : field A] (a b : A) (Ha : a ≠ 0) (Hb : b ≠ 0) : a / b ≠ 0 :=
|
||||||
|
begin
|
||||||
|
intro Hab,
|
||||||
|
have Habb : (a / b) * b = 0, by rewrite [Hab, zero_mul],
|
||||||
|
rewrite [div_mul_cancel _ Hb at Habb],
|
||||||
|
exact Ha Habb
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem div_helper [s : field A] (n d v : A) (Hd : d ≠ 0) (H : v * d = n) : n / d = v :=
|
||||||
|
begin
|
||||||
|
apply eq_of_mul_eq_mul_of_nonzero_right Hd,
|
||||||
|
rewrite (div_mul_cancel _ Hd),
|
||||||
|
exact eq.symm H
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem div_eq_div_helper [s : field A] (a b c d v : A) (H1 : a * d = v) (H2 : c * b = v)
|
||||||
|
(Hb : b ≠ 0) (Hd : d ≠ 0) : a / b = c / d :=
|
||||||
|
begin
|
||||||
|
apply eq_div_of_mul_eq,
|
||||||
|
exact Hd,
|
||||||
|
rewrite div_mul_eq_mul_div,
|
||||||
|
apply eq.symm,
|
||||||
|
apply eq_div_of_mul_eq,
|
||||||
|
exact Hb,
|
||||||
|
rewrite [H1, H2]
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem subst_into_div [s : has_div A] (a₁ b₁ a₂ b₂ v : A) (H : a₁ / b₁ = v) (H1 : a₂ = a₁)
|
||||||
|
(H2 : b₂ = b₁) : a₂ / b₂ = v :=
|
||||||
|
by rewrite [H1, H2, H]
|
||||||
|
|
||||||
|
end norm_num
|
||||||
|
|
|
||||||
|
|
@ -581,6 +581,115 @@ definition group_of_add_group (A : Type) [G : add_group A] : group A :=
|
||||||
|
|
||||||
end algebra
|
end algebra
|
||||||
|
|
||||||
|
namespace norm_num
|
||||||
|
open algebra
|
||||||
|
reveal add.assoc
|
||||||
|
variable {A : Type}
|
||||||
|
|
||||||
|
definition add1 [s : has_add A] [s' : has_one A] (a : A) : A := add a one
|
||||||
|
|
||||||
|
theorem add_comm_four [s : add_comm_semigroup A] (a b : A) : a + a + (b + b) = (a + b) + (a + b) :=
|
||||||
|
by rewrite [-add.assoc at {1}, add.comm, {a + b}add.comm at {1}, *add.assoc]
|
||||||
|
|
||||||
|
theorem add_comm_middle [s : add_comm_semigroup A] (a b c : A) : a + b + c = a + c + b :=
|
||||||
|
by rewrite [add.assoc, add.comm b, -add.assoc]
|
||||||
|
|
||||||
|
theorem bit0_add_bit0 [s : add_comm_semigroup A] (a b : A) : bit0 a + bit0 b = bit0 (a + b) :=
|
||||||
|
!add_comm_four
|
||||||
|
|
||||||
|
theorem bit0_add_bit0_helper [s : add_comm_semigroup A] (a b t : A) (H : a + b = t) :
|
||||||
|
bit0 a + bit0 b = bit0 t :=
|
||||||
|
by rewrite -H; apply bit0_add_bit0
|
||||||
|
|
||||||
|
theorem bit1_add_bit0 [s : add_comm_semigroup A] [s' : has_one A] (a b : A) :
|
||||||
|
bit1 a + bit0 b = bit1 (a + b) :=
|
||||||
|
begin
|
||||||
|
rewrite [↑bit0, ↑bit1, add_comm_middle], congruence, apply add_comm_four
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem bit1_add_bit0_helper [s : add_comm_semigroup A] [s' : has_one A] (a b t : A)
|
||||||
|
(H : a + b = t) : bit1 a + bit0 b = bit1 t :=
|
||||||
|
by rewrite -H; apply bit1_add_bit0
|
||||||
|
|
||||||
|
theorem bit0_add_bit1 [s : add_comm_semigroup A] [s' : has_one A] (a b : A) :
|
||||||
|
bit0 a + bit1 b = bit1 (a + b) :=
|
||||||
|
by rewrite [{bit0 a + _}add.comm, {a + _}add.comm]; apply bit1_add_bit0
|
||||||
|
|
||||||
|
theorem bit0_add_bit1_helper [s : add_comm_semigroup A] [s' : has_one A] (a b t : A)
|
||||||
|
(H : a + b = t) : bit0 a + bit1 b = bit1 t :=
|
||||||
|
by rewrite -H; apply bit0_add_bit1
|
||||||
|
|
||||||
|
theorem bit1_add_bit1 [s : add_comm_semigroup A] [s' : has_one A] (a b : A) :
|
||||||
|
bit1 a + bit1 b = bit0 (add1 (a + b)) :=
|
||||||
|
begin
|
||||||
|
rewrite ↑[bit0, bit1, add1, add.assoc],
|
||||||
|
rewrite [*add.assoc, {_ + (b + 1)}add.comm, {_ + (b + 1 + _)}add.comm,
|
||||||
|
{_ + (b + 1 + _ + _)}add.comm, *add.assoc, {1 + a}add.comm, -{b + (a + 1)}add.assoc,
|
||||||
|
{b + a}add.comm, *add.assoc]
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem bit1_add_bit1_helper [s : add_comm_semigroup A] [s' : has_one A] (a b t s: A)
|
||||||
|
(H : (a + b) = t) (H2 : add1 t = s) : bit1 a + bit1 b = bit0 s :=
|
||||||
|
begin rewrite [-H2, -H], apply bit1_add_bit1 end
|
||||||
|
|
||||||
|
theorem bin_add_zero [s : add_monoid A] (a : A) : a + zero = a := !add_zero
|
||||||
|
|
||||||
|
theorem bin_zero_add [s : add_monoid A] (a : A) : zero + a = a := !zero_add
|
||||||
|
|
||||||
|
theorem one_add_bit0 [s : add_comm_semigroup A] [s' : has_one A] (a : A) : one + bit0 a = bit1 a :=
|
||||||
|
begin rewrite ↑[bit0, bit1], rewrite add.comm end
|
||||||
|
|
||||||
|
theorem bit0_add_one [s : has_add A] [s' : has_one A] (a : A) : bit0 a + one = bit1 a :=
|
||||||
|
rfl
|
||||||
|
|
||||||
|
theorem bit1_add_one [s : has_add A] [s' : has_one A] (a : A) : bit1 a + one = add1 (bit1 a) :=
|
||||||
|
rfl
|
||||||
|
|
||||||
|
theorem bit1_add_one_helper [s : has_add A] [s' : has_one A] (a t : A) (H : add1 (bit1 a) = t) :
|
||||||
|
bit1 a + one = t :=
|
||||||
|
by rewrite -H
|
||||||
|
|
||||||
|
theorem one_add_bit1 [s : add_comm_semigroup A] [s' : has_one A] (a : A) :
|
||||||
|
one + bit1 a = add1 (bit1 a) := !add.comm
|
||||||
|
|
||||||
|
theorem one_add_bit1_helper [s : add_comm_semigroup A] [s' : has_one A] (a t : A)
|
||||||
|
(H : add1 (bit1 a) = t) : one + bit1 a = t :=
|
||||||
|
by rewrite -H; apply one_add_bit1
|
||||||
|
|
||||||
|
theorem add1_bit0 [s : has_add A] [s' : has_one A] (a : A) : add1 (bit0 a) = bit1 a :=
|
||||||
|
rfl
|
||||||
|
|
||||||
|
theorem add1_bit1 [s : add_comm_semigroup A] [s' : has_one A] (a : A) :
|
||||||
|
add1 (bit1 a) = bit0 (add1 a) :=
|
||||||
|
begin
|
||||||
|
rewrite ↑[add1, bit1, bit0],
|
||||||
|
rewrite [add.assoc, add_comm_four]
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem add1_bit1_helper [s : add_comm_semigroup A] [s' : has_one A] (a t : A) (H : add1 a = t) :
|
||||||
|
add1 (bit1 a) = bit0 t :=
|
||||||
|
by rewrite -H; apply add1_bit1
|
||||||
|
|
||||||
|
theorem add1_one [s : has_add A] [s' : has_one A] : add1 (one : A) = bit0 one :=
|
||||||
|
rfl
|
||||||
|
|
||||||
|
theorem add1_zero [s : add_monoid A] [s' : has_one A] : add1 (zero : A) = one :=
|
||||||
|
begin
|
||||||
|
rewrite [↑add1, zero_add]
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem one_add_one [s : has_add A] [s' : has_one A] : (one : A) + one = bit0 one :=
|
||||||
|
rfl
|
||||||
|
|
||||||
|
theorem subst_into_sum [s : has_add A] (l r tl tr t : A) (prl : l = tl) (prr : r = tr)
|
||||||
|
(prt : tl + tr = t) : l + r = t :=
|
||||||
|
by rewrite [prl, prr, prt]
|
||||||
|
|
||||||
|
theorem neg_zero_helper [s : add_group A] (a : A) (H : a = 0) : - a = 0 :=
|
||||||
|
by rewrite [H, neg_zero]
|
||||||
|
|
||||||
|
end norm_num
|
||||||
|
|
||||||
namespace simplifier
|
namespace simplifier
|
||||||
|
|
||||||
namespace unit
|
namespace unit
|
||||||
|
|
|
||||||
|
|
@ -1,272 +0,0 @@
|
||||||
/-
|
|
||||||
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
|
|
||||||
Released under Apache 2.0 license as described in the file LICENSE.
|
|
||||||
Author: Robert Y. Lewis
|
|
||||||
-/
|
|
||||||
|
|
||||||
import algebra.ordered_field
|
|
||||||
open algebra
|
|
||||||
|
|
||||||
namespace norm_num
|
|
||||||
|
|
||||||
variable {A : Type}
|
|
||||||
|
|
||||||
definition add1 [s : has_add A] [s' : has_one A] (a : A) : A := add a one
|
|
||||||
|
|
||||||
theorem add_comm_four [s : add_comm_semigroup A] (a b : A) : a + a + (b + b) = (a + b) + (a + b) :=
|
|
||||||
by rewrite [-add.assoc at {1}, add.comm, {a + b}add.comm at {1}, *add.assoc]
|
|
||||||
|
|
||||||
theorem add_comm_middle [s : add_comm_semigroup A] (a b c : A) : a + b + c = a + c + b :=
|
|
||||||
by rewrite [add.assoc, add.comm b, -add.assoc]
|
|
||||||
|
|
||||||
theorem bit0_add_bit0 [s : add_comm_semigroup A] (a b : A) : bit0 a + bit0 b = bit0 (a + b) :=
|
|
||||||
!add_comm_four
|
|
||||||
|
|
||||||
theorem bit0_add_bit0_helper [s : add_comm_semigroup A] (a b t : A) (H : a + b = t) :
|
|
||||||
bit0 a + bit0 b = bit0 t :=
|
|
||||||
by rewrite -H; apply bit0_add_bit0
|
|
||||||
|
|
||||||
theorem bit1_add_bit0 [s : add_comm_semigroup A] [s' : has_one A] (a b : A) :
|
|
||||||
bit1 a + bit0 b = bit1 (a + b) :=
|
|
||||||
begin
|
|
||||||
rewrite [↑bit0, ↑bit1, add_comm_middle], congruence, apply add_comm_four
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem bit1_add_bit0_helper [s : add_comm_semigroup A] [s' : has_one A] (a b t : A)
|
|
||||||
(H : a + b = t) : bit1 a + bit0 b = bit1 t :=
|
|
||||||
by rewrite -H; apply bit1_add_bit0
|
|
||||||
|
|
||||||
theorem bit0_add_bit1 [s : add_comm_semigroup A] [s' : has_one A] (a b : A) :
|
|
||||||
bit0 a + bit1 b = bit1 (a + b) :=
|
|
||||||
by rewrite [{bit0 a + _}add.comm, {a + _}add.comm]; apply bit1_add_bit0
|
|
||||||
|
|
||||||
theorem bit0_add_bit1_helper [s : add_comm_semigroup A] [s' : has_one A] (a b t : A)
|
|
||||||
(H : a + b = t) : bit0 a + bit1 b = bit1 t :=
|
|
||||||
by rewrite -H; apply bit0_add_bit1
|
|
||||||
|
|
||||||
theorem bit1_add_bit1 [s : add_comm_semigroup A] [s' : has_one A] (a b : A) :
|
|
||||||
bit1 a + bit1 b = bit0 (add1 (a + b)) :=
|
|
||||||
begin
|
|
||||||
rewrite ↑[bit0, bit1, add1, add.assoc],
|
|
||||||
rewrite [*add.assoc, {_ + (b + 1)}add.comm, {_ + (b + 1 + _)}add.comm,
|
|
||||||
{_ + (b + 1 + _ + _)}add.comm, *add.assoc, {1 + a}add.comm, -{b + (a + 1)}add.assoc,
|
|
||||||
{b + a}add.comm, *add.assoc]
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem bit1_add_bit1_helper [s : add_comm_semigroup A] [s' : has_one A] (a b t s: A)
|
|
||||||
(H : (a + b) = t) (H2 : add1 t = s) : bit1 a + bit1 b = bit0 s :=
|
|
||||||
begin rewrite [-H2, -H], apply bit1_add_bit1 end
|
|
||||||
|
|
||||||
theorem bin_add_zero [s : add_monoid A] (a : A) : a + zero = a := !add_zero
|
|
||||||
|
|
||||||
theorem bin_zero_add [s : add_monoid A] (a : A) : zero + a = a := !zero_add
|
|
||||||
|
|
||||||
theorem one_add_bit0 [s : add_comm_semigroup A] [s' : has_one A] (a : A) : one + bit0 a = bit1 a :=
|
|
||||||
begin rewrite ↑[bit0, bit1], rewrite add.comm end
|
|
||||||
|
|
||||||
theorem bit0_add_one [s : has_add A] [s' : has_one A] (a : A) : bit0 a + one = bit1 a :=
|
|
||||||
rfl
|
|
||||||
|
|
||||||
theorem bit1_add_one [s : has_add A] [s' : has_one A] (a : A) : bit1 a + one = add1 (bit1 a) :=
|
|
||||||
rfl
|
|
||||||
|
|
||||||
theorem bit1_add_one_helper [s : has_add A] [s' : has_one A] (a t : A) (H : add1 (bit1 a) = t) :
|
|
||||||
bit1 a + one = t :=
|
|
||||||
by rewrite -H
|
|
||||||
|
|
||||||
theorem one_add_bit1 [s : add_comm_semigroup A] [s' : has_one A] (a : A) :
|
|
||||||
one + bit1 a = add1 (bit1 a) := !add.comm
|
|
||||||
|
|
||||||
theorem one_add_bit1_helper [s : add_comm_semigroup A] [s' : has_one A] (a t : A)
|
|
||||||
(H : add1 (bit1 a) = t) : one + bit1 a = t :=
|
|
||||||
by rewrite -H; apply one_add_bit1
|
|
||||||
|
|
||||||
theorem add1_bit0 [s : has_add A] [s' : has_one A] (a : A) : add1 (bit0 a) = bit1 a :=
|
|
||||||
rfl
|
|
||||||
|
|
||||||
theorem add1_bit1 [s : add_comm_semigroup A] [s' : has_one A] (a : A) :
|
|
||||||
add1 (bit1 a) = bit0 (add1 a) :=
|
|
||||||
begin
|
|
||||||
rewrite ↑[add1, bit1, bit0],
|
|
||||||
rewrite [add.assoc, add_comm_four]
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem add1_bit1_helper [s : add_comm_semigroup A] [s' : has_one A] (a t : A) (H : add1 a = t) :
|
|
||||||
add1 (bit1 a) = bit0 t :=
|
|
||||||
by rewrite -H; apply add1_bit1
|
|
||||||
|
|
||||||
theorem add1_one [s : has_add A] [s' : has_one A] : add1 (one : A) = bit0 one :=
|
|
||||||
rfl
|
|
||||||
|
|
||||||
theorem add1_zero [s : add_monoid A] [s' : has_one A] : add1 (zero : A) = one :=
|
|
||||||
begin
|
|
||||||
rewrite [↑add1, zero_add]
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem one_add_one [s : has_add A] [s' : has_one A] : (one : A) + one = bit0 one :=
|
|
||||||
rfl
|
|
||||||
|
|
||||||
theorem subst_into_sum [s : has_add A] (l r tl tr t : A) (prl : l = tl) (prr : r = tr)
|
|
||||||
(prt : tl + tr = t) : l + r = t :=
|
|
||||||
by rewrite [prl, prr, prt]
|
|
||||||
|
|
||||||
-- multiplication
|
|
||||||
|
|
||||||
theorem mul_zero [s : mul_zero_class A] (a : A) : a * zero = zero :=
|
|
||||||
by rewrite [↑zero, mul_zero]
|
|
||||||
|
|
||||||
theorem zero_mul [s : mul_zero_class A] (a : A) : zero * a = zero :=
|
|
||||||
by rewrite [↑zero, zero_mul]
|
|
||||||
|
|
||||||
theorem mul_one [s : monoid A] (a : A) : a * one = a :=
|
|
||||||
by rewrite [↑one, mul_one]
|
|
||||||
|
|
||||||
theorem mul_bit0 [s : distrib A] (a b : A) : a * (bit0 b) = bit0 (a * b) :=
|
|
||||||
by rewrite [↑bit0, left_distrib]
|
|
||||||
|
|
||||||
theorem mul_bit0_helper [s : distrib A] (a b t : A) (H : a * b = t) : a * (bit0 b) = bit0 t :=
|
|
||||||
by rewrite -H; apply mul_bit0
|
|
||||||
|
|
||||||
theorem mul_bit1 [s : semiring A] (a b : A) : a * (bit1 b) = bit0 (a * b) + a :=
|
|
||||||
by rewrite [↑bit1, ↑bit0, +left_distrib, ↑one, mul_one]
|
|
||||||
|
|
||||||
theorem mul_bit1_helper [s : semiring A] (a b s t : A) (Hs : a * b = s) (Ht : bit0 s + a = t) :
|
|
||||||
a * (bit1 b) = t :=
|
|
||||||
begin rewrite [-Ht, -Hs, mul_bit1] end
|
|
||||||
|
|
||||||
theorem subst_into_prod [s : has_mul A] (l r tl tr t : A) (prl : l = tl) (prr : r = tr)
|
|
||||||
(prt : tl * tr = t) :
|
|
||||||
l * r = t :=
|
|
||||||
by rewrite [prl, prr, prt]
|
|
||||||
|
|
||||||
theorem mk_cong (op : A → A) (a b : A) (H : a = b) : op a = op b :=
|
|
||||||
by congruence; exact H
|
|
||||||
|
|
||||||
theorem mk_eq (a : A) : a = a := rfl
|
|
||||||
|
|
||||||
theorem neg_add_neg_eq_of_add_add_eq_zero [s : add_comm_group A] (a b c : A) (H : c + a + b = 0) :
|
|
||||||
-a + -b = c :=
|
|
||||||
begin
|
|
||||||
apply add_neg_eq_of_eq_add,
|
|
||||||
apply neg_eq_of_add_eq_zero,
|
|
||||||
rewrite [add.comm, add.assoc, add.comm b, -add.assoc, H]
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem neg_add_neg_helper [s : add_comm_group A] (a b c : A) (H : a + b = c) : -a + -b = -c :=
|
|
||||||
begin apply iff.mp !neg_eq_neg_iff_eq, rewrite [neg_add, *neg_neg, H] end
|
|
||||||
|
|
||||||
theorem neg_add_pos_eq_of_eq_add [s : add_comm_group A] (a b c : A) (H : b = c + a) : -a + b = c :=
|
|
||||||
begin apply neg_add_eq_of_eq_add, rewrite add.comm, exact H end
|
|
||||||
|
|
||||||
theorem neg_add_pos_helper1 [s : add_comm_group A] (a b c : A) (H : b + c = a) : -a + b = -c :=
|
|
||||||
begin apply neg_add_eq_of_eq_add, apply eq_add_neg_of_add_eq H end
|
|
||||||
|
|
||||||
theorem neg_add_pos_helper2 [s : add_comm_group A] (a b c : A) (H : a + c = b) : -a + b = c :=
|
|
||||||
begin apply neg_add_eq_of_eq_add, rewrite H end
|
|
||||||
|
|
||||||
theorem pos_add_neg_helper [s : add_comm_group A] (a b c : A) (H : b + a = c) : a + b = c :=
|
|
||||||
by rewrite [add.comm, H]
|
|
||||||
|
|
||||||
theorem sub_eq_add_neg_helper [s : add_comm_group A] (t₁ t₂ e w₁ w₂: A) (H₁ : t₁ = w₁)
|
|
||||||
(H₂ : t₂ = w₂) (H : w₁ + -w₂ = e) : t₁ - t₂ = e :=
|
|
||||||
by rewrite [sub_eq_add_neg, H₁, H₂, H]
|
|
||||||
|
|
||||||
theorem pos_add_pos_helper [s : add_comm_group A] (a b c h₁ h₂ : A) (H₁ : a = h₁) (H₂ : b = h₂)
|
|
||||||
(H : h₁ + h₂ = c) : a + b = c :=
|
|
||||||
by rewrite [H₁, H₂, H]
|
|
||||||
|
|
||||||
theorem subst_into_subtr [s : add_group A] (l r t : A) (prt : l + -r = t) : l - r = t :=
|
|
||||||
by rewrite [sub_eq_add_neg, prt]
|
|
||||||
|
|
||||||
theorem neg_neg_helper [s : add_group A] (a b : A) (H : a = -b) : -a = b :=
|
|
||||||
by rewrite [H, neg_neg]
|
|
||||||
|
|
||||||
theorem neg_mul_neg_helper [s : ring A] (a b c : A) (H : a * b = c) : (-a) * (-b) = c :=
|
|
||||||
begin rewrite [neg_mul_neg, H] end
|
|
||||||
|
|
||||||
theorem neg_mul_pos_helper [s : ring A] (a b c : A) (H : a * b = c) : (-a) * b = -c :=
|
|
||||||
begin rewrite [-neg_mul_eq_neg_mul, H] end
|
|
||||||
|
|
||||||
theorem pos_mul_neg_helper [s : ring A] (a b c : A) (H : a * b = c) : a * (-b) = -c :=
|
|
||||||
begin rewrite [-neg_mul_comm, -neg_mul_eq_neg_mul, H] end
|
|
||||||
|
|
||||||
theorem pos_bit0_helper [s : linear_ordered_semiring A] (a : A) (H : a > 0) : bit0 a > 0 :=
|
|
||||||
by rewrite ↑bit0; apply add_pos H H
|
|
||||||
|
|
||||||
theorem nonneg_bit0_helper [s : linear_ordered_semiring A] (a : A) (H : a ≥ 0) : bit0 a ≥ 0 :=
|
|
||||||
by rewrite ↑bit0; apply add_nonneg H H
|
|
||||||
|
|
||||||
theorem pos_bit1_helper [s : linear_ordered_semiring A] (a : A) (H : a ≥ 0) : bit1 a > 0 :=
|
|
||||||
begin
|
|
||||||
rewrite ↑bit1,
|
|
||||||
apply add_pos_of_nonneg_of_pos,
|
|
||||||
apply nonneg_bit0_helper _ H,
|
|
||||||
apply zero_lt_one
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem nonneg_bit1_helper [s : linear_ordered_semiring A] (a : A) (H : a ≥ 0) : bit1 a ≥ 0 :=
|
|
||||||
by apply le_of_lt; apply pos_bit1_helper _ H
|
|
||||||
|
|
||||||
theorem div_add_helper [s : field A] (n d b c val : A) (Hd : d ≠ 0) (H : n + b * d = val)
|
|
||||||
(H2 : c * d = val) : n / d + b = c :=
|
|
||||||
begin
|
|
||||||
apply eq_of_mul_eq_mul_of_nonzero_right Hd,
|
|
||||||
rewrite [H2, -H, right_distrib, div_mul_cancel _ Hd]
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem add_div_helper [s : field A] (n d b c val : A) (Hd : d ≠ 0) (H : d * b + n = val)
|
|
||||||
(H2 : d * c = val) : b + n / d = c :=
|
|
||||||
begin
|
|
||||||
apply eq_of_mul_eq_mul_of_nonzero_left Hd,
|
|
||||||
rewrite [H2, -H, left_distrib, mul_div_cancel' Hd]
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem div_mul_helper [s : field A] (n d c v : A) (Hd : d ≠ 0) (H : (n * c) / d = v) :
|
|
||||||
(n / d) * c = v :=
|
|
||||||
by rewrite [-H, field.div_mul_eq_mul_div_comm _ _ Hd, mul_div_assoc]
|
|
||||||
|
|
||||||
theorem mul_div_helper [s : field A] (a n d v : A) (Hd : d ≠ 0) (H : (a * n) / d = v) :
|
|
||||||
a * (n / d) = v :=
|
|
||||||
by rewrite [-H, mul_div_assoc]
|
|
||||||
|
|
||||||
theorem nonzero_of_pos_helper [s : linear_ordered_semiring A] (a : A) (H : a > 0) : a ≠ 0 :=
|
|
||||||
ne_of_gt H
|
|
||||||
|
|
||||||
theorem nonzero_of_neg_helper [s : linear_ordered_ring A] (a : A) (H : a ≠ 0) : -a ≠ 0 :=
|
|
||||||
begin intro Ha, apply H, apply eq_of_neg_eq_neg, rewrite neg_zero, exact Ha end
|
|
||||||
|
|
||||||
theorem nonzero_of_div_helper [s : field A] (a b : A) (Ha : a ≠ 0) (Hb : b ≠ 0) : a / b ≠ 0 :=
|
|
||||||
begin
|
|
||||||
intro Hab,
|
|
||||||
have Habb : (a / b) * b = 0, by rewrite [Hab, zero_mul],
|
|
||||||
rewrite [div_mul_cancel _ Hb at Habb],
|
|
||||||
exact Ha Habb
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem div_helper [s : field A] (n d v : A) (Hd : d ≠ 0) (H : v * d = n) : n / d = v :=
|
|
||||||
begin
|
|
||||||
apply eq_of_mul_eq_mul_of_nonzero_right Hd,
|
|
||||||
rewrite (div_mul_cancel _ Hd),
|
|
||||||
exact eq.symm H
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem div_eq_div_helper [s : field A] (a b c d v : A) (H1 : a * d = v) (H2 : c * b = v)
|
|
||||||
(Hb : b ≠ 0) (Hd : d ≠ 0) : a / b = c / d :=
|
|
||||||
begin
|
|
||||||
apply eq_div_of_mul_eq,
|
|
||||||
exact Hd,
|
|
||||||
rewrite div_mul_eq_mul_div,
|
|
||||||
apply eq.symm,
|
|
||||||
apply eq_div_of_mul_eq,
|
|
||||||
exact Hb,
|
|
||||||
rewrite [H1, H2]
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem subst_into_div [s : has_div A] (a₁ b₁ a₂ b₂ v : A) (H : a₁ / b₁ = v) (H1 : a₂ = a₁)
|
|
||||||
(H2 : b₂ = b₁) : a₂ / b₂ = v :=
|
|
||||||
by rewrite [H1, H2, H]
|
|
||||||
|
|
||||||
theorem neg_zero_helper [s : add_group A] (a : A) (H : a = 0) : - a = 0 :=
|
|
||||||
by rewrite [H, neg_zero]
|
|
||||||
|
|
||||||
end norm_num
|
|
||||||
|
|
@ -715,3 +715,32 @@ end
|
||||||
/- TODO: Multiplication and one, starting with mult_right_le_one_le. -/
|
/- TODO: Multiplication and one, starting with mult_right_le_one_le. -/
|
||||||
|
|
||||||
end algebra
|
end algebra
|
||||||
|
|
||||||
|
namespace norm_num
|
||||||
|
open algebra
|
||||||
|
variable {A : Type}
|
||||||
|
|
||||||
|
theorem pos_bit0_helper [s : linear_ordered_semiring A] (a : A) (H : a > 0) : bit0 a > 0 :=
|
||||||
|
by rewrite ↑bit0; apply add_pos H H
|
||||||
|
|
||||||
|
theorem nonneg_bit0_helper [s : linear_ordered_semiring A] (a : A) (H : a ≥ 0) : bit0 a ≥ 0 :=
|
||||||
|
by rewrite ↑bit0; apply add_nonneg H H
|
||||||
|
|
||||||
|
theorem pos_bit1_helper [s : linear_ordered_semiring A] (a : A) (H : a ≥ 0) : bit1 a > 0 :=
|
||||||
|
begin
|
||||||
|
rewrite ↑bit1,
|
||||||
|
apply add_pos_of_nonneg_of_pos,
|
||||||
|
apply nonneg_bit0_helper _ H,
|
||||||
|
apply zero_lt_one
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem nonneg_bit1_helper [s : linear_ordered_semiring A] (a : A) (H : a ≥ 0) : bit1 a ≥ 0 :=
|
||||||
|
by apply le_of_lt; apply pos_bit1_helper _ H
|
||||||
|
|
||||||
|
theorem nonzero_of_pos_helper [s : linear_ordered_semiring A] (a : A) (H : a > 0) : a ≠ 0 :=
|
||||||
|
ne_of_gt H
|
||||||
|
|
||||||
|
theorem nonzero_of_neg_helper [s : linear_ordered_ring A] (a : A) (H : a ≠ 0) : -a ≠ 0 :=
|
||||||
|
begin intro Ha, apply H, apply eq_of_neg_eq_neg, rewrite neg_zero, exact Ha end
|
||||||
|
|
||||||
|
end norm_num
|
||||||
|
|
|
||||||
|
|
@ -406,6 +406,90 @@ end
|
||||||
|
|
||||||
end algebra
|
end algebra
|
||||||
|
|
||||||
|
namespace norm_num
|
||||||
|
open algebra
|
||||||
|
variables {A : Type}
|
||||||
|
|
||||||
|
theorem mul_zero [s : mul_zero_class A] (a : A) : a * zero = zero :=
|
||||||
|
by rewrite [↑zero, mul_zero]
|
||||||
|
|
||||||
|
theorem zero_mul [s : mul_zero_class A] (a : A) : zero * a = zero :=
|
||||||
|
by rewrite [↑zero, zero_mul]
|
||||||
|
|
||||||
|
theorem mul_one [s : monoid A] (a : A) : a * one = a :=
|
||||||
|
by rewrite [↑one, mul_one]
|
||||||
|
|
||||||
|
theorem mul_bit0 [s : distrib A] (a b : A) : a * (bit0 b) = bit0 (a * b) :=
|
||||||
|
by rewrite [↑bit0, left_distrib]
|
||||||
|
|
||||||
|
theorem mul_bit0_helper [s : distrib A] (a b t : A) (H : a * b = t) : a * (bit0 b) = bit0 t :=
|
||||||
|
by rewrite -H; apply mul_bit0
|
||||||
|
|
||||||
|
theorem mul_bit1 [s : semiring A] (a b : A) : a * (bit1 b) = bit0 (a * b) + a :=
|
||||||
|
by rewrite [↑bit1, ↑bit0, +left_distrib, ↑one, mul_one]
|
||||||
|
|
||||||
|
theorem mul_bit1_helper [s : semiring A] (a b s t : A) (Hs : a * b = s) (Ht : bit0 s + a = t) :
|
||||||
|
a * (bit1 b) = t :=
|
||||||
|
begin rewrite [-Ht, -Hs, mul_bit1] end
|
||||||
|
|
||||||
|
theorem subst_into_prod [s : has_mul A] (l r tl tr t : A) (prl : l = tl) (prr : r = tr)
|
||||||
|
(prt : tl * tr = t) :
|
||||||
|
l * r = t :=
|
||||||
|
by rewrite [prl, prr, prt]
|
||||||
|
|
||||||
|
theorem mk_cong (op : A → A) (a b : A) (H : a = b) : op a = op b :=
|
||||||
|
by congruence; exact H
|
||||||
|
|
||||||
|
theorem mk_eq (a : A) : a = a := rfl
|
||||||
|
|
||||||
|
theorem neg_add_neg_eq_of_add_add_eq_zero [s : add_comm_group A] (a b c : A) (H : c + a + b = 0) :
|
||||||
|
-a + -b = c :=
|
||||||
|
begin
|
||||||
|
apply add_neg_eq_of_eq_add,
|
||||||
|
apply neg_eq_of_add_eq_zero,
|
||||||
|
rewrite [add.comm, add.assoc, add.comm b, -add.assoc, H]
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem neg_add_neg_helper [s : add_comm_group A] (a b c : A) (H : a + b = c) : -a + -b = -c :=
|
||||||
|
begin apply iff.mp !neg_eq_neg_iff_eq, rewrite [neg_add, *neg_neg, H] end
|
||||||
|
|
||||||
|
theorem neg_add_pos_eq_of_eq_add [s : add_comm_group A] (a b c : A) (H : b = c + a) : -a + b = c :=
|
||||||
|
begin apply neg_add_eq_of_eq_add, rewrite add.comm, exact H end
|
||||||
|
|
||||||
|
theorem neg_add_pos_helper1 [s : add_comm_group A] (a b c : A) (H : b + c = a) : -a + b = -c :=
|
||||||
|
begin apply neg_add_eq_of_eq_add, apply eq_add_neg_of_add_eq H end
|
||||||
|
|
||||||
|
theorem neg_add_pos_helper2 [s : add_comm_group A] (a b c : A) (H : a + c = b) : -a + b = c :=
|
||||||
|
begin apply neg_add_eq_of_eq_add, rewrite H end
|
||||||
|
|
||||||
|
theorem pos_add_neg_helper [s : add_comm_group A] (a b c : A) (H : b + a = c) : a + b = c :=
|
||||||
|
by rewrite [add.comm, H]
|
||||||
|
|
||||||
|
theorem sub_eq_add_neg_helper [s : add_comm_group A] (t₁ t₂ e w₁ w₂: A) (H₁ : t₁ = w₁)
|
||||||
|
(H₂ : t₂ = w₂) (H : w₁ + -w₂ = e) : t₁ - t₂ = e :=
|
||||||
|
by rewrite [sub_eq_add_neg, H₁, H₂, H]
|
||||||
|
|
||||||
|
theorem pos_add_pos_helper [s : add_comm_group A] (a b c h₁ h₂ : A) (H₁ : a = h₁) (H₂ : b = h₂)
|
||||||
|
(H : h₁ + h₂ = c) : a + b = c :=
|
||||||
|
by rewrite [H₁, H₂, H]
|
||||||
|
|
||||||
|
theorem subst_into_subtr [s : add_group A] (l r t : A) (prt : l + -r = t) : l - r = t :=
|
||||||
|
by rewrite [sub_eq_add_neg, prt]
|
||||||
|
|
||||||
|
theorem neg_neg_helper [s : add_group A] (a b : A) (H : a = -b) : -a = b :=
|
||||||
|
by rewrite [H, neg_neg]
|
||||||
|
|
||||||
|
theorem neg_mul_neg_helper [s : ring A] (a b c : A) (H : a * b = c) : (-a) * (-b) = c :=
|
||||||
|
begin rewrite [neg_mul_neg, H] end
|
||||||
|
|
||||||
|
theorem neg_mul_pos_helper [s : ring A] (a b c : A) (H : a * b = c) : (-a) * b = -c :=
|
||||||
|
begin rewrite [-neg_mul_eq_neg_mul, H] end
|
||||||
|
|
||||||
|
theorem pos_mul_neg_helper [s : ring A] (a b c : A) (H : a * b = c) : a * (-b) = -c :=
|
||||||
|
begin rewrite [-neg_mul_comm, -neg_mul_eq_neg_mul, H] end
|
||||||
|
|
||||||
|
end norm_num
|
||||||
|
|
||||||
namespace simplifier
|
namespace simplifier
|
||||||
|
|
||||||
namespace unit
|
namespace unit
|
||||||
|
|
|
||||||
|
|
@ -1,7 +1,6 @@
|
||||||
import algebra.numeral data.real
|
import data.real
|
||||||
open algebra real
|
open algebra real
|
||||||
|
|
||||||
|
|
||||||
/-
|
/-
|
||||||
variable {A : Type}
|
variable {A : Type}
|
||||||
variable [s : linear_ordered_field A]
|
variable [s : linear_ordered_field A]
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
-- Basic fusion
|
-- Basic fusion
|
||||||
import algebra.ring algebra.numeral
|
import algebra.ring
|
||||||
open algebra
|
open algebra
|
||||||
|
|
||||||
universe l
|
universe l
|
||||||
|
|
|
||||||
|
|
@ -1,4 +1,4 @@
|
||||||
import algebra.ring algebra.numeral
|
import algebra.ring
|
||||||
open algebra
|
open algebra
|
||||||
universe l
|
universe l
|
||||||
constants (A : Type.{l}) (s : comm_ring A) (x : A)
|
constants (A : Type.{l}) (s : comm_ring A) (x : A)
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
-- Basic fusion
|
-- Basic fusion
|
||||||
import algebra.ring algebra.numeral
|
import algebra.ring
|
||||||
open algebra
|
open algebra
|
||||||
|
|
||||||
universe l
|
universe l
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
-- Nested fusion
|
-- Nested fusion
|
||||||
import algebra.ring algebra.numeral
|
import algebra.ring
|
||||||
open algebra
|
open algebra
|
||||||
|
|
||||||
universe l
|
universe l
|
||||||
|
|
|
||||||
|
|
@ -1,4 +1,4 @@
|
||||||
import algebra.ring algebra.numeral
|
import algebra.ring
|
||||||
open algebra
|
open algebra
|
||||||
|
|
||||||
set_option simplify.max_steps 5000000
|
set_option simplify.max_steps 5000000
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue