The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

A few months ago, I was happy to find in the manual 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/