## Stream: Is there code for X?

### Topic: Order from embedding

#### David A (Feb 21 2021 at 03:58):

I would like to show that the length of a certain list is less than or equal to a certain bound N*N, by showing that there's an injective function from its indices to (fin N × fin N). Unfortunately I haven't found anything useful for, well, any of the steps of that proof; from relating the length of a list to functions on its indices, to relating injective functions and order, to the cardinality of tuples... Is this just the wrong sort of approach?

#### Thomas Browning (Feb 21 2021 at 04:00):

for transferring sizes along injective functions, docs#fintype.card_le_of_injective is a good lemma

#### Thomas Browning (Feb 21 2021 at 04:01):

and docs#fintype.card_prod tells you the cardinality of a product

#### Yakov Pechersky (Feb 21 2021 at 04:16):

It sounds like this might be more easily proven by inducting on the list itself.

#### Yakov Pechersky (Feb 21 2021 at 04:16):

Juggling indexing the list means having to construct the various hypotheses of being in bounds to use list.nth_le.

#### Yakov Pechersky (Feb 21 2021 at 04:17):

Do you have an example of your list defn?

#### Mario Carneiro (Feb 21 2021 at 04:20):

I agree with Yakov. Rather than constructing an injective function out of a list, it is easier and more natural to map your list to a list (fin N x fin N) that you can prove is nodup; it's easy to get from this to the claim that the length of the list is at most N^2

#### Mario Carneiro (Feb 21 2021 at 04:21):

and depending on the structure of the function, you might not even need fin N x fin N

#### David A (Feb 21 2021 at 04:29):

The idea of mapping + nodup makes sense. I'm still not sure how I can get from mapping to the product to the length of the list being bounded though.

My particular case is proving that unique lattice points drawn from those within N distance of the origin, according to the max norm, are less than 4*N*N.

#### David A (Feb 21 2021 at 04:33):

Btw I'm trying to stay away from fintype because I hit a weird bug where even just mentioning a finset in the type of a definition caused lean to hit a deterministic timeout apparently trying to find a normal form for the finset, even though (a) very little progress could actually be made reducing the finset, and (b) reducing the finset was not necessary to type-check the type or the definition... But I could never come up with a reduced failure case for this so I never posted it. It had to do with WF-induction, which is actually why I'm here now trying to get a natural number from of a list instead, to do induction on nat!

#### Mario Carneiro (Feb 21 2021 at 04:35):

My particular case is proving that unique lattice points drawn from those within N distance of the origin, according to the max norm, are less than 4*N*N.

How more precisely is this stated?

#### Mario Carneiro (Feb 21 2021 at 04:38):

It sounds like it might be easier to stay at the level of functions for this, don't bring in lists and instead prove that this set is a subset of Ioo (-N) N x Ioo (-N) N

#### Mario Carneiro (Feb 21 2021 at 04:39):

hopefully we have a theorem that says that Ico a b has cardinality b - a

#### Mario Carneiro (Feb 21 2021 at 04:41):

hm, this exact theorem isn't there but it shouldn't be hard to prove using int.range

#### David A (Feb 21 2021 at 04:41):

