Generic operations

The class definitions below are MathClasses-style overloaded operators. This is quite useful because common structures show up between modules and layers, and at different levels of their construction. We use Coq's excellent support for UTF-8, which helps with clarity and conciseness. Proof General users may want to use the TeX input method to type special characters: hit C-\, and Emacs will ask you "Input method:". If you answer tex, Emacs will automatically replace any LaTeX sequence you (say, \le) by the corresponding symbol (say, ≤). By convention, most of the time we use the LaTeX sequence of the operator as the name for the class and field, so the sequences for the operators below should be obvious. The only exception is compose, which is denoted by ̧\circ.

Generic operators for a type of specifications T

Sometimes we want eauto to unfold the generic operators so as to apply theorems about a specific implementation.

Generic properties

Now we can give generic definitions for some recurring properties, making use of the overloaded operators above.

Heterogenous transitivity

This heterogenous version of transitivity is useful with our category-indexed simulation relations, for which transitivity can go through different types.

XXX: ideally, here we'd have some typeclass to use instead of Proper such as SolveMonotonic, with the idea that Proper is the user-declared inputs, whereas SolveMonotonic is the automatically derived outputs.

This is the converse property, mainly used for simulation paths: if there is a simulation along path p23 ∘ p12, then there is a "midpoint" with simulations along p12 and p23. Like heterogenous transitivity, stating this property in terms of the following typeclass allows us to show easily that it carries through option_le and the like.

If we have both HTransitive and RTransitive instances, we can establish the following equivalence, which is useful for rewriting.

Hints for eauto and autorewrite

Most of the generic properties above cannot be used directly as hints because the head term is a variable. Hence we register a couple of versions specialized to often-used (families of) relations.

For rewriting we have a similar problem, where once things are filled in by unification with the match found, the generated subgoals (namely the typeclass instances to resolve) cannot contain existential variables. Hence we apply the same specialization strategy. Unfortunately, here we have to spell it out as separate lemmas, because the registered rewrite theorems cannot contain holes (only regular premises to be solved by the tactic provided).

Some properties of properties

Logical relationish kind of things

We should eventually drop the 'solve_monotonic' syntax, and use the 'rauto' tactic instead.

Generic instances for relation properties

Basic instances

Prop

Booleans

Boolean are sufficiently simple that we can prove pretty much anything by just enumerating all possibilities.

The Equivalence derived from a PreOrder

XXX: those should be generic properties of R ∩ flip R, since they also apply to say, eqrel = subrel ∩ flip subrel.

Trivial order