crnkjck
commented
6 years ago This requires a more flexible way of exporting rules from the Matcher module and grouping them into meaningful subsets. A rule should probably consist of:
- a matcher,
- a justification message (or two of them, see below), and
- a description of the rule itself to be shown in a help text.
Since there are different types of rules, they cannot be straightforwardly grouped into one list. There are several options how to do this (a rule set is a record of lists of rules of different types/a rule set is a single list of a union type with a variant for different rule/a rule set is a single list of records where the matcher is a union type/…?), each with different possible inconsistencies and redundancies.
It might be beneficial to have two justification messages: One shown below the formula and one above for eigen-variable rules (generalization: Fix an arbitrary x and show
; ∃ elimination Obtain x from (n) such that
).
We'd like to have a means to configure the proof-assistant to restrict the user to some set of rules (matchers) and some structural constructs (e.g., no cases or no lemmas inside proofs). We might want, e.g., pure hilbert-style system, pure tableaux-style system, full propositional system without first-order rules. It should also be possible for the user to easily find out which rules are enabled, and what do they do.