Uh, I mean, there's 1000 lines of definitions behind it because I'm actually talking about particular points, not all of them :)
And actually I have a list such that some of its elements can be converted to unique points, and a theorem which says those points have to be within distance N of the origin.
So it's like (list.length $list.filter my_filter my_list) ≤ 4 * N * N. #### David A (Feb 21 2021 at 04:42): Not sure if that's what you meant though. Also FWIW 4 * N * N doesn't matter, I literally just need any bound at all for the length of this list. #### Mario Carneiro (Feb 21 2021 at 04:42): I mean show the types of things #### Mario Carneiro (Feb 21 2021 at 04:43): it doesn't matter if it's only partial, but a complete definition of the term is useful #### Mario Carneiro (Feb 21 2021 at 04:44): specifically how is my_list defined #### Mario Carneiro (Feb 21 2021 at 04:48): Pasting the whole 1000 lines is also an option (say, in a gist or on a branch) if you don't know how to make #mwe of it #### David A (Feb 21 2021 at 04:48): So I really don't think I can provide a short version of the definition -_-. I have a quite complex type to work around lack of induction-recursion. So what I have is an argument jups : path₂, and my_list is actually jups.updates. path₂ is defined like: def path₁ := list update structure path₂ : Type := (updates : path₁) (justified : ∀ {upd ups}, list.cons upd ups <:+ updates → justified upd ups)  The points are actually defined by a partial function from tails of updates to ℤ × ℤ: def path₁.extension_point (ups : path₁) : option point  justified is an inductive type giving what I need to show that these points are unique and within distance N of the origin, where N actually comes from a function on path₂.updates. #### Mario Carneiro (Feb 21 2021 at 04:50): Just use sorry in all those functions you just described #### Mario Carneiro (Feb 21 2021 at 04:52): what I need to show that these points are unique What does this theorem look like? #### David A (Feb 21 2021 at 04:59): I think this is more-or-less self contained? : def point := ℤ × ℤ inductive update : Type | a (time : ℕ) : update | b (time : ℕ) : update | c (pt : point) : update def update.is_b (upd : update) : Prop := update.rec_on upd (λ _, false) (λ _, true) (λ _, false) instance update.is_b.dec (upd : update) : decidable upd.is_b := sorry def path_point_at_time (ups : path₁) (time : ℕ) : point := sorry def path_current_point (ups : path₁) : option point := sorry inductive path₁.is_preleft (ups : path₁) (pt : point) : Prop | halfplane : pt.fst < 0 → path₁.is_preleft | extension (ups' : path₁) : ups' <:+ ups → path_current_point ups' = some pt → path₁.is_preleft instance path₁.is_preleft.dec (ups : path₁) (pt : point) : decidable (ups.is_preleft pt) := sorry def path₁.can_extend_free (ups : path₁) (time : ℕ) : Prop := ¬ups.is_preleft (path_point_at_time ups time) def justified (hd : update) (tl : path₁) : Prop := update.rec_on hd (λ time, sorry) (λ time, sorry ∧ tl.can_extend_free time ∧ sorry) (λ eaten, true) def path₁.eaten_bound (ups : path₁) : ℕ := option.iget$ list.maximum $list.map (dist (0, 0))$ path₁.eaten ups

def path₂.extend_bound (jups : path₂)
: (list.length $list.filter update.is_b jups.updates) ≤ 4 * jups.updates.eaten_bound * jups.updates.eaten_bound := -- TRYING TO PROVE THIS  #### Mario Carneiro (Feb 21 2021 at 04:59): it's not an mwe yet, point isn't defined #### Mario Carneiro (Feb 21 2021 at 05:00): The usual trick is to paste it into a new file #### Mario Carneiro (Feb 21 2021 at 05:03): This works, although I made up dist and path1.eaten so I might not get the right idea there import data.list.min_max def point := ℤ × ℤ inductive update : Type | a (time : ℕ) : update | b (time : ℕ) : update | c (pt : point) : update def update.is_b (upd : update) : Prop := update.rec_on upd (λ _, false) (λ _, true) (λ _, false) instance update.is_b.dec (upd : update) : decidable upd.is_b := sorry def path₁ := list update def path_point_at_time (ups : path₁) (time : ℕ) : point := sorry def path_current_point (ups : path₁) : option point := sorry inductive path₁.is_preleft (ups : path₁) (pt : point) : Prop | halfplane : pt.fst < 0 → path₁.is_preleft | extension (ups' : path₁) : ups' <:+ ups → path_current_point ups' = some pt → path₁.is_preleft instance path₁.is_preleft.dec (ups : path₁) (pt : point) : decidable (ups.is_preleft pt) := sorry def path₁.can_extend_free (ups : path₁) (time : ℕ) : Prop := ¬ups.is_preleft (path_point_at_time ups time) def justified (hd : update) (tl : path₁) : Prop := update.rec_on hd (λ time, sorry) (λ time, sorry ∧ tl.can_extend_free time ∧ sorry) (λ eaten, true) def dist : ℕ × ℕ → ℕ × ℕ → ℕ := sorry def path₁.eaten : path₁ → list (ℕ × ℕ) := sorry def path₁.eaten_bound (ups : path₁) : ℕ := option.iget$ list.maximum $list.map (dist (0, 0))$ path₁.eaten ups

structure path₂ : Type :=
(justified : ∀ {upd ups}, list.cons upd ups <:+ updates → justified upd ups)

