Ssreflect Users Discussion List

[Bas Spitters <>]

I think we'd like to use the ring tactic whenever we have a canonical
Ring structure.
However, Add Ring does not seem to allow for ring structures to be 
parametrized.
Am I missing something?

On Mon, Sep 23, 2019 at 10:57 PM Erik Martin-Dorel
<>
 wrote:
>
> 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