Chain and Chain' and Pairwise

Stream: batteries

[Wrenna Robson]

I'm going to ask this here because List.Chain and List.Chain' live in batteries nowadays. I sort of asked this in an oblique way this morning but I think it's better here more directly.

a) Can we come up with a better name than Chain' for Chain'? I understand why one might want both, but on the other hand Chain' could just do everything. Having done a search this discussion has come up a couple of times in the past, but I am interested in people's thoughts.
b) Would there be value in having a chain Bool-valued predicate, something like:

def chain : List α → (α → α → Bool) → Bool
  | [], _ => true
  | [_], _ => true
  | x :: y :: t, R => R x y && chain (y :: t) R

Notably for a transitive predicate this does efficiently calculate whether the list is sorted according to it! You could also have chainM in the same way as anyM.
c) In a similar vein, would there be any interest in something like

def pairwise : List α → (α → α → Bool) → Bool
  | [], _ => true
  | x :: t, R => t.all (R x ·) && t.pairwise R

d) In a similar similar vein, one could define these for Arrays - in particular, one could define them efficienctly a la how Array.anyM etc. are done, rather than Array.Pairwise which just defers it to the list representation. I have done this but it's a bit long so I won't post it here.
e) I am not really sure if these things should do in core, Batteries, or even Mathlib (though I feel like surely not). I don't quite get why List.Pairwise is in core but List.Chain is in Batteries! So I would appreciate some help understanding the rationale here.

[François G. Dorais]

a) Unfortunately, batteries#1052 has gone stale. You could ask the author if you can help reviving it.

b,c) Makes sense. A Decidable instance is probably enough. Batteries tries to make sure these instances have efficient implementations, which probably amounts to your chain and pairwise.

d) That makes sense too. I would recommend a separate PR though.

e) "Keeping similar things together" is not a primary concern for the separation between core, Std and Batteries. Core and Std have interest in keeping their API surface small. As a rule of thumb, if it's not essential for Lean itself then core won't take it. Similarly, if it's not essential for the Lean programming language, then Std won't take it. Batteries is more welcoming but anything that is not useful for Lean programming per se probably belongs in Mathlib.

[Kim Morrison]

François G. Dorais said:

probably belongs in Mathlib

... if it is useful for doing mathematics.

[Kim Morrison]

I'd be happy to see Chain filled out for Array and Vector! I'd recommend Batteries for now.

[François G. Dorais]

Another clarification regarding e) I don't think it's the PR author's sole responsibility to decide where their contributions belong. It is especially discouraged to split PRs because some part belongs here and the other belongs there. In case of doubt, the default should be to send to Batteries. If that's not the right place, maintainers will point to the appropriate location. If it's more complicated than that, the FRO has qualified (and paid) staff to help with that; Batteries maintainers will also gladly help pinging the right people for this kind of surgery.

[Wrenna Robson]

Why is Pairwise essential for Lean programming? I don't deny that it is to be clear, I'm sure it comes up, but I don't know where that would be.

[Wrenna Robson]

François G. Dorais said:

a) Unfortunately, batteries#1052 has gone stale. You could ask the author if you can help reviving it.

b,c) Makes sense. A Decidable instance is probably enough. Batteries tries to make sure these instances have efficient implementations, which probably amounts to your chain and pairwise.

d) That makes sense too. I would recommend a separate PR though.

e) "Keeping similar things together" is not a primary concern for the separation between core, Std and Batteries. Core and Std have interest in keeping their API surface small. As a rule of thumb, if it's not essential for Lean itself then core won't take it. Similarly, if it's not essential for the Lean programming language, then Std won't take it. Batteries is more welcoming but anything that is not useful for Lean programming per se probably belongs in Mathlib.

Why do we have in some cases things like List.all/any, which is bool-valued, and in other cases we just use Decidable?

[Robin Arnez]

Wrenna Robson schrieb:

Why is Pairwise essential for Lean programming?

Well, it's maybe not essential for programming but it is a dependency of the hash maps and tree maps and thus needs to be in core. (I'm not sure this is how it got into core, it might have been there before, but that's at least one use case)

[Wrenna Robson]

Aha

[Wrenna Robson]

