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

.

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

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.

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

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

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

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

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.

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

Hum, `pi x y \ not (x = y)`

is always true, I don't get why you would add it as a clause.

I mean, `pi`

is not exactly `forall`

. Let me find a paper

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

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

Another intuition is that each `pi x`

makes `x`

fresh w.r.t. everything else

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

is not needed

since `x`

and `y`

are different by design

I mean, it is what `pi`

does

Oh I see

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

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