## Stream: Coq users

### Topic: reading ssreflect related books

#### Andrey Klaus (May 18 2021 at 08:05):

Hello, quick question if anybody has a minute...
What is `[pred y | y == x]`? It is on page 144, expression is `Notation count_mem x := (count [pred y | y == x])`.

#### Andrey Klaus (May 18 2021 at 08:09):

I see in general that this "count_mem x" is thing of type `t -> seq t-> nat`. I'm interested in comment about `[pred y | y == x]`. I'm not sure I understand this notation.

#### Kenji Maillard (May 18 2021 at 08:15):

It's a notation for the (bool-valued) predicate `fun y => y == x` defined in ssrbool

I see, thank you

#### Enrico Tassi (May 18 2021 at 10:27):

The pattern in mathcomp is to use `[something x | ...]` to denote comprehension like constructions. You find for example `[seq x | ...]` for the sequence of xs such that...

I see, thank you

#### Andrey Klaus (May 18 2021 at 13:20):

page 145

``````From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Inductive ordinal (n : nat) : Type := Ordinal m of m < n.
Notation "''I_' n" := (ordinal n).
Coercion nat_of_ord i := let: @Ordinal m _ := i in m.
``````

String `Coercion nat_of_ord i := let: @Ordinal m _ := i in m.` gives me an error: `Error: The constructor Ordinal (in type ordinal) expects 2 arguments.`.
Speaking roughtly, I think understand how should it work. But there is also the lemma `val_ord_enum` below `nat_of_ord` which rises an error too and I would like go through its proof. If anybody have quick fix, could you put it here please. If not, its not a big deal.

#### Enrico Tassi (May 18 2021 at 13:45):

Hum, looks like a typo. Ordinal has 3 arguments, n m and (p : m < n). Maybe it is defiend in a section in the actual mathcomp, and we made a mistake while testing the code in the book.

#### Enrico Tassi (May 18 2021 at 13:46):

I mean, it should be `let: @Ordinal _ m _ := i in m.`

#### Enrico Tassi (May 18 2021 at 13:48):

Oh no, wait. It's the `Set Asymmetric Patterns` thing. I guess it is on because you imported mathcomp, but we tested the code with a different header, which does not set it.

#### Enrico Tassi (May 18 2021 at 13:48):

`n` is a parameter, so you are not allowed to bind it in the pattern.

#### Enrico Tassi (May 18 2021 at 13:50):

OK, it's both ;-)

Here a line which works

