Stream: Elpi users & devs

Topic: State Injectivity


view this post on Zulip Théo Laurent (Jul 19 2022 at 15:11):

How to state injectivity of a function in elpi?
I tried inj F :- pi X Y \ F X = F Y => X = Y, but ran into Declaring a clause for built in predicate =.

view this post on Zulip Enrico Tassi (Jul 19 2022 at 19:25):

Hum, Elpi is a logic programming language, but it is not a prover where you state properties. What are you trying to do?

view this post on Zulip Théo Laurent (Jul 20 2022 at 06:06):

Again the long term idea was a sudoku soler. I'm trying to represent the grid as a function, so I want to constrain it.

view this post on Zulip Enrico Tassi (Jul 20 2022 at 08:16):

I did not try to run it (you need to adapt the syntax a little), but this seems a way to do it: https://gist.github.com/luan/1995582

view this post on Zulip Enrico Tassi (Jul 20 2022 at 08:17):

the domain predicate is the p one in the other thread https://coq.zulipchat.com/#narrow/stream/253928-Elpi-users-.26-devs/topic/Question.20on.20error.20message.20.22Evaluation.20of.20a.20non.20closed.20term.22

view this post on Zulip Théo Laurent (Jul 20 2022 at 08:54):

Théo Laurent said:

How to state injectivity of a function in elpi?
I tried inj F :- pi X Y \ F X = F Y => X = Y, but ran into Declaring a clause for built in predicate =.

Strangely enough, this seems to do the trick inj F :- pi x y \ not (x = y) => not (F x = F y).

view this post on Zulip Théo Laurent (Jul 20 2022 at 08:55):

  pred p o:int.
  p 1.
  p 2.
  p 3.
  p 4.
  p 5.
  p 6.
  p 7.
  p 8.
  p 9.
  inj F :- pi x y \ not (x = y) => not (F x = F y).
  dom F :- pi i \ p i => p (F i).

and then both dom F, inj F, coq.say "ok" F. and dom F, not (inj F), coq.say "ok" F. give me an answer.

view this post on Zulip Théo Laurent (Jul 20 2022 at 09:04):

although I get it won't actually help me for the sudoku, as I figure elpi won't be able to devise an arbitrary permutation out of the blue

view this post on Zulip James Wood (Jul 20 2022 at 09:15):

Generating permutations (of a list) is the classic logic program, and I think it should be possible to transcribe the results of that into a function.

view this post on Zulip Paolo Giarrusso (Jul 20 2022 at 09:16):

It's not clear that injectivity as you stated would work correctly... Elpi probably can't deduce x = y from F x = F y?

view this post on Zulip Enrico Tassi (Jul 20 2022 at 09:49):

Hum, pi x y \ not (x = y) is always true, I don't get why you would add it as a clause.

view this post on Zulip Enrico Tassi (Jul 20 2022 at 09:50):

I mean, pi is not exactly forall. Let me find a paper

view this post on Zulip Enrico Tassi (Jul 20 2022 at 09:51):

To get an intuition, see page 6 https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tocl-nabla.pdf (pi is specified by nabla)

view this post on Zulip Théo Laurent (Jul 20 2022 at 09:51):

but with my simple example, it does return me the identity function when I put inj F and a constant function when I put not (inj F)

view this post on Zulip Enrico Tassi (Jul 20 2022 at 09:51):

Another intuition is that each pi x makes x fresh w.r.t. everything else

view this post on Zulip Enrico Tassi (Jul 20 2022 at 09:52):

I'm saying that not (x = y) => is not needed

view this post on Zulip Enrico Tassi (Jul 20 2022 at 09:52):

since x and y are different by design

view this post on Zulip Enrico Tassi (Jul 20 2022 at 09:52):

I mean, it is what pi does

view this post on Zulip Théo Laurent (Jul 20 2022 at 09:53):

Oh I see

view this post on Zulip Théo Laurent (Jul 21 2022 at 09:17):

Enrico Tassi said:

I did not try to run it (you need to adapt the syntax a little), but this seems a way to do it: https://gist.github.com/luan/1995582

This GNU Prolog version use fd_all_different which add constraints to the resolution. How to do that with elpi (efficiently)?

view this post on Zulip Enrico Tassi (Jul 21 2022 at 13:00):

This is not super efficient, but does what you want:

pred alldiff i:list int.
alldiff L :- not (distinct L), !, fail.
alldiff L :- std.filter L var VL, if (VL = []) true (declare_constraint (alldiff L) VL).

pred distinct i:list int.
distinct [].
distinct [X|XS] :- var X, !, distinct XS.
distinct [X|XS] :- not(present X XS), distinct XS.

pred present i:int, i:list int.
present N [X|XS] :- var X, !, present N XS.
present N [N|_] :- !.
present N [_|XS] :- present N XS.

main :-
  alldiff [A,B,C],
  A = 1,
  not(B = 1),
  B = 2,
  not(C = 1),
  not(C = 2),
  C = 3.

Last updated: Feb 05 2023 at 13:02 UTC