How should I prove index in bounds?

Stream: new members

[R Dong]

I'm trying to use the indexing functions on Lists/Arrays, but I keep getting stuck on how to make the proofs. For instance, I can do this:

def xid (xs : List Nat) (id : Nat) (h : id < xs.length) : Nat :=
  xs[id]

But what about something like this?

def xids (xs : List Nat) (ids : List Nat) (h : sorry) : Nat :=
  ids.foldl (fun id => xid xs id ???) xs

And how about generating the ids?

opaque get_some_ids : List Nat -> List Nat
axiom ids_valid (xs : List Nat) : ∀ id ∈ get_some_ids xs, id < xs.length

I can't seem to connect them.

[Henrik Böving]

I would suggest using ids.attach.foldl and then working with what List.attach gives you

[R Dong]

I tried to understand where to use it, but I didn't figure it out

[Henrik Böving]

You can for example write something like:

def xid (xs : List Nat) (id : Nat) (h : id < xs.length) : Nat :=
  xs[id]

def xids (xs : List Nat) (ids : List Nat) (h : ∀ i ∈ ids, i < xs.length) : Nat :=
  ids.attach.foldl (init := 0) (fun acc ⟨id, h2⟩ => acc + xid xs id (h _ h2))

[R Dong]

The second argument doesn't seem to be a tuple?

type mismatch
  (id, h2)
has type
  ?m.3102 × ?m.3105 : Type (max ?u.3108 ?u.3107)
but is expected to have type
  { x // x ∈ ids } : Type

[Henrik Böving]

Yes, note that I didn't use normal tuple but angle brackets

[R Dong]

Oh, I didn't notice that

[R Dong]

But now I have this:

function expected at
  xid xs id
term has type
  ℕ

[R Dong]

Ah, I made the xid take an implicit h, that was why

[R Dong]

So, what does this notation mean: {x // x ∈ l}, is it an anonymous struct?

[Edward van de Meent]

i'm pretty sure it is notation for Subtype (. \in l)

[Edward van de Meent]

it pretends to be mathematical set notation

[R Dong]

Hmmm, but then why can I destructure with the angle brackets

[Edward van de Meent]

because docs#Subtype is a structure.