The Coq mailing list

[Tie Cheng <chengtie AT gmail.com>]

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

Is it possible?

Thanks and regards

Tie

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

Tie Cheng wrote:

I have "p : positive" in hypothsis and "match (Zpos p?=0%Z) with | Eq => ... | Gt => ... | Lt => ..." as part of the goal. Is there a tactic to remove the "match" from the goal?

I would expect [simpl] to do the job.