From 37209d45a5d3fb3973bb342591f2e5b49be07916 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 17 Dec 2016 20:20:55 -0800
Subject: [PATCH] feat(library/init/algebra/norm_num): add missing norm_num
 lemmas

---
 library/init/algebra/norm_num.lean     | 25 ++++++++++++++++++-
 library/init/algebra/ordered_ring.lean | 33 ++++++++++++++++++++++++++
 2 files changed, 57 insertions(+), 1 deletion(-)

diff --git a/library/init/algebra/norm_num.lean b/library/init/algebra/norm_num.lean
index daed6dfc34..74ead18775 100644
--- a/library/init/algebra/norm_num.lean
+++ b/library/init/algebra/norm_num.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis and Leonardo de Moura
 -/
 prelude
-import init.algebra.field
+import init.algebra.field init.algebra.ordered_ring
 
 namespace norm_num
 universe variable u
@@ -238,4 +238,27 @@ by rw [-prt, prr, prl]
 lemma neg_zero_helper [add_group α] (a : α) (h : a = 0) : - a = 0 :=
 begin rw h, simp end
 
+lemma pos_bit0_helper [linear_ordered_semiring α] (a : α) (h : a > 0) : bit0 a > 0 :=
+begin u, apply add_pos h h end
+
+lemma nonneg_bit0_helper [linear_ordered_semiring α] (a : α) (h : a ≥ 0) : bit0 a ≥ 0 :=
+begin u, apply add_nonneg h h end
+
+lemma pos_bit1_helper [linear_ordered_semiring α] (a : α) (h : a ≥ 0) : bit1 a > 0 :=
+begin
+  u,
+  apply add_pos_of_nonneg_of_pos,
+  apply nonneg_bit0_helper _ h,
+  apply zero_lt_one
+end
+
+lemma nonneg_bit1_helper [linear_ordered_semiring α] (a : α) (h : a ≥ 0) : bit1 a ≥ 0 :=
+begin apply le_of_lt,  apply pos_bit1_helper _ h end
+
+lemma nonzero_of_pos_helper [linear_ordered_semiring α] (a : α) (h : a > 0) : a ≠ 0 :=
+  ne_of_gt h
+
+lemma nonzero_of_neg_helper [linear_ordered_ring α] (a : α) (h : a ≠ 0) : -a ≠ 0 :=
+begin intro ha, apply h, apply neg_inj, rwa neg_zero end
+
 end norm_num
diff --git a/library/init/algebra/ordered_ring.lean b/library/init/algebra/ordered_ring.lean
index 615bd95fb3..4061376e8a 100644
--- a/library/init/algebra/ordered_ring.lean
+++ b/library/init/algebra/ordered_ring.lean
@@ -395,3 +395,36 @@ end
 instance linear_ordered_comm_ring.to_integral_domain [s: linear_ordered_comm_ring α] : integral_domain α :=
 {s with
  eq_zero_or_eq_zero_of_mul_eq_zero := @linear_ordered_comm_ring.eq_zero_or_eq_zero_of_mul_eq_zero α s }
+
+structure decidable_linear_ordered_comm_ring (α : Type u) extends linear_ordered_comm_ring α,
+    decidable_linear_ordered_mul_comm_group α renaming
+  mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero inv→neg
+  mul_left_inv→add_left_inv mul_comm→add_comm mul_le_mul_left→add_le_add_left
+  mul_lt_mul_left→add_lt_add_left
+
+/- we make it a class now (and not as part of the structure) to avoid
+   decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_comm_group to be an instance -/
+attribute [class] decidable_linear_ordered_comm_ring
+
+instance linear_ordered_comm_ring_of_decidable_linear_ordered_comm_ring
+         (α : Type u) [s : decidable_linear_ordered_comm_ring α] : linear_ordered_comm_ring α :=
+@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring α s
+
+instance decidable_linear_ordered_ab_group_of_decidable_linear_ordered_comm_ring
+         (α : Type u) [s : decidable_linear_ordered_comm_ring α] : decidable_linear_ordered_comm_group α :=
+@decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_mul_comm_group α s
+
+instance decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_semiring [d : decidable_linear_ordered_comm_ring α] :
+   decidable_linear_ordered_semiring α :=
+let s : linear_ordered_semiring α := @linear_ordered_ring.to_linear_ordered_semiring α _ in
+{d with
+ zero_mul                   := @linear_ordered_semiring.zero_mul α s,
+ mul_zero                   := @linear_ordered_semiring.mul_zero α s,
+ add_left_cancel            := @linear_ordered_semiring.add_left_cancel α s,
+ add_right_cancel           := @linear_ordered_semiring.add_right_cancel α s,
+ le_of_add_le_add_left      := @linear_ordered_semiring.le_of_add_le_add_left α s,
+ lt_of_add_lt_add_left      := @linear_ordered_semiring.lt_of_add_lt_add_left α s,
+ mul_le_mul_of_nonneg_left  := @linear_ordered_semiring.mul_le_mul_of_nonneg_left α s,
+ mul_le_mul_of_nonneg_right := @linear_ordered_semiring.mul_le_mul_of_nonneg_right α s,
+ mul_lt_mul_of_pos_left     := @linear_ordered_semiring.mul_lt_mul_of_pos_left α s,
+ mul_lt_mul_of_pos_right    := @linear_ordered_semiring.mul_lt_mul_of_pos_right α s}