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: Oct 13 2024 at 01:02 UTC