Using mathcomp

mathcomp is consists of many 'parts'. Including:ˡ:

mathcomp-algebra
mathcomp-character
mathcomp-field
mathcomp-fingroup
mathcomp-ssreflect

General

case eqn:H: to remember the relation even after a case split
<name>.+1: S for nat
- ie, n.+1 just another notation for writing S n
- This is probably because 1 by itself could mean the 1 of a ring.
- Eg: Compute 3.+1. (* = 4 : nat *)
- .+2, .+3 and .4 also available.
<name>.*2: double a nat
- Only n.*2 would work. n.*3 is syntax error.
- Eg: Compute 3.*2. (* = 6%N : nat *)
- Eg: Compute 3.*3. (* Syntax Error: Lexer: Undefined token *)
<name>./2: halve a nat (floor)
<name>^3: exponentiation for nat
- Looks like it's a ring operation for other types
<name>.1 and <name>.2: first and second elements of the tuple named name
<n>.-tuple:
- where n is a number
- Eg: 2.-tuple nat
#|typ|: cardinality of type
ffun: finite function
- ie, function whose domain is a finite type.
\sum_ (low <= i < high): Represents ∀i:ℕ, i ∈ [low, high), Σ i
- ie, sum of all natural numbers from low and upto high.
%/: ??
^+: ??
%|: check if LHS divides RHS
- Compute 8 %| 16. (* true: bool *)
|:: ??
:&:: ??
:==: ??
^: exponentiation (for nat)
- Eg: Compute 3 ^ 4. (* = 81 : nat *)
n`!: factorial (ie, n!)
[seq x <- lst | condition]: notation for filter (fun x => condition) lst
- Forget the seq in the beginning and then it might look better.
[seq x' | x <- lst]: notation for map (fun x => x') lst
=1 (infix): eqfun (1-arg functional extensionality)
=2 (infix): eqrel (2-arg functional extensionality)
=i (infix): eq_mem (extensional equality)
=P (infix): reflection involving bool
- Notation "x =P y" := (eqP : Bool.reflect (eq x y) (eq_op x y)) : eq_scope
Curly braces are used for types with parameters.
- Eg: {set A}
elim/<ind_principle>:
- where the /<ind_principle> is optional. It can be given if an induction principle other than the default one is to be used.

finset

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/finset.v

Set membership indicated by a finite function (ffun pred T)
Sets are defined only on finite types.
Empty boolean set??: [set: bool]
For set equality proofs, use apply/setP
To change from x \in s = false to x \notin s, use apply/negbTE

Inductive set_type (T: finType): predArgType :=
| FinSet: {ffun pred T} -> set_type T.

Essentially just the characteristic function of the set.

mem A: the predicate corresponding to A (from finset.v)
setX: Cartesian product
cover: 'flatten' a set of sets

Description	Mathcomp	Function
x ∈ A	x ∈ A
∅	set0
A U B	A :│: B	setU
A ∩ B	A :&: B	setI
{X} U A	X │: A
complement A	~: A	setC
A \ B	A :\: B	setD
A \ {x}	A :\ x
Powerset	powerset A
Singleton {x}		set1 x
Like a map fun	f @: A	imset
Like a map fun	f 2@: (A, B)	imset2
	f @^-1: A
Cardinality	#│A│
A == B	A :==: B	(bool)
A = B	A :=: B	(Prop)
A != B	A :!=: B	(bool)
A ≠ B	A :<>: B	(Prop)
??	A :=P: B	??

Example:

From mathcomp Require Import all_ssreflect.

Check [set true]: {set bool}.

Check [set true]: {set bool}.                                                
(* [set true] : {set bool} : {set bool} *)                                   

Check [set true; false]: {set bool}.                                         
(* [set true; false] : {set bool} *)                                         

Check [set true; false; false]: {set bool}.                                  
(* [set true; false; false] : {set bool} : {set bool} *)                     


Compute [set true; false; false]: {set bool}.                                
(*                                                                           
= [set x | (if                                                               
                  [set x0 | (if [set true] x0 then true else [set false] x0)]
                    x                                                        
                 then true                                                   
                 else [set false] x)]                                        
     : {set bool}
*)

More examples:

Example eg: {set bool*unit} := [set (true,tt); (false, tt)].

Check snd @: eg.
(* [set x.2 | x in eg] : {set Datatypes_unit__canonical__fintype_Finite} *)

Check snd @: eg : {set unit}.
(* [set x.2 | x in eg] : {set unit} : {set unit} *)

–

Not extraction friendly in terms of efficient computation.

finfun (`ffun`)

'functions with finite domain':
- https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/finfun.v
- f(x) ∉ {∞, -∞}

Inductive finfun_on (aT: finType) (rT: aT -> Type)
   : seq aT -> Type :=                            
| finfun_nil: finfun_on (aT:=aT) rT [::]          
| finfun_cons: forall (x : aT) (s : seq aT),      
    rT x ->                                       
    finfun_on (aT:=aT) rT s ->                    
    finfun_on (aT:=aT) rT (x :: s).

injective f: f x = f y -> x = y
f ^~ y\: essentially a means to flip the argument order of a 2-argument function
- f ^~ y : fun x > f x y

pred

From eqtype.v:

pred1
- pred1 a is fun (a:A) (b:A): bool := eqb a b
- pred2, pred3, pred4 also available
predC1 p: ¬p
- predC1 a is fun (a:A) (b:A): bool := negb (eqb a b)
predU p q: p ∪ q
predD p q: p \ q

in is usually associated with iteration. \in indicates membership.

ssrbool

rel: Type of a kind of relations
- rel: Type -> Type := T -> pred T

ssrfun

cancel f g: ∀x, g (f x) = x
- f is applied first, then g is applied

TODO Phantom types

Mathcomp book: 6.10.1

Some notations

==>: boolean implication

Bool

`&&`	`andb`
`││`	`orb`
`==`	`eqb`

pred

[pred x:T | condition]: unary boolean predicates
- Accept a value of type T and give bool result of the condition
- Like P: T -> bool

N-ary notations

Arbitrary arity:

[:: 1, 2, 3]	[1,2,3]
[:: 1, 2 & l]	1 :: 2 :: l]
[==> b1, b2 => b3]	b1 ==> b2 ==> b3
[&& true, false & true]	true && false && true
[││ true, false │ true]	true ││ false ││ true

Non-arbitrary arity:

[/\ p1, p2 & p3 ]	p1 /\ p2 /\ p3	only upto 5 terms
[\/ p1, p2 │ p3 ]	p1 \/ p2 \/ p3	only upto 4 terms

Bracket notations

[seq .. | .. ]

Page 39 mathcomp book

seq (lists)

mathcomp	stdlib
`[::]`	`[]`
`[:: a]`	`[a]`
`[:: 1, 2, 3]`	`[1,2,3]`
`[:: 1, 2 & l]`	`1 :: 2 :: l`

last: Get last element of x::l with last x l
- last: A -> seq A -> A
- Clever way to ensure the list is non-empty..
flatten: 'flatten' a list of lists to a simple list

finType

enum: like forall A:finType, list A

eqType

Types with decidable equality.

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/eqtype.v

Subtypes:

subType P: like x: T | P x
insub x: T -> option S
- Value corresponding to x:T in another type S which is a subtype of T, if it exists.
insubd x: T -> S
- Similar to insub except that a default value is given if there's no possible projection in the subtype.
Sub x Px: Generic constructor for a subtype
\val: Generic injection from a subtype to the supertype

Same as in standard coq but 'renamed'

mathcomp	stdlib	Reason
`seq`	`list`	`seq` used to be different earlier
`erefl`	`Logic.eq_refl`	MC's `eq_refl` is something else

Syntax

'let-in' construct (`:=`)

Can be used to have a name for an expression used multiple times.

An example from mathcomp book:

Lemma edivnP m d (ed := edivn m d):
  ((d>0) ==> (ed.2<md)) && (m == ed.1*d + ed.2).

where ed is defined and then used multiple times.

`let:`

Seems like a concise match.
Useful for types with only one constructor.

Example:

From mathcomp Require Import all_ssreflect all_algebra.

Inductive point: Type :=
| Point (x y z: nat).

Definition getX (p: point): nat :=
  let: Point x _ _ := p in x.
Compute getX (Point 1 2 3).
(* = 1 : nat *)

Some types

`bigop`

Definition and notations

A special form of foldr.

The name is 'big op' because it's used to represent operations commonly denoted using upper case Greek letters. Like Σ, Π, etc.

Takes following arguments:

`r: seq I`	a range
`op: R -> R -> R`	an operation
`idx: R`	a neutral element
`F: I -> R`	general term (transforms I to R)
`P : pred I`	filtering predicate

The actual operation is done like:

foldr (λi acc => if P i then op (F i) acc
                 else acc) idx r

Steps:

Take elements of r that satisfy P
Use F to convert these elements to type R
Use op to combine with accumulator value to get new accumulator.

Notations:

`\big[op / idx]_ (i <- r │ P) F`	`bigop {R I: Type} (idx: R) (op: R->R->R)`
	`(r: seq I) (P: pred I) (F: I->R): R`
`\sum_ (i <- r │ P) F`	`\big[+%N / 0%N]_ (i <- r │ P%B) F%N`	I: ℕ
		R: ℕ
		P: ℕ -> 𝔹
		F: ℕ -> ℕ

With upper and lower bounds:

`\big[op / idx]_ ( low <= i < high │ P) F`	`bigop idx op (index_iota low high) P F`
`\sum_ (low <= i < high │ P) F`	`\big[+%N / 0%N]_ (low <= i < high │ P%B) F%N`

i <-r | P means 'from r, take elements that satisfy P.

—

\sum_ is defined in terms of \big[ _ / _], which in turn is defined using bigop.

https://github.com/math-comp/math-comp/blob/mathcomp-2.0.0/mathcomp/ssreflect/bigop.v#L629
https://github.com/math-comp/math-comp/blob/mathcomp-2.0.0/mathcomp/ssreflect/bigop.v#L662
\big [ op / idx ]_ ( i <- r | P ) F is (bigop idx r (fun i => BigBody i op P%B F))
\sum_ ( i <- r | P ) F is (\big[+%N/0%N]_(i <- r | P%B) F%N)

As for Bigbody, it's apparently just a wrapper. From mathcomp source:

The bigbody wrapper is a workaround for a quirk of the Coq pretty-printer, which would fail to redisplay the notation when the <general_term> or <condition> do not depend on the bound index. The BigBody constructor packages both in in a term in which i occurs; it also depends on the iterated <op>, as this can give more information on the expected type of the <general_term>, thus allowing for the insertion of coercions.

The general form for iterated operators is ʳ:

<bigop>_<range> <general_term>

—

iota and similar

Function that generates all the nat numbers within a range.

iota start count

Example:

Compute iota 2 5.
(* = [:: 2%N; 3%N; 4%N; 5%N; 6%N] : seq nat *)

—

index_iota:

Similar to iota, except that instead of number of elements, upper limit (exclusive) is taken as argument.

Compute index_iota 2 8.
(* = [:: 2; 3; 4; 5; 6; 7] : seq nat *)

Compute index_iota 2 5.
(* = [:: 2; 3; 4] : seq nat *)

Lemmas
- big_ord_recr: recursion (right)
  - decompose to last element and remaining
- big_ord_recl: recursion (left)
  - decompose to first element and remaining
- big_mkcond: move filter P 'into the generic term'
- big_cat: bigop involving concatenation of two sequences
- big_ord0: base case

`ordinal`

'I_n: nat numbers less than n. Notation for ordinal n.
ord_enum: nat -> seq: enumerate all elements of type 'I_n
lift: 'I_n -> 'I_n.-1 -> 'I_n
unlift: 'I_n -> 'I_n -> option 'I_n.-1
lshift: 'I_m -> 'I_(m+n): Shift to left, making space in right
rshift: 'I_n -> 'I_(m+n): Shift to right, making space in left

tuple

n.-tuple is essentially a seq with a proof that its length is less than n.

n.-tuple is notation for tuple_of n
[tuple]: empty tuple
[tuple x1; x2; ... ; xn]: a value of type n.-tuple
tval: get seq component of n.-tuple

`matrix`

fun_of_matrix: get function that makes the matrix
'M[R]_ (rows, cols): type of rows x cols matrix with elements of type R.
'M[R]_ n: type of square matrix of size n with elements of type R.
\matrix_ (i, j) E: make a matrix value from a function.
- E is like a function that takes row and column indices and returns cell values.
\matrix_ (i < m, j < n) E: similar to \matrix_ (i, j) but with additional constraints.
- Eg: Definition diagonal := \matrix_ (i < 3, j < 3) if i==j then 1 else 0.
\tr m: find trace (ie, sum of main diagonal) of a square matrix m.
M^T or trmx M: transpose of a matrix M
addmx: matrix addition
*m: matrix multiplication (infix operator)
a%:M: scalar matrix with a-s on main diagonal.
- ie, 1%:M would be identity matrix.
M ^f or map_mx: map operation
const_mx: constant matrix

'M_(2,3): 2x3 matrix of unknown type
'M[int]_(2,3): 2x3 matrix of int type
'M_n: type of square matrix of size n (element type implicit)
- 'M[bool]_3: bool square matrix of size 3
'rV_2: row vector of size 2 (element type implicit)
'cV_2: column vector of size 2 (element type implicit)

Submatrices:

row i M: Get ith row
col j M: Get jth column
row' i M: Get M with ith row removed
col' j M: Get M with jth column removed

Block matrix building:

row_mx Ml Mr: stack Ml and Mr horizontally
col_mx Mu Md: stack Mu and Md vertically
block_mx Mul Mur Mdl Mdr: make a matrix with 4 other matrices

Check matrix bool 3 4.
(* 'M_(3, 4) : predArgType *)

Check 'M_(3, 4).
(*
'M_(3, 4)
     : predArgType
where
?R : [ |- Type]
*)

Check 'M[bool]_(3, 4).
(* 'M_(3, 4) : predArgType *)

(* A square matrix *)
Definition M2 : 'M[int]_(2,2) := \matrix_(i,j < 2) 3%:Z.

(* A non-square matrix *)
Example eg1: 'M[int]_ (3, 7) := \matrix_(i<3, j<7) 8%:Z.

(* A row matrix *)
Example eg7: 'rV_2 :=
  \row_(i<2) (if i==0 then true else false).

Lemmas
- ffunE

`seq`

seq seems to be simply notation for list.

Print seq.
(* Notation seq := list *)

Check [:: 1; 2; 3].
(* [:: 1; 2; 3] : seq nat *)

—

Infinite sequences are also possible:

(* Finite sequence *)
Check 1 :: 2 :: 3 :: nil.
(* [:: 1; 2; 3] : seq nat *)

(* Prepending to a list 'l' *)
Check fun l => 1 :: 2 :: 3 :: l.
(*
fun l : seq nat => [:: 1, 2, 3 & l]
     : seq nat -> seq nat
*)

Infinite sequence has an & at its end and its elements are separated by a , instead of ;.

—

algebra (`ssralg`)

https://math-comp.github.io/htmldoc/mathcomp.algebra.ssralg.html

comSemiRingType: Commutative semiring
- Only in mathcomp2
nmodType: Structure for additive Abelian monoid
zmodType: Structure for additive Abelian groups (ie, nmodType with additive inverses)

finType

ord0: smallest element of a 'I_n.+1
ord_max: largest element of a 'I_n.+1
lift: lift a 'I_n to 'I_n.+1 (ie, make the type 'wider' by one)
unlift: 'I_n to 'I_n.-1 if possible (ie, make the type 'narrower by one)

Locking and unlocking

https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#locking-unlocking

Controls unfolding during a simpl in proofs. To prevent large terms showing all at once.

Unfold locked term: rewrite unlock

lock: forall [A : Type] (x : A), x = locked x
unlock: forall [T : Type] [x : T] (C : unlockable x), unlocked C = x

composable_lock: unit

locked: forall [A : Type], A -> A
unlocked: forall [T : Type] [v : T], unlockable v -> T

unlockable: forall [T : Type], T -> Type
Unlockable: forall [T : Type] [v unlocked : T], unlocked = v -> unlockable v

locked_with: unit -> forall T : Type, T -> T
locked_with_unlockable: forall [T : Type], unit -> forall x : T, unlockable x

unlock_with:
  forall [T : Type] (k : unit) (x : T),
  unlocked (locked_with_unlockable k x) = x

Proof mode

/<lemma-name>: simplify with <lemma-name> and then use.
//: simplify beforehand
- Equivalent to try done.
/=: invokes the simpl tactic ʳ
//=: // followed by /=
- Equivalent to simpl; try done.
=>: revert a hypothesis from stack
:: move an assumption to stack (discharge)
have: like assert. Start a new sub-proof.
- Useful for forward reasoning.
move: move assumption to and from stack
rewrite -<lemma-name>: rewrite from right to left (the minus changes the direction)
rewrite !<lemma-name>: rewrite all occurrences (without the !, only 1st occurrence is rewritten)
Can rewrite with multiple theorems at once.
move=> ->. is same as move=> H; rewrite H.
{-2}n capture all occurrences of n except the second
- Example: rewrite {3}/foo. (rewrite only 3th instance of foo)

`rewrite`

Perhaps most useful part of ssreflect usage.

rewrite /<definition> is same as unfold <definition>
rewrite -/<definition> is same as fold <definition>

Tactics and tacticals

have
unlock
move
do: for iteration
- do 1? <tactic>: at most once
- do 2! <tactic>: exactly twice
- do ! <tactic>: as many times as possible, but at least once

`unlock` lemma

A lemma that can be used to unlock definitions?

Check unlock.
(*
unlock : forall (T : Type) (x : T) (C : unlockable x),
  unlocked C = x
*)

From https://www.math.nagoya-u.ac.jp/~garrigue/lecture/2017_AW/mathcomp-1.6/htmldoc/mathcomp.ssreflect.ssreflect.html:

unlockable v == interface for sealed constant definitions of v.

Naming conventions

Made uniformly in mathcomp. Makes it way easier to remember: https://github.com/math-comp/math-comp/blob/mathcomp-2.0.0/CONTRIBUTING.md#naming-conventions-for-lemmas-non-exhaustive

reflection view lemmas end with a 'P'.
- Example: eqnP
ubn lemmas: stands for 'upper bound'

—

C: Commutativity
A: Associativity
K: cancellation
- As in cancel the effect of a definition.

—

Functions available:

commutative
associative
transitive
antisymmetric
reflexive
antireflexive

ssreflect

Some tutorials:

Inductive reflect (P: Prop): bool -> Type :=
| Reflect_true : P -> reflect P true
| Reflect_false : ~P -> reflect P false.

reflect type usage is like

reflect (equality-in-Prop) (equality-in-bool)

by [] is equivalent to done tactic.

Given a value of reflect P b, these are useful to 'project' components:

elimT: .. reflect P b -> b -> P
introT: .. reflect P b -> P -> b
elimF: .. reflect P b -> ~b -> ~P
introF: .. reflect P b -> ~P -> ~b

mathcomp2

Uses Hierarchy builder (HB).

From HB Require Import structures.

Links:

Uses HB and mathcomp2 now: https://github.com/math-comp/dioid/blob/master/complete_dioid.v

Hierarchy builder (HB)

References:

https://perso.crans.org/cohen/JFLA23/hb.pdf (slides from 2023)
https://inria.hal.science/hal-02478907v6/document (paper)

Primitives in HB

https://perso.crans.org/cohen/JFLA23/hb.pdf

HB.mixin
HB.factory
HB.builders: like constructor for a factory??
HB.structure
HB.instance

`HB.about`

From mathcomp Require Import ssralg.

HB.about comSemiRingType.
(*
HB: comSemiRingType is a structure (from "./algebra/ssralg.v", line 2502)

HB: comSemiRingType characterizing operations and axioms are:
    - mulrC

HB: GRing.ComSemiRing is a factory for the following mixins:
    - GRing.isNmodule
    - hasChoice
    - hasDecEq
    - GRing.Nmodule_isSemiRing
    - GRing.SemiRing_hasCommutativeMul (* new, not from inheritance *)

HB: GRing.ComSemiRing inherits from:
    - eqtype.Equality
    - choice.Choice
    - GRing.Nmodule
    - GRing.SemiRing

HB: GRing.ComSemiRing is inherited by:
    - GRing.ComRing
    - GRing.ComAlgebra
    - GRing.ComUnitRing
    - GRing.ComUnitAlgebra
    - GRing.IntegralDomain
    - GRing.Field
    - GRing.DecidableField
    - GRing.ClosedField
    - GRing.SubComSemiRing
    - GRing.SubComRing
    - GRing.SubComUnitRing
    - GRing.SubIntegralDomain
    - GRing.SubField
    - Num.NumDomain
    - Num.ArchiNumDomain
    - Num.NumField
    - Num.ClosedField
    - Num.RealDomain
    - Num.RealField
    - Num.RealClosedField
    - Num.ArchiNumField
    - Num.ArchiClosedField
    - Num.ArchiDomain
    - Num.ArchiField
    - Num.ArchiRealClosedField
    - FinRing.ComSemiRing
    - FinRing.ComRing
    - FinRing.ComUnitRing
    - FinRing.IntegralDomain
    - FinRing.Field
    - CountRing.ComSemiRing
    - CountRing.ComRing
    - CountRing.ComUnitRing
    - CountRing.IntegralDomain
    - CountRing.Field
    - CountRing.DecidableField
    - CountRing.ClosedField
*)

`HB.howto`

Shows possible ways in which a structure can be attained for a type.

(* Show how to make [option] type a commutative semiring *)
HB.howto option comSemiRingType.
(*
HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
    - GRing.isNmodule; GRing.Nmodule_isComSemiRing
    - GRing.isSemiRing; GRing.SemiRing_hasCommutativeMul
    - GRing.isNmodule; GRing.Nmodule_isSemiRing;
      GRing.SemiRing_hasCommutativeMul
*)

Here, 3 possible routes are shown.

Terms

Telescope
Phantom parameters
Packed class

`:>` symbol

Coq syntax.

https://stackoverflow.com/questions/51404367/the-coq-symbol

Focusing on subgoals

Unlike usual coq, by default, mathcomp makes doesn't focus on subgoal when we use bullets.

We can use focus brackets (ie, a { , } pair). A { focuses on first sub-goal.

Could also focus on n-th subgoal with n-{ <tactics> }.

Another way is to change the setting with

Set Bullet Behavior "Strict Subproofs".

Don't use Focus. It's deprecated.

–

Info thanks to this discussion.

Info

fold / unfold is usually not needed with ssreflect because rewrite handles that as well (among many other things with its numerous flags).
- https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#rewriting-ssr
Usage with nix: https://github.com/math-comp/math-comp/wiki/Using-nix/
eqn is same as Nat.eqb

Doubts

[ ] program obligation not applicable to mathcomp?
[X] refine not applicable to mathcomp? It is
[ ] under tactic
[ ] [] in rewrite. To override default inferred args?

Resources

mathcomp book
ssreflect manual

General

finset

finfun (ffun)

pred

ssrbool

ssrfun

TODO Phantom types

Some notations

Bool

pred

N-ary notations

Bracket notations

seq (lists)

finType

eqType

Same as in standard coq but 'renamed'

Syntax

'let-in' construct (:=)

let:

Some types

bigop

ordinal

tuple

matrix

seq

algebra (ssralg)

finType

Locking and unlocking

Proof mode

rewrite

Tactics and tacticals

unlock lemma

Naming conventions

ssreflect

mathcomp2

Hierarchy builder (HB)

Primitives in HB

HB.about

HB.howto

Terms

:> symbol

Focusing on subgoals

Info

Doubts

Resources

finfun (`ffun`)

'let-in' construct (`:=`)

`let:`

`bigop`

`ordinal`

`matrix`

`seq`

algebra (`ssralg`)

`rewrite`

`unlock` lemma

`HB.about`

`HB.howto`

`:>` symbol