Info on some coq packages.

• CoqEAL
• QuickChick
• Hierarchy builder
• coqdoc
• company-coq (emacs)
• Ltac2
• 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

Ltac2

• https://github.com/tchajed/ltac2-tutorial

Import with:

From Ltac2 Require Import Ltac2.

Modify a previously defined tactic

Use Ltac2 mutable when defining the tactic for the first time.

• https://coq.inria.fr/doc/v8.19/refman/proof-engine/ltac2.html#ltac2-definitions
• https://sympa.inria.fr/sympa/arc/coq-club/2024-12/msg00023.html

From Ltac2 Require Import Ltac2.

(* Initial definition *)
Ltac2 mutable x_mut := 3.
Ltac2 Eval x_mut.   (* - : int = 3 *)        

(* Changing definition *)
Ltac2 Set x_mut := 2.    
Ltac2 Eval x_mut.   (* - : int = 2 *)        

Attempts to modify an ltac2 tactic which was not explicitly set as mutable results in error.

Ltac2 x_immut := 3.                          

Fail Ltac2 Set x_immut := 2.                 
(*                                           
The command has indeed failed with message:  
The tactic x_immut is not declared as mutable
*)                                           

Old value of a mutable tactic can be accessed while redefining it using as:

Ltac2 mutable f x := Int.add x 1.                          
Ltac2 Eval f 3.                                            
(* - : int = 4 *)                                          

Ltac2 Set f as oldf := fun x => Int.add 10 (oldf x).       
Ltac2 Eval f 3.                                            
(* - : int = 14 *)                                         

Use ltac1 tactics in ltac2

Possible with ltac1:(tactic_name).

Ltac2 newintros () := ltac1:(intros).                                 

Tactic definitions without arguments

Must have at least a () as argument.

Fail Ltac2 newintros := ltac1:(intros).                               
(*
The command has indeed failed with message:                           
Tactic definition must be a syntactical value. Consider using a thunk.
*)

Ltac2 newintros () := ltac1:(intros).                                 

Notations

Ltac1 tactics are not available when using ltac2. Notations are helpful to reclaim use of ltac1.

Ltac2 newintros () := ltac1:(intros).                                 
Ltac2 Notation "intros" := newintros ().

Changing default tactic language

https://coq.inria.fr/doc/v8.19/refman/proofs/writing-proofs/proof-mode.html#coq:opt.Default-Proof-Mode

(* Use ltac1. This is the default. *)
Default Proof Mode "Classic".


(* Use ltac2. Require it first. *)
(* Importing Ltac2 implicitly sets default proof mode to ltac2. *)
From Ltac2 Require Ltac2.
Default Proof Mode "Ltac2".

Exceptions

• Panics: Non-backtracking exceptions
• There are also 'backtracking primitives'

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