Did we have any insights on Chain versus Chain'? I am still kinda of the view that the current state of affairs there is non-ideal.

[Wrenna Robson]

But maybe I'm missing something.

[Robin Arnez]

I'm fine with the Decidable instances using this separation of [] and a :: as on the top level and then doing it like the current Chain since that reduces the amount of destructuring operations but I'm not sure whether it's worth actually separating them out into different predicates. I'd done something like:

inductive List.IsChain (r : α → α → Prop) : List α → Prop where
  | nil : IsChain r []
  | singleton (a : α) : IsChain r [a]
  | cons (hr : r a b) (h : IsChain r (b :: l)) : IsChain r (a :: b :: l)

instance instDecidableIsChain (r : α → α → Prop) [h : DecidableRel r] (l : List α) : Decidable (List.IsChain r l) :=
  match l with
  | [] => .isTrue .nil
  | a :: l => go a l
where
  go (a : α) (l : List α) : Decidable (List.IsChain r (a :: l)) :=
    match l with
    | [] => .isTrue (.singleton a)
    | b :: l' =>
      match h a b with
      | .isFalse h' => .isFalse (fun | .cons hr _ => absurd hr h')
      | .isTrue h' =>
        @decidable_of_decidable_of_iff _ _ (go b l') ⟨.cons h', fun | .cons _ h'' => h''⟩

[Wrenna Robson]

So IsChain here replaces the current Chain and Chain'?

[Robin Arnez]

Yeah, List.Chain' becomes List.IsChain and List.Chain r a l becomes List.IsChain r (a :: l)

[Wrenna Robson]

That does feel better. Why the change to IsChain instead of Chain?

[Robin Arnez]

No idea, got inspired by batteries#1052?

[Robin Arnez]

I guess that also allows us to do more proper deprecation without suddenly changing the meaning of something

[Wrenna Robson]

Yes true

[Wrenna Robson]

Why is it you use go rather than an extra match case in the top level match?

[Wrenna Robson]

Does it give some computational advantage?

[Robin Arnez]

Yeah, because otherwise you have to match twice on every list

[Wrenna Robson]

Oh, wheras this way you only do one match because go is compiled into a function, or something?

[Robin Arnez]

Right, the code generated looks like

    def instDecidableIsChain._redArg (x_1 : obj) (x_2 : tobj) : u8 :=
      case x_2 : tobj of
      List.nil →
        ...
      List.cons →
        ...
        let x_6 : u8 := instDecidableIsChain.go._redArg x_1 x_4 x_5;
        ret x_6

    def instDecidableIsChain.go._redArg (x_1 : obj) (x_2 : tobj) (x_3 : tobj) : u8 :=
      case x_3 : tobj of
      List.nil →
        ...
      List.cons →
        ...
        let x_7 : tagged := app x_1 x_2 x_5;
        let x_8 : u8 := unbox x_7;
        case x_8 : u8 of
        Bool.false →
          ...
        Bool.true →
          let x_10 : u8 := instDecidableIsChain.go._redArg x_1 x_5 x_6;
          ret x_10

while the other one would look like:

    def instDecidableIsChain2._redArg (x_1 : obj) (x_2 : tobj) : u8 :=
      case x_2 : tobj of
      List.nil →
        ...
      List.cons →
        ...
        case x_5 : tobj of
        List.nil →
          ...
        List.cons →
          ...
          let x_8 : tagged := app x_1 x_4 x_7;
          let x_9 : u8 := unbox x_8;
          case x_9 : u8 of
          Bool.false →
            ...
          Bool.true →
            let x_11 : u8 := instDecidableIsChain2._redArg x_1 x_5;
            case x_11 : u8 of
            Bool.false →
              ret x_11
            Bool.true →
              ret x_6

[Wrenna Robson]

Got it.

[Wrenna Robson]

I hadn't appreciated there was a meaningful difference computationally there.

[Wrenna Robson]

Hmm. So you can decide IsChain R [] or IsChain R [a] even when R isn't decidable, right? Is there a way to register that? Is that a bad idea?

[Wrenna Robson]

instance instDecidableIsChainNil : Decidable ([].IsChain R) := .isTrue .nil
instance instDecidableIsChainSingleton (a : α) : Decidable ([a].IsChain R) :=
  .isTrue <| .singleton a

Like we also have these.

[Robin Arnez]

I guess but what would be the use case?

[Robin Arnez]

When you write if h : [].IsChain R then you could've also just omitted the if

[Wrenna Robson]

True

[Wrenna Robson]

(As an aside, arguably List.Forall should also be in batteries under a similar rationale and more clearly linked to List.all. We have List.Forall₂ in batteries!)

[Wrenna Robson]

I have a slight adapation: what do you think of this?

inductive IsChain : List α → Prop where
  /-- A list of length 0 is a chain. -/
  | nil : IsChain []
  /-- A list of length 1 is a chain. -/
  | singleton (a : α) : IsChain [a]
  /-- If `a` relates to `b` and `b::l` is a chain, then `a :: b :: l` is also a chain. -/
  | cons (hr : R a b) (h : IsChain (b :: l)) : IsChain (a :: b :: l)

@[simp] theorem isChain_nil : IsChain R [] := .nil
@[simp] theorem isChain_singleton : IsChain R [a] := .singleton a
@[simp] theorem isChain_cons₂ : IsChain R (a :: b :: l) ↔ R a b ∧ IsChain R (b :: l) :=
  ⟨fun | .cons hr h => ⟨hr, h⟩, fun ⟨hr, h⟩ => .cons hr h⟩

instance instDecidableIsChain [h : DecidableRel R] (l : List α) : Decidable (l.IsChain R) :=
  match l with
  | [] => isTrue .nil
  | a :: l => go a l
  where
    go (a : α) (l : List α) : Decidable ((a :: l).IsChain R) :=
      match l with
      | [] => isTrue <| .singleton a
      | b :: l => haveI := (go b l); decidable_of_iff'  _ (isChain_cons₂ _)

[Wrenna Robson]

Basically I think we want these simp lemmas and then once you have them it makes sense to use them in the decidability proof I think.

[Robin Arnez]

Seems good, the code generated seems to be the same

[Wrenna Robson]

Though possible these lemmas should go in Data.List.Lemmas, in which case we should indeed use your version.

[Wrenna Robson]

But I tend to like putting them here.

[Wrenna Robson]

Incidentally: when I change my cases in my match statement, VScode or Lean (not sure which is messing up) flags a syntax error for the wrong cases which goes away if I refresh the page or cut/paste the problematic part, causing a recheck

[Wrenna Robson]

Which suggests some kind of bug I think?

[Wrenna Robson]

I've created batteries#1421. This is the first time I've done work in batteries that requires changes in mathlib, so bear with me on that: do I want to get it fully reviewed in batteries first and then make the changes downstream?

[Wrenna Robson]

Also if this does pass review, batteries#1052 can be dropped.

[Wrenna Robson]

@Robin Arnez would you be able to review first of all?

[Robin Arnez]

Yeah, I'll take a look

[Wrenna Robson]

Thanks. I've included lemmas that seemed analogous to ones we have for Pairwise in core or batteries, but ultimately it is to taste a little. It is possible that there are lemmas for Chain or Chain' in Mathlib that should move over (or vice versa).

[Aaron Liu]

Wrenna Robson said:

Incidentally: when I change my cases in my match statement, VScode or Lean (not sure which is messing up) flags a syntax error for the wrong cases which goes away if I refresh the page or cut/paste the problematic part, causing a recheck

This happens to me too it doesn't impact my work but is annoying

[Wrenna Robson]

Yeah it's a small thing but annoying.

[Wrenna Robson]

For the mathlib fixing, there's no cache availiable - does that mean that I need to build mathlib by hand?

[Robin Arnez]

Really? Are you on the right branch?

[Wrenna Robson]

I think so?

[Wrenna Robson]

nightly-testing/batteries-pr-testing-1421 (or, well, my local copy).

[Wrenna Robson]

Possibly I have misconfigured something?

[Wrenna Robson]

I did update the copy of batteries so it was my most recent commit which I guess probably broke something.

[Wrenna Robson]

I don't know if I'm meant to upload those manually or if CI handles it.

[Robin Arnez]

Well, I get 1709/7224 files in cache, you get nothing?

[Wrenna Robson]

Yes. Is that with batteries updated or as it was when it was first pushed.

[Robin Arnez]

Oh it might've not updated yet

[Wrenna Robson]

Yeah IDK how that works :)

