Stream: Elpi users & devs

Topic: std.forall vs manual loop

Mathis Bouverot-Dupuis (Sep 20 2024 at 08:42):

Hi all, I have two lists of (coq) term As and Bs, and a term T. I would like to replace each Ai by Bi in T.
My first attempt to do this was :

std.forall2 As Bs copy => copy T U

But it does not seem to do anything (U is simply equal to T). I did find a working solution :

pred copy-with i:list term, i:list term, i:term, o:term.
copy-with [] [] T U :- copy T U.
copy-with [A|As] [B|Bs] T U :- copy A B => copy-with As Bs T U.

My question is : why does the first solution not work ?

Quentin VERMANDE (Sep 20 2024 at 08:53):

I guess this is because when you reach the point where you need to replace Ai by Bi, elpi looks for a clause copy Ai Bi in the database, but you accumulated std.forall2 As Bs copy, which does not match. In the second case, you accumulate every copy Aj Bj, so elpi finds the relevant one.

Mathis Bouverot-Dupuis (Sep 20 2024 at 08:57):

Oh I think I get it : in elpi-land std.forall2 As Bs copy is provable if each copy Ai Bi is provable, however the converse is not true i.e. std.forall As Bs copy does not allow one to prove copy Ai Bi.

Enrico Tassi (Sep 20 2024 at 08:57):

Indeed you did not accumulate the clauses you think.
This (untested) should clarify:

std.map2 As Bs (x\y\r\ r = copy x y) Clauses, Clauses => copy T U.

Mathis Bouverot-Dupuis (Sep 20 2024 at 08:59):

Enrico Tassi said:

Indeed you did not accumulate the clauses you think.
This (untested) should clarify:

std.map2 As Bs (x\y\r\ r = copy x y) Clauses, Clauses => copy T U.

Ahah this is what I was trying to do ! I'll give it a go.

Enrico Tassi (Sep 20 2024 at 09:00):

Mathis Bouverot-Dupuis said:

Oh I think I get it : in elpi-land std.forall2 As Bs copy is provable if each copy Ai Bi is provable, however the converse is not true i.e. std.forall As Bs copy does not allow one to prove copy Ai Bi.

Your intuition makes sense, but for that to work you would need something like

(pi A B\ copy A B :- std.exists2 As Bs (x\y\x = A, y = B)) => copy T U.

Enrico Tassi (Sep 20 2024 at 09:01):

Anyway, your code copy-with is very idiomatic, and short. I would use that one in my programs, not any of the other snippets I wrote. I wrote them just to explain what happens.

Last updated: Oct 13 2024 at 01:02 UTC