Andrey Klaus (May 18 2021 at 08:05): 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
Andrey Klaus (May 18 2021 at 08:19):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...
Andrey Klaus (May 18 2021 at 10:41):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.
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].
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.
Andrey Klaus (Jun 04 2021 at 14:30):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.
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
Andrey Klaus (Jun 04 2021 at 16:12):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.
To know what is mulrC you should do Check mulrC. and to know where it is defined Locate mulrC. .
Hope this helps
Andrey Klaus (Jun 07 2021 at 06:21):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.
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?
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
Andrey Klaus (Jun 20 2021 at 21:41):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):Question about HTT library.
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:
Question about HTT library.
How can I provevalid (x :-> X \+ y :-> Y)when I havevalid (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.
Andrey Klaus (Jul 30 2021 at 12:00):I haven't figure out in which library was it by myself. Your advice worked perfectly. Thank you very much, @Alexander Gryzlov.
Last updated: Oct 13 2024 at 01:02 UTC