The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

> On 28 déc. 2014, at 17:02, CHAUVIN Barnabe 
> <barnabe.chauvin AT gmail.com>
>  wrote:
> 
> 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 ?
Unfortunately, the proof requires some interaction :(

Require Import ZArith Psatz.
Open Scope Z_scope.

Goal forall
(x : Z) (y : Z)
(H : x * y = 1)
(H1 : x <> 1)
(H2 : x <> -1), False.
Proof.
  intros.
  assert (y >= 0 \/ y <= 0) by lia.
  nia.
Qed.




> 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/
>