Search code examples
coq

How to prove an absurd rule in Coq

I have to prove the following statement, however I am getting the error The type of H is not inductive. when trying to use inversion statement:

enter image description here

How can I do that correctly?

Variables phi: Prop.
Section absurd_rule.
Hypothesis H1: phi -> true = false.
Lemma absurd_rule: ~phi.
Proof.
intro H.
inversion H.
End absurd_rule.
Solution

  • inversion is not the right rule to be used here, as there is nothing to invert on H : phi.

    Let's take a pause after you intro H:

    H1 : phi -> true = false
H : phi
______________________________________(1/1)
False

    First of all, note that H1 H : true = false (simple application). Let's take advantage of it by writing apply H1 in H:

    H : true = false
______________________________________(1/1)
False

    Almost there! Now, it is necessarily contradictory that true = false, and that's because of conflicting constructors. There is a dedicated rule to deal with such cases, namingly discriminate H.

    No more subgoals, we are there. The full proof session looks like this:

    Variables phi: Prop.
Section absurd_rule.

Hypothesis H1 : phi -> true = false.

Lemma absurd_rule : ~phi.
Proof.
intro H.
apply H1 in H.
discriminate H.
Qed.

    Also, worth noting that you can use False to describe bottom (lowercase false is a different thing -- an inductive boolean, instead of an empty Prop).

    A simpler version of your proof would be just

    Variables phi: Prop.
Section absurd_rule.

Hypothesis H1 : phi -> False.

Lemma absurd_rule : ~phi.
Proof.
assumption.
Qed.

    ...which is not a big discovery, because you just assumed phi to be false.

    After a second of reflection...

    You can't "prove a rule". Rules are semantics of the language, laws you use to derive conclusions from assumptions. They are not "theorems" to be proven, but a sort of prior reasoning you use to manipulate sentences. They are even distinct from axioms, it's something on the meta level. You can prove an implication, but not a deduction rule.

    Thus, the "solution" to your problem is just an identity. Your absurd_rule is just a lemma that not phi implies not phi, which is trivially true -- remember that in intuitionistic logic negation is very often defined as to imply false.