Introduce mem-rel! function in builtin_stdlib.elpi

[patrick-nicodemus]

The motivation is that if f is of type o:A, i:B, then mem-rel! A f Bs is a bit more readable than mem! B {map As {swap f} }.

for example,

pred f i:term i:prop.
f C (decl C _ _).
f C (def C _ _ _).

mem-rel! C f Ctx.

Not sure what the name should be.

[gares]

I'm a bit lost, the implementation of mem-rel! A R L is literally exists! L (R A), I don't get what one gains by using the new API.

In particular I don't get the example with map and swap. The {{ are the Rocq ones?

[patrick-nicodemus]

In particular I don't get the example with map and swap. The {{ are the Rocq ones?

Sorry, I mixed up the notation with Rocq quotation and spilling. I meant spilling. I have edited my comment.

I'm a bit lost, the implementation of mem-rel! A R L is literally exists! L (R A), I don't get what one gains by using the new API.

You are probably right, maybe it is not useful. My point is that:

• if I want to check if A is an element of a list L, I can do mem! A L
• if I want to check if f A is an element of a list L, I can do mem! {f A} L
• if I want to check if A is an element of map g L, my first instinct is to write it as mem! A {map g L}, but this is inefficient.

I guess this solution is obvious but I am suggesting that it is a special case of exists! that could be more commonly used, for example we could define mem! X L as exists! L (Y\ X = Y) but it has its own name mem! instead.

Maybe it would be more useful if R was flipped,
something like

mem-map! A G L :- exists! L (Y\ G Y A).

so that
mem-map! A G L iff mem! A {map G L}

[gares]

I see. In this case I usually prefer the non-cutting (relational) combinators (some of which are not even in elpi stdlib) and write mem X L, g X Y, !. It is really generate + test (and commit if cut).

It seems more of a "style" than an API to me. So I'm happy to add all the APIs to make the style comfortable.

Maybe generate-test P Q could be an idiomatic way to express that, but I'm not so sure it is as flexible as just putting two relational predicates together with ,. Maybe some logic-programming DSL for functional languages like minikaren found a good set of APIs for that, but I'm a little ignorant there.