From c66ff4904521596a23b5a0751ba1a1ef721a5c8c Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 30 Oct 2020 13:26:14 +0000 Subject: [PATCH] feat(algebra, logic): Pi instances for nontrivial and monoid_with_zero (#4766) Co-authored-by: Yury G. Kudryashov --- src/algebra/group/pi.lean | 36 +++++++-------------- src/algebra/ring/pi.lean | 3 -- src/data/pi.lean | 51 ++++++++++++++++++++++++++++++ src/logic/function/basic.lean | 3 ++ src/logic/nontrivial.lean | 59 +++++++++++++++++++---------------- 5 files changed, 97 insertions(+), 55 deletions(-) create mode 100644 src/data/pi.lean diff --git a/src/algebra/group/pi.lean b/src/algebra/group/pi.lean index 3b15e9a8615ef..538f9445a5782 100644 --- a/src/algebra/group/pi.lean +++ b/src/algebra/group/pi.lean @@ -3,7 +3,9 @@ Copyright (c) 2018 Simon Hudon. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Simon Hudon, Patrick Massot -/ +import data.pi import algebra.ordered_group +import algebra.group_with_zero import tactic.pi_instances /-! # Pi instances for groups and monoids @@ -82,6 +84,15 @@ instance ordered_comm_group [∀ i, ordered_comm_group $ f i] : ..pi.comm_group, ..pi.partial_order } +instance mul_zero_class [∀ i, mul_zero_class $ f i] : + mul_zero_class (Π i : I, f i) := +by refine_struct { zero := (0 : Π i, f i), mul := (*), .. }; tactic.pi_instance_derive_field + +instance comm_monoid_with_zero [∀ i, comm_monoid_with_zero $ f i] : + comm_monoid_with_zero (Π i : I, f i) := +by refine_struct { zero := (0 : Π i, f i), one := (1 : Π i, f i), mul := (*), .. }; + tactic.pi_instance_derive_field + section instance_lemmas open function @@ -95,31 +106,6 @@ variables {α β γ : Type*} end instance_lemmas -variables [decidable_eq I] -variables [Π i, has_zero (f i)] - -/-- The function supported at `i`, with value `x` there. -/ -def single (i : I) (x : f i) : Π i, f i := -λ i', if h : i' = i then (by { subst h, exact x }) else 0 - -@[simp] -lemma single_eq_same (i : I) (x : f i) : single i x i = x := -begin - dsimp [single], - split_ifs, - { refl, }, - { exfalso, exact h rfl, } -end - -@[simp] -lemma single_eq_of_ne {i i' : I} (h : i' ≠ i) (x : f i) : single i x i' = 0 := -begin - dsimp [single], - split_ifs with h', - { exfalso, exact h h', }, - { refl, } -end - end pi section monoid_hom diff --git a/src/algebra/ring/pi.lean b/src/algebra/ring/pi.lean index 6d41616e06a77..9bb6eda05e986 100644 --- a/src/algebra/ring/pi.lean +++ b/src/algebra/ring/pi.lean @@ -19,9 +19,6 @@ variable {I : Type u} -- The indexing type variable {f : I → Type v} -- The family of types already equipped with instances variables (x y : Π i, f i) (i : I) -instance mul_zero_class [Π i, mul_zero_class $ f i] : mul_zero_class (Π i : I, f i) := -by refine_struct { zero := (0 : Π i, f i), mul := (*), .. }; tactic.pi_instance_derive_field - instance distrib [Π i, distrib $ f i] : distrib (Π i : I, f i) := by refine_struct { add := (+), mul := (*), .. }; tactic.pi_instance_derive_field diff --git a/src/data/pi.lean b/src/data/pi.lean new file mode 100644 index 0000000000000..d9496c970de68 --- /dev/null +++ b/src/data/pi.lean @@ -0,0 +1,51 @@ +/- +Copyright (c) 2020 Eric Wieser. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Simon Hudon, Patrick Massot, Eric Wieser +-/ +import tactic.split_ifs +import tactic.simpa +/-! +# Theorems on pi types + +This file defines basic structures on Pi Types +-/ + +universes u v w +variable {I : Type u} -- The indexing type +variable {f : I → Type v} -- The family of types already equipped with instances +variables (x y : Π i, f i) (i : I) + +namespace pi + +variables [decidable_eq I] +variables [Π i, has_zero (f i)] + +/-- The function supported at `i`, with value `x` there. -/ +def single (i : I) (x : f i) : Π i, f i := +λ i', if h : i' = i then (by { subst h, exact x }) else 0 + +@[simp] +lemma single_eq_same (i : I) (x : f i) : single i x i = x := +begin + dsimp [single], + split_ifs, + { refl, }, + { exfalso, exact h rfl, } +end + +@[simp] +lemma single_eq_of_ne {i i' : I} (h : i' ≠ i) (x : f i) : single i x i' = 0 := +begin + dsimp [single], + split_ifs with h', + { exfalso, exact h h', }, + { refl, } +end + +variables (f) + +lemma single_injective (i : I) : function.injective (single i : f i → Π i, f i) := +λ x y h, by simpa only [single, dif_pos] using congr_fun h i + +end pi diff --git a/src/logic/function/basic.lean b/src/logic/function/basic.lean index a0a339ca67167..ee2b3d0520c5f 100644 --- a/src/logic/function/basic.lean +++ b/src/logic/function/basic.lean @@ -306,6 +306,9 @@ if h : a = a' then eq.rec v h.symm else f a @[simp] lemma update_same (a : α) (v : β a) (f : Πa, β a) : update f a v a = v := dif_pos rfl +lemma update_injective (f : Πa, β a) (a' : α) : injective (update f a') := +λ v v' h, have _ := congr_fun h a', by rwa [update_same, update_same] at this + @[simp] lemma update_noteq {a a' : α} (h : a ≠ a') (v : β a') (f : Πa, β a) : update f a' v a = f a := dif_neg h diff --git a/src/logic/nontrivial.lean b/src/logic/nontrivial.lean index a210613aff993..7fad215ce3eab 100644 --- a/src/logic/nontrivial.lean +++ b/src/logic/nontrivial.lean @@ -3,6 +3,8 @@ Copyright (c) 2020 Sébastien Gouëzel. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sébastien Gouëzel -/ +import data.pi +import data.prod import logic.unique import logic.function.basic @@ -80,36 +82,9 @@ by { rw [← not_nontrivial_iff_subsingleton, or_comm], exact classical.em _ } lemma false_of_nontrivial_of_subsingleton (α : Type*) [nontrivial α] [subsingleton α] : false := let ⟨x, y, h⟩ := exists_pair_ne α in h $ subsingleton.elim x y -instance nontrivial_prod_left [nontrivial α] [nonempty β] : nontrivial (α × β) := -begin - inhabit β, - rcases exists_pair_ne α with ⟨x, y, h⟩, - use [(x, default β), (y, default β)], - contrapose! h, - exact congr_arg prod.fst h -end - -instance nontrivial_prod_right [nontrivial α] [nonempty β] : nontrivial (β × α) := -begin - inhabit β, - rcases exists_pair_ne α with ⟨x, y, h⟩, - use [(default β, x), (default β, y)], - contrapose! h, - exact congr_arg prod.snd h -end - instance option.nontrivial [nonempty α] : nontrivial (option α) := by { inhabit α, use [none, some (default α)] } -instance function.nontrivial [nonempty α] [nontrivial β] : nontrivial (α → β) := -begin - rcases exists_pair_ne β with ⟨x, y, h⟩, - use [λ _, x, λ _, y], - contrapose! h, - inhabit α, - exact congr_fun h (default α) -end - /-- Pushforward a `nontrivial` instance along an injective function. -/ protected lemma function.injective.nontrivial [nontrivial α] {f : α → β} (hf : function.injective f) : nontrivial β := @@ -137,6 +112,36 @@ begin { exact ⟨x₂, h⟩ } end +instance nontrivial_prod_right [nonempty α] [nontrivial β] : nontrivial (α × β) := +prod.snd_surjective.nontrivial + +instance nontrivial_prod_left [nontrivial α] [nonempty β] : nontrivial (α × β) := +prod.fst_surjective.nontrivial + +namespace pi + +variables {I : Type*} {f : I → Type*} + +/-- A pi type is nontrivial if it's nonempty everywhere and nontrivial somewhere. -/ +lemma nontrivial_at (i' : I) [inst : Π i, nonempty (f i)] [nontrivial (f i')] : + nontrivial (Π i : I, f i) := +by classical; exact +(function.update_injective (λ i, classical.choice (inst i)) i').nontrivial + +/-- +As a convenience, provide an instance automatically if `(f (default I))` is nontrivial. + +If a different index has the non-trivial type, then use `haveI := nontrivial_at that_index`. +-/ +instance nontrivial [inhabited I] [inst : Π i, nonempty (f i)] [nontrivial (f (default I))] : + nontrivial (Π i : I, f i) := +nontrivial_at (default I) + +end pi + +instance function.nontrivial [h : nonempty α] [nontrivial β] : nontrivial (α → β) := +h.elim $ λ a, pi.nontrivial_at a + mk_simp_attribute nontriviality "Simp lemmas for `nontriviality` tactic" protected lemma subsingleton.le [preorder α] [subsingleton α] (x y : α) : x ≤ y :=