Next: UTac Up: LEGO Release 1.3 Documentation Previous: Then

LEGO Version 1.3: Theorems and Configure Theorems

Simple inductive datatypes can be equipped with useful gadgets by the new version of the Theorems switch, in accordance with the parameters set up by the Configure Theorems command. This configuration can work in one of two ways:

Configure Theorems true_type absurd_type eq_subst;
instructs Theorems to prepare proof that constructors are disjoint via the substitutive property of equality, where eq_subst is the name of this property as registered with Configure Equality, and true_type and absurd_type are the names of (respectively) the polymorphic identity function and absurd function types for an appropriate universe (eg trueProp and absurd for Prop).
Configure Theorems true_value false_value true_not_false;
instructs Theorems to prepare similar proofs by mapping conflicting constructors to the named distinct true_value and false_value and applying the named true_not_false proof that they are distinct.

  Inductive [simple:SET] Theorems
  Constructors
    [con1:T11->..->T1j1->simple]
    ..
    [conk:Tk1->..->Tkjk->simple];

will build for each constructor coni a function simple_is_coni

acting like

fun simple_is_coni (coni xi1 .. xiji) = true_type or true_value
| simple_is_coni _ = absurd_type or false_value

These functions can then be used, with eq_subst or true_not_false according to the configuration, to synthesise constructor conflict theorems as required.

Also constructed where possible are the injectivity theorems:

  simple_coni_injective : {xi1,yi1|Ti1}..{xiji,yiji|Tiji}
                              (Eq (coni xi1 .. xiji) (coni yi1 .. yiji))->
                              {P|subst_univ} ((Eq xi1 yi1)->..->(Eq xiji yiji)->P)->P

where subst_univ is the universe over which eq_subst substitutes.

At present, LEGO fails to generate an injectivity theorem for any constructor whose arguments contain type dependencies such that the injected equalities are not well-typed. In these circumstances, the user is informed of the omission, but the inductive definition goes though anyway, along with those injectivity theorems which can be generated.

Note that the Theorems package uses the equality set up by Configure Equality. The library's default equality comes with an appropriate Theorems configuration.

The Qnify tactic uses the facilities generated by Theorems to solve first-order unification problems involving constructors and variables expressed as equational premises in the goal.