Stream: Elpi users & devs

Topic: ✔ std.forall vs manual loop

Mathis Bouverot-Dupuis (Sep 20 2024 at 09:03):

Enrico Tassi said:

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.

Ok, but I would also need another clause to relate std.exists2 to std.forall2 right?

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

Well, I was dropping the forall2, and put an exists2 to the other side...

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

Here your "data" is As and Bs

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

As Quentin explained, copy will look for "copy" so you must load "copy". Either a bunch of them, or a single one scanning your lists.

Note that in the first option, you would load a "copy" only if there exists a corresponding pair in As Bs. This is why your "forall" becomes an "exists" now.

Mathis Bouverot-Dupuis (Sep 20 2024 at 09:12):

Ok I hadn't understood your "exists" snippet actually, now it makes sense ("a single one scanning your lists").

Mathis Bouverot-Dupuis (Sep 20 2024 at 09:12):

Thanks Quentin and Enrico for your help :)

Notification Bot (Sep 20 2024 at 09:12):

Mathis Bouverot-Dupuis has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC