New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: port Order.OrderIsoNat #1753
Closed
Closed
Changes from all commits
Commits
Show all changes
12 commits
Select commit
Hold shift + click to select a range
cc7277c
feat: port Order.OrderIsoNat
aricursion 57492bb
Initial file copy from mathport
aricursion d6b7769
automated fixes
aricursion e93ebc7
initial
aricursion 39636e5
a few left
aricursion 60b51db
missing congrm tactic so proof is gross
aricursion ecae814
simp not work?
aricursion fdac59b
everything compiles
aricursion 20c92bb
lint fix?
aricursion cdb0cb7
lint fix?
aricursion 6ed12b2
spacing
aricursion 50cf97a
Update Mathlib/Order/OrderIsoNat.lean
ChrisHughes24 File filter
Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,282 @@ | ||
/- | ||
Copyright (c) 2017 Mario Carneiro. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Mario Carneiro | ||
|
||
! This file was ported from Lean 3 source module order.order_iso_nat | ||
! leanprover-community/mathlib commit 2445c98ae4b87eabebdde552593519b9b6dc350c | ||
! Please do not edit these lines, except to modify the commit id | ||
! if you have ported upstream changes. | ||
-/ | ||
|
||
import Mathlib.Data.Nat.Lattice | ||
import Mathlib.Logic.Denumerable | ||
import Mathlib.Logic.Function.Iterate | ||
import Mathlib.Order.Hom.Basic | ||
|
||
/-! | ||
# Relation embeddings from the naturals | ||
|
||
This file allows translation from monotone functions `ℕ → α` to order embeddings `ℕ ↪ α` and | ||
defines the limit value of an eventually-constant sequence. | ||
|
||
## Main declarations | ||
|
||
* `natLt`/`natGt`: Make an order embedding `Nat ↪ α` from | ||
an increasing/decreasing function `Nat → α`. | ||
* `monotonicSequenceLimit`: The limit of an eventually-constant monotone sequence `Nat →o α`. | ||
* `monotonicSequenceLimitIndex`: The index of the first occurence of `monotonicSequenceLimit` | ||
in the sequence. | ||
-/ | ||
|
||
|
||
variable {α : Type _} | ||
|
||
namespace RelEmbedding | ||
|
||
variable {r : α → α → Prop} [IsStrictOrder α r] | ||
|
||
/-- If `f` is a strictly `r`-increasing sequence, then this returns `f` as an order embedding. -/ | ||
def natLt (f : ℕ → α) (H : ∀ n : ℕ, r (f n) (f (n + 1))) : ((· < ·) : ℕ → ℕ → Prop) ↪r r := | ||
ofMonotone f <| Nat.rel_of_forall_rel_succ_of_lt r H | ||
#align rel_embedding.nat_lt RelEmbedding.natLt | ||
|
||
@[simp] | ||
theorem coe_natLt {f : ℕ → α} {H : ∀ n : ℕ, r (f n) (f (n + 1))} : ⇑(natLt f H) = f := | ||
rfl | ||
#align rel_embedding.coe_nat_lt RelEmbedding.coe_natLt | ||
|
||
/-- If `f` is a strictly `r`-decreasing sequence, then this returns `f` as an order embedding. -/ | ||
def natGt (f : ℕ → α) (H : ∀ n : ℕ, r (f (n + 1)) (f n)) : ((· > ·) : ℕ → ℕ → Prop) ↪r r := | ||
haveI := IsStrictOrder.swap r | ||
RelEmbedding.swap (natLt f H) | ||
#align rel_embedding.nat_gt RelEmbedding.natGt | ||
|
||
@[simp] | ||
theorem coe_natGt {f : ℕ → α} {H : ∀ n : ℕ, r (f (n + 1)) (f n)} : ⇑(natGt f H) = f := | ||
rfl | ||
#align rel_embedding.coe_nat_gt RelEmbedding.coe_natGt | ||
|
||
theorem exists_not_acc_lt_of_not_acc {a : α} {r} (h : ¬Acc r a) : ∃ b, ¬Acc r b ∧ r b a := by | ||
contrapose! h | ||
refine' ⟨_, fun b hr => _⟩ | ||
by_contra hb | ||
exact h b hb hr | ||
#align rel_embedding.exists_not_acc_lt_of_not_acc RelEmbedding.exists_not_acc_lt_of_not_acc | ||
|
||
/-- A value is accessible iff it isn't contained in any infinite decreasing sequence. -/ | ||
theorem acc_iff_no_decreasing_seq {x} : | ||
Acc r x ↔ IsEmpty { f : ((· > ·) : ℕ → ℕ → Prop) ↪r r // x ∈ Set.range f } := by | ||
constructor | ||
· refine' fun h => h.recOn fun x _ IH => _ | ||
constructor | ||
rintro ⟨f, k, hf⟩ | ||
exact IsEmpty.elim' (IH (f (k + 1)) (hf ▸ f.map_rel_iff.2 (lt_add_one k))) ⟨f, _, rfl⟩ | ||
· have : ∀ x : { a // ¬Acc r a }, ∃ y : { a // ¬Acc r a }, r y.1 x.1 := | ||
by | ||
rintro ⟨x, hx⟩ | ||
cases exists_not_acc_lt_of_not_acc hx with | ||
| intro w h => exact ⟨⟨w, h.1⟩, h.2⟩ | ||
obtain ⟨f, h⟩ := Classical.axiom_of_choice this | ||
refine' fun E => | ||
by_contradiction fun hx => E.elim' ⟨natGt (fun n => ((f^[n]) ⟨x, hx⟩).1) fun n => _, 0, rfl⟩ | ||
simp only [Function.iterate_succ'] | ||
apply h | ||
#align rel_embedding.acc_iff_no_decreasing_seq RelEmbedding.acc_iff_no_decreasing_seq | ||
|
||
theorem not_acc_of_decreasing_seq (f : ((· > ·) : ℕ → ℕ → Prop) ↪r r) (k : ℕ) : ¬Acc r (f k) := by | ||
rw [acc_iff_no_decreasing_seq, not_isEmpty_iff] | ||
exact ⟨⟨f, k, rfl⟩⟩ | ||
#align rel_embedding.not_acc_of_decreasing_seq RelEmbedding.not_acc_of_decreasing_seq | ||
|
||
/-- A relation is well-founded iff it doesn't have any infinite decreasing sequence. -/ | ||
theorem wellFounded_iff_no_descending_seq : | ||
WellFounded r ↔ IsEmpty (((· > ·) : ℕ → ℕ → Prop) ↪r r) := by | ||
constructor | ||
· rintro ⟨h⟩ | ||
exact ⟨fun f => not_acc_of_decreasing_seq f 0 (h _)⟩ | ||
· intro h | ||
exact ⟨fun x => acc_iff_no_decreasing_seq.2 inferInstance⟩ | ||
#align rel_embedding.well_founded_iff_no_descending_seq RelEmbedding.wellFounded_iff_no_descending_seq | ||
|
||
theorem not_wellFounded_of_decreasing_seq (f : ((· > ·) : ℕ → ℕ → Prop) ↪r r) : ¬WellFounded r := by | ||
rw [wellFounded_iff_no_descending_seq, not_isEmpty_iff] | ||
exact ⟨f⟩ | ||
#align rel_embedding.not_well_founded_of_decreasing_seq RelEmbedding.not_wellFounded_of_decreasing_seq | ||
|
||
end RelEmbedding | ||
|
||
namespace Nat | ||
|
||
variable (s : Set ℕ) [Infinite s] | ||
|
||
/-- An order embedding from `ℕ` to itself with a specified range -/ | ||
def orderEmbeddingOfSet [DecidablePred (· ∈ s)] : ℕ ↪o ℕ := | ||
(RelEmbedding.orderEmbeddingOfLTEmbedding | ||
(RelEmbedding.natLt (Nat.Subtype.ofNat s) fun _ => Nat.Subtype.lt_succ_self _)).trans | ||
(OrderEmbedding.subtype s) | ||
#align nat.order_embedding_of_set Nat.orderEmbeddingOfSet | ||
|
||
/-- `Nat.Subtype.ofNat` as an order isomorphism between `ℕ` and an infinite subset. See also | ||
`Nat.Nth` for a version where the subset may be finite. -/ | ||
noncomputable def Subtype.orderIsoOfNat : ℕ ≃o s := by | ||
classical | ||
exact | ||
RelIso.ofSurjective | ||
(RelEmbedding.orderEmbeddingOfLTEmbedding | ||
(RelEmbedding.natLt (Nat.Subtype.ofNat s) fun n => Nat.Subtype.lt_succ_self _)) | ||
Nat.Subtype.ofNat_surjective | ||
#align nat.subtype.order_iso_of_nat Nat.Subtype.orderIsoOfNat | ||
|
||
--porting note: Added the decidability requirement, I'm not sure how it worked in lean3 without it | ||
variable {s} [dP : DecidablePred (· ∈ s)] | ||
|
||
@[simp] | ||
theorem coe_orderEmbeddingOfSet : ⇑(orderEmbeddingOfSet s) = (↑) ∘ Subtype.ofNat s := | ||
rfl | ||
#align nat.coe_order_embedding_of_set Nat.coe_orderEmbeddingOfSet | ||
|
||
theorem orderEmbeddingOfSet_apply {n : ℕ} : orderEmbeddingOfSet s n = Subtype.ofNat s n := | ||
rfl | ||
#align nat.order_embedding_of_set_apply Nat.orderEmbeddingOfSet_apply | ||
|
||
@[simp] | ||
theorem Subtype.orderIsoOfNat_apply {n : ℕ} : Subtype.orderIsoOfNat s n = Subtype.ofNat s n := by | ||
simp only [orderIsoOfNat, RelIso.ofSurjective_apply, | ||
RelEmbedding.orderEmbeddingOfLTEmbedding_apply, RelEmbedding.coe_natLt] | ||
suffices (fun a => Classical.propDecidable (a ∈ s)) = (fun a => dP a) by | ||
rw [this] | ||
simp | ||
#align nat.subtype.order_iso_of_nat_apply Nat.Subtype.orderIsoOfNat_apply | ||
|
||
variable (s) | ||
|
||
theorem orderEmbeddingOfSet_range : Set.range (Nat.orderEmbeddingOfSet s) = s := | ||
Subtype.coe_comp_ofNat_range | ||
#align nat.order_embedding_of_set_range Nat.orderEmbeddingOfSet_range | ||
|
||
theorem exists_subseq_of_forall_mem_union {s t : Set α} (e : ℕ → α) (he : ∀ n, e n ∈ s ∪ t) : | ||
∃ g : ℕ ↪o ℕ, (∀ n, e (g n) ∈ s) ∨ ∀ n, e (g n) ∈ t := by | ||
classical | ||
have : Infinite (e ⁻¹' s) ∨ Infinite (e ⁻¹' t) := by | ||
simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union, | ||
Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ] | ||
cases this | ||
exacts[⟨Nat.orderEmbeddingOfSet (e ⁻¹' s), Or.inl fun n => (Nat.Subtype.ofNat (e ⁻¹' s) _).2⟩, | ||
⟨Nat.orderEmbeddingOfSet (e ⁻¹' t), Or.inr fun n => (Nat.Subtype.ofNat (e ⁻¹' t) _).2⟩] | ||
#align nat.exists_subseq_of_forall_mem_union Nat.exists_subseq_of_forall_mem_union | ||
|
||
end Nat | ||
|
||
theorem exists_increasing_or_nonincreasing_subseq' (r : α → α → Prop) (f : ℕ → α) : | ||
∃ g : ℕ ↪o ℕ, | ||
(∀ n : ℕ, r (f (g n)) (f (g (n + 1)))) ∨ ∀ m n : ℕ, m < n → ¬r (f (g m)) (f (g n)) := by | ||
classical | ||
let bad : Set ℕ := { m | ∀ n, m < n → ¬r (f m) (f n) } | ||
by_cases hbad : Infinite bad | ||
· haveI := hbad | ||
refine' ⟨Nat.orderEmbeddingOfSet bad, Or.intro_right _ fun m n mn => _⟩ | ||
have h := @Set.mem_range_self _ _ ↑(Nat.orderEmbeddingOfSet bad) m | ||
rw [Nat.orderEmbeddingOfSet_range bad] at h | ||
exact h _ ((OrderEmbedding.lt_iff_lt _).2 mn) | ||
· rw [Set.infinite_coe_iff, Set.Infinite, not_not] at hbad | ||
obtain ⟨m, hm⟩ : ∃ m, ∀ n, m ≤ n → ¬n ∈ bad := | ||
by | ||
by_cases he : hbad.toFinset.Nonempty | ||
· | ||
refine' | ||
⟨(hbad.toFinset.max' he).succ, fun n hn nbad => | ||
Nat.not_succ_le_self _ | ||
(hn.trans (hbad.toFinset.le_max' n (hbad.mem_toFinset.2 nbad)))⟩ | ||
· exact ⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩ | ||
have h : ∀ n : ℕ, ∃ n' : ℕ, n < n' ∧ r (f (n + m)) (f (n' + m)) := | ||
by | ||
intro n | ||
have h := hm _ (le_add_of_nonneg_left n.zero_le) | ||
simp only [exists_prop, not_not, Set.mem_setOf_eq, not_forall] at h | ||
obtain ⟨n', hn1, hn2⟩ := h | ||
obtain ⟨x, hpos, rfl⟩ := exists_pos_add_of_lt hn1 | ||
refine' ⟨n + x, add_lt_add_left hpos n, _⟩ | ||
rw [add_assoc, add_comm x m, ← add_assoc] | ||
exact hn2 | ||
let g' : ℕ → ℕ := @Nat.rec (fun _ => ℕ) m fun n gn => Nat.find (h gn) | ||
exact | ||
⟨(RelEmbedding.natLt (fun n => g' n + m) fun n => | ||
Nat.add_lt_add_right (Nat.find_spec (h (g' n))).1 m).orderEmbeddingOfLTEmbedding, | ||
Or.intro_left _ fun n => (Nat.find_spec (h (g' n))).2⟩ | ||
#align exists_increasing_or_nonincreasing_subseq' exists_increasing_or_nonincreasing_subseq' | ||
|
||
/-- This is the infinitary Erdős–Szekeres theorem, and an important lemma in the usual proof of | ||
Bolzano-Weierstrass for `ℝ`. -/ | ||
theorem exists_increasing_or_nonincreasing_subseq (r : α → α → Prop) [IsTrans α r] (f : ℕ → α) : | ||
∃ g : ℕ ↪o ℕ, | ||
(∀ m n : ℕ, m < n → r (f (g m)) (f (g n))) ∨ ∀ m n : ℕ, m < n → ¬r (f (g m)) (f (g n)) := by | ||
obtain ⟨g, hr | hnr⟩ := exists_increasing_or_nonincreasing_subseq' r f | ||
· refine' ⟨g, Or.intro_left _ fun m n mn => _⟩ | ||
obtain ⟨x, rfl⟩ := exists_add_of_le (Nat.succ_le_iff.2 mn) | ||
induction' x with x ih | ||
· apply hr | ||
· apply IsTrans.trans _ _ _ _ (hr _) | ||
exact ih (lt_of_lt_of_le m.lt_succ_self (Nat.le_add_right _ _)) | ||
· exact ⟨g, Or.intro_right _ hnr⟩ | ||
#align exists_increasing_or_nonincreasing_subseq exists_increasing_or_nonincreasing_subseq | ||
|
||
theorem WellFounded.monotone_chain_condition' [Preorder α] : | ||
WellFounded ((· > ·) : α → α → Prop) ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → ¬a n < a m := by | ||
refine' ⟨fun h a => _, fun h => _⟩ | ||
· have hne : (Set.range a).Nonempty := ⟨a 0, by simp⟩ | ||
obtain ⟨x, ⟨n, rfl⟩, H⟩ := h.has_min _ hne | ||
exact ⟨n, fun m _ => H _ (Set.mem_range_self _)⟩ | ||
· refine' RelEmbedding.wellFounded_iff_no_descending_seq.2 ⟨fun a => _⟩ | ||
obtain ⟨n, hn⟩ := h (a.swap : ((· < ·) : ℕ → ℕ → Prop) →r ((· < ·) : α → α → Prop)).toOrderHom | ||
exact hn n.succ n.lt_succ_self.le ((RelEmbedding.map_rel_iff _).2 n.lt_succ_self) | ||
#align well_founded.monotone_chain_condition' WellFounded.monotone_chain_condition' | ||
|
||
--porting note: congrm tactic doesn't exist so this proof is much messier | ||
/-- The "monotone chain condition" below is sometimes a convenient form of well foundedness. -/ | ||
theorem WellFounded.monotone_chain_condition [PartialOrder α] : | ||
WellFounded ((· > ·) : α → α → Prop) ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → a n = a m := | ||
WellFounded.monotone_chain_condition'.trans <| by | ||
refine' ⟨fun h a => _, fun h a => _⟩ <;> specialize h a <;> cases' h with n h <;> | ||
use n <;> intro m hmn <;> specialize h m hmn | ||
· rw [lt_iff_le_and_ne] at h | ||
push_neg at h | ||
apply h | ||
simp [a.mono hmn] | ||
· rw [lt_iff_le_and_ne] | ||
push_neg | ||
intro _ | ||
exact h | ||
#align well_founded.monotone_chain_condition WellFounded.monotone_chain_condition | ||
|
||
/-- Given an eventually-constant monotone sequence `a₀ ≤ a₁ ≤ a₂ ≤ ...` in a partially-ordered | ||
type, `monotonicSequenceLimitIndex a` is the least natural number `n` for which `aₙ` reaches the | ||
constant value. For sequences that are not eventually constant, `monotonicSequenceLimitIndex a` | ||
is defined, but is a junk value. -/ | ||
noncomputable def monotonicSequenceLimitIndex [Preorder α] (a : ℕ →o α) : ℕ := | ||
infₛ { n | ∀ m, n ≤ m → a n = a m } | ||
#align monotonic_sequence_limit_index monotonicSequenceLimitIndex | ||
|
||
/-- The constant value of an eventually-constant monotone sequence `a₀ ≤ a₁ ≤ a₂ ≤ ...` in a | ||
partially-ordered type. -/ | ||
noncomputable def monotonicSequenceLimit [Preorder α] (a : ℕ →o α) := | ||
a (monotonicSequenceLimitIndex a) | ||
#align monotonic_sequence_limit monotonicSequenceLimit | ||
|
||
theorem WellFounded.supᵢ_eq_monotonicSequenceLimit [CompleteLattice α] | ||
(h : WellFounded ((· > ·) : α → α → Prop)) (a : ℕ →o α) : supᵢ a = monotonicSequenceLimit a := | ||
by | ||
suffices (⨆ m : ℕ, a m) ≤ monotonicSequenceLimit a by exact le_antisymm this (le_supᵢ a _) | ||
apply supᵢ_le | ||
intro m | ||
by_cases hm : m ≤ monotonicSequenceLimitIndex a | ||
· exact a.monotone hm | ||
· replace hm := le_of_not_le hm | ||
let S := { n | ∀ m, n ≤ m → a n = a m } | ||
have hInf : infₛ S ∈ S := by | ||
refine' Nat.infₛ_mem _ | ||
rw [WellFounded.monotone_chain_condition] at h | ||
exact h a | ||
change a m ≤ a (infₛ S) | ||
rw [hInf m hm] | ||
#align well_founded.supr_eq_monotonic_sequence_limit WellFounded.supᵢ_eq_monotonicSequenceLimit |
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do you need it for the statements, or for the proofs?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
For the statements. In particular,
orderEmbeddingOfSet
andSubtype.ofNat
require itThere was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is the
classical
leakage in Lean3 again