feat(data): port finsupp.ne_locus/lex to dfinsupp (#16777)

+ Add new files *dfinsupp/ne_locus* and *dfinsupp/lex* mostly by copying the finsupp counterparts and making trivial adaptions. Use the `dfinsupp` lemmas/constructions to golf the `finsupp` counterpart, e.g. the `linear_order` on `finsupp.lex`.

+ Add lemmas `lex_lt_of_lt(_of_preorder)` for each of pi/finsupp/dfinsupp that shows the (<) relation on the product of a family of partial orders is a subrelation of the lexicographic (<), for any choice of well-founded relation (in the case of pi) or strict total order (in the case of (d)finsupp) on the set of coordinates. Useful to deduce well-foundedness of the product order from the well-foundedness of the lexicographic order in #16772.



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

src/data/dfinsupp/lex.lean

@@ -0,0 +1,159 @@
+/-
+Copyright (c) 2022 Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Damiano Testa, Junyan Xu
+-/
+import data.dfinsupp.order
+import data.dfinsupp.ne_locus
+
+/-!
+# Lexicographic order on finitely supported dependent functions
+
+This file defines the lexicographic order on `dfinsupp`.
+-/
+
+variables {ι : Type*} {α : ι → Type*}
+
+namespace dfinsupp
+
+section has_zero
+
+variable [Π i, has_zero (α i)]
+
+/-- `dfinsupp.lex r s` is the lexicographic relation on `Π₀ i, α i`, where `ι` is ordered by `r`,
+and `α i` is ordered by `s i`.
+The type synonym `lex (Π₀ i, α i)` has an order given by `dfinsupp.lex (<) (λ i, (<))`.
+-/
+protected def lex (r : ι → ι → Prop) (s : Π i, α i → α i → Prop) (x y : Π₀ i, α i) : Prop :=
+pi.lex r s x y
+
+lemma _root_.pi.lex_eq_dfinsupp_lex {r : ι → ι → Prop} {s : Π i, α i → α i → Prop}
+  (a b : Π₀ i, α i) : pi.lex r s (a : Π i, α i) b = dfinsupp.lex r s a b := rfl
+
+lemma lex_def {r : ι → ι → Prop} {s : Π i, α i → α i → Prop} {a b : Π₀ i, α i} :
+  dfinsupp.lex r s a b ↔ ∃ j, (∀ d, r d j → a d = b d) ∧ s j (a j) (b j) := iff.rfl
+
+instance [has_lt ι] [Π i, has_lt (α i)] : has_lt (lex (Π₀ i, α i)) :=
+⟨λ f g, dfinsupp.lex (<) (λ i, (<)) (of_lex f) (of_lex g)⟩
+
+lemma lex_lt_of_lt_of_preorder [Π i, preorder (α i)] (r) [is_strict_order ι r]
+  {x y : Π₀ i, α i} (hlt : x < y) : ∃ i, (∀ j, r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i :=
+begin
+  obtain ⟨hle, j, hlt⟩ := pi.lt_def.1 hlt, classical,
+  obtain ⟨i, hi, hl⟩ := (x.ne_locus y).finite_to_set.well_founded_on.has_min
+    {i | x i < y i} ⟨⟨j, mem_ne_locus.2 hlt.ne⟩, hlt⟩, swap 3, { assumption },
+  exact ⟨i, λ k hk, ⟨hle k, not_not.1 $ λ h,
+    hl ⟨k, mem_ne_locus.2 (ne_of_not_le h).symm⟩ ((hle k).lt_of_not_le h) hk⟩, hi⟩,
+end
+
+lemma lex_lt_of_lt [Π i, partial_order (α i)] (r) [is_strict_order ι r]
+  {x y : Π₀ i, α i} (hlt : x < y) : pi.lex r (λ i, (<)) x y :=
+by { simp_rw [pi.lex, le_antisymm_iff], exact lex_lt_of_lt_of_preorder r hlt }
+
+instance lex.is_strict_order [linear_order ι] [Π i, partial_order (α i)] :
+  is_strict_order (lex (Π₀ i, α i)) (<) :=
+let i : is_strict_order (lex (Π i, α i)) (<) := pi.lex.is_strict_order in
+{ irrefl := to_lex.surjective.forall.2 $ λ a, @irrefl _ _ i.to_is_irrefl a,
+  trans := to_lex.surjective.forall₃.2 $ λ a b c, @trans _ _ i.to_is_trans a b c }
+
+variables [linear_order ι]
+
+/-- The partial order on `dfinsupp`s obtained by the lexicographic ordering.
+See `dfinsupp.lex.linear_order` for a proof that this partial order is in fact linear. -/
+instance lex.partial_order [Π i, partial_order (α i)] : partial_order (lex (Π₀ i, α i)) :=
+partial_order.lift (λ x, to_lex ⇑(of_lex x)) dfinsupp.coe_fn_injective
+
+section linear_order
+
+variable [Π i, linear_order (α i)]
+
+/-- Auxiliary helper to case split computably. There is no need for this to be public, as it
+can be written with `or.by_cases` on `lt_trichotomy` once the instances below are constructed. -/
+private def lt_trichotomy_rec {P : lex (Π₀ i, α i) → lex (Π₀ i, α i) → Sort*}
+  (h_lt : Π {f g}, to_lex f < to_lex g → P (to_lex f) (to_lex g))
+  (h_eq : Π {f g}, to_lex f = to_lex g → P (to_lex f) (to_lex g))
+  (h_gt : Π {f g}, to_lex g < to_lex f → P (to_lex f) (to_lex g)) :
+  Π f g, P f g :=
+lex.rec $ λ f, lex.rec $ λ g,
+  match _, rfl : ∀ y, (f.ne_locus g).min = y → _ with
+  | ⊤, h := h_eq (ne_locus_eq_empty.mp $ finset.min_eq_top.mp h)
+  | (wit : ι), h := (mem_ne_locus.mp $ finset.mem_of_min h).lt_or_lt.by_cases
+      (λ hwit, h_lt ⟨wit, λ j hj, not_mem_ne_locus.mp (finset.not_mem_of_lt_min hj h), hwit⟩)
+      (λ hwit, h_gt ⟨wit, λ j hj, not_mem_ne_locus.mp
+        (finset.not_mem_of_lt_min hj $ by rwa ne_locus_comm), hwit⟩)
+  end
+
+@[irreducible] instance lex.decidable_le : @decidable_rel (lex (Π₀ i, α i)) (≤) :=
+lt_trichotomy_rec
+  (λ f g h, is_true $ or.inr h)
+  (λ f g h, is_true $ or.inl $ congr_arg _ h)
+  (λ f g h, is_false $ λ h', (lt_irrefl _ (h.trans_le h')).elim)
+
+@[irreducible] instance lex.decidable_lt : @decidable_rel (lex (Π₀ i, α i)) (<) :=
+lt_trichotomy_rec
+  (λ f g h, is_true h)
+  (λ f g h, is_false h.not_lt)
+  (λ f g h, is_false h.asymm)
+
+/--  The linear order on `dfinsupp`s obtained by the lexicographic ordering. -/
+instance lex.linear_order : linear_order (lex (Π₀ i, α i)) :=
+{ le_total := lt_trichotomy_rec
+    (λ f g h, or.inl h.le)
+    (λ f g h, or.inl h.le)
+    (λ f g h, or.inr h.le),
+  decidable_lt := by apply_instance,
+  decidable_le := by apply_instance,
+  decidable_eq := by apply_instance,
+  ..lex.partial_order }
+
+end linear_order
+
+variable [Π i, partial_order (α i)]
+
+lemma to_lex_monotone : monotone (@to_lex (Π₀ i, α i)) :=
+λ a b h, le_of_lt_or_eq $ or_iff_not_imp_right.2 $ λ hne, by classical; exact
+  ⟨finset.min' _ (nonempty_ne_locus_iff.2 hne),
+    λ j hj, not_mem_ne_locus.1 (λ h, (finset.min'_le _ _ h).not_lt hj),
+    (h _).lt_of_ne (mem_ne_locus.1 $ finset.min'_mem _ _)⟩
+
+lemma lt_of_forall_lt_of_lt (a b : lex (Π₀ i, α i)) (i : ι) :
+  (∀ j < i, of_lex a j = of_lex b j) → of_lex a i < of_lex b i → a < b :=
+λ h1 h2, ⟨i, h1, h2⟩
+
+end has_zero
+
+section covariants
+variables [linear_order ι] [Π i, add_monoid (α i)] [Π i, linear_order (α i)]
+
+/-!  We are about to sneak in a hypothesis that might appear to be too strong.
+We assume `covariant_class` with *strict* inequality `<` also when proving the one with the
+*weak* inequality `≤`.  This is actually necessary: addition on `lex (Π₀ i, α i)` may fail to be
+monotone, when it is "just" monotone on `α i`. -/
+section left
+variables [Π i, covariant_class (α i) (α i) (+) (<)]
+
+instance lex.covariant_class_lt_left :
+  covariant_class (lex (Π₀ i, α i)) (lex (Π₀ i, α i)) (+) (<) :=
+⟨λ f g h ⟨a, lta, ha⟩, ⟨a, λ j ja, congr_arg ((+) _) (lta j ja), add_lt_add_left ha _⟩⟩
+
+instance lex.covariant_class_le_left :
+  covariant_class (lex (Π₀ i, α i)) (lex (Π₀ i, α i)) (+) (≤) := has_add.to_covariant_class_left _
+
+end left
+
+section right
+variables [Π i, covariant_class (α i) (α i) (function.swap (+)) (<)]
+
+instance lex.covariant_class_lt_right :
+  covariant_class (lex (Π₀ i, α i)) (lex (Π₀ i, α i)) (function.swap (+)) (<) :=
+⟨λ f g h ⟨a, lta, ha⟩, ⟨a, λ j ja, congr_arg (+ (of_lex f j)) (lta j ja), add_lt_add_right ha _⟩⟩
+
+instance lex.covariant_class_le_right :
+  covariant_class (lex (Π₀ i, α i)) (lex (Π₀ i, α i)) (function.swap (+)) (≤) :=
+has_add.to_covariant_class_right _
+
+end right
+
+end covariants
+
+end dfinsupp

src/data/dfinsupp/ne_locus.lean

@@ -0,0 +1,132 @@
+/-
+Copyright (c) 2022 Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Damiano Testa, Junyan Xu
+-/
+import data.dfinsupp.basic
+
+/-!
+# Locus of unequal values of finitely supported dependent functions
+
+Let `N : α → Type*` be a type family, assume that `N a` has a `0` for all `a : α` and let
+`f g : Π₀ a, N a` be finitely supported dependent functions.
+
+## Main definition
+
+* `dfinsupp.ne_locus f g : finset α`, the finite subset of `α` where `f` and `g` differ.
+In the case in which `N a` is an additive group for all `a`, `dfinsupp.ne_locus f g` coincides with
+`dfinsupp.support (f - g)`.
+-/
+
+variables {α : Type*} {N : α → Type*}
+
+namespace dfinsupp
+variable [decidable_eq α]
+
+section N_has_zero
+variables [Π a, decidable_eq (N a)] [Π a, has_zero (N a)] (f g : Π₀ a, N a)
+
+/--  Given two finitely supported functions `f g : α →₀ N`, `finsupp.ne_locus f g` is the `finset`
+where `f` and `g` differ. This generalizes `(f - g).support` to situations without subtraction. -/
+def ne_locus (f g : Π₀ a, N a) : finset α :=
+(f.support ∪ g.support).filter (λ x, f x ≠ g x)
+
+@[simp] lemma mem_ne_locus {f g : Π₀ a, N a} {a : α} : a ∈ f.ne_locus g ↔ f a ≠ g a :=
+by simpa only [ne_locus, finset.mem_filter, finset.mem_union, mem_support_iff,
+    and_iff_right_iff_imp] using ne.ne_or_ne _
+
+lemma not_mem_ne_locus {f g : Π₀ a, N a} {a : α} : a ∉ f.ne_locus g ↔ f a = g a :=
+mem_ne_locus.not.trans not_ne_iff
+
+@[simp] lemma coe_ne_locus : ↑(f.ne_locus g) = {x | f x ≠ g x} :=
+by { ext, exact mem_ne_locus }
+
+@[simp] lemma ne_locus_eq_empty {f g : Π₀ a, N a} : f.ne_locus g = ∅ ↔ f = g :=
+⟨λ h, ext (λ a, not_not.mp (mem_ne_locus.not.mp (finset.eq_empty_iff_forall_not_mem.mp h a))),
+  λ h, h ▸ by simp only [ne_locus, ne.def, eq_self_iff_true, not_true, finset.filter_false]⟩
+
+@[simp] lemma nonempty_ne_locus_iff {f g : Π₀ a, N a} : (f.ne_locus g).nonempty ↔ f ≠ g :=
+finset.nonempty_iff_ne_empty.trans ne_locus_eq_empty.not
+
+lemma ne_locus_comm : f.ne_locus g = g.ne_locus f :=
+by simp_rw [ne_locus, finset.union_comm, ne_comm]
+
+@[simp]
+lemma ne_locus_zero_right : f.ne_locus 0 = f.support :=
+by { ext, rw [mem_ne_locus, mem_support_iff, coe_zero, pi.zero_apply] }
+
+@[simp]
+lemma ne_locus_zero_left : (0 : Π₀ a, N a).ne_locus f = f.support :=
+(ne_locus_comm _ _).trans (ne_locus_zero_right _)
+
+end N_has_zero
+
+section ne_locus_and_maps
+
+variables {M P : α → Type*} [Π a, has_zero (N a)] [Π a, has_zero (M a)] [Π a, has_zero (P a)]
+
+lemma subset_map_range_ne_locus [Π a, decidable_eq (N a)] [Π a, decidable_eq (M a)]
+  (f g : Π₀ a, N a) {F : Π a, N a → M a} (F0 : ∀ a, F a 0 = 0) :
+  (f.map_range F F0).ne_locus (g.map_range F F0) ⊆ f.ne_locus g :=
+λ a, by simpa only [mem_ne_locus, map_range_apply, not_imp_not] using congr_arg (F a)
+
+lemma zip_with_ne_locus_eq_left [Π a, decidable_eq (N a)] [Π a, decidable_eq (P a)]
+  {F : Π a, M a → N a → P a} (F0 : ∀ a, F a 0 0 = 0)
+  (f : Π₀ a, M a) (g₁ g₂ : Π₀ a, N a) (hF : ∀ a f, function.injective (λ g, F a f g)) :
+  (zip_with F F0 f g₁).ne_locus (zip_with F F0 f g₂) = g₁.ne_locus g₂ :=
+by { ext, simpa only [mem_ne_locus] using (hF a _).ne_iff }
+
+lemma zip_with_ne_locus_eq_right [Π a, decidable_eq (M a)] [Π a, decidable_eq (P a)]
+  {F : Π a, M a → N a → P a} (F0 : ∀ a, F a 0 0 = 0)
+  (f₁ f₂ : Π₀ a, M a) (g : Π₀ a, N a) (hF : ∀ a g, function.injective (λ f, F a f g)) :
+  (zip_with F F0 f₁ g).ne_locus (zip_with F F0 f₂ g) = f₁.ne_locus f₂ :=
+by { ext, simpa only [mem_ne_locus] using (hF a _).ne_iff }
+
+lemma map_range_ne_locus_eq [Π a, decidable_eq (N a)] [Π a, decidable_eq (M a)] (f g : Π₀ a, N a)
+  {F : Π a, N a → M a} (F0 : ∀ a, F a 0 = 0) (hF : ∀ a, function.injective (F a)) :
+  (f.map_range F F0).ne_locus (g.map_range F F0) = f.ne_locus g :=
+by { ext, simpa only [mem_ne_locus] using (hF a).ne_iff }
+
+end ne_locus_and_maps
+
+variables [Π a, decidable_eq (N a)]
+
+@[simp] lemma ne_locus_add_left [Π a, add_left_cancel_monoid (N a)] (f g h : Π₀ a, N a) :
+  (f + g).ne_locus (f + h) = g.ne_locus h  :=
+zip_with_ne_locus_eq_left _ _ _ _ $ λ a, add_right_injective
+
+@[simp] lemma ne_locus_add_right [Π a, add_right_cancel_monoid (N a)] (f g h : Π₀ a, N a) :
+  (f + h).ne_locus (g + h) = f.ne_locus g  :=
+zip_with_ne_locus_eq_right _ _ _ _ $ λ a, add_left_injective
+
+section add_group
+variables [Π a, add_group (N a)] (f f₁ f₂ g g₁ g₂ : Π₀ a, N a)
+
+@[simp] lemma ne_locus_neg_neg : ne_locus (-f) (-g) = f.ne_locus g :=
+map_range_ne_locus_eq _ _ (λ a, neg_zero) (λ a, neg_injective)
+
+lemma ne_locus_neg : ne_locus (-f) g = f.ne_locus (-g) := by rw [←ne_locus_neg_neg, neg_neg]
+
+lemma ne_locus_eq_support_sub : f.ne_locus g = (f - g).support :=
+by rw [←@ne_locus_add_right α N _ _ _ _ _ (-g), add_right_neg, ne_locus_zero_right, sub_eq_add_neg]
+
+@[simp] lemma ne_locus_sub_left : ne_locus (f - g₁) (f - g₂) = ne_locus g₁ g₂ :=
+by simp only [sub_eq_add_neg, @ne_locus_add_left α N _ _ _, ne_locus_neg_neg]
+
+@[simp] lemma ne_locus_sub_right : ne_locus (f₁ - g) (f₂ - g) = ne_locus f₁ f₂ :=
+by simpa only [sub_eq_add_neg] using @ne_locus_add_right α N _ _ _ _ _ _
+
+@[simp] lemma ne_locus_self_add_right : ne_locus f (f + g) = g.support :=
+by rw [←ne_locus_zero_left, ←@ne_locus_add_left α N _ _ _ f 0 g, add_zero]
+
+@[simp] lemma ne_locus_self_add_left : ne_locus (f + g) f = g.support :=
+by rw [ne_locus_comm, ne_locus_self_add_right]
+
+@[simp] lemma ne_locus_self_sub_right : ne_locus f (f - g) = g.support :=
+by rw [sub_eq_add_neg, ne_locus_self_add_right, support_neg]
+
+@[simp] lemma ne_locus_self_sub_left : ne_locus (f - g) f = g.support :=
+by rw [ne_locus_comm, ne_locus_self_sub_right]
+
+end add_group
+end dfinsupp