List.destutter'

Stream: mathlib4

[Yury G. Kudryashov]

I'm looking at @Alex Meiburg 's #9082 and I wonder why docs#List.destutter' works as a special case of docs#List.destutter . I think that we'll get better lemmas if we drop a from the answer. What do you think?

[Yury G. Kudryashov]

E.g., with the current definition we have

theorem tail_destutter'_congr (h : ∀ c, R a c ↔ R b c) :
    (l.destutter' R a).tail = (l.destutter' R b).tail := by

and we'll be able to drop tail if we drop the head from the output of List.destutter'.

[Yury G. Kudryashov]

AFAICT, this is an auxiliary definition which is only used to prove properties of List.destutter, so I assume that we can change its definition without worrying about backwards compatibility too much.

[Eric Rodriguez]

Yeah, it was much easier to develop the theory with having destutter' around, much like docs#List.Chain'. At least, that was my experience whilst writing it.

[Yury G. Kudryashov]

Another question: since we don't hardcode R = \ne, should we call it something like List.greedyChain instead of destutter?

[Yury G. Kudryashov]

It can be used, e.g., to construct monotone chains too.

[Yury G. Kudryashov]

Another question: should we rename docs#List.Chain' to Chain and docs#List.Chain to something else?

[Violeta Hernández]

Yury G. Kudryashov said:

Another question: should we rename docs#List.Chain' to Chain and docs#List.Chain to something else?

That would be great, I'm tired of having to fight the docPrime linter every time I write anything involving pairwise relations...

[Violeta Hernández]

Maybe docs#List.Chain can be List.ChainWith?

[Yury G. Kudryashov]

In fact, I don't understand why we need it at all.

[Yury G. Kudryashov]

We can define

def List.IsChain (R : α → α → Prop) (l : List α) : Prop :=
  (l.zipWith R l.tail).Forall

or

def List.IsChain (R : α → α → Prop) (l : List α) : Prop :=
  l.dropLast.Forall₂ R l.tail

[Yury G. Kudryashov]

Then List.Chain' R a l = List.IsChain R (a :: l)

[Violeta Hernández]

Well, List.Chain R a l is already the same as List.Chain' R (a :: l), so its only value is being easier to prove things about

[Violeta Hernández]

The main difference in my experience is that docs#List.chain_cons is nicer than docs#List.chain'_cons or docs#List.chain'_cons'

[Yury G. Kudryashov]

It will become List.isChain_cons_cons.

[Yury G. Kudryashov]

(if we drop one of 2 predicates)

[Violeta Hernández]

Yury G. Kudryashov said:

We can define

def List.IsChain (R : α → α → Prop) (l : List α) : Prop :=
  (l.zipWith R l.tail).Forall

or

def List.IsChain (R : α → α → Prop) (l : List α) : Prop :=
  l.dropLast.Forall₂ R l.tail

These re-definitions seem harder to reason about and possibly worse in terms of performance. What about something like this instead?

inductive List.IsChain (R : α → α → Prop) : List α → Prop
  | nil : List.IsChain R []
  | singleton (a : α) : List.IsChain R [a]
  | cons_cons {a b : α} (l : List α) : R a b → List.IsChain R (b :: l) → List.IsChain R (a :: b :: l)

[Violeta Hernández]

Actually nevermind, performance isn't really a factor here since this is a function into Prop and not into Bool or anything of the sort.

[Violeta Hernández]

Still, I feel an inductive definition is probably going to be the easiest to work with no matter what. We can prove equivalences to the zipWith, etc. definitions separately.

[Kim Morrison]

@Mario Carneiro / @François G. Dorais, any opinions here? If we're going to change the definition of Chain I'd prefer to do to sooner rather than later.

[Yury G. Kudryashov]

We can prove API lemmas starting with any definition. Since it's computationally irrelevant, I don't care much about which one we use.

[Yury G. Kudryashov]

Possibly, an inductive one is better, because Lean won't try to unify it with something else.

