feat: DepArray

[JamesGallicchio]

Dependent array -- the types of each element can depend on the index.

This is a very minimal proof of concept implementation, but a DepArray would fit nicely in a hierarchy of array primitives "lower" than the built-in Array. It is a generalization of SciLean.Data.ArrayN and LeanColls.ArrayUninit.

It is also useful for caching dependent functions over FinEnum domains, which is my use case.

[digama0]

Just FYI, axiom is forbidden in std, it can't be merged as is.

[JamesGallicchio]

Understandable. I'd rather push for Erased to be supported in core; perhaps for now we replace it with a sigma type and pretend it has no overhead? :-)

[fgdorais]

Perhaps only Inhabited types should be erasable, that way you can use partial instead of axiom.

[digama0]

Here's a proof that this axiom is false:

import Mathlib.SetTheory.Cardinal.Ordinal

namespace Std.TypeErased

structure Intf.{u} where
  TypeErased : Type u
  type : TypeErased → Type u
  proj (t : TypeErased) : type t
  inj : α → TypeErased
  type_inj (a : α) : type (inj a) = α
  proj_inj (a : α) : proj (inj a) = cast (type_inj a).symm a

open Order Cardinal Function in
example : ¬ Nonempty (TypeErased.Intf.{u})
  | ⟨{ TypeErased, type, inj, type_inj, .. }⟩ => by
    have a (c : Cardinal.{u}) : (succ c).out :=
      (mk_ne_zero_iff.1 (mk_out _ ▸ succ_ne_zero _)).some
    let F (c) := inj (a c)
    have {c} : (#type (F c)) = succ c := type_inj _ ▸ mk_out _
    have : Injective F := fun a b h => succ_injective <|
      this.symm.trans <| (congrArg (#type ·) h).trans this
    have := lift_mk_le.{u+1}.2 ⟨⟨_, this⟩⟩
    rw [lift_id, mk_cardinal, ← not_lt] at this
    exact this (lift_lt_univ _)