File: bug_6191.v

package info (click to toggle)
rocq-stdlib 9.0.0-3
  • links: PTS, VCS
  • area: main
  • in suites: experimental
  • size: 11,828 kB
  • sloc: python: 2,928; sh: 444; makefile: 319; javascript: 24; ml: 2
file content (16 lines) | stat: -rw-r--r-- 422 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
 
(* Check a 8.7.1 regression in ring_simplify *)

From Stdlib Require Import ArithRing BinNat.
Goal forall f x, (2+x+f (N.to_nat 2)+3=4).
intros.
ring_simplify (2+x+f (N.to_nat 2)+3).
match goal with |- x + f (N.to_nat 2) + 5 = 4 => idtac end.
Abort.

From Stdlib Require Import ZArithRing BinInt.
Open Scope Z_scope.
Goal forall x, (2+x+3=4).
intros.
ring_simplify (2+x+3).
match goal with |- x+5 = 4 => idtac end.
Abort.