[François G. Dorais]

Just to be sure: the two alternatives are?

[Yury G. Kudryashov]

I gave 2 similar definitions of List.IsChain in terms of zipWith, @Violeta Hernández wrote a direct inductive definition. Also, there is a status quo (Chain and Chain').

[Yury G. Kudryashov]

I don't like status quo, because List.Chain R a l is just List.Chain' R (a :: l).

[François G. Dorais]

There seems to be two issues:

• List.Chain : α → List α → Prop is begging for a nonempty list type as input.
• List.Chain': List α → Prop is the right notion for a possibly empty list.

[Violeta Hernández]

There's also the less important but still relevant issue of having a primed name.

[François G. Dorais]

As far as the definitions of List.IsChain, this is probably more efficient:

def List.IsChain (R : α → α → Prop) : List α → Prop
  | [] | [_] => True
  | x::xs@(y::_) => R x y ∧ IsChain R xs

But Violeta's inductive definition is perhaps easier to reason with.

[François G. Dorais]

Violeta Hernández said:

There's also the less important but still relevant issue of having a primed name.

Prime names are convenient in the short term but never good in the long term.

[Violeta Hernández]

François G. Dorais said:

As far as the definitions of List.IsChain, this is probably more efficient:

def List.IsChain (R : α → α → Prop) : List α → Prop
  | [] | [_] => True
  | x::xs@(y::_) => R x y ∧ IsChain xs

But Violeta's inductive definition is perhaps easier to reason with.

I think yours might be better actually, since it makes List.IsChain.cons_cons an iff trivially.

[François G. Dorais]

But "efficiency" is not so relevant unless R is decidable.

[Violeta Hernández]

I think your recursive definition should also make it easier to prove decidability of IsChain (for decidable relations)

[François G. Dorais]

@Kim Morrison I support replacing List.Chain with the current List.Chain'.

[Violeta Hernández]

Pinging @Bhavik Mehta since he recently added some Chain lemmas in one of my PRs for golfing purposes

[François G. Dorais]

@Violeta Hernández But your inductive definition comes with an inductive principle, which is nice to have.

[François G. Dorais]

Note that this is actually tail recursive:

def List.isChain (r : α → α → Bool) : List α → Bool
  | [] | [_] => true
  | x::xs@(y::_) => r x y && isChain r xs

[Yury G. Kudryashov]

Is it? I mean, does Lean treat && so that this definition becomes tail recursive?

[François G. Dorais]

Yes, because && is short circuiting, so if r x y = false then isChain r xs is not evaluated.

[Yury G. Kudryashov]

BTW, can we somehow ask Lean whether it treats a given definition as tail recursive?

[François G. Dorais]

I think Mario wrote some code for that but I just inspect the IR.

[François G. Dorais]

set_option trace.compiler.ir.result true in
def List.isChain (r : α → α → Bool) : List α → Bool
  | [] | [_] => True
  | x::xs@(y::_) => r x y && isChain r xs

The key is at the end:

      Bool.true →
        let x_11 : u8 := List.isChain._rarg x_1 x_4;
        ret x_11

[François G. Dorais]

Found it! https://leanprover.zulipchat.com/#narrow/channel/348111-batteries/topic/tail.20recursion/near/404515501

[Bhavik Mehta]

I find List.Chain useful as it is, I don't think it's just there to make the definition of List.Chain' any easier. Indeed when proving things about lists, I often find myself copying the Chain/Chain' pattern in order to make the proofs go more smoothly, having support to induct on a list without changing its first element is pretty useful! So I'm in favour of keeping it, since I use List.Chain quite a bit more than I use List.Chain'. But really if we keep the induction principles that Chain currently has, phrased in terms of Chain', then I'd be happy too.

[Yury G. Kudryashov]

You can induct on l in IsChain R (a :: l).

[Yury G. Kudryashov]

I'll try to make some proof-of-concept PR tonight or tomorrow.