coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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?:You must (re)read the reference manual.
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 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
- [Coq-Club] ring_simplify strangeness, Jonathan Leivent, 09/22/2015
- Re: [Coq-Club] ring_simplify strangeness, Michel Levy, 09/22/2015
- Re: [Coq-Club] ring_simplify strangeness, Jonathan Leivent, 09/22/2015
- Re: [Coq-Club] ring_simplify strangeness, Michel Levy, 09/22/2015
Archive powered by MHonArc 2.6.18.