Zulip Chat Archive

Stream: new members

Topic: list.pairwise of list.repeat

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?

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?

Jalex Stark (Jun 26 2020 at 14:49):

can you state the lemma formally?

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)

Jalex Stark (Jun 26 2020 at 14:50):

also by builtin do you mean available in mathlib?

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.

Jalex Stark (Jun 26 2020 at 14:51):

docs#list.pairwise

Jalex Stark (Jun 26 2020 at 14:52):

the lemma doesn't sound mathematically useful

Jalex Stark (Jun 26 2020 at 14:52):

why do you need it?

Jalex Stark (Jun 26 2020 at 14:52):

#xy

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)

Eric Wieser (Jun 26 2020 at 14:54):

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

Jalex Stark (Jun 26 2020 at 14:55):

it should be an easy list induction

Eric Wieser (Jun 26 2020 at 14:56):

Too "easy" to have a place in mathlib?

Jalex Stark (Jun 26 2020 at 14:57):

not sure yet

Jalex Stark (Jun 26 2020 at 14:57):

i'm working on it but haven't finished

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!

Eric Wieser (Jun 26 2020 at 14:57):

Thanks!

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.

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

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

Reid Barton (Jun 26 2020 at 15:01):

I suspect you don't even need induction.

Kevin Buzzard (Jun 26 2020 at 15:02):

you always need induction

Kevin Buzzard (Jun 26 2020 at 15:02):

somewhere

Kevin Buzzard (Jun 26 2020 at 15:02):

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

Reid Barton (Jun 26 2020 at 15:04):

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

Kevin Buzzard (Jun 26 2020 at 15:05):

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

Reid Barton (Jun 26 2020 at 15:06):

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

Reid Barton (Jun 26 2020 at 15:08):

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

Johan Commelin (Jun 26 2020 at 15:08):

Yep, I think sorted_repeat or repeat_sorted exists

Last updated: Dec 20 2023 at 11:08 UTC