[Robin Arnez]

Just lake update seemed to work

[Robin Arnez]

You might need to pull that branch now

[Wrenna Robson]

DId you have to change the json file?

[Wrenna Robson]

lake-manifest.json, I mean.

[Robin Arnez]

No, just lake update

[Robin Arnez]

It changes it automatically

[Wrenna Robson]

Huh. That feels unexpected. OK.

[Wrenna Robson]

Right, got it. Where is the CI for the Mathlib build?

[Robin Arnez]

Just on the commits in https://github.com/leanprover-community/mathlib4-nightly-testing/tree/batteries-pr-testing-1421

[Wrenna Robson]

I don't have the rights to push to nightly-testing - should I push to my own mathlib fork and create a PR?

[Robin Arnez]

Yeah, you can make a PR and I can then just merge it

[Robin Arnez]

I took care of some of the simpler stuff (which you might need to pull) but I'll let you do everything in Mathlib.Data.List.Chain

[Wrenna Robson]

OK, I have created #29809

[Robin Arnez]

Wrong target, you need to put it to leanprover-community/mathlib-nightly-testing:batteries-pr-testing-1421 (might need to do manually)

[Wrenna Robson]

I am trying to manually create the PR but I can't fill in leanprover-community/mathlib-nightly-testing into the base repo..

