feat(algebra/group,...): add with_zero, with_one structures

other ways to add an element to an algebraic structure:
* Add a top or bottom to an order (with_top, with_bot)
* add a unit to a semigroup (with_zero, with_one)
* add a zero to a multiplicative semigroup (with_zero)
* add an infinite element to an additive semigroup (with_top)

algebra/group.lean

@@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura
 
 Various multiplicative and additive structures.
 -/
-import tactic.interactive
+import tactic.interactive data.option
 
 section pending_1857
 
@@ -68,6 +68,9 @@ attribute [to_additive add_monoid] monoid
 attribute [to_additive add_monoid.mk] monoid.mk
 attribute [to_additive add_monoid.to_has_zero] monoid.to_has_one
 attribute [to_additive add_monoid.to_add_semigroup] monoid.to_semigroup
+attribute [to_additive add_monoid.add] monoid.mul
+attribute [to_additive add_monoid.add_assoc] monoid.mul_assoc
+attribute [to_additive add_monoid.zero] monoid.one
 attribute [to_additive add_monoid.zero_add] monoid.one_mul
 attribute [to_additive add_monoid.add_zero] monoid.mul_one
 
@@ -147,6 +150,14 @@ instance [add_semigroup α] : semigroup (multiplicative α) :=
 { mul := ((+) : α → α → α),
   mul_assoc := @add_assoc _ _ }
 
+instance [comm_semigroup α] : add_comm_semigroup (additive α) :=
+{ add_comm := @mul_comm _ _,
+  ..additive.add_semigroup }
+
+instance [add_comm_semigroup α] : comm_semigroup (multiplicative α) :=
+{ mul_comm := @add_comm _ _,
+  ..multiplicative.semigroup }
+
 instance [left_cancel_semigroup α] : add_left_cancel_semigroup (additive α) :=
 { add_left_cancel := @mul_left_cancel _ _,
   ..additive.add_semigroup }
@@ -231,14 +242,66 @@ namespace units
 
 end units
 
+@[to_additive with_zero]
+def with_one (α) := option α
+
+@[to_additive with_zero.has_coe_t]
+instance : has_coe_t α (with_one α) := ⟨some⟩
+
+instance [semigroup α] : monoid (with_one α) :=
+{ one       := none,
+  mul       := option.lift_or_get (*),
+  mul_assoc := (option.lift_or_get_assoc _).1,
+  one_mul   := (option.lift_or_get_is_left_id _).1,
+  mul_one   := (option.lift_or_get_is_right_id _).1 }
+
+attribute [to_additive with_zero.add_monoid._proof_1] with_one.monoid._proof_1
+attribute [to_additive with_zero.add_monoid._proof_2] with_one.monoid._proof_2
+attribute [to_additive with_zero.add_monoid._proof_3] with_one.monoid._proof_3
+attribute [to_additive with_zero.add_monoid] with_one.monoid
+
+instance [semigroup α] : mul_zero_class (with_zero α) :=
+{ zero      := none,
+  mul       := λ o₁ o₂, o₁.bind (λ a, o₂.map (λ b, a * b)),
+  zero_mul  := by simp,
+  mul_zero  := λ a, by cases a; simp,
+  ..with_zero.add_monoid }
+
+instance [semigroup α] : semigroup (with_zero α) :=
+{ mul_assoc := λ a b c, begin
+    cases a with a, {refl},
+    cases b with b, {refl},
+    cases c with c, {refl},
+    simp [mul_assoc]
+  end,
+  ..with_zero.mul_zero_class }
+
+instance [comm_semigroup α] : comm_semigroup (with_zero α) :=
+{ mul_comm := λ a b, begin
+    cases a with a; cases b with b; try {refl},
+    exact congr_arg some (mul_comm _ _)
+  end,
+  ..with_zero.semigroup }
+
+instance [monoid α] : monoid (with_zero α) :=
+{ one := some 1,
+  one_mul := λ a, by cases a;
+    [refl, exact congr_arg some (one_mul a)],
+  mul_one := λ a, by cases a;
+    [refl, exact congr_arg some (mul_one a)],
+  ..with_zero.semigroup }
+
+instance [comm_monoid α] : comm_monoid (with_zero α) :=
+{ ..with_zero.monoid, ..with_zero.comm_semigroup }
+
 instance [monoid α] : add_monoid (additive α) :=
