## Stream: Elpi users & devs

### Topic: State Injectivity

#### 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 =`.

#### 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?

#### 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.

#### 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

#### 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

#### 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).`

#### 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.

#### 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

#### 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.

#### 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?

#### 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.

#### Enrico Tassi (Jul 20 2022 at 09:50):

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

#### 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)

#### 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)`

#### Enrico Tassi (Jul 20 2022 at 09:51):

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

#### Enrico Tassi (Jul 20 2022 at 09:52):

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

#### Enrico Tassi (Jul 20 2022 at 09:52):

since `x` and `y` are different by design

#### Enrico Tassi (Jul 20 2022 at 09:52):

I mean, it is what `pi` does

Oh I see

#### 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)?

#### 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