Kazuhiko Sakaguchi

icon indicating an email [email protected]

icon location Lyon, France icon location Postdoc in the Plume team at CNRS, ENS de Lyon, UCBL, LIP | Interests: interactive theorem proving, formalization of mathematics, and proof by reflection

Results 306 comments of Kazuhiko Sakaguchi

Use predicators even extensively

For the record, there was a discussion about this PR in [the last MC call](https://github.com/math-comp/math-comp/wiki/Minutes-September-23-2020).

Use predicators even extensively

Should I consider cherry-picking non-problematic and useful changes from this PR, to include in 1.13.0?

Failure of automatic lemma invocation

I had the same problem in #270 and it's currently solved by `Hint Extern`.

[rfc] constant to mark terms to be ignored by matching

I have some examples of failure as I mentioned in #280 which indicate this feature is needed. I will produce small examples and their description later.

[rfc] constant to mark terms to be ignored by matching

I'm sorry to procrastinate. Here is an example. ```coq From mathcomp Require Import all_ssreflect all_algebra. Goal forall n m, @GRing.mul int_Ring n m = @GRing.mul int_comRing m n. Proof. move=>...

Make the finType structure equipped with indexing functions

@CohenCyril Thank you for the explanation. @ggonthier > I think that there are better ways of doing this that what you've experimented with, I have fixed an incompatibility issue of...

Missing subset lemmas

Note that the first lemma is not `seq` specific.

[Recurring issue] Checking that all new lemmas, Exports modules, and Canonical Structures are exported in ssralg.v

For the record, here is the list of constants defined/proved in `GRing` but not exported (as constants) in `GRing.Theory` (generated by `sed`, `sort`, `diff` from the output of `Print GRing.`...

[Recurring issue] Checking that all new lemmas, Exports modules, and Canonical Structures are exported in ssralg.v

Oh, the meaning of the `Local Canonical` command (in modules) might be changed from "the unqualified name of this constant is local" to "the unification hint synthesized from this declaration...

[Recurring issue] Checking that all new lemmas, Exports modules, and Canonical Structures are exported in ssralg.v

I suggest putting a milestone here not to forget to check `ssralg` before every release. After checking, it should be postponed to the next milestone.