Skip to Content.
Sympa Menu

coq-club - [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities


Chronological Thread 
  • From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities
  • Date: Wed, 13 Apr 2016 15:54:59 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f179.google.com
  • Ironport-phdr: 9a23:ElQFtB02uv6C3eThsmDT+DRfVm0co7zxezQtwd8ZsegQKvad9pjvdHbS+e9qxAeQG96Lu7QZ0KGP6P6ocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC34LqjKvroMObSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6Lpyv/JHBK79ZuEzSaFSRGAtNHlw78n2vzHCSxGO7z0SSDNFvABPBl3s5hH7RZf8sWPTsON71GHONMf2TKs0VDfk5qFiThOuiSYbOBY29WjWjop7i6cN80HpnAB234OBONLdD/F5ZK6IJd4=

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,



Archive powered by MHonArc 2.6.18.

Top of Page