-{ zero := (1 : α),
+{ zero     := (1 : α),
   zero_add := @one_mul _ _,
   add_zero := @mul_one _ _,
   ..additive.add_semigroup }
 
 instance [add_monoid α] : monoid (multiplicative α) :=
-{ one := (0 : α),
+{ one     := (0 : α),
   one_mul := @zero_add _ _,
   mul_one := @add_zero _ _,
   ..multiplicative.semigroup }
@@ -277,6 +340,15 @@ section monoid
 
 end monoid
 
+instance [comm_semigroup α] : comm_monoid (with_one α) :=
+{ mul_comm := (option.lift_or_get_comm _).1,
+  ..with_one.monoid }
+
+instance [add_comm_semigroup α] : add_comm_monoid (with_zero α) :=
+{ add_comm := (option.lift_or_get_comm _).1,
+  ..with_zero.add_monoid }
+attribute [to_additive with_zero.add_comm_monoid] with_one.comm_monoid
+
 instance [comm_monoid α] : add_comm_monoid (additive α) :=
 { add_comm := @mul_comm α _,
   ..additive.add_monoid }

algebra/ordered_group.lean

@@ -5,7 +5,7 @@ Authors: Mario Carneiro, Johannes Hölzl
 
 Ordered monoids and groups.
 -/
-import algebra.group tactic
+import algebra.group order.bounded_lattice tactic.basic
 
 universe u
 variable {α : Type u}
@@ -130,8 +130,93 @@ iff.intro
    and.intro ‹a = 0› ‹b = 0›)
   (assume ⟨ha', hb'⟩, by rw [ha', hb', add_zero])
 
+lemma bit0_pos {a : α} (h : 0 < a) : 0 < bit0 a :=
+add_pos' h h
+
 end ordered_comm_monoid
 
+namespace with_zero
+open lattice
+
+instance [partial_order α] : partial_order (with_zero α) := with_bot.partial_order
+instance [partial_order α] : order_bot (with_zero α) := with_bot.order_bot
+instance [lattice α] : lattice (with_zero α) := with_bot.lattice
+instance [linear_order α] : linear_order (with_zero α) := with_bot.linear_order
+instance [decidable_linear_order α] :
+ decidable_linear_order (with_zero α) := with_bot.decidable_linear_order
+
+def ordered_comm_monoid [ordered_comm_monoid α]
+  (zero_le : ∀ a : α, 0 ≤ a) : ordered_comm_monoid (with_zero α) :=
+begin
+  suffices, refine {
+    add_le_add_left := this,
+    ..with_zero.partial_order,
+    ..with_zero.add_comm_monoid, ..},
+  { intros a b c h,
+    refine ⟨λ b h₂, _, λ h₂, h.2 $ this _ _ h₂ _⟩,
+    cases h₂, cases c with c,
+    { cases h.2 (this _ _ bot_le a) },
+    { refine ⟨_, rfl, _⟩,
+      cases a with a,
+      { exact with_bot.some_le_some.1 h.1 },
+      { exact le_of_lt (lt_of_add_lt_add_left' $
+          with_bot.some_lt_some.1 h), } } },
+  { intros a b h c ca h₂,
+    cases b with b,
+    { rw le_antisymm h bot_le at h₂,
+      exact ⟨_, h₂, le_refl _⟩ },
+    cases a with a,
+    { change c + 0 = some ca at h₂,
+      simp at h₂, simp [h₂],
+      exact ⟨_, rfl, by simpa using add_le_add_left' (zero_le b)⟩ },
+    { simp at h,
+      cases c with c; change some _ = _ at h₂;
+        simp [-add_comm] at h₂; subst ca; refine ⟨_, rfl, _⟩,
+      { exact h },
+      { exact add_le_add_left' h } } }
+end
+
+end with_zero
+
+namespace with_top
+open lattice
+
+instance [add_semigroup α] : add_semigroup (with_top α) :=
+@additive.add_semigroup _ $ @with_zero.semigroup (multiplicative α) _
+
+instance [add_comm_semigroup α] : add_comm_semigroup (with_top α) :=
+@additive.add_comm_semigroup _ $ @with_zero.comm_semigroup (multiplicative α) _
+
+instance [add_monoid α] : add_monoid (with_top α) :=
+@additive.add_monoid _ $ @with_zero.monoid (multiplicative α) _
+
+instance [add_comm_monoid α] : add_comm_monoid (with_top α) :=
+@additive.add_comm_monoid _ $ @with_zero.comm_monoid (multiplicative α) _
+
+instance [ordered_comm_monoid α] : ordered_comm_monoid (with_top α) :=
+begin
+  suffices, refine {
+    add_le_add_left := this,
+    ..with_top.partial_order,
+    ..with_top.add_comm_monoid, ..},
+  { intros a b c h,
+    refine ⟨λ c h₂, _, λ h₂, h.2 $ this _ _ h₂ _⟩,
+    cases h₂, cases a with a,
+    { exact (not_le_of_lt h).elim le_top },
+    cases b with b,
+    { exact (not_le_of_lt h).elim le_top },
+    { exact ⟨_, rfl, le_of_lt (lt_of_add_lt_add_left' $
+        with_top.some_lt_some.1 h)⟩ } },
+  { intros a b h c ca h₂,
+    cases c with c, {cases h₂},
+    cases b with b; cases h₂,
+    cases a with a, {cases le_antisymm h le_top},
+    simp at h,
+    exact ⟨_, rfl, add_le_add_left' h⟩, }
+end
+
+end with_top
+
 section canonically_ordered_monoid
 variables [canonically_ordered_monoid α] {a b c d : α}
 
@@ -148,6 +233,24 @@ iff.intro
   (assume h, le_antisymm h (zero_le a))
   (assume h, h ▸ le_refl a)
 
+instance with_zero.canonically_ordered_monoid :
+  canonically_ordered_monoid (with_zero α) :=
+{ le_iff_exists_add := λ a b, begin
+    cases a with a,
+    { exact iff_of_true lattice.bot_le ⟨b, (zero_add b).symm⟩ },
+    cases b with b,
+    { exact iff_of_false
+        (mt (le_antisymm lattice.bot_le) (by simp))
+        (λ ⟨c, h⟩, by cases c; cases h) },
+    { simp [le_iff_exists_add, -add_comm],
+      split; intro h; rcases h with ⟨c, h⟩,
+      { exact ⟨some c, congr_arg some h⟩ },
+      { cases c; cases h,
+        { exact ⟨_, (add_zero _).symm⟩ },
+        { exact ⟨_, rfl⟩ } } }
+  end,
+  ..with_zero.ordered_comm_monoid zero_le }
+
 end canonically_ordered_monoid
 
 instance ordered_cancel_comm_monoid.to_ordered_comm_monoid
@@ -190,9 +293,6 @@ by split; apply le_antisymm; try {assumption};
    rw ← hab; simp [ha, hb],
 λ ⟨ha', hb'⟩, by rw [ha', hb', add_zero]⟩
 
-lemma bit0_pos {a : α} (h : 0 < a) : 0 < bit0 a :=
-add_pos h h
-
 end ordered_cancel_comm_monoid
 
 section ordered_comm_group

algebra/ring.lean

@@ -18,6 +18,22 @@ section
   (two_mul _).symm
 end
 
+instance [semiring α] : semiring (with_zero α) :=
+{ left_distrib := λ a b c, begin
+    cases a with a, {refl},
+    cases b with b; cases c with c; try {refl},
+    exact congr_arg some (left_distrib _ _ _)
+  end,
+  right_distrib := λ a b c, begin
+    cases c with c,
+    { change (a + b) * 0 = a * 0 + b * 0, simp },
+    cases a with a; cases b with b; try {refl},
+    exact congr_arg some (right_distrib _ _ _)
+  end,
+  ..with_zero.add_comm_monoid,
+  ..with_zero.mul_zero_class,
+  ..with_zero.monoid }
+
 section
   variables [ring α] (a b c d e : α)
 

data/option.lean

@@ -146,6 +146,14 @@ instance lift_or_get_idem (f : α → α → α) [h : is_idempotent α f] :
   is_idempotent (option α) (lift_or_get f) :=
 ⟨λ a, by cases a; simp [lift_or_get, h.idempotent]⟩
 
+instance lift_or_get_is_left_id (f : α → α → α) :
+  is_left_id (option α) (lift_or_get f) none :=
+⟨λ a, by cases a; simp [lift_or_get]⟩
+
+instance lift_or_get_is_right_id (f : α → α → α) :
+  is_right_id (option α) (lift_or_get f) none :=
+⟨λ a, by cases a; simp [lift_or_get]⟩
+
 theorem lift_or_get_choice {f : α → α → α} (h : ∀ a b, f a b = a ∨ f a b = b) :
   ∀ o₁ o₂, lift_or_get f o₁ o₂ = o₁ ∨ lift_or_get f o₁ o₂ = o₂
 | none     none     := or.inl rfl