def path₂.extend_bound (jups : path₂)
: (list.length $list.filter update.is_b jups.updates) ≤ 4 * jups.updates.eaten_bound * jups.updates.eaten_bound := sorry -- TRYING TO PROVE THIS  #### David A (Feb 21 2021 at 05:06): Sorry, didn't realize you were going to try to run it. This actually typechecks: import init.function import data.list.min_max def point := ℤ × ℤ inductive update : Type | a (time : ℕ) : update | b (time : ℕ) : update | c (pt : point) : update def update.is_b (upd : update) : Prop := update.rec_on upd (λ _, false) (λ _, true) (λ _, false) instance update.is_b.dec (upd : update) : decidable upd.is_b := sorry def path₁ := list update def dist_to_origin : point → ℕ := sorry def path_point_at_time (ups : path₁) (time : ℕ) : point := sorry def path_current_point (ups : path₁) : option point := sorry def more_path_points (ups : path₁) : list point := sorry inductive path₁.is_preleft (ups : path₁) (pt : point) : Prop | halfplane : pt.fst < 0 → path₁.is_preleft | extension (ups' : path₁) : ups' <:+ ups → path_current_point ups' = some pt → path₁.is_preleft instance path₁.is_preleft.dec (ups : path₁) (pt : point) : decidable (ups.is_preleft pt) := sorry def path₁.can_extend_free (ups : path₁) (time : ℕ) : Prop := ¬ups.is_preleft (path_point_at_time ups time) def justified (hd : update) (tl : path₁) : Prop := update.rec_on hd (λ time, sorry) (λ time, sorry ∧ tl.can_extend_free time ∧ sorry) (λ eaten, true) structure path₂ : Type := (updates : path₁) (justified : ∀ {upd ups}, list.cons upd ups <:+ updates → justified upd ups) def path₁.bound (ups : path₁) : ℕ := option.iget$ list.maximum $list.map dist_to_origin$ more_path_points ups

def path₂.extend_bound (jups : path₂)
: (list.length $list.filter update.is_b jups.updates) ≤ 4 * jups.updates.bound * jups.updates.bound := sorry  #### David A (Feb 21 2021 at 05:09): Not 100% sure this has everything needed for the proof though. is_preleft should suffice for uniqueness. Definitely missing boundedness; let me try to put that back in. #### Mario Carneiro (Feb 21 2021 at 05:09): You should add in theorems (with sorry proofs) that you think are necessary for the main theorem, so that people can prove the goal without the setup #### Mario Carneiro (Feb 21 2021 at 05:10): You don't need to add more stuff in the inductives or structures, it's fine if the lemmas are not provable because they aren't the focus #### Mario Carneiro (Feb 21 2021 at 05:11): like I doubt the definition of justified needs to be provided here, unless you think that unfolding it is an important part of the proof you want help with #### David A (Feb 21 2021 at 05:12): Okay, didn't realize we were going full crowd-sourcing on a proof here; I was really just looking for pointers and that's why I was confused about the point of providing a mwe. :) Yeah, a lot of this stuff is pointless. Let me think about it for a while. #### Mario Carneiro (Feb 21 2021 at 05:13): Well it's easiest to get pointers starting from a well formed source #### Mario Carneiro (Feb 21 2021 at 05:14): I want to use the code to demonstrate some things in context but I want to make sure the advice is applicable to your actual problem #### Mario Carneiro (Feb 21 2021 at 05:15): for example I see now that lists are actually kind of integral to your setup, so my earlier suggestion about sets isn't useful #### Mario Carneiro (Feb 21 2021 at 05:15): but it's still not clear to me where the uniqueness is coming from here - is jups.updates a nodup list? #### Mario Carneiro (Feb 21 2021 at 05:16): remember that the list [(0,0), (0,0), .. ] can be arbitrarily long and still stay within N of the origin #### David A (Feb 21 2021 at 05:17): Yeah, that's what's missing here; path_point_at_time and path_current_point are obviously related, so that the "unique points" are actually the current_points which are unique thanks to can_extend_free. #### Mario Carneiro (Feb 21 2021 at 05:18): which are unique thanks to can_extend_free. is that a lemma that you can give a formal statement to in the language of the mwe? #### Mario Carneiro (Feb 21 2021 at 05:19): I assume you already have something along these lines proven, it seems like some property that follows from justified #### Mario Carneiro (Feb 21 2021 at 05:20): so you probably don't have to go as far as can_extend_free #### Mario Carneiro (Feb 21 2021 at 05:20): (if you haven't made a lemma about this, you should) #### David A (Feb 21 2021 at 05:46): Okay, based on my mental model of the problem I expect this to be provable: import data.list.min_max def point := ℤ × ℤ def norm : point → ℕ | (x, y) := max x.nat_abs y.nat_abs def path : Type := sorry def update : Type := sorry def updates := list update def path.raw_list : path → updates := sorry def path.tail : path → option path := sorry def path.tail_raw_list (jups : path) : jups.raw_list.tail = option.iget (option.map path.raw_list jups.tail) := sorry def update.new_bound : update → option ℕ := sorry def update.new_point : update → updates → option point := sorry def update.has_new_point (upd : update) : Prop := update.new_point upd [] ≠ none instance update.has_new_point_dec (upd : update) : decidable upd.has_new_point := sorry -- new_point is none/some depending only upon its upd argument: def update.has_new_point_correct (upd : update) (upds : updates) : upd.has_new_point ↔ upd.new_point upds ≠ none := sorry def updates.head_point : updates → option point | [] := none | (hd :: tl) := update.new_point hd tl def updates.all_points (ups : updates) : list point := ups.tails.filter_map updates.head_point def path.max_bound (jups : path) : ℕ := option.iget$ list.maximum $list.filter_map update.new_bound jups.raw_list def path.points_unique (jups : path) : ∀ hd tl, (hd :: tl) <:+ jups.raw_list → update.new_point hd tl ∉ list.map some (updates.all_points tl) := sorry def path.points_in_bounds (jups : path) : ∀ hd tl pt, (hd :: tl) = jups.raw_list → hd.new_point tl = some pt → norm pt < jups.max_bound := sorry def want_to_show (jups : path) : (list.length$ list.filter update.has_new_point jups.raw_list) ≤ 4 * jups.max_bound * jups.max_bound := sorry


