Support Alt-Ergo's cut and check

[bclement-ocp]

Alt-Ergo has cut and check primitives that are not supported by dolmen:

File "check_cut.ae", line 1, character 15-35:
1 | goal g_check : check (true = false) -> true = false
                   ^^^^^^^^^^^^^^^^^^^^
Error The following Dolmen builtin is currently not handled during typing
      `check`. Please report upstream

These should have type bool -> bool and are used as markers by Alt-Ergo to introduce auxiliary goals.

goal g : H1 -> check H2 -> G

should be understood as

goal _check : H1 -> H2
goal g : H1 -> G

and

goal g : H1 -> cut H2 -> G

should be understood as

goal _cut : H1 -> H2
goal g : H1 -> H2 -> G

I am not sure if Dolmen should implement the invariant "check and cut can only appear on the left of an implication in a goal" (including the left of an implication inside another check or cut), but it should at least expose check and cut as bool -> bool primitives so that Alt-Ergo can pick them up.

[Gbury]

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) ?

[bclement-ocp]

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 ]

[bclement-ocp]

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.

[bclement-ocp]

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.

[Gbury]

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.

[bclement-ocp]

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).

[Gbury]

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

[bclement-ocp]

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.

[Gbury]

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.

[bclement-ocp]

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.

[Gbury]

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.

[bclement-ocp]

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.

[Gbury]

@bclement-ocp is this still needed ?

[bclement-ocp]

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.

[Gbury]

Ok, I'll close this issue then.

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