Minutes July 12 2023 - math-comp/math-comp GitHub Wiki

Participants: Pierre, Reynald, Enrico, Yves

replacing coqdoc with coq2html?

Inductive nat := O | S : nat -> nat.
Check O.
Check nat_ind.

DIGEST 0bf36c9b42718c756ee7627948c3aece
Ftest
ind 10:12 <> nat
constr 17:17 <> O
constr 21:21 <> S
R28:31 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R25:27 test <> nat:1 ind
R32:34 test <> nat:1 ind
scheme 10:12 <> nat_rect
scheme 10:12 <> nat_ind
scheme 10:12 <> nat_rec
scheme 10:12 <> nat_sind
R43:43 test <> O constr
R52:58 test <> nat_ind scheme

coercions/notations for %:R, %:~R, %:E... (short demo)

branch: https://github.com/proux01/math-comp/tree/ring_coercions

From mathcomp Require Import all_ssreflect ssralg.

Import GRing.Theory.

Local Open Scope ring_scope.

Section DemoCoercions.

Variable R : ringType.

Variables (x : R) (n : nat).

Lemma test : x + n + 1 = x + n.+1.
Proof.
rewrite -addn1.
(* now we need some printing of coercions *)
Enable Notation : ring_coercions.
rewrite natrD.
Disable Notation : ring_coercions.
by rewrite addrA.
Qed.

(* still need improvement *)
Fail Check x + (n + 1).
(* The term "n + 1" has type "GRing.Nmodule.sort Datatypes_nat__canonical__GRing_Nmodule" while it is expected to have type *)
(*  "GRing.Nmodule.sort R". *)

(* Unfortunately, sometimes %:R remains required *)
Fail Check n + x.
(* The term "x" has type "GRing.Ring.sort R" while it is expected to have type "GRing.Nmodule.sort Datatypes_nat__canonical__GRing_Nmodule". *)
Check n%:R + x.

End DemoCoercions.
  • NB: use n :> R rather than n : R (no cast left in the term)
  • TODO Pierre: try to isaolate nat semiring instances in a module so that n + x would be n%:R + x by default

performance of MC2, last benchmarks:

  • MathComp
    coq: aaaf8994b0 (V8.19+alpha + improved printing of reverse coercion)
    coq-elpi: coq-master-merge 8be42fa (coq-master + merge master + print timing)
    hierarchy-builder: coq-master+batch-accumulation 6d81cdf (coq-master + cherry-pick "speedup: do not use grafting" & "Accumulate clauses in batch")
    mathcomp: master 1e6f7e5f
    total: 27:28 (1,9 GB)
    assemble: 00:01
    extend: 04:51
    optimization: 00:24
    runtime: 11:23
  • Analysis (same Coq, coq-elpi, HB, mathcomp)
    analysis: hierarchy-builder 06ca9d80
    total analysis: 40:25 (2,7 GB)
    assemble: 00:00
    extend: 15:38
    optimization: 00:28
    runtime: 09:12

Discussion: