coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] contradiction

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] contradiction
Date: Sat, 4 Jun 2016 16:16:04 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-wm0-f41.google.com
Ironport-phdr: 9a23:XfxmExB42rel1pLlfue4UyQJP3N1i/DPJgcQr6AfoPdwSP74pMbcNUDSrc9gkEXOFd2CrakU2qyI7uu5BjBIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/nhqbsptaKPFkArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5JbGwakx8AMQHB7Q/zFsPvoCL+t/R08CKfIIv7Qa1iCmfq1LtiVBK90HRPDDU+6myC0sE=

Hi!

Sometimes I have goals which contain contradiction in a hypotheses. In some simple cases tactics like congruence or omega take care of these, but some times hypotheses needs to be massaged a bit to show the contradiction.

While trying to do 'apply' or 'rewrite' on such hypothesis, sometimes I could not do this because they are references to them in the goal. Usually I solve this by generalizing parts the goal to get rid of such dependencies. This often involves lengthy "generalize" statements.

I was wondering if there is an easy way to generalize as much of the goal as possible so I will be free to manipulate hypotheses to prove a contradiction?

Thanks!

CMU ECE PhD candidate

Mobile: +1(510)220-1060

[Coq-Club] contradiction, Vadim Zaliva, 06/05/2016
- Re: [Coq-Club] contradiction, Cyprien Mangin, 06/05/2016