Minutes September 7 2022

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:

• mechanism that also allows to rewrite from right to left https://github.com/math-comp/math-comp/blob/ea0fb35771d762fee04622a4bf0cafe041022cc2/mathcomp/algebra/ssralg.v#L2350-L2386
• not a priority because we could handle it in different ways but should be ported

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