predicate mapping

Stream: lean4

[Alexandre Rademaker]

I would like to implement a function like

 def h₁ (Qs Ps : x → Prop) (Qt : t) (Pt : t → t → Prop) : Prop :=
   ∀ x y e, (Qs x ∧ Ps y ∧ (poss e y x ∨ _of_p e y x ∨ compound e y x)) → ∃ v, Pt Qt v

But Qt and Pt are 'translations' from Qs and Ps. So it would be better to do something like:

 def h₁ (Qs Ps : x → Prop) (map : ???) : Prop :=
   ∀ x y e, (Qs x ∧ Ps y ∧ (poss e y x ∨ _of_p e y x ∨ compound e y x)) → ∃ v, (map Ps) (map Qs) v

What options do I have to implement the mapping? An inductive type? How do we extract the mapping from types like the ones below?

 inductive NodeMap : (x -> Prop) -> t -> Type :=
 | nm_benzene : NodeMap _benzene_n_1 benzene

 inductive EdgeMap : (x -> Prop) -> (t -> t -> Prop) -> Type :=
 | em_toxicity : EdgeMap _toxicity_n_1 toxicity

[Alexandre Rademaker]

Another option would be implementing a hashtable from x → Prop to t (node mappings). The point is that those mappings will be obtained from external processes.