1

I did this code :

section
  variable p : Prop

example : ¬ (p ∧ ¬ p) :=
    assume h : p ∧ ¬ p,
      show false, from  (and.left h) (and.right h) 
end

But I have the following message error :

function expected at
  h.left
term has type
  p

But, in the other hand,

section
  variable A : Prop
  variable h1 : ¬ A
  variable h2 : A

example : false := h1 h2
end

works fine...

How can I eliminate the "not" operator ?

Netchaiev
  • 4,811

1 Answers1

3

In Lean, ¬ p is just shorthand for p -> false.

Therefore, if we have h1 : ¬ p and h2 : p, then h1 is a function h1 : p -> false. Therefore, h1 h2 : false. This is why the example works.

In your example, we have (and.left h) : p while (and.right h) : ¬ p. The expression (and.left h) (and.right h) means "Apply the function (and.left h to the value (and.right h)". But there's no reason based on the types to think that (and.left h) is a function.

The correct way to prove it is, of course, to exhibit an element of type false through the expression (and.right h) (and.left h). This is because and.right h : p -> false and and.left h : p.

Mark Saving
  • 31,855