Zulip Chat Archive

Stream: Is there code for X?

Topic: Order from embedding


view this post on Zulip 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?

view this post on Zulip Thomas Browning (Feb 21 2021 at 04:00):

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

view this post on Zulip Thomas Browning (Feb 21 2021 at 04:01):

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

view this post on Zulip Yakov Pechersky (Feb 21 2021 at 04:16):

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

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Feb 21 2021 at 04:17):

Do you have an example of your list defn?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 21 2021 at 04:39):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 21 2021 at 04:42):

I mean show the types of things

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 21 2021 at 04:44):

specifically how is my_list defined

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 21 2021 at 04:50):

Just use sorry in all those functions you just described

view this post on Zulip Mario Carneiro (Feb 21 2021 at 04:52):

what I need to show that these points are unique

What does this theorem look like?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 21 2021 at 04:59):

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

view this post on Zulip Mario Carneiro (Feb 21 2021 at 05:00):

The usual trick is to paste it into a new file

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 21 2021 at 05:13):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 21 2021 at 05:20):

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

view this post on Zulip Mario Carneiro (Feb 21 2021 at 05:20):

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

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Feb 21 2021 at 08:15):

@David A

view this post on Zulip 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