diff --git a/algebra/group.lean b/algebra/group.lean index b72d1bddce2fd..3f758169c238e 100644 --- a/algebra/group.lean +++ b/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 } diff --git a/algebra/ordered_group.lean b/algebra/ordered_group.lean index 597e95b805e27..87d4c6e6309c5 100644 --- a/algebra/ordered_group.lean +++ b/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 diff --git a/algebra/ring.lean b/algebra/ring.lean index 2638f3b1624e9..b93455c384a75 100644 --- a/algebra/ring.lean +++ b/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 : α) diff --git a/data/option.lean b/data/option.lean index 0d47271ce647b..c64c56908c694 100644 --- a/data/option.lean +++ b/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 diff --git a/order/bounded_lattice.lean b/order/bounded_lattice.lean index a7df9f6f94988..afa421e116597 100644 --- a/order/bounded_lattice.lean +++ b/order/bounded_lattice.lean @@ -241,9 +241,14 @@ instance bounded_lattice_fun {α : Type u} {β : Type v} [bounded_lattice β] : bot_le := assume f a, bot_le, ..partial_order_fun } +end lattice + def with_bot (α : Type*) := option α namespace with_bot +open lattice + +instance : has_coe_t α (with_bot α) := ⟨some⟩ instance partial_order [partial_order α] : partial_order (with_bot α) := { le := λ o₁ o₂ : option α, ∀ a ∈ o₁, ∃ b ∈ o₂, a ≤ b, @@ -265,15 +270,22 @@ instance order_bot [partial_order α] : order_bot (with_bot α) := bot_le := λ a a' h, option.no_confusion h, ..with_bot.partial_order } -@[simp] theorem some_le_some [partial_order α] {a b : α} : - @has_le.le (with_bot α) _ (some a) (some b) ↔ a ≤ b := +@[simp] theorem coe_le_coe [partial_order α] {a b : α} : + (a : with_bot α) ≤ b ↔ a ≤ b := ⟨λ h, by rcases h a rfl with ⟨_, ⟨⟩, h⟩; exact h, λ h a' e, option.some_inj.1 e ▸ ⟨b, rfl, h⟩⟩ -theorem some_le [partial_order α] {a b : α} : - ∀ {o : option α}, b ∈ o → - (@has_le.le (with_bot α) _ (some a) o ↔ a ≤ b) -| _ rfl := some_le_some +@[simp] theorem some_le_some [partial_order α] {a b : α} : + @has_le.le (with_bot α) _ (some a) (some b) ↔ a ≤ b := coe_le_coe + +theorem coe_le [partial_order α] {a b : α} : + ∀ {o : option α}, b ∈ o → ((a : with_bot α) ≤ o ↔ a ≤ b) +| _ rfl := coe_le_coe + +@[simp] theorem some_lt_some [partial_order α] {a b : α} : + @has_lt.lt (with_bot α) _ (some a) (some b) ↔ a < b := +(and_congr some_le_some (not_congr some_le_some)) + .trans lt_iff_le_not_le.symm instance linear_order [linear_order α] : linear_order (with_bot α) := { le_total := λ o₁ o₂, begin @@ -283,6 +295,16 @@ instance linear_order [linear_order α] : linear_order (with_bot α) := end, ..with_bot.partial_order } +instance decidable_linear_order [decidable_linear_order α] : decidable_linear_order (with_bot α) := +{ decidable_le := λ a b, begin + cases a with a, + { exact is_true bot_le }, + cases b with b, + { exact is_false (mt (le_antisymm bot_le) (by simp)) }, + { exact decidable_of_iff _ some_le_some } + end, + ..with_bot.linear_order } + instance semilattice_sup [semilattice_sup α] : semilattice_sup_bot (with_bot α) := { sup := option.lift_or_get (⊔), le_sup_left := λ o₁ o₂ a ha, @@ -334,6 +356,9 @@ end with_bot def with_top (α : Type*) := option α namespace with_top +open lattice + +instance : has_coe_t α (with_top α) := ⟨some⟩ instance partial_order [partial_order α] : partial_order (with_top α) := { le := λ o₁ o₂ : option α, ∀ b ∈ o₂, ∃ a ∈ o₁, a ≤ b, @@ -355,15 +380,23 @@ instance order_top [partial_order α] : order_top (with_top α) := le_top := λ a a' h, option.no_confusion h, ..with_top.partial_order } -@[simp] theorem some_le_some [partial_order α] {a b : α} : - @has_le.le (with_top α) _ (some a) (some b) ↔ a ≤ b := +@[simp] theorem coe_le_coe [partial_order α] {a b : α} : + (a : with_top α) ≤ b ↔ a ≤ b := ⟨λ h, by rcases h b rfl with ⟨_, ⟨⟩, h⟩; exact h, λ h a' e, option.some_inj.1 e ▸ ⟨a, rfl, h⟩⟩ -theorem le_some [partial_order α] {a b : α} : +@[simp] theorem some_le_some [partial_order α] {a b : α} : + @has_le.le (with_top α) _ (some a) (some b) ↔ a ≤ b := coe_le_coe + +theorem le_coe [partial_order α] {a b : α} : ∀ {o : option α}, a ∈ o → - (@has_le.le (with_top α) _ o (some b) ↔ a ≤ b) -| _ rfl := some_le_some + (@has_le.le (with_top α) _ o b ↔ a ≤ b) +| _ rfl := coe_le_coe + +@[simp] theorem some_lt_some [partial_order α] {a b : α} : + @has_lt.lt (with_top α) _ (some a) (some b) ↔ a < b := +(and_congr some_le_some (not_congr some_le_some)) + .trans lt_iff_le_not_le.symm instance linear_order [linear_order α] : linear_order (with_top α) := { le_total := λ o₁ o₂, begin @@ -373,6 +406,16 @@ instance linear_order [linear_order α] : linear_order (with_top α) := end, ..with_top.partial_order } +instance decidable_linear_order [decidable_linear_order α] : decidable_linear_order (with_top α) := +{ decidable_le := λ a b, begin + cases b with b, + { exact is_true le_top }, + cases a with a, + { exact is_false (mt (le_antisymm le_top) (by simp)) }, + { exact decidable_of_iff _ some_le_some } + end, + ..with_top.linear_order } + instance semilattice_inf [semilattice_inf α] : semilattice_inf_top (with_top α) := { inf := option.lift_or_get (⊓), inf_le_left := λ o₁ o₂ a ha, @@ -419,5 +462,3 @@ instance bounded_lattice [bounded_lattice α] : bounded_lattice (with_top α) := { ..with_top.lattice, ..with_top.order_top, ..with_top.order_bot } end with_top - -end lattice diff --git a/order/lattice.lean b/order/lattice.lean index a13b33c5969da..dede3a735dfac 100644 --- a/order/lattice.lean +++ b/order/lattice.lean @@ -6,8 +6,7 @@ Authors: Johannes Hölzl Defines the inf/sup (semi)-lattice with optionally top/bot type class hierarchy. -/ -import order.basic tactic.finish -open auto +import order.basic set_option old_structure_cmd true