Home | Blog | Wiki | About

Info on some coq packages.

• CoqEAL
• QuickChick
• Hierarchy builder
• coqdoc
• company-coq (emacs)
• More packages

---

CoqEAL

General

• hrel: heterogeneous relation
• fun_hrel: To make a value of refines ??
• computable_scope notations with scope key C.

refines

refines: (A -> B -> Type) -> A -> B -> Type
         |              |
         +--------------+
            |
        refinement relation

From here:

Refinement relation:

(* Type of refinement relations *)
R: SpecT -> ImplT -> Type

Transport lemma:

R_op: refines refinement_relation Spec Impl

Example:

Definition tup2seq (n:nat)
  : n.-tuple bool -> seq bool -> Type :=
  fun btup bseq => tval btup = bseq.

(Pseudo-) examples:

• n.-tuple -> Vector.t n -> Type

Refinement relation for seqmx in CoqEAL

Rseqmx: https://github.com/coq-community/coqeal/blob/1.1.3/refinements/seqmx.v#L298

R ==> S (hrel)

If there are functions R: A -> B and S: A' -> B', then there exists a function (A -> A') -> (B -> B').

—

Notation for hrespectful R S.

From rel_scope.

R: A -> B -> Type
S: C -> D -> Type
f: A -> C
g: B -> D

is

R ==> S

which in turn is

hrespectful R S: (A->C) -> (B->D) -> Type :=

fun f g => forall (a:A) (b:B),
    R a b -> S (f a) (g b)

Guesses

R spec impl means

• R spec impl s i -> impl_of s = i (introduction)
• R spec impl s i -> spec_of i = s (elimination)

—

• spec_of: impl -> spec -> Type: type of specification functions
• impl_of: spec -> spec -> Type: type of implementation functions

fun_hrel

fun_hrel
     : forall A B : Type, (B -> A) -> A -> B -> Type

Like:

fun_hrel (A:=Spec) (B:=Impl): (Impl -> Spec) -> s -> i -> Type

QuickChick

Coq version of quickcheck

• Make a Show instance for printing test cases
  • Execution might get slower though..

Combinators:

• elems_: Select from a list of values
  • First argument is a default value
  • elems notation automatically generates the default value argument
• oneOf_: select from a list of generators
  • Notation: oneOf
• freq_: instruct qc to skew the distribution
  • Each generator has a nat-value as associated weight
  • Notation: freq
• listOf: Get a list of random length from a generator
• vectorOf: Get a list of fixed length from a generator
• choose: select a value from a given range
• sample: sample a generator

Check choose (0,3).
(* choose (0, 3) : G nat *)

Check List.hd 5 (sample (choose (0,3))).
(* List.hd 5 (sample (choose (0, 3))) : nat *)

Check choose.
(* choose : BinNums.N * BinNums.N -> G BinNums.N *)

Typeclasses:

• G: generator
• Producer: For types that are both enumerators and generators
  • Probably not meant to be used directly by users..

Links:

• https://softwarefoundations.cis.upenn.edu/qc-current/QuickChickInterface.html
• https://github.com/QuickChick/QuickChick/blob/master/examples/RedBlack/testing.v
• https://softwarefoundations.cis.upenn.edu/qc-current/QC.html

Hierarchy builder

General

• HB.about
• HB.check

HB.about isFinite.
(*
HB: isFinite is a factory (from "./fintype.v", line 161)

HB: isFinite operations and axioms are:
    - enum_subdef
    - enumP_subdef

HB: isFinite requires the following mixins:
    - hasDecEq

HB: isFinite provides the following mixins:
    - isFinite
*)

Links:

• https://github.com/math-comp/hierarchy-builder/
• https://math-comp.github.io/competing-inheritance-paths-in-dependent-type-theory/analysis-slides-ijcar.pdf

eta

From structures.v.

Notation "[ 'eta' f ]" := (fun x => f x) : fun_scope (default interpretation)

Core

• mixin: operator + properties

  • Naming convention: isStruct (eg: isFinite)

• structure: carrier + mixin

  • Naming convention: Struct

• (Canonical) Structure instance: Z_module

• factory

• builder

• abbreviation

coqdoc

https://coq.inria.fr/refman/using/tools/coqdoc.html

Sections

(** * Level 1

    H1 size section. *)

(** ** Level 2

    H2 size section. *)

Increase the number of asterisks accordingly.

Verbatim

Enclose between << and >>.

Multi-line

Like,

<<
  let rec fact n =
    if n <= 1 then 1 else n * fact (n-1)
>>

Inline

Like,

caml expression: << fact (n-1) >>

company-coq (emacs)

• View documentation of a word: C-c C-d

• View code outline in a separate buffer: C-c C-, (M-x company-coq-occur)

• Fold definition: C-c C-/

• Unfold definition: C-c C-\

• Make current goal a separate lemma: C-c C-a C-x

• Go to definition of identifier if present: M-. (doesn't play well with evil-mode)

• Insert a match case line: M-Ret

• grep current word in current directory sub-tree: C-c C-&

• Show diff of expected and actual types upon error: C-c C-a C-d

• Compare with error messages in docs: C-c C-a C-e

• Show/unshow definition of a name as an overlay: M-F12:

• Show documentation for a term if available: Type its name (at least partially) and do C-h

More packages

• mathcomp 2.0:

  • uses hierarchy builder.
  • not completely compatible with older versions.

• coq-ext-lib: has an hlist implementation

• trocq: refinements, proof transfer

• coinduction

• param

• CoRN

• CoLoR

• paramcoq:

  • https://github.com/coq-community/paramcoq
  • Provides Parametricity vernacular command.

• Pretty output/interface:

  • CoqdocJS
  • Alectryon

Better 'stdlib'

Efforts have been made to augment Coq's stdlib. ʳ.

• stdpp (std++)
• stdlib2 (looks bit inactive)
  • Seems to use mathcomp under the hood.

mathcomp has got a lot of stuff as well.

SAT/SMT interfaces, AI, etc

• coq-hammer
• tactician
  • tactician enable: makes ~/.coqrc file that always import tactician.
  • opam install coq-tactician-stdlib: Optional, recompiles standard library
• SMTCoq