From 99d312956441e631699f3fc7e7f65aca84fd25ac Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Mon, 24 Oct 2022 07:29:29 +0000 Subject: [PATCH] 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 --- src/data/dfinsupp/lex.lean | 159 ++++++++++++++++++++++++++++++++ src/data/dfinsupp/ne_locus.lean | 132 ++++++++++++++++++++++++++ src/data/finsupp/lex.lean | 79 ++++------------ src/data/pi/lex.lean | 27 +++--- 4 files changed, 324 insertions(+), 73 deletions(-) create mode 100644 src/data/dfinsupp/lex.lean create mode 100644 src/data/dfinsupp/ne_locus.lean diff --git a/src/data/dfinsupp/lex.lean b/src/data/dfinsupp/lex.lean new file mode 100644 index 0000000000000..ef595d5f4c594 --- /dev/null +++ b/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 diff --git a/src/data/dfinsupp/ne_locus.lean b/src/data/dfinsupp/ne_locus.lean new file mode 100644 index 0000000000000..1bb54495eeb1f --- /dev/null +++ b/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 diff --git a/src/data/finsupp/lex.lean b/src/data/finsupp/lex.lean index aa4e4066bf532..2b4be491a0721 100644 --- a/src/data/finsupp/lex.lean +++ b/src/data/finsupp/lex.lean @@ -3,9 +3,10 @@ Copyright (c) 2022 Damiano Testa. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Damiano Testa -/ -import data.pi.lex import data.finsupp.order import data.finsupp.ne_locus +import data.dfinsupp.lex +import data.finsupp.to_dfinsupp /-! # Lexicographic order on finitely supported functions @@ -23,7 +24,7 @@ variables [has_zero N] /-- `finsupp.lex r s` is the lexicographic relation on `α →₀ N`, where `α` is ordered by `r`, and `N` is ordered by `s`. -The type synonym `_root_.lex (α →₀ N)` has an order given by `finsupp.lex (<) (<)`. +The type synonym `lex (α →₀ N)` has an order given by `finsupp.lex (<) (<)`. -/ protected def lex (r : α → α → Prop) (s : N → N → Prop) (x y : α →₀ N) : Prop := pi.lex r (λ _, s) x y @@ -35,9 +36,20 @@ rfl lemma lex_def {r : α → α → Prop} {s : N → N → Prop} {a b : α →₀ N} : finsupp.lex r s a b ↔ ∃ j, (∀ d, r d j → a d = b d) ∧ s (a j) (b j) := iff.rfl +lemma lex_eq_inv_image_dfinsupp_lex (r : α → α → Prop) (s : N → N → Prop) : + finsupp.lex r s = inv_image (dfinsupp.lex r $ λ a, s) to_dfinsupp := rfl + instance [has_lt α] [has_lt N] : has_lt (lex (α →₀ N)) := ⟨λ f g, finsupp.lex (<) (<) (of_lex f) (of_lex g)⟩ +lemma lex_lt_of_lt_of_preorder [preorder N] (r) [is_strict_order α r] + {x y : α →₀ N} (hlt : x < y) : ∃ i, (∀ j, r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i := +dfinsupp.lex_lt_of_lt_of_preorder r (id hlt : x.to_dfinsupp < y.to_dfinsupp) + +lemma lex_lt_of_lt [partial_order N] (r) [is_strict_order α r] + {x y : α →₀ N} (hlt : x < y) : pi.lex r (λ i, (<)) x y := +dfinsupp.lex_lt_of_lt r (id hlt : x.to_dfinsupp < y.to_dfinsupp) + instance lex.is_strict_order [linear_order α] [partial_order N] : is_strict_order (lex (α →₀ N)) (<) := let i : is_strict_order (lex (α → N)) (<) := pi.lex.is_strict_order in @@ -46,73 +58,20 @@ let i : is_strict_order (lex (α → N)) (<) := pi.lex.is_strict_order in variables [linear_order α] -/-- The partial order on `finsupp`s obtained by the lexicographic ordering. +/-- The partial order on `finsupp`s obtained by the lexicographic ordering. See `finsupp.lex.linear_order` for a proof that this partial order is in fact linear. -/ instance lex.partial_order [partial_order N] : partial_order (lex (α →₀ N)) := partial_order.lift (λ x, to_lex ⇑(of_lex x)) finsupp.coe_fn_injective--fun_like.coe_injective -section linear_order - -variable [linear_order N] - -/-- 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 (α →₀ N) → lex (α →₀ N) → 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 (finsupp.ne_locus_eq_empty.mp (finset.min_eq_top.mp h)) - | (wit : α), h := - have hne : f wit ≠ g wit := mem_ne_locus.mp (finset.mem_of_min h), - hne.lt_or_lt.by_cases - (λ hwit, h_lt ⟨wit, λ j hj, mem_ne_locus.not_left.mp (finset.not_mem_of_lt_min hj h), hwit⟩) - (λ hwit, h_gt ⟨wit, by exact λ j hj, begin - refine mem_ne_locus.not_left.mp (finset.not_mem_of_lt_min hj _), - rwa ne_locus_comm, - end, hwit⟩) - end - -@[irreducible] instance lex.decidable_le : @decidable_rel (lex (α →₀ N)) (≤) := -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 (α →₀ N)) (<) := -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 `finsupp`s obtained by the lexicographic ordering. -/ -instance lex.linear_order : linear_order (lex (α →₀ N)) := -{ 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 +instance lex.linear_order [linear_order N] : linear_order (lex (α →₀ N)) := +{ ..lex.partial_order, + ..linear_order.lift' (to_lex ∘ to_dfinsupp ∘ of_lex) finsupp_equiv_dfinsupp.injective } variable [partial_order N] -lemma lex.le_of_forall_le {a b : lex (α →₀ N)} (h : ∀ i, of_lex a i ≤ of_lex b i) : a ≤ b := -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 lex.le_of_of_lex_le {a b : lex (α →₀ N)} (h : of_lex a ≤ of_lex b) : a ≤ b := -lex.le_of_forall_le h - lemma to_lex_monotone : monotone (@to_lex (α →₀ N)) := -λ _ _, lex.le_of_forall_le +λ a b h, dfinsupp.to_lex_monotone (id h : ∀ i, of_lex (to_dfinsupp a) i ≤ of_lex (to_dfinsupp b) i) lemma lt_of_forall_lt_of_lt (a b : lex (α →₀ N)) (i : α) : (∀ j < i, of_lex a j = of_lex b j) → of_lex a i < of_lex b i → a < b := diff --git a/src/data/pi/lex.lean b/src/data/pi/lex.lean index c19d46ac522f7..927c30bba3fc6 100644 --- a/src/data/pi/lex.lean +++ b/src/data/pi/lex.lean @@ -46,6 +46,15 @@ notation `Πₗ` binders `, ` r:(scoped p, lex (Π i, p i)) := r @[simp] lemma to_lex_apply (x : Π i, β i) (i : ι) : to_lex x i = x i := rfl @[simp] lemma of_lex_apply (x : lex (Π i, β i)) (i : ι) : of_lex x i = x i := rfl +lemma lex_lt_of_lt_of_preorder [Π i, preorder (β i)] {r} (hwf : well_founded 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 := +let h' := pi.lt_def.1 hlt, ⟨i, hi, hl⟩ := hwf.has_min _ h'.2 in + ⟨i, λ j hj, ⟨h'.1 j, not_not.1 $ λ h, hl j (lt_of_le_not_le (h'.1 j) h) hj⟩, hi⟩ + +lemma lex_lt_of_lt [Π i, partial_order (β i)] {r} (hwf : well_founded 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 hwf hlt } + lemma is_trichotomous_lex [∀ i, is_trichotomous (β i) s] (wf : well_founded r) : is_trichotomous (Π i, β i) (pi.lex r @s) := { trichotomous := λ a b, @@ -86,29 +95,21 @@ noncomputable instance [linear_order ι] [is_well_order ι (<)] [∀ a, linear_o @linear_order_of_STO (Πₗ i, β i) (<) { to_is_trichotomous := is_trichotomous_lex _ _ is_well_founded.wf } (classical.dec_rel _) -lemma lex.le_of_forall_le [linear_order ι] [hwf : is_well_order ι (<)] [Π a, partial_order (β a)] - {a b : lex (Π i, β i)} (h : ∀ i, a i ≤ b i) : a ≤ b := -or_iff_not_imp_left.2 $ λ hne, - let ⟨i, hi, hl⟩ := hwf.to_is_well_founded.wf.has_min {i | a i ≠ b i} (function.ne_iff.1 hne) in - ⟨i, λ j hj, by { contrapose! hl, exact ⟨j, hl, hj⟩ }, (h i).lt_of_ne hi⟩ - -lemma lex.le_of_of_lex_le [linear_order ι] [is_well_order ι (<)] [Π a, partial_order (β a)] - {a b : lex (Π i, β i)} (h : of_lex a ≤ of_lex b) : a ≤ b := -lex.le_of_forall_le h - lemma to_lex_monotone [linear_order ι] [is_well_order ι (<)] [Π a, partial_order (β a)] : monotone (@to_lex (Π i, β i)) := -λ _ _, lex.le_of_forall_le +λ a b h, or_iff_not_imp_left.2 $ λ hne, + let ⟨i, hi, hl⟩ := is_well_founded.wf.has_min {i | a i ≠ b i} (function.ne_iff.1 hne) in + ⟨i, λ j hj, by { contrapose! hl, exact ⟨j, hl, hj⟩ }, (h i).lt_of_ne hi⟩ instance [linear_order ι] [is_well_order ι (<)] [Π a, partial_order (β a)] [Π a, order_bot (β a)] : order_bot (lex (Π a, β a)) := { bot := to_lex ⊥, - bot_le := λ f, lex.le_of_of_lex_le bot_le } + bot_le := λ f, to_lex_monotone bot_le } instance [linear_order ι] [is_well_order ι (<)] [Π a, partial_order (β a)] [Π a, order_top (β a)] : order_top (lex (Π a, β a)) := { top := to_lex ⊤, - le_top := λ f, lex.le_of_of_lex_le le_top } + le_top := λ f, to_lex_monotone le_top } instance [linear_order ι] [is_well_order ι (<)] [Π a, partial_order (β a)] [Π a, bounded_order (β a)] : bounded_order (lex (Π a, β a)) :=