[Wrenna Robson]

Oh it's mathlib4-nightly-testing, isn't it?

[Wrenna Robson]

Still can't see it though.

[Robin Arnez]

Oh, my bad

[Robin Arnez]

Does this work? https://github.com/leanprover-community/mathlib4-nightly-testing/compare/batteries-pr-testing-1421...linesthatinterlace:mathlib4:batteries-pr-testing-1421

[Wrenna Robson]

Yes!

[Wrenna Robson]

OK so I have mathlib4-nightly-testing#70

[Wrenna Robson]

Does that look correct?

[Wrenna Robson]

Why didn't I want to create a regular Mathlib PR?

[Robin Arnez]

Because regular mathlib doesn't have your batteries version?

[Wrenna Robson]

Right... but the batteries version is specified by the lakefile

[Wrenna Robson]

Which the PR updates!

[Wrenna Robson]

I'm going off the workflow described here: https://github.com/leanprover-community/batteries/

[Robin Arnez]

Yeah, I mean you can't just PR something to mathlib that adds https://github.com/linesthatinterlace/batteries to the lakefile

[Wrenna Robson]

No I know.

[Wrenna Robson]

The README explains this.

[Wrenna Robson]

Mathlib Adaptations

Batteries PRs often affect Mathlib, a key component of the Lean ecosystem.
When Batteries changes in a significant way, Mathlib must adapt promptly.
When necessary, Batteries contributors are expected to either create an adaptation PR on Mathlib, or ask for assistance for and to collaborate with this necessary process.

Every Batteries PR has an automatically created Mathlib branch called batteries-pr-testing-N where N is the number of the Batteries PR.
This is a clone of Mathlib where the Batteries requirement points to the Batteries PR branch instead of the main branch.
Batteries uses this branch to check whether the Batteries PR needs Mathlib adaptations.
A tag builds-mathlib will be issued when this branch needs no adaptation; a tag breaks-mathlib will be issued when the branch does need an adaptation.

The first step in creating an adaptation PR is to switch to the batteries-pr-testing-N branch and push changes to that branch until the Mathlib CI process works.
Changes to the Batteries PR will be integrated automatically as you work on this process.
Do not redirect the Batteries requirement to main until the Batteries PR is merged.
Please ask questions to Batteries and Mathlib maintainers if you run into issues with this process.

When everything works, create an adaptation PR on Mathlib from the batteries-pr-testing-N branch.
You may need to ping a Mathlib maintainer to review the PR, ask if you don't know who to ping.
Once the Mathlib adaptation PR and the original Batteries PR have been reviewed and accepted, the Batteries PR will be merged first. Then, the Mathlib PR's lakefile needs to be repointed to the Batteries main branch: change the Batteries line to

