The Coq mailing list

["Stefan O'Rear" <stefanor AT cox.net>]

On Mon, Oct 01, 2007 at 11:08:17AM +0200, Marko Maliković wrote:
> Greetings,
> 
> I will explain my problem with very simple example. Example is stupid
> because my actual environment is very complex and very long:
> 
> (*Definitions and declarations:*)
> Section A.
> Parameter y : nat.
> Let x:=3 : nat.
> Definition funkcija y := y*y.
> 
> (*Goal:*)
> 
> Goal (y = funkcija x -> 1=1) /\ (y = funkcija x -> 1<>1).

Your goal as written is false.  Let y be 9.  Then funkcija x = 9, and

proj2 Unnamed_thm : 9 = funkcija 3 -> 1 <> 1
proj2 Unnamed_thm refl_equal : 1 <> 1
proj2 Unnamed_thm refl_equal refl_equal : False

Contradiction

I don't think /\ means what you think it does.

Stefan

Attachment: signature.asc
Description: Digital signature