General stuff

General

Vernaculars like Theorem, lemma, etc

All of the following¹ can be used interchangably:

All of these are same as far as coq is concerned but judicious use can improve readability.

Variant vs Inductive

From the manual:

The Variant command is similar to the Inductive command, except that it disallows recursive definition of types (for instance, lists cannot be defined using Variant). No induction scheme is generated for this variant, unless the Nonrecursive Elimination Schemes flag is on.

Variant is same as Inductive except that:

Example:

Variant mbool : Type := mtrue | mfalse.
(* mbool is defined *)

Inductive mbool : Type := mtrue | mfalse.
(*
mbool is defined
mbool_rect is defined
mbool_ind is defined
mbool_rec is defined
mbool_sind is defined
*)

Variant mlist (A:Type) : Type :=
| mnil: mlist A
| mcons: A -> mlist A -> mlist A.
(*
Error:
Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.
*)

Nonrecursive Elimination Schemes flag can be set to allow induction principles generated for variants (and records) as well.

Set Nonrecursive Elimination Schemes.

Variant mbool : Type := mtrue | mfalse.
(*
mbool is defined
mbool_rect is defined
mbool_ind is defined
mbool_rec is defined
mbool_sind is defined
*)

See here for a discussion on Variant and Inductive.

'Record syntax' in inductive type definition

This is possible:

Inductive foo :=  go {_a:nat}.                
Print foo.                                    
(* Inductive foo : Set :=  go : nat -> foo. *)

Inductive foo2 :=  go {_a:nat; _b:nat}.                 
Print foo2.                                             
(* Inductive foo2 : Set :=  go : nat -> nat -> foo2.  *)

Case analysis a list into 3 parts

Goal forall (A:Type) (l : list A),
  match l with
  | [] => 0
  | [a] => 1
  | _ => 2
  end = length l.
