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])`

.

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.

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

defined in ssrbool

I see, thank you

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

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.

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.

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

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.

`n`

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

OK, it's both ;-)

Here a line which works

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

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

Thank you, Enrico. It works.

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).
```

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].
```

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.

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.

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

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

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

.

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

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).

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

I did Open Scope ring_scope and it solved the problem.

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).`

this will work if you constrain `R`

to be of type say `ringType`

but for this you’d better load basic algebra theories

you can add `ssralg`

before `algebra.matrix`

for example

`From mathcomp Require Import all_algebra.`

and also specifying the type helped. Thank you.

well, now the proof

```
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.
```

```
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".
```

Aren't you just missing a `%R`

on the right? `(A i j * B j i)%R`

thanks!

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.
```

To know what is `mulrC`

you should do `Check mulrC.`

and to know where it is defined `Locate mulrC. `

.

Hope this helps

Thank you.

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.
```

Coq's answer is

```
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?

Your lemma `max_sym`

is wrong, it's a no-op, and rewrite "detects" it

really! thank you!

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?

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.

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

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

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]`

?

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).

Today you can't declare a coercion like that

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

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

@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.

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

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

@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.

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?

well, now I do `move => /andP [ ] /andP [ ]`

. Still question is actual, is it possible to use `and3P`

and/or is there a better way?

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.

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

Question about HTT library.

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

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

?

Andrey Klaus said:

Question about HTT library.

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

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

?

Thanks for the interest in the library! :) Technically, this is a question about the underlying FCSL-PCM library, because that's where validity and heaps are defined.

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.`

I haven't figure out in which library was it by myself. Your advice worked perfectly. Thank you very much, @Alexander Gryzlov.

Last updated: Feb 01 2023 at 11:04 UTC