-
Notifications
You must be signed in to change notification settings - Fork 42
#Ceil
Unifying a variable X with a term foo() introduces a condition #Ceil( foo() ).
If this happens when unifying the left-hand side of a rule with the configuration, then #Ceil( foo() ) becomes a requirement to apply the rule.
Recall that the backend splits the configuration on the rule's requirements:
- the state where the requirement holds, so the rule applies (
#Ceil( foo() )etc.) - the state where the requirement does not hold, so the rule does not apply (
#Not( #Ceil( foo() ) )etc.)
Usually, the #Not #Ceil( foo() ) case needs to be refuted, or the proof becomes stuck.
This case can often be refuted by applying the formula T = T #And #Ceil(T) to the configuration.
(Note that this formula is valid in Matching Logic for all patterns.)
The backend applies this formula to the left-hand side of the claim when checking the final implication,
introducing #Ceil(left-hand side) into the side condition at the top level.
When foo() appears in the left-hand term, the #Ceil(left-hand side) will contradict the #Not #Ceil( foo() )
so that the claim is shown to hold by the principle ex falso quodlibet.
If and only if foo() cannot be evaluated directly and does not appear as a sub-term of the left-hand side of the claim,
it may be necessary to add a rule or rules that define #Ceil( foo() ) so that #Not( #Ceil( foo() ) ) can be refuted by other conditions on the claim.
However, it is very unusual for this to actually be necessary and the user should do so only after submitting a bug report.