Ssreflect Users Discussion List

[Erik Martin-Dorel <>]

Dear Benjamin,

I had noticed a similar behavior when doing some experiments with
ssrint and "cring"
(http://tamadi.gforge.inria.fr/CoqHensel/coqhensel-2.1.0-coqdoc/CoqHensel.ssr_tactics.html)

The issue you observe is due to the fact that the ring_theory implicit
argument is automatically inferred to
"(GRing.Zmodule.sort (GRing.Ring.zmodType int_Ring))"
(which is unfortunate in this case, as it should be "int")

You can address this issue just by using the "@" prefix to make this
type parameter choice explicit. See complete excerpt below.

--8<---------------cut here---------------start------------->8---
From mathcomp Require Export all_ssreflect.
From mathcomp Require Export all_algebra.

Open Scope ring_scope.
Open Scope int_scope.

Export intRing.
Export intZmod.

Lemma int_ring : ring_theory 0 1 addz mulz (fun n m => n - m) oppz (@eq _).
Set Printing All.
(* @ring_theory (GRing.Zmodule.sort (GRing.Ring.zmodType int_Ring))
    (GRing.zero (GRing.Ring.zmodType int_Ring)) (GRing.one int_Ring) addz mulz
    (fun n m : GRing.Zmodule.sort (GRing.Ring.zmodType int_Ring) =>
     @GRing.add (GRing.Ring.zmodType int_Ring) n (@GRing.opp 
(GRing.Ring.zmodType int_Ring) m)) oppz
    (@eq (GRing.Zmodule.sort (GRing.Ring.zmodType int_Ring)))
 *)
Abort.
Unset Printing All.

Lemma int_ring : @ring_theory int 0 1 addz mulz (fun n m => n - m) oppz (@eq 
_).
Proof. split.
       exact add0z.
       exact addzC.
       exact addzA.
       exact mul1z.
       exact mulzC.
       exact mulzA.
       exact mulz_addl.
       by [].
       move=> x. rewrite addzC. apply addNz. Qed.

Add Ring int_ring_ssr : int_ring.

Lemma test (n m : int) : addz n m = addz m n.
Proof. ring. Qed.
--8<---------------cut here---------------end--------------->8---

But I let the mathcomp devs comment on whether a similar "Add Ring"
invocation should be directly added to core coq-mathcomp-algebra?

Best regards,
Erik

Le lundi 23 septembre 2019 à 16:01 +0000, Benjamin Salling Hvass a écrit :
> I tried making the ring tactic work for the int type by running the 
> following code
> 
> From mathcomp Require Export all_ssreflect.
> From mathcomp Require Export all_algebra.
> 
> Open Scope ring_scope.
> Open Scope int_scope.
> 
> Export intRing.
> Export intZmod.
> 
> Lemma int_ring : ring_theory 0 1 addz mulz (fun n m => n - m) oppz (@eq _).
> Proof. split.
>        exact add0z.
>        exact addzC.
>        exact addzA.
>        exact mul1z.
>        exact mulzC.
>        exact mulzA.
>        exact mulz_addl.
>        by [].
>        move=> x. rewrite addzC. apply addNz. Qed.
> 
> Add Ring int_ring_ssr : int_ring.
> 
> Lemma test (n m : int) : addz n m = addz m n.
> Proof. ring.
> 
> But it complains that it cannot find a declared ring structure for int?
> According to the documentation for Add Ring this should work. What have I 
> missed?
> 
> Best regards,
> Benjamin

-- 
Érik Martin-Dorel, PhD
Maître de Conférences, Lab. IRIT, Univ. Toulouse 3


https://www.irit.fr/~Erik.Martin-Dorel