Wtypes

[CalosciMatteo]

The ground term algebra is a W-type.

• Derivation of the propositional computation rule 'beta' for the ground term algebra. In doing so I also reformalized the propositional introduction and elimination principles.

  The idea beneath the proof is to take the already proved results in Terms.v for the ground algebra and translate them in the appropriate context. These are build_gterm, term_ind and term_ind_step and I translated them respectively in sup, ind and beta. The "translation" is just the image of the terms above via some equivalences. Those equivalences are obtained by combining together the following basic equivalences via weqonsec and its variations:

  • gtweq_sec which translate the "subterms' vector" to the function "selecting the subtree";
  • lower_predicate which "forgets" the sort's parameter of terms, which is always tt in this case;
  • ind_HP_Hypo which translates the vector of the inductive hypothesis on subterm in the function of the inductive hypothesis on subtrees. Making this equivalence compute propperly and understanding the relation between h2map and the relevant lambda term in beta was the main challenge. This also required various lemmas about vec_fill in Vectors.v and Hvectors.v.

  A smart trick seemed to first prove beta changing its variables with the corresponding variables in the preimages of their translation, thus making explicit in the goal the translation equivalences. Finally the correct statement is proved via weqonsecbase in a bit clunky but straightforward way.

• Some improvements in Vectors.v and Hvectors.v made for completeness or needed for the proof above.

[amato-gianluca]

Commits imported off-line.