Преобразуйте `not A` в` A -> False` в Coq

Question

Я хочу доказать not A, приняв A и найдя False.Какой самый короткий и самый общий способ преобразования цели not A в A -> False?

Я пытался exfalso, но это не добавляет A к моим предположениям ...

Answer 1

Самый быстрый способ сделать intro x, это даст вам x : A.not A на самом деле определяется как A -> False, так что это уже то, что вы хотите:

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

Если вы действительно хотите изменить свою цель на A -> False, unfold not подойдет просто отлично.

Наконец exfalso - это тактика замены текущей цели на False.Цель состоит в том, чтобы заявить, что текущий контекст противоречив.