``````Coercion nat_of_ord n (i : 'I_n) := let: @Ordinal _ m _ := i in m.
``````

#### Enrico Tassi (May 18 2021 at 13:51):

I've opened an issue: https://github.com/math-comp/mcb/issues/116

#### Andrey Klaus (May 18 2021 at 15:13):

Thank you, Enrico. It works.

#### Andrey Klaus (May 18 2021 at 15:29):

the next string namely
`Canonical ordinal_subType := [subType for nat_of_ord].` says to me now
```The term "nat_of_ord" has type "forall n : nat, 'I_n -> nat" while it is expected to have type "nat -> ?T" (cannot instantiate "?T" because "n" is not in its scope).```

#### Enrico Tassi (May 18 2021 at 16:08):

It's the section problem, the code was copied from a Section with a variable n. This should work:

``````Canonical ordinal_subType n := [subType for nat_of_ord n].
``````

#### Andrey Klaus (May 19 2021 at 08:12):

Thank you.
To give a bit more details, first small problem for me in Chapter 7 was in the 2nd line of code (p.138)

``````From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Structure tuple_of n T := Tuple { tval :> seq T; _ : size tval == n }.
Notation "n .-tuple T" := (tuple_of n T).
``````

Just to clarify, I create new file for each new chapter of the book and then I copy headers from the very first chapter. So, this one is named `Ch7.v` and you can see above what it contains.
Coq answers me next when I give him code above `Error: A left-recursive notation must have an explicit level.`
I changed last line to `Notation "n .-tuple T" := (tuple_of n T) (at level 0).` and it works.

But some other code blocks in the book below give an errors to me too. In example (p.139),

``````From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Structure tuple_of n T := Tuple { tval :> seq T; _ : size tval == n }.
Notation "n .-tuple T" := (tuple_of n T) (at level 0).

Notation "X (*...*)" := (let x := X in let y := _ in x)  (at level 100, format "X (*...*)").
Notation "[LHS ’of’ equation ]" := (let LHS := _ in let _infer_LHS := equation : LHS = _ in LHS)  (at level 4).
Notation "[unify X ’with’ Y ]" := (let unification := erefl _ : X = Y in True).

Check forall T n (t : n.-tuple T),
let LHS := [LHS of size_tuple _] in
let RDX := size (rev t) in
[unify LHS with RDX].
``````

says me `Error: Syntax error: [term level 200] expected after ':=' (in [binder_constr]).`
I'm not sure how the book reader is intended to organize his code. I think this can be an issue.

#### Enrico Tassi (May 19 2021 at 12:27):

Well, at some point we had these files available on the website via jscoq: https://github.com/math-comp/mcb/blob/master/coq/chSigma.v but we had no energy to put them back online.

#### Enrico Tassi (May 19 2021 at 12:28):

I guess we remove from the TeX the level of the notation, since we were not discussing it.

#### Andrey Klaus (May 19 2021 at 13:38):

Thanks for the link. Code from chSigma.v works with minor changes.

#### Andrey Klaus (May 19 2021 at 13:39):

Some parts of code in the book are skipped by some reason. In example `Arguments Tuple {n T _} _.`.

#### Andrey Klaus (May 19 2021 at 13:40):

My skills were not enough to figure out how should it work, so, chSigma.v helped very much to me.

#### Andrey Klaus (Jun 04 2021 at 12:32):

on page 151 we have

``````Lemma mxtrace_mulC R m n (A : 'M[R]_(m, n)) B : \tr (A *m B) = \tr (B *m A).
``````

I try to compile an expression above using mathcomp.algebra.matrix.

``````From mathcomp Require Import all_ssreflect.
From mathcomp Require Import algebra.matrix.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma mxtrace_mulC R m n (A : 'M[R]_(m, n)) B : \tr (A *m B) = \tr (B *m A).
``````

I have next error in result

``````Error: Unknown interpretation for notation "\tr _".
``````

I can see that "\tr" is defined here https://math-comp.github.io/htmldoc_1_12_0/mathcomp.algebra.matrix.html .

``````\$ opam list -i
...
coq                    8.13.2      Formal proof management system
coq-mathcomp-algebra   1.12.0      Mathematical Components Library on Algebra
coq-mathcomp-fingroup  1.12.0      Mathematical Components Library on finite groups
coq-mathcomp-ssreflect 1.12.0      Small Scale Reflection
...
``````

What is wrong and how to fix it?

Just as a small notice, I was not able to have it work without importing algebra.matrix also (so, using the book's code only).

#### Guillaume Melquiond (Jun 04 2021 at 13:06):

Notice how the notation is defined in the `ring_scope` scope. So, you either need to type `(\tr (A *m B))%R` or do `Open Scope ring_scope.`

thank you

#### Andrey Klaus (Jun 04 2021 at 14:31):

I did Open Scope ring_scope and it solved the problem.

#### Andrey Klaus (Jun 04 2021 at 14:39):

But now there is another problem with this code:

``````From mathcomp Require Import all_ssreflect.
From mathcomp Require Import algebra.matrix.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Open Scope ring_scope.

Lemma mxtrace_mulC R m n (A : 'M[R]_(m, n)) B : \tr ( A *m B) = \tr ( A *m B).
``````

The error message is

``````Error:
In environment
R : Type
m : nat
n : nat
A : 'M_(m, n)
B : ?T
The term "A" has type "'M_(m, n)" while it is expected to have type "'M_(?m, ?n0)".
``````

When I provide type for B error message stays the same.
`Lemma mxtrace_mulC R m n (A : 'M[R]_(m, n)) (B : 'M[R]_(n, m)) : \tr ( A *m B) = \tr ( A *m B).`

#### Reynald Affeldt (Jun 04 2021 at 14:53):

this will work if you constrain `R` to be of type say `ringType`

#### Reynald Affeldt (Jun 04 2021 at 14:54):

but for this you’d better load basic algebra theories

#### Reynald Affeldt (Jun 04 2021 at 14:54):

you can add `ssralg` before `algebra.matrix` for example

#### Andrey Klaus (Jun 04 2021 at 14:57):

`From mathcomp Require Import all_algebra.` and also specifying the type helped. Thank you.

#### Andrey Klaus (Jun 04 2021 at 16:09):

well, now the proof

#### Andrey Klaus (Jun 04 2021 at 16:10):

``````From mathcomp Require Import all_ssreflect.
From mathcomp Require Import all_algebra.
From mathcomp Require Import all_fingroup.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma mxtrace_mulC (R : ringType) m n (A : 'M[R]_(m, n)) B : (\tr ( A *m B))%R = (\tr ( A *m B))%R.
Proof.
have -> : (\tr (A *m B))%R = \sum_i \sum_j A i j * B j i.
``````

#### Andrey Klaus (Jun 04 2021 at 16:10):

``````Error:
In environment
R : ringType
m, n : nat
A : 'M_(m, n)
B : 'M_(n, m)
i : ordinal_finType m
j : ordinal_finType n
The term "A i j" has type "GRing.Ring.sort R" while it is expected to have type "nat".
``````

#### Guillaume Melquiond (Jun 04 2021 at 16:11):

Aren't you just missing a `%R` on the right? `(A i j * B j i)%R`

thanks!

#### Andrey Klaus (Jun 07 2021 at 06:06):

The same proof. The last string of proof is
`by do 2!apply: eq_bigr => ? _; apply: mulrC.`. Where to find mulrC? I would think in package `all_algebra`, namely in `ssralg` but all_algebra is imported. And I'm not able to find mulrC after importing algebra.ssralg too.
Code is

``````From mathcomp Require Import all_ssreflect.
(* From mathcomp Require Import algebra.ssralg. *)
From mathcomp Require Import all_algebra.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Search mulrC.
``````

#### Laurent Théry (Jun 07 2021 at 06:13):

To know what is `mulrC` you should do `Check mulrC.` and to know where it is defined `Locate mulrC. `.
Hope this helps

Thank you.

#### Andrey Klaus (Jun 18 2021 at 16:32):

Quite simple thing.

``````From mathcomp Require Import ssreflect ssrnat ssrbool eqtype.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Definition maxn m n := if m < n then n else m.

Lemma max_sym m n: maxn m n = maxn m n.
Proof.
wlog : m n / m < n; last by rewrite /maxn => ->.
by case: (leqP n m).
Qed.

Lemma succ_max_distr n m : (maxn n m).+1 = maxn (n.+1) (m.+1).
Proof.
rewrite max_sym.
``````

``````Error: all matches of The LHS of max_sym
(maxn _ _)
are equal to the RHS
``````

And I'm not able to find a way to have coq rewrite what I want (so, things like rewrite (max_sym n m), rewrite {1} (max_sym n m).. etc) do not work for me. What am I missing?

#### Enrico Tassi (Jun 18 2021 at 21:30):

Your lemma `max_sym` is wrong, it's a no-op, and rewrite "detects" it

#### Andrey Klaus (Jun 19 2021 at 06:58):

really! thank you!

#### Andrey Klaus (Jun 20 2021 at 14:57):

Here we have code for `tnth` https://math-comp.github.io/mcb/snippets/ch7_4.html (line 42).
I would like to put next string on line 44 (so, right after tnth definition): `Eval compute in tnth ([:: 1; 2; 3]) 1.`
After reading the book I had an impression that this should just work (it is possible it is wrong impression).
Question: should `Eval compute in tnth ([:: 1; 2; 3]) 1.` work and if yes - how to make it work?

#### Enrico Tassi (Jun 20 2021 at 15:49):

No, you have to write something like

``````Eval compute in tnth (@Tuple 3 nat [:: 1; 2; 3] isT) (@Ordinal 3 1 isT).
``````

I see why you thought so, but the automatic "enrichment" works if something is already a tuple, and is projected down to a sequence in order to apply a sequence operation. Here `[:: 1;2;3]` is a sequence, plain and simple. One needs to wrap it into a constructor and prove a property a bout the length, that in this case is trivial (`isT` proves "true = true"). Ditto for the ordinal, `1` is a nat, you have to prove first that is is smaller than 3 in order to use it with tnth.

Said that, tuples are useful mostly to reason about abstract sequences with an invariant on the length. Not on concrete ones.

#### Enrico Tassi (Jun 20 2021 at 15:51):

If you feel like the book should be improved to clarify all that, please open an issue on github.

#### Enrico Tassi (Jun 20 2021 at 15:55):

Also, it may be worth putting this example in the jscoq code snippet as well.

#### Andrey Klaus (Jun 20 2021 at 17:22):

Thank you. I see in general that i didnt understand this part.. but in a bit more details, if you have a minute, shouldn't the problem like `Tuple _ _ ~ seq nat` arise when I write `tnth _ [::1;2;3]`?

#### Enrico Tassi (Jun 20 2021 at 18:00):

Yes, precisely the type error comes from `tuple_of _ _ =?= seq nat`. This does not fall in the domain of Canonical Structures (e.g. there is no projection involved, in particular no occurrence of `tval`). It could be covered by Coercions, but at the time of writing the elaborator of Coq is too limited. I mean, the term `[:: 1;2;3]` has type `seq nat` but is expected to have type `tuple_of _ _`: one could apply this "cast" code `@Tuple _ _ <here> isT` every time this problem pops up, and elaborate `[:: 1;2;3]` into `@Tuple _ _ [:: 1;2;3] isT` which has the expected type `tuple_of _ _` (and infer the `_` running type inference again).

#### Enrico Tassi (Jun 20 2021 at 18:22):

Today you can't declare a coercion like that

#### Emilio Jesús Gallego Arias (Jun 20 2021 at 20:40):

I think today you can use some of the notations, that is ```Eval compute in tnth [tuple 1; 2; 3] (sub_ord 1). ```

#### Emilio Jesús Gallego Arias (Jun 20 2021 at 20:40):

that should do the trick and use the right reflection so your statement computes

#### Andrey Klaus (Jun 20 2021 at 21:22):

@Emilio Jesús Gallego Arias , thank you, it looks very nice.
@Enrico Tassi Thank you very much for the explanation. As for book, the 2nd part of book was rather complicated for me. It is possible that I'm not a part of target audience of the 2nd part of the book (my experience in Coq is just the first 3 parts of software foundations). I think the 2nd part of the book was hard for me because there are many technical details and not enough for me examples how to use all of this. Adding this thing will make book a bit more informative, but also a bit more detailed. So, I'm not sure if book does need to mention this or it does not. Example of code I think needs to be added still, but to the first part of book where examples of `[:: 1; 2]` notation are given and in the Emilio's form. I think it is rather easy to get the idea of how it can be used when discuss notations. I will open an issue.

#### Emilio Jesús Gallego Arias (Jun 20 2021 at 21:29):

Indeed, thanks @Andrey Klaus ; note tho that in general computing with tuples and ordinals is not going to work very well, my understanding is that math-comp was just not designed to do that

#### Emilio Jesús Gallego Arias (Jun 20 2021 at 21:29):

You can find more details in the CoqEAL literature, where the notion of "proof-friendly representation" and "computation-friendly representation" is more widely discussed

I see, thank you

#### Andrey Klaus (Jun 22 2021 at 19:25):

@Enrico Tassi I've changed my opinion a bit. Actually, the book already contains most of this information. So, it is not a big amount of information to add. And I think that outlining the difference between coercions and canonical structures will help for better understanding of the both of them. So, I've created an issue.

#### Andrey Klaus (Jul 06 2021 at 07:11):

One more question: suppose I have goal like ` a && b && c -> somegoal`. Could I use `and3P` to convert `a && b && c ` to `a /\ b /\ c`? Now I do something like `move /andP; case => /andP; case`. Is there a better way?

#### Andrey Klaus (Jul 06 2021 at 07:24):

well, now I do `move => /andP [ ] /andP [ ]`. Still question is actual, is it possible to use `and3P` and/or is there a better way?

#### Christian Doczkal (Jul 06 2021 at 07:32):

well, you can do `rewrite -andbA => /and3P[A B C].` the "problem" is that `_ && _` associates to the left, while `[&& _ , _ & _]` is syntax for a conjunction that associates to the right.

#### Andrey Klaus (Jul 06 2021 at 09:29):

Now I see why /and3P did not work. Thanks for advice!

#### Andrey Klaus (Jul 30 2021 at 10:05):

How can I prove `valid (x :-> X \+ y :-> Y)` when I have `valid (x :-> Y \+ y :-> X)`?

#### Alexander Gryzlov (Jul 30 2021 at 11:14):

Andrey Klaus said:

How can I prove `valid (x :-> X \+ y :-> Y)` when I have `valid (x :-> Y \+ y :-> X)`?
If you have something like `Lemma valid_swap {A B} x y (X : A) (Y : B) : valid (x :-> Y \+ y :-> X) -> valid (x :-> X \+ y :-> Y).` then the quickest way to prove this is by fully unrolling all validity conditions: `rewrite !validPtUn !validPt !domPt.`