Page 748 of 800
| Page 748 of 800 | Search internet |
During tactic expansion, the unification tactic 
takes a conclusion y and tries to instantiate metavariables in x in such a way that x ends up proving y. The unification tactic is beneficial for human readers who can see from y what a given proof line is supposed to prove. It is also beneficial for proof authors who can leave unspecified e.g. how each axiom and lemma should be instantiated. The tactic reads x conclude y in the lgs source.
Unification does lots of things to massage x into proving y. The most important task is to add At sequent operators 
for instantiating bound variables and also provide a value of v. Among other, the unification tactic is responsible for making proof lines like
work. The A1 axiom says
It is the unification tactic which has the overall responsibility to instantiate 
to 
and, in parallel, instantiate to 
.
The unification tactic also has the responsibility to ensure that Axiom A1 gets proved. The unification tactic can see that Axiom A1 is no lemma because it has no proof so it adds the sequent operators appropriate for axioms. Otherwise, the unification tactic would have added the sequent operators appropriate for lemmas.
Unification is a quite complex operation which has to treat different operators differently and which has to be open to new user defined features. For that reason, the unification tactic has its own system of tactics. The unification tactics are called 'unitac' tactics. It is possible to define both a tactic aspect and a unitac aspect of an operator so that the operator has one behavior when it occurs inside the scope of a unification tactic and another behavior outside such a scope.
| Page 748 of 800 | Search logiweb.eu |