require "leanprover-community" / "batteries" @ git "main"

Once CI once again checks out on Mathlib, the adaptation PR can be merged using the regular Mathlib process.

[Wrenna Robson]

So I was just going to change the lakefile once it was done.

[Wrenna Robson]

But this does seem to assume you're doing a regular Mathlib PR to do the adaption.

[Robin Arnez]

Yeah, right... but you don't have access to the batteries-pr-testing-N branch

[Wrenna Robson]

Well I have access to my one.

[Robin Arnez]

Hmm yeah it seems like this description doesn't incorporate the new PR from fork model

[Wrenna Robson]

That is what I was wondering.

[Wrenna Robson]

It is not a super clear process but on the "PR from fork" model I feel like #29809 would have been fine (it just couldn't have actually merged until the batteries PR merged, which is fine).

[Robin Arnez]

Hmm yeah you might be right

[Robin Arnez]

I guess you just don't get a builds-mathlib conformation then?

[Wrenna Robson]

Yeah I'm not sure how that part is meant to work.

[Robin Arnez]

Well, we can probably work with how it is now; once you get a clean build, I'll merge and then we can look from there

[Wrenna Robson]

The nightly testing PR?

[Robin Arnez]

I guess?

[Wrenna Robson]

OK :). Worse comes to worst I can put it somewhere else

[Mario Carneiro]

Wrenna Robson said:

(As an aside, arguably List.Forall should also be in batteries under a similar rationale and more clearly linked to List.all. We have List.Forall₂ in batteries!)

List.Forall deliberately doesn't exist, you are supposed to use ∀ x ∈ l, p x

[Wrenna Robson]

Right! Somewhat confusing that it does exist in Mathlib but I do see why that's better.

[Wrenna Robson]

@Robin Arnez It was a bit of work, but Data/List/Chain is cleaned up, I just pushed it. Let's see where that gets us.

[Robin Arnez]

Hmm seems lika Data.List.Chain works now but there are at least 8 new files with problems

[Wrenna Robson]

About what I expected :) - But I'm done for the day I think. Feel free though to look at the other files - my hope is that they will be more minor adapations

[Wrenna Robson]

@Robin Arnez god willing, the latest push to mathlib4-nightly-testing#70 ought to fix it.

[Violeta Hernández]

I'm really happy to see Chain and Chain' merged into one. I've always figured the former should have been an implementation detail at most.

[Wrenna Robson]

We're not there yet but it's getting there.

[Wrenna Robson]

Something is going wrong with the cache uploading which is substantially slowing matters.

[François G. Dorais]

Wrenna Robson said:

Something is going wrong with the cache uploading which is substantially slowing matters.

Could you make an issue about that? I've noticed this but I think my maintainer privileges prevent me from fully experiencing the issue.

[Wrenna Robson]

Where ought that to be?

[François G. Dorais]

Batteries for now. We'll retarget once the issue has been narrowed down.

[Wrenna Robson]

Righto.

[François G. Dorais]

Thanks!

[Robin Arnez]

There are also a few existing discussions about similar problems I believe

[François G. Dorais]

Yes, but no significant progress there either AFAIK.

[Robin Arnez]

Yeah, right. I think this might be a problem specifically (or at least primarily) for PRs

[François G. Dorais]

I think we need a CI guru to look into this.

[Wrenna Robson]

https://github.com/leanprover-community/batteries/issues/1425

[Wrenna Robson]

I have a religious holiday tomorrow and this issue has made my tidying up take much longer than it ought to have,

[Wrenna Robson]

and then I have other things to do.

[Wrenna Robson]

So if my final push hasn't fixed all the little issues that would be SO much easier to fix if I had a full cache to work with...

[Wrenna Robson]

It's going to have to wait, or someone take on getting it over the line.

[Wrenna Robson]

Ah so the good news is we are good! Building Mathlib finally and I've addressed all the comments on the batteries PR. I'm not sure if I now want to consider moving my Mathlib PR over to the main branch or what.

[Wrenna Robson]

Basically not sure how this landing part works

[Kim Morrison]

Can someone open the Mathlib PR, please?

[Kim Morrison]

