.build.yml: continuous integration for SourceHut

Topological: uniform structure on topological groups

Dynamical: discrete-time topological dynamical systems Previously known as Miscellaneous, but it wasn't anymore.

Pattern_Sets, Concatenation: separate modules from Patterns

Metric_Space: separate module for some metric properties

Decidable: module for dealing with e.g. the finiteness

Language: separate module for languages as pattern-sets

Patterns_US: module for the uniform structure on patterns

Local_Rule: separate module for the anchored local rule

Prodiscrete: separete module for the topology-related stuff

Patterns: extended the equivalence proof (LR = UC) to subsets

55af6384
—
Pierre Guillon
6 months ago

adapted roadmap

Patterns: generalized the definition of entourage a little

Patterns: optimized the local rule and uniformity definitions They actually do not depend on the pro-discrete topology anyhow. These may & should be formulated directly with the configurations, so no conversion to/from the point-set is needed anymore. Thus moved the topology-related stuff to the end of the module.

Patterns: optimized the definition of an anchored pattern

Patterns: proved that the finite supports are decidable

Patterns: the local rule is equivalent to uniform continuity* * modulo the simplifications (only full shift, not any sub-shift), and also couple reasonable assumptions (e.g. decidable supports)

Uniform: fixed / clarified the definition of uniform continuity

Added a copying information (LGPL 2.1); improved .gitignore Same terms as of the dependencies: Coq itself and the topology library.

Patterns: broke up the uniformity proof into multiple lemmas