# Zulip Chat Archive

## 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 :=
(updates : path₁)
(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_point`

s 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 _ _],
simp [← int.coe_nat_add],
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)

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

@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