14.277 Unification

Prev Up Next Page 748 of 800 Search internet

During tactic expansion, the unification tactic x conclude y 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 x conclude y 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 u at v for instantiating bound variables and also provide a value of v. Among other, the unification tactic is responsible for making proof lines like

A1 conclude #y imply ( #x imply #x ) imply #y

work. The A1 axiom says

axiom A1 : All #x ,, #y : #x imply #y imply #x end axiom

It is the unification tactic which has the overall responsibility to instantiate #x to #y and, in parallel, instantiate #y to #x imply #x.

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.

Prev Up Next Page 748 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05