feat: Array.mem: Avoid DecidableEq, set up decreasing_trivial

[nomeata]

The notation a ∈ as for Arrays was previously only defined with
DecidableEq on the elements, for (apparently) no good reason. This
drops this requirements (by using a ∈ as.data), and simplifies a bunch
of proofs by simply lifting the corresponding proof from lists.

Also, sizeOf_lt_of_mem was defined, but not set up to be picked up by
decreasing_trivial in the same way that the corresponding List lemma
was set up, so this adds the tactic setup.

The definition for a ∈ as is intentionally not defeq to a ∈ as.data
so that the termination tactics for Arrays don’t spuriously apply when
recursing through lists.

[nomeata]

awaiting-review

[nomeata]

A first attempt failed tests like

inductive Term where
  | app (f : String) (args : List Term)

def printFns : Term → IO Unit
  | Term.app f args => do
     IO.println f
     for h : arg in args do
       have : sizeOf arg < 1 + sizeOf f + sizeOf args := Nat.lt_trans (List.sizeOf_lt_of_mem h) (by simp_arith)
       printFns arg

where there is not even any Array around.

It seemed that apply Nat.lt_trans (Array.sizeOf_lt_of_mem ?h) could fire due to unwanted defeq between the element-relatio for Array and List. Fixed by making Array.Mem an inductive.

[leanprover-community-mathlib4-bot]

• ✅ Mathlib branch lean-pr-testing-2774 has successfully built against this PR. (2023-10-26 23:50:38) View Log
• ✅ Mathlib branch lean-pr-testing-2774 has successfully built against this PR. (2023-10-27 10:19:15) View Log
• 💥 Mathlib branch lean-pr-testing-2774 build failed against this PR. (2023-10-28 23:22:42) View Log
• ✅ Mathlib branch lean-pr-testing-2774 has successfully built against this PR. (2023-10-29 12:44:26) View Log

[digama0]

You should make it a structure instead of an inductive, assuming def doesn't work (it should work though).

[nomeata]

Will do. Is there a difference between a one field structure and a one field one constructor inductive? Ive seen both patterns so far.

[digama0]

Structures have various additional niceties, I don't see why you would ever not use them unless you don't meet the restrictions. Do you have an example? (The field projection is the main important nicety in this case.)

[nomeata]

I've seen it mostly with rose trees recently:

lean4/src/Lean/Data/PrefixTree.lean

Line 11 in 6c5f79c

inductive PrefixTreeNode (α : Type u) (β : Type v) where

(and similar data structures)

Maybe the benefit of an inductive is that you don't have to think of a name for the projection :-)

[nomeata]

Fixed in 9a7d350, PTAL.

[nomeata]

Squashed.

(And because Github is very strange in that squashing is just one click away when merging, but basically impossible without a laptop and a command line for the PR authors, in the process I wrote half a Github App that squashes PRs… :-)

[digama0]

Maybe the benefit of an inductive is that you don't have to think of a name for the projection :-)

My suggestion would be to just use val for one-field structures, rather than coming up with bespoke names that have to be remembered.

[nomeata]

My suggestion would be to just use val for one-field structures, rather than coming up with bespoke names that have to be remembered.

done