Order from embedding

Stream: Is there code for X?

[David A]

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]

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

[Thomas Browning]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

Do you have an example of your list defn?

[Mario Carneiro]

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]

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

[David A]

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]

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]

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]

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]

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

[Mario Carneiro]

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

[David A]

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]

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]

I mean show the types of things

[Mario Carneiro]

it doesn't matter if it's only partial, but a complete definition of the term is useful

[Mario Carneiro]

specifically how is my_list defined

[Mario Carneiro]

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]

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]

Just use sorry in all those functions you just described

[Mario Carneiro]

what I need to show that these points are unique

What does this theorem look like?

[David A]

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]

it's not an mwe yet, point isn't defined

[Mario Carneiro]

The usual trick is to paste it into a new file

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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]

Well it's easiest to get pointers starting from a well formed source

[Mario Carneiro]

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]

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]

but it's still not clear to me where the uniqueness is coming from here - is jups.updates a nodup list?

[Mario Carneiro]

remember that the list [(0,0), (0,0), .. ] can be arbitrarily long and still stay within N of the origin

[David A]

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]

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]

I assume you already have something along these lines proven, it seems like some property that follows from justified

[Mario Carneiro]

so you probably don't have to go as far as can_extend_free

[Mario Carneiro]

(if you haven't made a lemma about this, you should)

[David A]

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]

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]

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]

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]

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

[Mario Carneiro]

@David A

[David A]

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...