i.e. there needs to be a PR in which you've run lake update, and fixed the problems from these deprecations.

[Kim Morrison]

My preference is that when we know that an adaptation is needed, we don't merge the Batteries PR until the corresponding Mathlib PR actually exists (although that PR will need to point Mathlib's lakefile to the Batteries PR branch, and this will then subsequently need to be updated before the Mathlib PR can be merged).

Having this PR open, and linked to from the Batteries PR, means we're not stuck in this situation where nightly-testing isn't working, but I need to wait on someone else before fixing it.

[Kim Morrison]

Also, I see that this PR was merged despite open review comments from @Robin Arnez. What is the status of these? Do they need to be addressed in a follow-up PR?

[Wrenna Robson]

@Kim Morrison hi Kim. Apologies for the confusion here: I was not expecting people to merge stuff before I came back from Rosh HaShanah.

There was some confusion about whether it needs to be a Mathlib PR or a Mathlib Nightly PR. I've done the latter and that exists with the required adaptions - I did open the former but I was told that was wrong? If I'm honest the guidance wasn't entirely clear to me. I'm happy to open one and migrate my branch over, if I can manage that.

[Wrenna Robson]

I'm not sure what the open comments from Robin Arnez were. I don't remember seeing those on Monday - when were they made?

[Robin Arnez]

I've opened #29928 now

[Robin Arnez]

I've opened review comments shortly before the PR was merged, they are not urgent though and are more style-related, we could address them in a follow-up

[Wrenna Robson]

Read your comments now. I don't disagree with what you're saying but happy I think it probably can be addressed in a future PR. The need for isChain_cons* was that I was worrying I'd been too overzealous in regressing previous lemmas and I had a couple places in Mathlib where it was easier to just drop that in. But it ought to be fixable.

[Kim Morrison]

Robin Arnez said:

I've opened #29928 now

Unfortunately there are significant conflicts with master.

[Wrenna Robson]

Oh dear.

[Wrenna Robson]

I see the build is failing as well, even after all the work in mathlib4-nightly-testing#70?

[Wrenna Robson]

Assuming #29928 brings that over.

[Wrenna Robson]

I'm not sure I'll be able to contribute to this either as I don't think I have permissions to push to someone else's PR.

[Kim Morrison]

Wrenna Robson said:

There was some confusion about whether it needs to be a Mathlib PR or a Mathlib Nightly PR.

It needs to be a PR against Mathlib master. The branch lives on the mathlib4-nightly-testing fork for convenience (we don't give out write access to the main repo, but it's helpful if Batteries contributors can be given access to these branches).

[Kim Morrison]

Wrenna Robson said:

I'm not sure I'll be able to contribute to this either as I don't think I have permissions to push to someone else's PR.

You can make a PR to the PR.

[Wrenna Robson]

Thanks Kim - that was what I originally started with :S

[Kim Morrison]

#29928 is made directly from the batteries-pr-testing-1421 branch. So you just need to keep pushing to that!

[Kim Morrison]

(which I think you already have permission to do, right?)

[Wrenna Robson]

I think so. I have been pushing to a branch on my fork I think?

[Wrenna Robson]

This is all slightly beyond what I've done with Git before because I'm juggling like three remotes. So it's very possible I've misconfigured something.

[Wrenna Robson]

I'm still on the way into work but I'll look at this ASAP.

[Wrenna Robson]

That'll be on my work computer though which I wasn't on before, so I guess I'll have to set it up. A guide would be somewhat useful.

[Wrenna Robson]

Set it up for working on this branch I mean.

[Robin Arnez]

Fixed the merge conflicts and updated to the right batteries revision, so let's see how the build goes

[Wrenna Robson]

Aha

[Wrenna Robson]

We are looking good!

[François G. Dorais]

@Kim Morrison That process makes sense but it's very different from what we used to do!

I merged Wrenna's PR into batteries-pr-testing-1421 and then I merged the PR into Batteries right after the CI passed at timestamp 2025-09-23 14:16:45. How did CI on batteries-pr-testing-1421 fail after that?

PS: Robin's last comments were posted in the split second between the time I checked that batteries-pr-testing-1421 passed CI and pressed the button to put the PR in the merge queue. What luck!

