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

Last updated: Jun 06 2023 at 23:01 UTC