Converting from relation prop to list mapping

Stream: new members

[aron]

I've got this type that represents a mapping from one list to another according to some relation prop p : α → β → Prop:

inductive ListMappingRel (p : α → β → Prop) : (list : List α) → (newList : List β) → Prop where
  | nil : ListMappingRel p [] []
  | cons :
    p head newHead →
    ListMappingRel p tail newTail →
    ListMappingRel p (head :: tail) (newHead :: newTail)

I want to be able to represent the equivalence between this list relation prop and the actual implementation of a List.map. I want to do something like this:

theorem ListMappingRel.equiv {p : α → β → Prop} : ListMappingRel p list newList ↔ newList = list.map (fun item ↦ ∃ {rel : p item newItem}, newItem) := by sorry

but that isn't right.

Alternatively I could do this but then I'm going to need more lemmas to convert between this theorem about list indexes to actually saying something about List.map:

theorem ListMappingRel.equiv' {p : α → β → Prop} :
  ListMappingRel p list newList ↔
  ∀ i, (hlen : i < list.length) → (hnlen : i < newList.length) →
  p list[i] newListItem → newList[i] = newListItem :=
  by sorry

Otherwise I think the best option might need to be to ask for some function f, prove that it implements the relation, and then prove equivalence between my list relation with prop p and List.map with mapping function f:

theorem ListMappingRel.equiv''' {p : α → β → Prop} {f : α → β}
  (funcRelEquiv : ∀ a b, f a = b ↔ p a b)
  : ListMappingRel p list newList ↔ newList = list.map f := by sorry

Is the last one the best way to express this? Is there a more direct way to do this without having to pass in a function f that implements relation prop p?

[Matt Diamond]

Are you trying to prove the existence of such a mapping function, or just prove something about it if it exists?

[Matt Diamond]

after all, it might not exist if there are some values a : α for which no b : β satisfies the relation

[Matt Diamond]

however, you could prove that such a function exists for { a : α // a ∈ list }

perhaps something like:

∃ (f : (a : α) → a ∈ list → β),
  newList = list.pmap f (fun _ => id) ∧
  ∀ a (ha : a ∈ list), p a (f a ha)

[aron]

Matt Diamond said:

after all, it might not exist if there are some values a : α for which no b : β satisfies the relation

Right, that's a good point. Yeah for that reason I think there's no real way around passing in a function f as the "implementation" of the relation p

[aron]

I was assuming that there exists a relation for every input a : α, and that each such input has one unambiguous output b : β. In which case it might be possible to infer what the output b for every input a should be

[aron]

But what if that is indeed the case? how would I express that a relation is "function-like"? i.e. that there is an output for every possible input value, and that the relation is injective (that the same input will always have the same output)?

[Aaron Liu]

just pass a function?