search

math-comp / algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components
33 stars 2 forks source link

Support for `nat` ? #40

Closed amahboubi closed 1 year ago

amahboubi commented 2 years ago 
From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp Require Import ring.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma doo (n m : nat) : m + n = n + m.
Fail ring.

Is ring supposed to eventually work for type nat ? For semi-rings in general? Note that ring does not fail if we remove the Require Import ring line.

pi8027 commented 2 years ago

For natural numbers, I would recommend using lia instead for now. However, we will eventually be able to add the semiring structure to the hierarchy (MathComp 2.0 required), and then it makes sense to implement a tactic for semirings.

pi8027 commented 2 years ago

Aha, but ssrnat adapts ring to nat equations. So this is indeed bad.

amahboubi commented 2 years ago

But may be could we consider changing this in ssrnat.