Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] "match (Zpos p?=0%Z) with ..." given "p : positive"

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "match (Zpos p?=0%Z) with ..." given "p : positive"


chronological Thread 
  • From: Adam Chlipala <adam AT chlipala.net>
  • To: Tie Cheng <chengtie AT gmail.com>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] "match (Zpos p?=0%Z) with ..." given "p : positive"
  • Date: Thu, 17 Feb 2011 13:39:12 -0500

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



Archive powered by MhonArc 2.6.16.

Top of Page