Zulip Chat Archive

Stream: new members

Topic: list.pairwise of list.repeat


view this post on Zulip Eric Wieser (Jun 26 2020 at 14:47):

Is there a builtin proof that list.pairwise r (list.repeat x n) is true if r x x?

view this post on Zulip Eric Wieser (Jun 26 2020 at 14:48):

And if not, under what name would it be appropriate to define it in data/list/pairwise.lean?

view this post on Zulip Jalex Stark (Jun 26 2020 at 14:49):

can you state the lemma formally?

view this post on Zulip Jalex Stark (Jun 26 2020 at 14:49):

(the way i would try to answer this question is to state the lemma formally, try library_search, and then go read the file where list.pairwise is defined)

view this post on Zulip Jalex Stark (Jun 26 2020 at 14:50):

also by builtin do you mean available in mathlib?

view this post on Zulip Eric Wieser (Jun 26 2020 at 14:50):

Sure, let me try. I've already read through that file, and nothing jumps out as what I want.

Yes, I mean mathlib.

view this post on Zulip Jalex Stark (Jun 26 2020 at 14:51):

docs#list.pairwise

view this post on Zulip Jalex Stark (Jun 26 2020 at 14:52):

the lemma doesn't sound mathematically useful

view this post on Zulip Jalex Stark (Jun 26 2020 at 14:52):

why do you need it?

view this post on Zulip Jalex Stark (Jun 26 2020 at 14:52):

#xy

view this post on Zulip Eric Wieser (Jun 26 2020 at 14:53):

lemma pairwise_of_rep_is_reflexive {α : Type} (r : α  α  Prop) (x : α) (n : ) : r x x  list.pairwise r (list.repeat x n)

view this post on Zulip Eric Wieser (Jun 26 2020 at 14:54):

I need it in order to construct a list subtyped to satisfy a pairwise predicate.

view this post on Zulip Jalex Stark (Jun 26 2020 at 14:55):

it should be an easy list induction

view this post on Zulip Eric Wieser (Jun 26 2020 at 14:56):

Too "easy" to have a place in mathlib?

view this post on Zulip Jalex Stark (Jun 26 2020 at 14:57):

not sure yet

view this post on Zulip Jalex Stark (Jun 26 2020 at 14:57):

i'm working on it but haven't finished

view this post on Zulip Eric Wieser (Jun 26 2020 at 14:57):

library_search finds nothing at any rate. I'll have a go at proving it myself, and then learn from your simpler proof!

view this post on Zulip Eric Wieser (Jun 26 2020 at 14:57):

Thanks!

view this post on Zulip Scott Olson (Jun 26 2020 at 14:58):

Maybe just call it pairwise_repeat? I think the guidelines only suggest describing the hypotheses in the name if necessary for disambiguation.

view this post on Zulip Jalex Stark (Jun 26 2020 at 14:58):

I think this specific case would not deserve a name, probably one can prove an induction principle so that the proof of this is new_induction_principle; simp

view this post on Zulip Kevin Buzzard (Jun 26 2020 at 14:58):

import tactic

open list

example (X : Type) (x : X) (n : ) (r : X  X  Prop) (hr : r x x) :
  pairwise r (repeat x n) :=
begin
  induction n with d hd,
  { exact pairwise.nil},
  { apply pairwise.cons _ hd,
    intros a ha,
    convert hr,
    exact eq_of_mem_repeat ha,
  }
end

view this post on Zulip Reid Barton (Jun 26 2020 at 15:01):

I suspect you don't even need induction.

view this post on Zulip Kevin Buzzard (Jun 26 2020 at 15:02):

you always need induction

view this post on Zulip Kevin Buzzard (Jun 26 2020 at 15:02):

somewhere

view this post on Zulip Kevin Buzzard (Jun 26 2020 at 15:02):

you'll use a lemma which uses induction :-)

view this post on Zulip Reid Barton (Jun 26 2020 at 15:04):

Looks like the lemma I want to use doesn't quite exist though

view this post on Zulip Kevin Buzzard (Jun 26 2020 at 15:05):

(forall a b in l, a r b) -> pairwise l r

view this post on Zulip Reid Barton (Jun 26 2020 at 15:06):

You could prove it from pairwise.imp_of_mem but pairwise.true is missing too.

view this post on Zulip Reid Barton (Jun 26 2020 at 15:08):

do we know that repeat x n is sorted? this seems like a valid use case

view this post on Zulip Johan Commelin (Jun 26 2020 at 15:08):

Yep, I think sorted_repeat or repeat_sorted exists


Last updated: May 12 2021 at 05:19 UTC