18.5 Libraries

The tactic comes with some libraries, useful to write programs and specifications. The first set of libraries is automatically loaded with the module Programs. Among them, you can find the modules:

ProgWf: : this module defines a family of relations Zwf on type Z by
(Zwf c) = l x,y. cŁ x c Ł y x < y
and establishes that this relation is well-founded for all c (lemma Zwf_well_founded). This lemma is automatically used by the tactic Correctness when necessary. When no relation is given for the variant of a loop or a recursive function, then (Zwf 0) is used i.e. the usual order relation on positive integers.
Arrays: : this module defines an abstract type array for arrays, with the corresponding operations new, access and store. Access in a array t at index i may be written t#[i] in Coq, and in particular inside specifications. This module also provides some axioms to manipulate arrays expression, among which store_def_1 and store_def_2 allow you to simplify expressions of the kind (access (store t i v) j).

Other useful modules, which are not automatically loaded, are the following:

Exchange: : this module defines a predicate (exchanget t' i j) which means that elements of indexes i and j are swapped in arrays t and t', and other left unchanged. This modules also provides some lemmas to establish this property or conversely to get some consequences of this property.
Permut: : this module defines the notion of permutation between two arrays, on a segment of the arrays (sub_permut) or on the whole array (permut). Permutations are inductively defined as the smallest equivalence relation containing the transpositions (defined in the module Exchange).
Sorted: : this module defines the property for an array to be sorted, on the whole array (sorted_array) or on a segment (sub_sorted_array). It also provides a few lemmas to establish this property.