Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] ring_simplify strangeness

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] ring_simplify strangeness


Chronological Thread 
  • From: Jonathan Leivent <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] ring_simplify strangeness
  • Date: Tue, 22 Sep 2015 17:34:32 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qg0-f53.google.com
  • Ironport-phdr: 9a23:w9+5NBR2+xBqq2v8J75J1R43Rdpsv+yvbD5Q0YIujvd0So/mwa64YBWN2/xhgRfzUJnB7Loc0qyN4/ymBTRLuMjY+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8GVP10D3WTkKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayLOwESulTCy1jOGQo7uXqswPCRE2B/CgySGITxzhPBQHZ7Bj8FrP8szX3sPY1jCudO8z1QLQ5VByt6q5qTFnjjyJRZG1xy33elsEl1PETmxmmvREqm4M=



On 09/22/2015 04:57 PM, Michel Levy wrote:
On 22/09/2015 21:33, Jonathan Leivent wrote:
Is the following a bug or a feature of ring_simplify?:

Require Import ZArith.
Open Scope Z_scope.

Variable F : Z -> Z -> Type.
Variable G : Z -> Type.

Goal F (1+1) (2+2).
ring_simplify. (*works: F 2 4 is new goal*)
Abort.

Goal G (1+1).
ring_simplify. (*Error: ring: cannot find relation*)

This occurs in 8.5.

Does ring_simplify really need G to be a relation, and if so, why?

-- Jonathan

You must (re)read the reference manual.
You can write
ring_simplify (1+1) and the goal will be simplified in G 2.
Or if you write ring_simplify without arguments, it is written in 8.17.2
If no term is given, then the conclusion should be an equation and both
hand sides are normalized.


I have read the reference manual enough times to know it doesn't tell the whole truth ;)

I need a tactic that will simplify all ring terms everywhere, not just in equations. The reference manual lead me to believe - as you stated - that ring_simplify without term args only works on equations - so that I would have to write my own tactic (based on ring_simplify) to simplify other occurrences of ring terms.

But, as I was experimenting with this, I noticed that often times, ring_simplify alone did what I wanted - and I didn't need a new tactic. It also would obviously do so much faster than a new tactic would, because a new tactic would have to dig for ring terms using match and context in a loop. So, it seemed that ring_simplify had abilities beyond what the reference manual implied. However, I guess it considers F an equality function on Z, merely because its (last) 2 args are Z.

-- Jonathan




Archive powered by MHonArc 2.6.18.

Top of Page