feat(algebra, logic): Pi instances for nontrivial and monoid_with_zero (#4766)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author: eric-wieser

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

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
 

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

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
 

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 :=