The Coq mailing list

[Saint Wesonga <saintwesonga AT gmail.com>]

I now realize that inversion is not a valid approach for trying to dispatch this case. I had the goal "v=v0" and the contradictory proposition "v = v0 -> False" since I had done case splitting on "V_eq_dec v v0" (hence my claim that it was a contradiction). (v=v0) -> False was just a hypothesis, not the goal I was trying to solve.

On Mon, Apr 23, 2012 at 12:33 PM, Jonas Oberhauser <s9joober AT googlemail.com> wrote:

Hello Saint!
Let me see if I understood your question.
You are in a situation where you have to show "a = b",  but your
assumption is that "a <> b" - the opposite!
Withouth any further information about a and b, this seems impossible.
Just because you have to show something which contradicts your
assumptions, that doesn't mean your in a contradictory case, it only
means a) your assumptions are too weak or b) you're trying to show
something /which does not hold/.

You said you somehow tried to do inversion on "a <> b"? Inversion is
some sort of a "clever case analysis". You can perform case analysis
on inductive types and proofs (Inductive ... := ...), like v or v0, or
even "p : eq v v0", but you can not destruct a "Product" (= function
type). In fact, you can basicaly destruct most* of the things A of the
form:
A : T
T : Type
or
A : T
T : Prop
you can destruct on A if T is an inductive type, like False, True,
nat, ...; But if T is a Product (False -> True, v=v0 -> False) you
can't.
Even if you could, what would the case analysis look like? What are
the different cases of what a proof that (v=v0)->False can look like?

Kind regards,
Jonas

2012/4/23 Bernard Hurley <bernard AT marcade.biz>:

> Sorry I was getting confused!
>
> Bernard.
>
> On Mon, Apr 23, 2012 at 07:15:23AM -0700, Chad E Brown wrote:
>> (~p -> p) implies ~~p constructively, and p classically.
>>
>> It does not imply ~p and it does not imply False.
>>
>> Variable p : Prop.
>> Goal ((~p -> p) -> ~~p).
>>
>> exact (fun f g => g (f g)).
>> Qed.
>>
>> Hope this helps,
>>
>> Chad
>>
>>
>> ________________________________
>>  From: Bernard Hurley <bernard AT marcade.biz>
>> To: Adam Chlipala <adamc AT csail.mit.edu>
>> Cc: coq-club AT inria.fr
>> Sent: Monday, April 23, 2012 3:56 PM
>> Subject: Re: [Coq-Club] Inversion of a Prop Hypothesis
>>
>> On Mon, Apr 23, 2012 at 09:23:53AM -0400, Adam Chlipala wrote:
>> > On 04/23/2012 09:20 AM, Bernard Hurley wrote:
>> >> I think Saint is trying to obtain a contradiction from the fact that
>> >> he can prove v = v0 from v = v0 -> False.
>> >
>> > There fairly clearly is no contradiction inherent in such a deduction.
>> > For instance, let [v = 0] and [v0 = 0].  The goal would be proved by
>> > reflexivity.
>>
>> The point I was making is that in Classical logic if you can derive P from ¬P from this you can derive ¬P giving a contradiction. It is easy to imagine this can be done in a case like this,
>>
>> However in Intitionistic logic "I can derive P from ¬P" informally means something like:
>>
>> "I have a construction that would turn a proof that 'a proof of P is impossible' into a proof of P."
>>
>> Clearly this does not allow you to find a proof that "a proof of P is impossible" which is what you need to prove ¬P, so no contradiction can be derived without some further assumptions (e.g. that P is decidable.)
>>
>> Bernard.