(Edit: fixed updates.all_points to be a filter_map, but tbh this is not quite how I express it in my code anyways as it gets tangled up in the induction-recursion.)

#### David A (Feb 21 2021 at 06:12):

I'm not sure yet how to express a lemma about the relationship between jups.raw_list and the uniqueness of new_point; I guess I was thinking about the bijection between indices of raw_list and tails of raw_list, and the way points_unique is really saying that the non-filtered non-empty tails of raw_list are in bijection with the elements of updates.all_points from the path.

And ultimately want_to_show is helping define a measure on path, which must among other properties must decrease as more points are added. So I need an upper bound on that value:

def path.cons (upd : update) (jups : path) /- also requires some proofs about upd -/ : path := sorry
def path.cons.really_cons (upd : update) (jups : path) : (jups.cons upd).raw_list = upd :: jups.raw_list := sorry
def path.measure_other_updates (jups : path) : ℕ := sorry
def path.measure (jups : path) := jups.measure_other_updates + 4 * jups.max_bound * jups.max_bound - (list.length $list.filter update.has_new_point jups.raw_list) def really_want_to_show (upd : update) (jups : path) : let jups' := jups.cons upd in jups'.max_bound = jups.max_bound → jups'.measure_other_updates < jups.measure_other_updates + (if upd.has_new_point then 1 else 0) → jups'.measure < jups.measure := sorry  Or something like that, I'm really quite set on using a nat measure here due to aforementioned bug, so I don't expect to need or want to change this latter code. #### Mario Carneiro (Feb 21 2021 at 08:10): Here's a proof modulo the proof that all elements of the list are in the bounds, because I think you stated path.points_in_bounds incorrectly so I didn't try to use it import data.list.min_max import data.list.nodup import data.fintype.basic import data.int.range import tactic.ring theorem int.range_nodup (m n) : (int.range m n).nodup := begin rw [int.range, list.nodup_map_iff], apply list.nodup_range, exact λ a b h, int.coe_nat_inj (add_left_cancel h), end theorem int.length_range (m n) : (int.range m n).length = int.to_nat (n - m) := by simp [int.range] def point := ℤ × ℤ def norm : point → ℕ | (x, y) := max x.nat_abs y.nat_abs @[reducible] def X : Type := ℕ @[reducible] def path : Type := list X def path.raw_list : path → list X := sorry def path.tail : path → option path := sorry def path.tail_raw_list (P : path) : P.raw_list.tail = option.iget (option.map path.raw_list P.tail) := sorry def X.new_bound : X → option ℕ := sorry def X.new_point : X → list X → option point := sorry @[reducible] def X.ok (upd : X) : Prop := X.new_point upd [] ≠ none instance X.ok_dec (upd : X) : decidable upd.ok := sorry -- new_point is none/some depending only upon its upd argument: def X.ok_correct (upd : X) (upds : list X) : upd.ok ↔ upd.new_point upds ≠ none := sorry def X.head_point : list X → option point | [] := none | (hd :: tl) := X.new_point hd tl def X.all_points (ups : list X) : list point := ups.tails.filter_map X.head_point def path.N (P : path) : ℕ := option.iget$ list.maximum \$ list.filter_map X.new_bound P.raw_list

