The Coq mailing list

[Tie Cheng <chengtie AT gmail.com>]

Indeed, [simpl Zcompare] evaluates what i need, thanks Adam.

Tie

On Thu, Feb 17, 2011 at 7:39 PM, Adam Chlipala <adam AT chlipala.net> wrote:

Tie Cheng wrote:

Actually, the structure of goal looks like:

(Zpos p * a_formula))%Z =
a_function
  match (Zpos p ?=0)%Z with
     | Eq => ...
     | Lt => ...
     | Gt ==> a_value
  end

After "Simpl.", it changes to:

match (a_formula)%Z with
  | 0%Z => 0%Z
  | Zpos y' => Zpos (p * y')
  | Zneg y' => Zneg (p * y')
end =
(a_function a_value)%Z

But i do not know if a_formula is Zpos or Zneg or 0, i would expect a tactic such that it changes the goal to

(Zpos p * a_formula))%Z =
(a_function a_value)%Z

The operator [?=] is notation for [Zcompare], so, if you only want that part of the term to simplify, run [simpl Zcompare].