coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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].
- [Coq-Club] "match (Zpos p?=0%Z) with ..." given "p : positive", Tie Cheng
- Re: [Coq-Club] "match (Zpos p?=0%Z) with ..." given "p : positive",
Adam Chlipala
- Re: [Coq-Club] "match (Zpos p?=0%Z) with ..." given "p : positive",
Tie Cheng
- Re: [Coq-Club] "match (Zpos p?=0%Z) with ..." given "p : positive", Adam Chlipala
- Re: [Coq-Club] "match (Zpos p?=0%Z) with ..." given "p : positive",
Tie Cheng
- Re: [Coq-Club] "match (Zpos p?=0%Z) with ..." given "p : positive", Andreas Abel
- Re: [Coq-Club] "match (Zpos p?=0%Z) with ..." given "p : positive",
Adam Chlipala
Archive powered by MhonArc 2.6.16.