Stream: math-comp devs

Topic: Coercion Hook

Pierre Roux (Jul 03 2023 at 16:36):

And here is a version that works for any substructure of (semi)ringType:

From elpi.apps Require Import coercion.
#[warnings="-notation-overridden,-ambiguous-paths"]
From mathcomp Require Import all_ssreflect ssralg.

Elpi Accumulate Coercion lp:{{
coercion _ N {{ nat }} Expected Res :-
  coq.unify-eq {{ GRing.SemiRing.sort lp:R }} Expected ok, !,
  coq.unify-eq {{ GRing.Nmodule.sort lp:V }} Expected ok, !,
  Res = {{ @GRing.natmul lp:V (GRing.one lp:R) lp:N }}.
}}.
Elpi Typecheck Coercion.

Section TestNatMul.

Variable R : fieldType.
Variable n : nat.

Check n : R.  (* elaborated to n%:R *)

End TestNatMul.

Karl Palmskog (Jul 03 2023 at 16:39):

should we move this topic to #Hierarchy Builder devs & users #Elpi users & devs maybe?

Pierre Roux (Jul 03 2023 at 16:39):

To get this fully usable in MathComp, we still need to figure out the printing part. My current idea is to put a printing only notation in ring_scope that hides GRing.natmul and a printing only notation %:R in a new ring_coercions so that Enable/Disable Notation : ring_coercions can show/hide coercions in the middle of a proof. But any other idea is welcome.

Pierre Roux (Jul 03 2023 at 16:40):

Karl Palmskog said:

should we move this topic to #Hierarchy Builder devs & users maybe?

Maybe in math-comp devs? as it is more linked to MC than HB.

Notification Bot (Jul 03 2023 at 16:40):

This topic was moved here from #CUDW 2023 > Coercion Hook by Karl Palmskog.

Pierre Roux (Jul 03 2023 at 16:41):

Thanks @Karl Palmskog !

Last updated: Nov 29 2023 at 22:01 UTC