Proof.
  move => A [|a[|l']].
(*
3 subgoals

A : Type

========================= (1 / 3)

0 = length []

========================= (2 / 3)

1 = length [a]

========================= (3 / 3)

forall l : list A, 2 = length (a :: l' :: l)
*)

–

Or the non-ssreflect way:

Goal forall (A:Type) (l : list A),
  match l with
  | [] => 0
  | [a] => 1
  | _ => 2
  end = length l.
Proof.
  intros A l.
  destruct l as [|a [|l']].
(*
3 subgoals

A : Type

========================= (1 / 3)

0 = length []

========================= (2 / 3)

1 = length [a]

========================= (3 / 3)

2 = length (a :: l' :: l)
*)

SProp

Strict Prop

Goal                                      
  forall (A:SProp) (P: A -> Prop) (x y:A),
    P x -> P y.                           
Proof.                                    
  intros.                                 
(*                                        
1 subgoal                                 

A : SProp                                 
P : A -> Prop                             
x, y : A                                  
H : P x

========================= (1 / 1)

P y
*)
  exact H.                                
  (* ∵ [x] and [y] are equivalent proofs of the same [SProp]: [A] *)
Qed.

https://coq.inria.fr/refman/addendum/sprop.html#basic-constructs

A Prop vs Type thing

https://stackoverflow.com/questions/40289890/coq-cant-discriminate-between-constructors-for-dependently-typed-inductive-prop

Tactic Notation

Notations at the tactic level.

See https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#coq:cmd.Tactic-Notation

Coercions

(Implicit) Coercions in Coq are merely for better convenience, it doesn't add any extra power. https://coq.inria.fr/doc/v8.18/refman/addendum/implicit-coercions.html

:> in record types

Have an implicit corecion from the record type to a particular field of that record.

For example ˡ:

Record nfa : Type := {
   nfa_state :> finType
 ; nfa_s : { set nfa_state }
 ; nfa_fin : { set nfa_state }
 ; nfa_trans : nfa_state -> char -> nfa_state -> bool
}.

Now we can have a value of type nfa and it can be implicitly converted to the value of its nfa_state field if needed.

A caveat

If we have a coercion like a2b: A >-> B,

Apparently, coercion search happens only in the RHS.

coqdoc

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

Verbatim

Code block example:

<<<
Definition incr (n: nat): nat := S n.
>>>

Inline example: << fst >> will give first element of a tuple

>> (and >> ??) can't show up in the verbatim text if we use the inline version.

Hiding/unhiding

(* begin hide *)
<hidden code>
(* end hide *)

Show some code when it's part of a hidden chunk:

(* begin show *)
<hidden code>
(* end show *)

Not sure

Canonical structures

Generalized rewriting

See: https://coq.inria.fr/doc/V8.19.0/refman/addendum/generalized-rewriting.html

Links:

(* Like cross-product. Length of output is product of lengths of inputs *)
Compute list_prod [1; 2] [3;4;5].                 
(*                                                
= [(1, 3); (1, 4); (1, 5); (2, 3); (2, 4); (2, 5)]
     : seq.seq (nat * nat)                        
*)                                                

(* Length of output is min of length of inputs *) 
Compute combine [1; 2] [3;4;5].                   
(*                                                
= [(1, 3); (2, 4)]                                
     : seq.seq (nat * nat)                        
*)

Tips

clear implicits

Instead of first declaring a type argument implicit in a bunch of constructors as in:

Inductive instr (A:Type) : Type :=
| Binop: instr A -> instr A -> instr A
| Unop: instr A -> instr A
| Const: A -> instr A.
Arguments Binop {A}.
Arguments Unop {A}.
Arguments Const {A}.

we could just do:

Inductive instr {A:Type} : Type :=
| Binop: instr -> instr -> instr
| Unop: instr -> instr
| Const: A -> instr.

Check instr.
(*
instr
     : Type
where
?A : [ |- Type]
*)

Arguments instr : clear implicits.

Check instr.
(* instr : Type -> Type *)

Got the idea from here.

A similar effect (not same) can be attained using the Uniform Inductive Parameters flag.

Set Uniform Inductive Parameters.

Inductive instr (A:Type) : Type :=
| Binop: instr -> instr -> instr
| Unop: instr -> instr
| Const: A -> instr.

Check instr.
(* instr : Type -> Type *)

Check Const.
(*
Const
     : forall A : Type, A -> instr A
*)

Mutually inductive types

Once got parameters got to be the same for all types in a mutually inductive setup. (ltamer)

Using Variable inside Section made it work.

This got error:

Inductive term {V:type->Type} {res:type} : Type :=
| Halt: V res -> term
| Bind: forall t:type,
    primop t       (* operation *)
 -> (V t -> term)  (* next thing to do *)
 -> term
| App:             (* Invoke a continuation *)
    V (Cont t)     (* Next thing. Why can't it just be [Cont t]? *)
 -> V t            (* Value to throw at the continuation *)
 -> term
with primop {V:type->Type} : type -> Type :=
| Var: forall {t:type}, V t -> primop t
| Tru: primop Bool
| Fls: primop Bool
| Pair: forall {t1 t2:type},
    V t1 -> V t2 -> primop (Prod t1 t2)
| Fst: forall {t1 t2:type}, Var (Prod t1 t2) -> primop t1
| Snd: forall {t1 t2:type}, Var (Prod t1 t2) -> primop t2.

This worked fine:

Section Foo.

Variable V:type->Type.
Variable res:type.

Inductive term : Type :=
| Halt: V res -> term
| Bind: forall t:type,
    primop t       (* operation *)
 -> (V t -> term)  (* next thing to do *)
 -> term
| App: forall t:type, (* Invoke a continuation *)
    V (Cont t)     (* Next thing. Why can't it just be [Cont t]? *)
 -> V t            (* Value to throw at the continuation *)
 -> term
with primop : type -> Type :=
| Var: forall {t:type}, V t -> primop t
| Tru: primop Bool
| Fls: primop Bool
| Pair: forall {t1 t2:type},
    V t1 -> V t2 -> primop (Prod t1 t2)
| Fst: forall {t1 t2:type}, V (Prod t1 t2) -> primop t1
| Snd: forall {t1 t2:type}, V (Prod t1 t2) -> primop t2.

End Foo.

Explicit type annotation advantage?

Could it be that having explicit type annotations can help reduce time to perform type checks?

Found this here:

The apparently redundant type annotation reduces checking time by 30%.

Succeed ⁹

Similar to Fail. Checks if the command succeeds and reverts its effects.

'Useful for writing tests.'

Succeed Compute S 3.
(*
= 4
     : nat

The command has succeeded and its effects have been reverted.
*)

Succeed Set Implicit Arguments.
(* The command has succeeded and its effects have been reverted. *)

Succeed Set Printing Notations.
(*
Set this option from the IDE menu instead

The command has succeeded and its effects have been reverted.
*)

Settings

Printing Projections

Changes the way record projections are printed.

Record egrec := BuildEgRec {
  num: nat
; flag: bool
}.

Example r := BuildEgRec 3 true.
Check num r.
(* num r : nat *)

Set Printing Projections.

Check num r.
(* r.(num) : nat *)

https://coq.inria.fr/refman/language/core/records.html#coq:flag.Printing-Projections

TODO Primitive Projections

https://coq.inria.fr/refman/language/core/records.html#coq:flag.Primitive-Projections

Use Print Implicit.

Eg:

Print Implicit inl.
(*
inl : forall {A B : Type}, A -> A + B

When applied to no more than 1 argument:
  Arguments A, B are implicit and maximally inserted
When applied to 2 arguments:
  Argument A is implicit
*)

Show memory used by coq

Print Debug GC.
(*
minor words: 7311684983.
promoted words: 119611354.
major words: 175152082.
minor_collections: 230
major_collections: 13
heap_words: 39796736
heap_chunks: 9
live_words: 13361868
live_blocks: 3944198
free_words: 26434337
free_blocks: 3
largest_free: 10299904
fragments: 531
compactions: 2
top_heap_words: 90810368
stack_size: 239
*)

Reference: https://coq.inria.fr/refman/proofs/writing-proofs/proof-mode.html#controlling-memory-usage

Debug

Test Debug shows the list of options related to debugging⁷:

Test Debug.
(*
Debug: -all,-backtrace,-vernacinterp,-unification,-tactic-unification,-proof-using,-native-compiler,-misc,-ho-unification,-congruence,-RAKAM,-Cbv
*)
RAKAM: Refolding Algebraic Krivine Abstract Machine [[8][⁸]]

have and opaqueness

Set vs Type

I guess only 'full types' can be Set:

Check bool: Set.
Check bool -> bool : Set.
Check list nat : Set.

Check list : Set.
(*
The term "list" has type "Type -> Type" while it is expected to have type
 "Set".
*)

coqc flags and options

https://rocq-prover.org/doc/v8.9/refman/practical-tools/coq-commands.html

Found from here:

(* Search only for definitions *)
Search (nat -> nat -> nat) is:Definition.
(* Fixpoints don't appear with this as of coq8.19, apparently *)

Hint databases

Links:

—

ltac

Intro

ltac debugging

https://stackoverflow.com/questions/52997319/is-printf-debugging-possible-in-ltac

Use idtac <msg-string>.

Misc

.
├── .github
│   └── workflows
│       ├── action-foo.yml
│       └── action-bar.yml
├── CHANGELOG.md
├── LICENSE
├── Makefile
├── Makefile.coq.local
├── README.md
├── _CoqProject
├── coq-project-name.opam
├── dune-project
├── meta.yml
└── theories
    ├── dune
    ├── foo.v
    └── bar.v

As per this convention, many of the files are meant to be autogenerated based on the information made available in the meta.yml file.