Status of data.list.defs?

Stream: mathlib4

[Arien Malec]

This one shows up in the dependency graph all over the place. It's spuriously "blocked" by RBTree/RBMap, I think (these are now upstream).

When I look at this file, it has a bunch of commented out lines that I haven't investigated -- my supposition is that these are method that are implemented upstream as well?

[Yury G. Kudryashov]

Most of the definitions are in Lean 4 core.

[Yury G. Kudryashov]

The first exception I found was docs#list.nth_le. There is docs4#List.get but it bundles the arguments.

[Yury G. Kudryashov]

So, we need to either introduce List.get' or migrate mathlib to the Lean 4-style API.

[Yury G. Kudryashov]

Also, you can start migrating files that depend on data.list.defs and hope that all the required definitions are in the Std library.

[Scott Morrison]

Let's introduce primed versions to make porting easy. We can eventually add a @[deprecated] tag and do a rename PR.

[Arien Malec]

@Yury G. Kudryashov -- are you working on this? I'm wading through & happy to do the dirty work with you as a reviewer. I'm trying to cross align through name changes, etc.

[Yury G. Kudryashov]

No, I'm not working. I had a look, then decided not to start actual work.

[Arien Malec]

@Yury G. Kudryashov this is ready for review in mathlib4#803

There are still a few typing issues that are eluding me, and some comments I've mostly marked with "porting notes" or "TODO" that might require review.

[Kevin Buzzard]

This branch doesn't compile for me; PermutationsAux.rec can't prove that it terminates and I've just spent over an hour banging my head against a wall trying to figure out how termination_by works :-(

[Mario Carneiro]

what's the declaration?

[Mario Carneiro]

looking at src#list.permutations_aux.rec (which I assume is what you are talking about), it looks like the termination metric is (length l + length i, length l), so something along the lines of termination_by _ ts is => (length ts + length is, length ts) should work

[Mario Carneiro]

FYI, the lean 4 name of that definition should be List.permutationsAux.rec. The permutationsAux part should not be upcased because this is an inner function

[Kevin Buzzard]

Yeah, Scott already observed that in the PR. Your suggestion doesn't work; Lean can't prove the false goal length ts + succ (length is) < succ (length ts) + length is

[Kevin Buzzard]

I'm not sure what the default order is on Nat x Nat but I want to use prod.lex

[Mario Carneiro]

that should be the default order

[Mario Carneiro]

if you want to use a relation directly instead of a type that happens to be well founded, you should use termination_by' (which should have been the output of mathport)

[Kevin Buzzard]

Oh is that actually a thing?

[Kevin Buzzard]

I assumed it was a bug!

[Mario Carneiro]

do you have a MWE?

[Arien Malec]

addressed naming

Working on #mwe

[Kevin Buzzard]

mathlib4#803

[Mario Carneiro]

MWE

[Mario Carneiro]

I assume the declaration on its own works as such

[Mario Carneiro]

since we're talking about data.list.defs here

[Kevin Buzzard]

ironically the only reason I was trying to get this file fixed was to get hold of List.nthLe which doesn't seem to be in this file anyway

[Kevin Buzzard]

Talking of which, has anyone seen List.map₂?

[Mario Carneiro]

what about it?

[Kevin Buzzard]

I was trying to port lean_core.data.vector but it needs List.nthLe and List.map₂

[Mario Carneiro]

that's zipWith isn't it?

[Mario Carneiro]

src#list.map₂ src#list.zip_with

[Arien Malec]

import Std.Data.Nat.Lemmas
open List
open Nat

