The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

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].