Implement experimental :match-conclusion for rules

[hansjoergschurr]

This adds a keyword to define-rule that makes the conclusion the first argument of a rule, and introduces step to make a given conclusion the first argument, or fail if no conclusion is given.

(declare-rule match1 ((F1 Bool) (F2 Bool))
    :match-conclusion (and F1 F2)
)

(declare-const c1 Bool)
(declare-const c2 Bool)
(step test1 (and c1 c2) :rule match1)

; This fails
(step test2 :rule match1)

The proof term test1 is just (match1 (and c1 c2)).

Justification

After some experiments with Alethe Classic rules, I am changing my opinion about needing a feature to capture explicitly given conclusions.

For example, the simple not_not rule for double-negation elimination. It introduces the clause (not (not (not T))), T. You would like to write this as a proof rule that takes T as an argument. However, in Alethe Classic the solver is free to choose the order of the literals in the conclusion. Hence, a rule with :conclusion (cl (not (not (not T))) (not T)) could fail if the solver prints the conclusion in the wrong order.
Therefore, any Alethe Classic rule that does not generate a unit clause would need the entire conclusion as an argument.

Whit this change the rule becomes:

(program check_not_not ((phi Bool))
    (Bool) Bool
    (
    ((check_not_not (cl (not (not (not phi))) phi)) true)
    ((check_not_not (cl phi (not (not (not phi))))) true)
    )
)
(declare-rule not_not ((CL Bool))
  :requires ((check_not_not CL) true)
  :match-conclusion CL
)

Still not perfect, but better.

Implementation

When defining a rule, one can use :match-conclusion instead of :conclusion. If this is used, the conclusion must be given in the step. To achieve this, define-rule with a :match-conclusion T adds an additional argument Quote T to the start of the argument list, and sets the conclusion to Proof T. The step command detects rules annotated with :match-conclusion and hands the conclusion to the rule as the first argument.

Hence, this feature doesn't change functional semantic of rules, it is just syntactic sugar for step.

TODO: support in compiled version and write docu.

[ajreynol]

This functionality should now be subsumed by alf.conclusion, see 0078381.