private def meas : (Σ'_ : List α, List α) → Nat × Nat
  | ⟨l, i⟩ => (length l + length i, length l)

/-- Local notation for termination relationship used in `rec` below
-/
local infixl:50 " ≺ " => InvImage (Prod.Lex (· < ·) (· < ·)) meas

/-- A recursor for pairs of lists. To have `C l₁ l₂` for all `l₁`, `l₂`, it suffices to have it for
`l₂ = []` and to be able to pour the elements of `l₁` into `l₂`. -/
@[elab_as_elim]
def permutationsAux.rec {C : List α → List α → Sort v} (H0 : ∀ is, C [] is)
    (H1 : ∀ t ts is, C ts (t :: is) → C is [] → C (t :: ts) is) : ∀ l₁ l₂, C l₁ l₂
  | [], is => H0 is
  | t :: ts, is =>
    have h1 : ⟨ts, t :: is⟩ ≺ ⟨t :: ts, is⟩ :=
      show Prod.Lex _ _
           (succ (length ts + length is), length ts)
           (succ (length ts) + length is, length (t :: ts)) by
        rw [Nat.succ_add] <;> exact Prod.Lex.right _ (lt_succ_self _)
    have h2 : ⟨is, []⟩ ≺ ⟨t :: ts, is⟩ := Prod.Lex.left _ _ (Nat.lt_add_of_pos_left (succ_pos _))
    H1 t ts is (permutationsAux.rec H0 H1 ts (t :: is)) (permutationsAux.rec H0 H1 is [])
    termination_by'
      ⟨(· ≺ ·), @InvImage.wf _ _ _ meas (Prod.instWellFoundedRelationProd lt_wfRel lt_wfRel)⟩

[Arien Malec]

I think both @Kevin Buzzard and @Ruben Van de Velde have tried to crack this one...

[Mario Carneiro]

def permutationsAux.rec {C : List α → List α → Sort v} (H0 : ∀ is, C [] is)
    (H1 : ∀ t ts is, C ts (t :: is) → C is [] → C (t :: ts) is) : ∀ l₁ l₂, C l₁ l₂
  | [], is => H0 is
  | t :: ts, is =>
    H1 t ts is (permutationsAux.rec H0 H1 ts (t :: is)) (permutationsAux.rec H0 H1 is [])
termination_by _ ts is => (length ts + length is, length ts)
decreasing_by simp_wf; simp [Nat.succ_add]; decreasing_tactic

[Mario Carneiro]

alternatively:

attribute [local simp] Nat.succ_add in
/-- A recursor for pairs of lists. To have `C l₁ l₂` for all `l₁`, `l₂`, it suffices to have it for
`l₂ = []` and to be able to pour the elements of `l₁` into `l₂`. -/
def permutationsAux.rec {C : List α → List α → Sort v} (H0 : ∀ is, C [] is)
    (H1 : ∀ t ts is, C ts (t :: is) → C is [] → C (t :: ts) is) : ∀ l₁ l₂, C l₁ l₂
  | [], is => H0 is
  | t :: ts, is =>
    H1 t ts is (permutationsAux.rec H0 H1 ts (t :: is)) (permutationsAux.rec H0 H1 is [])
termination_by _ ts is => (length ts + length is, length ts)

[Arien Malec]

Now it just doesn't like [elab_as_elim]

[Mario Carneiro]

note that I removed it

[Mario Carneiro]

lean 4 is more picky about elab_as_elim declarations

[Arien Malec]

Will add as porting comment

[Arien Malec]

Where is decreasing_tactic documented? I was so close on this....

[Mario Carneiro]

docs4#tacticDecreasing_tactic

[Mario Carneiro]

basically, if you don't provide a decreasing_by clause then it acts like decreasing_by decreasing_tactic, which calls simp and a few other simple things for reducing common WF proof goals

[Mario Carneiro]

and if it fails it prints the big error message you can see at src4#tacticDecreasing_with_

[Arien Malec]

The last issue here is making my eyes cross:

import Std.Data.Nat.Lemmas

open List
open Nat

def permutationsAux2 (t : α) (ts : List α) (r : List β) : List α → (List α → β) → List α × List β
  | [], _ => (ts, r)
  | y :: ys, f =>
    let (us, zs) := permutationsAux2 t ys r ys (fun x: List α => f (y :: x))
    (y :: us, f (t :: y :: us) :: zs)

/-- A recursor for pairs of lists. To have `C l₁ l₂` for all `l₁`, `l₂`, it suffices to have it for
`l₂ = []` and to be able to pour the elements of `l₁` into `l₂`. -/
def permutationsAux.rec {C : List α → List α → Sort v} (H0 : ∀ is, C [] is)
    (H1 : ∀ t ts is, C ts (t :: is) → C is [] → C (t :: ts) is) : ∀ l₁ l₂, C l₁ l₂
  | [], is => H0 is
  | t :: ts, is =>
    H1 t ts is (permutationsAux.rec H0 H1 ts (t :: is)) (permutationsAux.rec H0 H1 is [])
  termination_by _ ts is => (length ts + length is, length ts)
  decreasing_by simp_wf; simp [Nat.succ_add]; decreasing_tactic


/-- An auxiliary function for defining `permutations`. `permutations_aux ts is` is the set of all
permutations of `is ++ ts` that do not fix `ts`. -/
def permutationsAux : List α → List α → List (List α) :=
  @permutationsAux.rec (fun _ _ => List (List α)) (fun is => []) fun t ts is IH1 IH2 =>
    foldr (fun y r => (permutationsAux2 t ts r y id).2) IH1 (is :: IH2)

The fun _ _ => List (List α) bit is a direct translation from mathlib, but fails here with what looks like a universe issue:

application type mismatch
  @permutationsAux.rec fun x x ↦ List (List α)
argument
  fun x x ↦ List (List α)
has type
  (x : ?m.45085) → ?m.45092 x → Type ?u.45055 : Sort (max (max ?u.45084 ?u.45087) (?u.45055 + 2))
but is expected to have type
  Type ?u.45082 : Type (?u.45082 + 1)

If I provide more inference hints ((fun (xs: List α) (ys: List α) => List (List α))), I get a different type issue:

application type mismatch
  @permutationsAux.rec fun xs ys ↦ List (List α)
argument
  fun xs ys ↦ List (List α)
has type
  List α → List α → Type ?u.45055 : Type (?u.45055 + 1)
but is expected to have type
  Type ?u.45082 : Type (?u.45082 + 1)

where we are in the same universe at least.

[Arien Malec]

The more that I look at that fun the less I understand what it even wants to do

[Arien Malec]

Or how it was supposed to work in Lean 3 -- it looks like I'm taking two lists and producing a type...

[Scott Morrison]

I think there are just earlier arguments that you need to specify if you're using @?

[Arien Malec]

That did it!

/-- An auxiliary function for defining `permutations`. `permutations_aux ts is` is the set of all
permutations of `is ++ ts` that do not fix `ts`. -/
def permutationsAux : List α → List α → List (List α) :=
  permutationsAux.rec (fun _ => []) fun t ts is IH1 IH2 =>
    foldr (fun y r => (permutationsAux2 t ts r y id).2) IH1 (is :: IH2)
#align list.permutations_aux List.permutationsAux