Coq library for reasoning inductively and coinductively on infinite sequences, using modal operators similar to those in linear temporal logic (LTL).
- Author(s):
- Yuxin Deng (initial)
- Jean-Francois Monin (initial)
- Karl Palmskog
- Ryan Doenges
- Compatible Coq versions: 8.7 or later
- Additional dependencies: none
- Coq namespace:
InfSeqExt
- Related publication(s): none
The easiest way to install InfSeqExt is via OPAM:
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
opam install coq-inf-seq-ext
To instead build and install manually, do:
git clone https://github.com/DistributedComponents/InfSeqExt.git
cd InfSeqExt
make # or make -j <number-of-cores-on-your-machine>
make install
InfSeqExt is based on an earlier library by Deng and Monin. It is intended as a more comprehensive alternative to Streams in the Coq standard library. In particular, InfSeqExt provides machinery commonly used when reasoning about temporal properties of system execution traces, and follows the modal operator name conventions used in the Spin model checker.
infseq.v
: main definitions and results- coinductive definition of infinite sequences
- definitions and notations for modal operators and connectors
- basic modal operators:
now
,next
,consecutive
,always1
,always
,weak_until
,until
,release
,eventually
- composite modal operators:
inf_often
,continuously
- modal connectors:
impl_tl
(->_
),and_tl
(/\_
),or_tl
(\/_
),not_tl
(~_
)
- basic modal operators:
- lemmas about modal operators and connectors
- tactics
map.v
: corecursive definitions of themap
andzip
functions for use on infinite sequences, and related lemmasexteq.v
: coinductive definition of extensional equality (exteq
) for infinite sequences, and related lemmassubseq.v
: coinductive definitions of infinite subsequences and related lemmasclassical.v
: lemmas about modal operators and connectors when assuming classical logic (excluded middle)
InfSeqExt has some overlap with the less exhaustive CTLTCTL and LTL Coq contributions, which provide similar machinery. In contrast to CTLTCTL and LTL, InfSeqExt does not provide a definition of traces following some labeled reduction relation, nor an explicit notion of time. Fairness is also left up to library users to define.