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

#### Théo Laurent (Jul 20 2022 at 09:53):

Oh I see

Last updated: Jun 06 2023 at 23:01 UTC