coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] ring_simplify strangeness

From: Michel Levy <michel.levy1948 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] ring_simplify strangeness
Date: Tue, 22 Sep 2015 22:57:48 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michel.levy1948 AT gmail.com; spf=Pass smtp.mailfrom=michel.levy1948 AT gmail.com; spf=None smtp.helo=postmaster AT mail-wi0-f171.google.com
Ironport-phdr: 9a23:uOjSxxTb+Eg6Hx5YetmV2ZGw7dpsv+yvbD5Q0YIujvd0So/mwa64YBaN2/xhgRfzUJnB7Loc0qyN4/ymBTRLuMvc+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8GVP10D3WfgKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayLOwESulTCy1jOGQo7uXqswPCRE2B/CgySGITxz9JCAjI6FneU4ng+n//t+F91S3cOcDoXOllBWSK4KJiSRuugyACYW1quFrLg9B92foI6CmqoAZyltbZ

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.

-- 
email : michel.levy1948 AT gmail.com
http://membres-liglab.imag.fr/michel.levy

[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