The Coq mailing list

[Assia Mahboubi <Assia.Mahboubi AT inria.fr>]

Dear Abhishek,

  sorry for this late answer.


The ring tactic decides an equality by comparing the normal forms of two
polynomials, inferred respectively from the right and left hand side of the
equality. By default, polynomials are in Z[X1,...,Xn] (for n sufficiently
large), i.e. the coefficients are in Z, as this is correct in any ring.

But as explained in the corresponding paper [1], another choice for the
coefficients can possibly be smarter, like in the case of rings with a 
positive
characteristic (like boolean rings). You can hence tell the tactic to use 
rather
polynomials in Z/2Z[X1,...,Xn] in its normalization procedure, provided that
you're able to prove that this is correct. And this will allow the tactic to
prove more identities, like 1 + 1 = 0.

The ring tactic hence has a syntax for that purpose: I attach a file where I
modify your example slightly, in order to use bool as (the data structure for
Z/2Z which models) the type of coefficients.

This will save you from adding equations of the form x + x = 0:
ring_test_1 shows that they are provable and ring_test_2 provides an example 
of
identity relying on this fact.

Now this does not address the problem of normalizing expressions with powers,
and I do not currently have a better suggestion for using a hypothesis like x 
*
x = x. Indeed, the ring tactic is unfortunately not able to deal with symbolic
ring expressions involved in the powers.

Yet if you only need closed instances of powers, you could implement the power
function as:
Definition rpower (r : R) (n : N) := match n with N0 => 1 | _ => r end.

and simplify your goal before calling the decision procedure.

Hope this helps,

assia

[1] Proving Equalities in a Commutative Ring Done Right in Coq,
    B. Grégoire and A.M., Proceedings of TPHOLs 2005.
http://link.springer.com/chapter/10.1007%2F11541868_7

Le 13/04/2016 21:54, Abhishek Anand a écrit :
> A few months ago, I was happy to find in the manual
> <https://coq.inria.fr/refman/Reference-Manual028.html> that the ring tactic 
> can
> be supplied with
> additional ring equalities using the ring [...] syntax.
> However, it seems that the ring tactic is NOT complete w.r.t the supplied
> equalities. This is illustrated in the example below, which was checked 
> with Coq
> 8.5.
> Is there some other tactic (for unquantified ring equations) that is 
> complete
> w.r.t the supplied (unquantified) ring equalities and the ring laws? It 
> need not
> be complete w.r.t. definitional equalities.
> 
> Also, is there a similar tactic for boolean rings (where forall x, x*x=x),
> instead of regular rings?
> 
> Require Import Ring.
> Section RingTest.
> Generalizable Variables R rO rI radd rmul rsub ropp.
> Context `{Rt: @ring_theory R rO rI radd rmul rsub ropp eq}.
> 
> Add Ring Rr : Rt.
> 
> Notation "0" := rO.
> Notation "1" := rI.
> Infix "+" := radd.
> Infix "*" := rmul.
> Notation "2" := (1+1).
> Lemma ring_test1 : forall (y:R),  2*y = y -> y + y= 0.
> Proof.
>   intros.
>   try  (ring [H]). (* fails *)
>   symmetry in H.
>   try  (ring [H]). (* still fails *)
>   
>   apply (f_equal (radd (ropp y))) in H.
>   ring_simplify in H.
>   try  (ring [H]). (* still fails *)
>   symmetry in H.
>   ring [H]. (* succeeds *)
> Qed.
> 
> Thanks,
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/

Attachment: ring_bool.v
Description: application/save-to-disk