theorem path.points_unique (P : path) :
∀ hd tl, (hd :: tl) <:+ P.raw_list →
X.new_point hd tl ∉ list.map some (X.all_points tl) := sorry

theorem path.points_in_bounds (P : path) :
∀ hd tl pt, (hd :: tl) = P.raw_list →
hd.new_point tl = some pt → norm pt < P.N := sorry

def good_points : list X → list point
| [] := []
| (hd :: tl) :=
match X.new_point hd tl with
| none := good_points tl
| some a := a :: good_points tl
end

theorem good_points_bound : ∀ l, (list.filter X.ok l).length ≤ (good_points l).length
| [] := le_refl _
| (hd::tl) := begin
rw good_points,
cases e : hd.new_point tl; rw good_points,
{ rw list.filter_cons_of_neg,
{ exact good_points_bound tl },
{ intro h, exact (X.ok_correct _ _).1 h e } },
{ by_cases hd.ok,
{ rw list.filter_cons_of_pos _ h,
exact nat.succ_le_succ (good_points_bound tl) },
{ rw list.filter_cons_of_neg _ h,
exact nat.le_succ_of_le (good_points_bound tl) } }
end

theorem good_points_all (l) : good_points l ⊆ X.all_points l :=
begin
intros x h,
simp [X.all_points],
induction l with hd tl IH, cases h,
have IH : x ∈ good_points tl →
∃ (a : list X), a <:+ hd::tl ∧ X.head_point a = some x,
{ intro h,
obtain ⟨a, h', e⟩ := IH h,
exact ⟨a, h'.trans (list.suffix_cons _ _), e⟩ },
revert h,
rw good_points,
cases e : hd.new_point tl; rw good_points; intro h,
{ exact IH h },
rcases h with rfl | h,
{ exact ⟨_, list.suffix_refl _, e⟩ },
{ exact IH h },
end

theorem good_points_nodup (P : path) : ∀ l, l <:+ P.raw_list → (good_points l).nodup
| [] _ := dec_trivial
| (hd::tl) h := begin
rw good_points,
have IH := good_points_nodup tl ((list.suffix_cons _ _).trans h),
cases e : hd.new_point tl; rw good_points,
{ exact IH },
refine list.nodup_cons.2 ⟨λ h', _, IH⟩,
have := path.points_unique _ _ _ h,
rw e at this,
simp at this,
exact this (good_points_all _ h')
end

theorem want_to_show (P : path) : list.length (list.filter X.ok P.raw_list) ≤
4 * P.N * P.N :=
begin
refine le_trans (good_points_bound _) _,
let S : finset (ℤ × ℤ) := ⟨⟦good_points P.raw_list⟧, good_points_nodup _ _ (list.suffix_refl _)⟩,
let T : finset ℤ := ⟨⟦int.range (-P.N) P.N⟧, int.range_nodup _ _⟩,
change S.card ≤ _,
have : S ⊆ T.product T,
{ intros x h,
simp [int.mem_range_iff] at h ⊢,
suffices : norm x < P.N,
{ cases x, simp [norm] at this ⊢,
simp [← int.coe_nat_lt, ← int.abs_eq_nat_abs, abs_lt] at this,
simp [this, le_of_lt] },
sorry },
refine le_trans (finset.card_le_of_subset this) _,
rw [finset.card_product, show T.card = _, from int.length_range _ _],
ring,
end


#### Mario Carneiro (Feb 21 2021 at 08:14):

As far as takeaways, the key is the good_points definition, which I think is equal to list.filter ok P.raw_list but is defined in a way which makes the proof of nodup from your lemmas easier.

#### Mario Carneiro (Feb 21 2021 at 08:15):

(also I shortened the names a bit to make it easier to see, hope you don't mind)

@David A

#### David A (Feb 21 2021 at 17:21):

Thanks, this not only gives me a way forward but also provides some much needed formatting hints ;)

path.points_in_bounds is stated the way I intended but it actually only proves the head point is in bounds (and should have just used the new function I added); then I have to use the definition of bounds and the projection of all the proofs path contains onto its own tail to show the result for the tails. So I should probably just make that at a separate lemma...

Last updated: May 19 2021 at 02:10 UTC