Minutes September 7 2022 - math-comp/math-comp GitHub Wiki

Participants: Assia, Cyril, Enrico, Pierre, Reynald, Yves

About the port to HB #733

non_forgetful_inheritance in ssralg.v (Additive instance out of Scale)

Pierre:

  • morphisms have been ported (ring morphisms, etc.)
  • Problem:
    • Scale is *:
    • for a given r, x |-> r *: x is always additive
    • this gives a non forgetful inheritance warning
    • is it ok to desactivate the warning locally?

Cyril:

  • overapproximation of non-forgetful inheritance?
  • HB does not distinguish proof irrelevance
  • but there is no danger when we deal with propositions
  • however, since HB cannot autocomplete all transitions in the graph, this might lead to missing instances

port of the closedness predicates hierarchy in ssralg

Pierre:

  • drop the keying predicate stuff, main advantage: easier to use (e.g.

    - Variables (S : {pred M}) (oppS : opprPred S) (kS : keyed_pred oppS).
+ Variable S : opprClosed M.

    ), declarations not much easier (e.g.,

    - Definition monic := [qualify p | lead_coef p == 1].
- Fact monic_key : pred_key monic. Proof. by []. Qed.
- Canonical monic_keyed := KeyedQualifier monic_key.
+ Definition monic_pred := fun p => lead_coef p == 1.
+ Arguments monic_pred _ /.
+ Definition monic := [qualify p | monic_pred p].

    ) and have to be careful when instantiating (e.g. HB.instance Definition _ := GRing.isMulClosed.Build _ monic_pred monic_mulr_closed.)

    drawback: qualifE now rewrites p \is monic to monic_pred p so qualifE/= must be used to unfold monic_pred
    drawback: lost the DefaultPred module with default instantiations (allowed to use lemmas about *Pred without instances, opening proof obligations) but was only used in 2 proofs in whole MC + dependencies in CI
    Overall mostly looks like a reasonable trade-off?

Pierre:

  • simplification of an existing mechanism (one argument instead of three)

Yves:

  • there is no tutorial about the key mechanism (there is only doc in ssrbool.v, now part of Coq)

Cyril:

  • the key mechanism is justified by the behavior w.r.t. simpl

  • for predicates, the roadmap was to extend HB afterwards to handle predicates

  • we'd like to avoid seeing __canonical__ stuffs / having to include /= in middle of rewriting chains

  • a more limited version of simpl is desirable (implies to change Coq or rewrite, automatic simplification after rewrite)

  • we can keep the change, no need to wait for a future version of HB

  • the /= after qualifE are not really worrying, it would be after rpred (Pierre: seems Ok, no such occurence encountered in the CI)

Assia:

  • handle the problem with a vernacular command a la simpl never? Cyril:
  • yes, we'd like "transparent" definitions that behave like notations

Cyril:

  • we may need to test wrt to the libraries graph-theory (Pierre: Ok, it's already in CI) and Coq-combi
    • need to port Coq-combi to the last version of MathComp
    • propose to Florent to move to coq-community?

about right-to-left rewrite and linearZ

Pierre:

  • while porting morphism hierarchy in ssralg: complicated mechanism I don' fully understand about linearZ allowing to not unfold canonical instances when rewriting left to right (allowing use of rewrite linearZ instead of rewrite linearZ /= or even rarely rewrite !linearZ instead of rewrite !linearZ /= !linearZ /=), why not similar mechanism on other morphism related lemmas (rmorphD, rmorphM,...), is it worth porting, does anyone understand the technical details?

Cyril:

others

Pierre: A number of FIXMEs are remaining, we should check them

Cyril:

  • about the replacement of pred
  • pred used to create instance of structure by subtyping?
    • yes in multinomial, no particular problem, that was a syntactic change, tests says it's ok

main remaining point : documentation

postpone, to be done during September