|Page 328 of 800||Search internet|
One of the things an argumentation can contain is a reference to an axiom. As an example, Line L03 below uses Axiom to prove :
Line L03 may seem trivial. It just proves as an instance of Axiom . But verifying Line L03 is not completely trivial.
The complexity is due to generality. The Logiweb proof checker can handle a wide spectrum of theories. That has a cost in the form of some complexity.
The description in the following explains how Line L03 is verified in all its glory. When you are done with that explanation you have the general picture and know most there is to know about tactic expansion.
To understand what happens at code level you have to read the check page. If you do so, you will still benefit from having read the present documentation first. The present documentation explains the system top down. The check page describes the system bottom up.
That statement macro expands into two definitions:
Furthermore, contains :
Thus, states , it behaves as defined by inside argumentations, and it belongs to the theory which we work inside.
During tactic expansion of the proof of , the conclusions of proof lines are accumulated in of the tactic state . The value of is a list of items of form where is the line number, is the conclusion of the given line, and can be used by individual tactics for their own purposes. The elements of can be used as premises for reasoning later in the proof ('pre' for 'premise').
Thus, when Line L03 is tactic expanded, the expander knows that we have 'proved' ('proved' it by assuming it) and the expander knows that L01 stands for . The expander also knows that we have proved the conclusion of Line L02 and that L02 stands for that conclusion. So in Line L03 we can use and the conclusion of L02 as premises.
The value above which individual tactics can use for their own purposes typically has form where is a proof of the given line expressed in the Logiweb sequent calculus.
Line L03 is an argumentation line, so it is tactic expanded by invoking the unification tactic on it. The unification tactic in turn does unitac expansion of the argumentation with the goal of proving the conclusion .
Note that the proof is expanded by two, distinct expansion machineries: tactic expansion and unitac expansion. Each time the tactic expander meets an argumentation line, it invokes the unitac expander on the argumentation of that line. Thus, the tactic expander does overall expansion of the proof whereas the unitac expander expands individual argumentations.
Now the unitac expander expands the argumentation with the goal of proving . Since the unitac aspect of is defined to be , the unitac expander invokes on a structure which contains everything a unitac needs.
Among other, the structure above contains the tactic state . looks up to see how rules (i.e. axioms and inference rules) are handled in this, particular proof. The value of is so invokes . The function defines the 'standard' way of treating rules.
As an example of a proof which does not treat rules the standard way, consider the multzero proof whose source starts thus:
PA proof of 3.2l : ...
The initial 'PA' causes the proof to be tactic expanded using the tactic definition of PA. The PA tactic installs a non-standard value in in order to handle hypotheses properly. In general, one needs a non-standard rule-unitac when using deduction. Furthermore, one will need different non-standard rule-unitacs for theories with different kinds of deduction theorems (like map theory versus first order logic).
Now back to the proof of above. The standard rule unitac looks up the statement aspect of and sees that stands for .
Then the unitac looks up in the tactic state to see what it can use for proving and finds that it can use the assumption and the conclusion of Line L02. Then the unitac scans the assumptions and finds in the statement aspect of . Then the unitac constructs a proof expressed in the Logiweb sequent calculus which derives from .
The return value from the unitac is a new tactic state for which is a sequent proof and is the conclusion of the proof ('arg' for 'argumentation' and 'con' for 'conclusion').
The unitac sets the conclusion to since that is what the axiom says. Then the unitac sets to the sequent proof which derives from .
So now we have proved but the goal was to prove .
As mentioned, Line L03 is tactic expanded by the unification tactic. The unification tactic does unitac expansion of the argumentation and then tries to adapt the outcome to the intended conclusion.
The unitac outcome is a proof of and the goal is to prove the intended conclusion
Or, rather, since proof checking occurs after macro expansion, the unitac outcome is a proof of
The unification tactic notes that the principal operator of the unitac outcome is a meta-quantifier and that the principal operator of the intended conclusion is no meta-quantifier. Thus, the unification tactic decides to instantiate the unitac outcome.
To instantiate the unitac outcome, the unification tactic constructs a fresh variable called something like . is an indexed meta-variable which the unification tactic thinks does not occur in the proof. Never use unifresh to construct your own variables or you may be in trouble.
Then the unification tactic adds a sequent operator to the unitac outcome which instantiates to . The result is a proof of
Again, the unification tactic notes that the principal operator of the unitac outcome is a meta-quantifier and that the principal operator of the intended conclusion is no meta-quantifier, so it instantiates again to get a proof of
Note how the fresh variables have two indexes: one which shows the variable name before freshening and one which makes the fresh variable unique. Fresh variables often occur in error messages where the name before freshening is nice to have.
So now we have proved
but the goal was to prove
After adaption, the unification tactic tries to unify the unitac outcome to the intended conclusion. Unification of
has the following solution:
Thus, the unification tactic adds sequent operators to the unitac outcome which replaces with and with , yielding a proof of the intended conclusion .
If you write e.g. in a proof then the unification tactic will try to unify
which is impossible since and are distinct meta-variables. In this case you will get an Unable to unify x with y error message. In general, when unification is impossible you will get an error message telling you that you cannot unify some term with some other term.
Quite often, it is difficult the spot the error based on the two terms which cannot be unified. Typically, it is much faster just to look at the proof line which is in error. Normally, the error is obvious.
In some cases, unification is not enough to see how all variables should be instantiated. In such cases you get an error message like Incomplete unification. Uninstantiated variable: x. We shall see examples of that later.
In the example above, adaption removed meta-quantifiers from the root of the unitac outcome. In general, adaption can remove meta-quantifiers , inferences , and endorsements . In practice, adaption removes lots of quantifiers and endorsements and few inferences. At least that is what happens for the proofs I write.
Adaption removes quantifiers by instantiating them and removes endorsements by verifying them. An endorsement is removed by evaluating the side condition and checking that it evaluates to .
Adaption does not do instantiation and verification itself. Rather, it adds sequent operators for doing so and leaves it to the sequent calculus to do the actual instantiations and verifications.
As long as you do not violate side conditions, adaption will make side conditions go away. If you accidentally do violate a side condition, you will get a Verify-seqop used on false condition message from the sequent calculus.
Adaption will be covered in more detail various places in the following.
|Page 328 of 800||Search logiweb.eu|