The Coq mailing list

[CHAUVIN Barnabe <barnabe.chauvin AT gmail.com>]

Thank you for your answer ! This is much clearer :)

I have another question, not really related to the [cut] tactic :
I have the following hypothesis :
       x : Z
    y : Z
    H : x * y = 1
    H1 : x <> 1
    H2 : x <> -1
How can I prove the contradiction here ?

On 25/12/2014 00:44, Abhishek Anand wrote:

I'm trying to simplify an hypothesis which contains something like this [a + - a = _] over Z (Let's call this hypothesis H).
So I thought it would be good to use the Zegal_left to do it, but Zegal_left do it the other way .. (i.e. It prove that [forall n m : Z, n = m -> n + - m = 0])

The rewrite tactic can be used to rewrite in hypothesis. Here is an example:

Require Import ZArith.

Open Scope Z_scope.

Lemma xyz : forall a:Z, a + - a = 2 -> False.

intros a H.

rewrite Zegal_left in H.

 

If H was a (sub)goal, I could have used the [cut] tactic, and it would have generated the [a=a] subgoal.
But because it's an hypothesis, I cannot use this tactic ..
I guess there is an easy workaround to do such a simplification in hypothesis ?

By the way, is-it possible, to directly rewrite this hypothesis ? Now, assume the hypothesis is of the form [0 = x0 * (x1 * a) + - a] (still over Z).
How can simplify it like [0=a * (x0 * x1 - 1)] ?  (And how can I simplify it if it was a goal ?)

Use the ring properties of arithmetic on Z, e.g. associativity, commutativity, distributivity etc.

http://en.wikipedia.org/wiki/Ring_%28mathematics%29

You can either manually invoke the ring lemmas, or assert the equality you want and prove it by the ring tactic.

I'll show the second option here:

Require Import ZArith.

Open Scope Z_scope.

Lemma xyzz : forall (x0 x1 a: Z),

x0 * (x1 * a) + - a = a * (x0 * x1 - 1).

intros.

ring.

Qed.

I take this email to ask one little question that has no relation to the original subject.
What is the best to do a case disjunction on the value of a term during a proof ?
For example, if there is the term z:Z in the current goal, how do I create two subgoals with the hypothesis z=0 and z<>0 ?
Someone answered me on IRC to use the {}+{} types (sorry, I don't remember his name ..). It works very well, but I still have to prove the disjunction. So here is the extra question, how do I prove this :

   Lemma Z_0_or_not : forall z:Z, {z=0} + {z<>0}.

Thanks in advance !

The lemma you are looking for is Z_zerop. Here's how I found it:

SearchPattern ( {?z=0} + {?z<>0}).

On bad days, I might have to issue more queries like

SearchPattern ( {?z<>0} + {?z = 0}).

SearchPattern ( {?z<>0} + {0 = ?z}).

.... i.e their might be a lemma with a logically equivalent, but syntactically different form.

My question to Coq gurus : Is there a smarter version of SearchPattern?

 Regards,

-- Abhishek

http://www.cs.cornell.edu/~aa755/