Support Alt-Ergo's `cut` and `check` about dolmen HOT 15 CLOSED

I'm a bit confused on the exact semantics of check and cut : you mention that it should only be used on the let of an implication in a goal, but in your examples, it looks to me as if the important part is the implication where cut/check appears on the right (i.e. each time it's the implication with H1 and H2). Is there any hope of having a formal semantics of cut and check (or at least an algorithm for desugaring those constructs) ?

from dolmen.

You are right, I was not clear. By "on the left of an an implication" I mean that it must be one of the hypotheses (note that H1 -> H2 -> G is H1 -> (H2 -> G) so H2 is on the left of G).

More formally, I believe that the valid positions for cut and check in an expression are defined by the contexts G[ ⬚ ] (where E represents an expression)

G ::= E | ⬚ → E | E → G | check G → E

So in particular something like goal g : cut e is not valid.

My understanding is that Alt-Ergo then essentially saturates the following rewriting (top-down) from expr to lists of exprs (but again I don't know if it should be done in Dolmen):

E ⇒ [ E ]
cut E' → E ⇒ [ E' ; (E' → E) ]
check G → E ⇒ [ E₁; ...; En ; E ] when G ⇒ [ E₁; ...; En ]
E → G ⇒ [ (E → E₁) ; ... ; (E → En) ] when G ⇒ [ E₁; ... En ]

So for the examples:

For H1 → check H2 → G:

check H2 → G ⇒ [ H2; G ]
H1 → check H2 → G ⇒ [ H1 → H2 ; H1 → G ]

For H1 → cut H2 → G:

cut H2 → G ⇒ [ H2; H2 → G ]
H1 → cut H2 → G ⇒ [ H1 → H2; H1 → H2 → G ]

An example with nesting: H1 → check (cut H2 → H3) → G:

cut H2 → H3 ⇒ [H2; H2 → H3]
check (cut H2 → H3) → G ⇒ [ H2; H2 → H3; G ]
H1 → check (cut H2 → H3) → G ⇒ [ H1 → H2; H1 → H2 → H3; H1 → G ]

from dolmen.

In other words, cut E and check E don't really have semantics, but cut E → E' is E ∧ (E → E') and check E → E' is E ∧ E' where the ∧ creates new goals (and so the context must be duplicated, at least conceptually). I don't know if that can be expressed with Dolmen's existing primitives for sequents.

from dolmen.

Actually although the nesting is "syntactically" supported by Alt-Ergo I don't think it is intended to be supported and Alt-Ergo has inconsistent behavior on that case; we should probably ignore that possibility, so the context grammar should just be:

G ::= E | ⬚ → E | E → G

and not be nested inside checks.

The way all of this is implemented by Alt-Ergo is that an implication H1 → H2 → ... → Hn → G is processed as a sequence of imperative commands:

hyp H1;
hyp H2;
...
hyp Hn;
query G

I think this is similar to antecedent H1; antecedent H2; ...; antecedent Hn; consequent G; check for Dolmen (although the query in Alt-Ergo then discards all the hypotheses).

If there are cut/check in the goal, then they are processed in the same way using a second-level of local sequents, so H1 → H2 → cut (L1 → L2 → C) → G becomes:

hyp H1;
hyp H2;
local_hyp L1;
local_hyp L2;
local_query C;
hyp C;
query G

where local_query will discard the local_hyp only.

Edit: now that I have written the above, the best way to deal with this at the Dolmen level would probably be to implement the goal flattening and introduce appropriate push/pop statements. I don't know if we are equipped to deal with that on the Alt-Ergo side though.

from dolmen.

I think we indeed need to handle that in Dolmen, if only so that users of dolmen (other than alt-ergo) do not need to handle those.

From what I can tell, we have two options:

• deconstruct/flattening goal implications as you suggest, using push/pop operations, but that has the downside that push/pop operations are not always well supported
• instead of completely flattening the goal, we could instead split it into multliple implications, that can then each become a toplevel goal, that way I don't think think we need push/pop operations.

from dolmen.

that has the downside that push/pop operations are not always well supported

Yeah, that is my concern as well :(

instead of completely flattening the goal, we could instead split it into multliple implications, that can then each become a toplevel goal, that way I don't think think we need push/pop operations.

My only issue with that approach is that this would mean that the shared hypotheses have to be duplicated, where they are not currently (although I don't think that Alt-Ergo exploits this sharing currently, so maybe it is fine).

from dolmen.

If want to avoid duplication we could make it so that the shared formulas are defined before the new goals.

from dolmen.

I don't think that works because the hypotheses must themselves only be local to the goal (in Alt-Ergo the query command then flushes the hypotheses). So this:

goal g1 : H1 -> cut (L1 -> H2) -> G1
goal g2 : H2 -> G2

which alt-ergo translates as:

hyp H1;
local_hyp L1;
local_query H2;
hyp (L1 -> H2);
query G1;
hyp H2;
query G2

has the same semantics as the smt-lib script:

(push 1)
(assert H1)
(push 1)
(assert (not (=> L1 H2)))
(check-sat)
(pop 1)
(assert (=> L1 H2))
(assert (not G1))
(check-sat)
(pop 1)
(push 1)
(assert H2)
(assert (not (G2))
(check-sat)
(pop 1)

H1 is removed from the context after the first goal.

from dolmen.

Right, but taking your example

goal g1 : H1 -> cut (L1 -> H2) -> G1
goal g2 : H2 -> G2

We could translate it as

goal g1' : H1 -> (L1 -> H2)
goal g1 : H1 -> (L1 -> H2) -> G1
goal g2 : H2 -> G2

and further if we want to avoid duplication, we could have

define-prop h1 := H1
define-prop lh := L1 -> H2
goal g1' : h1 -> lh
goal g1 : h1 -> lh -> G1
goal g2 : H2 -> G2

Note here that we did not try and de-duplicate H2, we juste defined (e.g. let-bound at toplevel) the parts that the cut operation would duplicate.

from dolmen.

I don't think binding them really solves the issue; with this encoding it is harder to reuse internal solver state. If a solver proves h1 inconsistent during the proof of g1 then it may be able to reuse that information when trying to prove g1' and that seems harder with this encoding. Although maybe not because this is essentially check-sat-assuming now.

Another issue (but this is specific to Alt-Ergo and might be able to fix it) is that Alt-Ergo will not look inside the definition of lh while preprocessing the goal, so the behavior will be different.

from dolmen.

I'm not sure I see why and how it would make re-using internal solver state harder (or at least significantly harder): if a solver does keep and re-use its (or parts of its) internal state across push/pop/check-sat-assuming, then I expect that there shouldn't be much difference (except if one only does extremely naive things).

Considering that this only occurs in problems in alt-ergo's native language, that I expect not a lot of things actually generate problems that use cut/check (e.g. I don't think Why3 would generate problems using those) and therefore that problems that make use of cut/check are not too big, plus the fact that solvers would typically translate and hash-cons such terms before doing proving, I think that it's not actually a big problem if we duplicate expressions in that situation.

from dolmen.

I was thinking about hanging the behavior of Alt-Ergo on goals that don't use cut/check but if we don't do anything here then I think you are right, duplicating for the cases where there are cut / check is fine.

from dolmen.

@bclement-ocp is this still needed ?

from dolmen.

I think that with Why3 migrating to SMT-LIB input for Alt-Ergo it will not be needed. I don't think we need to do anything unless someone complains that this obscure functionality is broken.

from dolmen.

Ok, I'll close this issue then.

If anyone encounters this error and needs this fixed, please feel free to re-open this issue.

from dolmen.