Search code examples
coqtheorem-proving

Transform `not A` into `A -> False` in Coq

I want to prove not A by assuming A and finding False. What is the shortest and most generic way to transform goal not A into A -> False?

I tried exfalso, but it does not add A to my assumptions...

Solution

  • The fastest way is to do intro x, it will give you x : A. not A is actually defined as A -> False, so it is already what you want:

    not = fun A : Prop => A -> False
     : Prop -> Prop

    If you really want to change your goal to A -> False, unfold not will do just fine.

    Finally exfalso is tactic to replace the current goal with False. The aim is to state that the current context is inconsistent.