update to Lean 4.16

[cdisselkoen]

Biggest change for us is (quoting from the Lean changelog):

leanprover/lean4#6379 replaces the inductive predicate List.lt with an upstreamed version of List.Lex from Mathlib.
(Previously Lex.lt was defined in terms of <; now it is generalized to take an arbitrary relation.)
This subtly changes the notion of ordering on List α.

List.lt was a weaker relation: in particular if l₁ < l₂, then a :: l₁ < b :: l₂ may hold according to List.lt even if a and b are merely incomparable (either neither a < b nor b < a), whereas according to List.Lex this would require a = b.

When < is total, in the sense that ¬ · < · is antisymmetric, then the two relations coincide.

Mathlib was already overriding the order instances for List α, so this change should not be noticed by anyone already using Mathlib.

We simultaneously add the boolean valued List.lex function, parameterised by a BEq typeclass and an arbitrary lt function. This will support the flexibility previously provided for List.lt, via a == function which is weaker than strict equality.

Separately, Lean introduced its own DecidableLT. For now, to get things working, I kept our DecidableLT and just qualified it as Cedar.Data.DecidableLT when ambiguous. In a future PR we can look at replacing our DecidableLT with the Lean one.

[emina]

I'm guessing this renaming was necessary to avoid a conflict with a newly introduced theorem in Lean?

Can we rename it to List.slt_asymm to be consistent with List.slt_trans (which we also had to rename because of a conflict in the last update)?

[cdisselkoen]

sure. What does the s stand for?

[emina]

Curious why we need to consecutive simp onlys here. Stylistic choice or Lean does the wrong thing if we use a single simp only that calls both sets of theorems?

Edited to add: this is not a blocker, just curiosity :)

[cdisselkoen]

Yes, if we combine it all then Lean throws maximum recursion depth has been reached

[cdisselkoen]

I think that LT.lt and Name.lt recurse infinitely with each other, so those are the two that needed separating