[Wrenna Robson]

I think because it wasn't fully merged into master and that broke things - as far as I can tell fixing the merge conflicts appears to have made things fine.

[Wrenna Robson]

My experience of this was that contributing to batteries is relatively user-friendly but specifically adapting Mathlib is a somewhat trickier process. But I suspect there's some easy wins in terms of making the process clear and consistent! :)

[François G. Dorais]

You're one of the first outside PRs we've had that needed significant Mathlib adaptation since Mathlib switched to using forks. So you're unfortunately the guinea pig for that new process.

[Wrenna Robson]

I am chill and happy. These things take time and everyone is patient for the most part.

[Wrenna Robson]

#29928 looks good to go incidentally from my eye.

[François G. Dorais]

I made minor edits to the Mathlib adaptation process: batteries#1428

[Bryan Gin-ge Chen]

#29928 looks like it still needs a few more fixes, but I'm happy to merge once it's green.

[Wrenna Robson]

Yes, it looks like Rob has been improving my adapation (which makes sense, I was just trying to get it working without too much concern for doing so in the best way).

[Wrenna Robson]

Incidentally, @Robin Arnez IDK what you think, but at some point after this as a Mathlib PR I think we should kill off destutter' and integrate it into destutter in pretty much exactly the same way.

[Wrenna Robson]

/--
A recursion principle for lists which separates the singleton case.
-/
@[elab_as_elim]
def twoStepInduction {motive : (l : List α) → Sort*} (nil : motive [])
    (singleton : ∀ x, motive [x])
    (cons_cons : ∀ x y xs, motive xs → (∀ y, motive (y :: xs)) → motive (x :: y :: xs))
    (l : List α) : motive l := match l with | [] => nil | y :: l => go y l
  where
    go (y : α) (l : List α) : motive (y :: l) :=
    match l with
    | [] => singleton y
    | x :: xs =>
      cons_cons y x xs (twoStepInduction nil singleton cons_cons xs) (fun y => go y xs)

Also: is this a better implementation of twoStepInduction? I am wondering in particular for defining stuff, analogous to your approach for the decidable instance.

[Robin Arnez]

Why did you introduce IsChain.concat_induction?

[Wrenna Robson]

I think it may have been an overabundance of enthusiasm.

[Robin Arnez]

Heh I guess you wanted symmetry for backwards_cons_induction and cons_induction

[Robin Arnez]

I'll remove them for now

[Robin Arnez]

Actually, I don't quite know what to do with this situation... I guess we can keep them? idk

[Wrenna Robson]

Oh! Yes that is what it was.

[Wrenna Robson]

Putting aside the annoying fact that concat does not refer to List.concat, because the standard spelling is l ++ [a]...

[Wrenna Robson]

Wrenna Robson said:

Also: is this a better implementation of twoStepInduction? I am wondering in particular for defining stuff, analogous to your approach for the decidable instance.

[Wrenna Robson]

Any thoughts on this?

[Robin Arnez]

I guess if you would use this to write definitions, it would be a bit faster; but I feel like it would be over-kill to care about these details -- I wouldn't expect people to define functions through such a function usually anyway.

[Wrenna Robson]

I do this <_< - but perhaps it is a bad habit.

[Robin Arnez]

Can you give an example?

[Wrenna Robson]

Something like:

instance instDecidableIsChain {R : α → α → Prop} [h : DecidableRel R] (l : List α) :
    Decidable (l.IsChain R) := l.twoStepInduction
    (isTrue .nil)
    (fun a => isTrue <| .singleton a)
    (fun _ y _ _ rec => haveI := (rec y); decidable_of_iff' _ isChain_cons_cons)

[Wrenna Robson]

Let's use this thread to collect any further cleanup that is needed:

[Wrenna Robson]

docs#Acc.list_chain' and docs#WellFounded.list_chain look like they could do with name changes?

[Wrenna Robson]

Not sure if we introduced this but: "This file provides basic results about List.IsChain from betteries." -> batteries

[Wrenna Robson]

Also I just started this thread which is outside the scope of this discussion but is related.

[Wrenna Robson]

#mathlib4 > The Sorted predicate. @ 💬