Proof explanations for multi_rewrite

[K-dizzled]

Hi everyone!
I was exploring proof construction with egg. I needed to have non-symmetrical rules, so that when I check (a, b) for equivalence it is true, and (b, a) is not. I used a hack from tests/prop.rs with multi_rewrite, but I am facing something weird right now. If an Explanation<L> provided by explain_equivalence contains a multi_rewrite rule, its name in the graph is something like .../.cargo/registry/src/github.com-1ecc6299db9ec823/egg-0.9.3/src/multipattern.rs:167:32. I have just added a printing of a proof to tests/prop.rs here.

Trying to prove goal 5: (-> x z)
Explanation: (& (-> x y) (-> y z))
(Rewrite<= /Users/andrei/.cargo/registry/src/github.com-1ecc6299db9ec823/egg-0.9.3/src/multipattern.rs:167:32 (| (~ x) z))
(Rewrite=> def_imply_flip (-> x z))
test prove_chain ... ok

[oflatt]

Sorry, explanations do not currently properly support multipatterns. We should add this to the documentation.
It's possible you could work around it with a custom applier that introduces a new node for the multiple terms on the lhs.

[K-dizzled]

I see... But, anyway, could you please tell if it will hypothetically work? I've seen your post on the topic of backward rewrites. As I understood, there you are explaining why it's impossible to construct a e-graph, not treating the rewrites as symmetrical operators, but, at the same time, the multirewrite seems to be working just the way I want it to work and the only point here is that the proof is shown strangely.

[oflatt]

I think they partially work right now, but don't guarantee that the proof term actually matches the multi-rewrite (since the multirewrite could have matched multiple terms somewhere in the egraph).

As for being displayed weirdly, we could fix that by giving a name to the multirewrite instead of printing the weird debug string

[K-dizzled]

I see, thank you, I will try to get the real names of the multi-rewrites. But still, I don't get one thing. Isn't multirewrite a solution to the problem "how to turn off backward rewrites"?

[oflatt]

No- "backwards rewrites" can still happen when you use multi-rewrites.
The reason these show up is that congruence is bidirectional, and so different proofs of congruence may use one rule application in two different directions. We may need to use a rewrite both "forwards" and "backwards" in the proof.

Did that help?

[K-dizzled]

Yeah, I understand that simply multi-rewrites will not solve the problem. I am talking about the idea used in Prop example. Manually add a servitude e-class, join it to the starting term and then, when making a rewrite, search for the equivalence with that node in the lhs of the rewrite as like in:

multi_rewrite!(
        "lem_imply";
        "?value = true = (& (-> ?a ?b) (-> (~ ?a) ?c))"
        =>
        "?value = (| ?b ?c)"
    )

[oflatt]

I think that even when you use rewrites like that one, a proof may still contain "backward" rewrites due to congruence.

[K-dizzled]

I tried creating a graph from term A, added such kind of rewrite A -> B, and then tried to explain equivalence(B, A) and it gave me a message that terms are not equivalent(while explain_eq(A, B) works). However, when doing the same procedure with regular rewrites, it gives an explanation as such Rewrite<= a_eq_b.

[oflatt]

It sounds like the terms were not equivalent-
Did you set up the egraph with the initial term being equal to true?

[K-dizzled]

I've set them to true, yes. Unfortunately, I now tried making a min-repr example for you, but now it seems to proof things in both directions. I guess I made some mistake last time testing. Well, thank you for your help and explanations. I guess I am now clear with the way things work. However, I cannot solve my problem using egg(

[oflatt]

I'm currently working on proofs for multi patterns in egglog:
https://github.com/egraphs-good/egglog

When that is done it will support this feature