CODEWITHSUNDEEP
coqproof
user3343768
user3343768

Reputation: 71

How to prove forall x, (R x \/ ~ R x) [in the Coq proof assistant]?

How does one prove forall x, (R x \/ ~R x) in Coq. I'm a noob at this and don't know much of this tool. This is what I wrote:

Variables D: Set.
Variables R: D -> Prop.
Variables x:D.

Lemma tes : forall x, (R x \/ ~R x).

I tried this and it worked, but only in auto mode. And if I print the proof I cannot understand the meaning of what's printed (so I can go back and try to do it not in auto mode):

Require Import Classical.

Variables D: Set.
Variables R: D -> Prop.
Variables x:D.

Lemma tes : forall x, (R x \/ ~R x).
Proof.
intro.
tauto.
Qed.

Print tes.

tes = 
fun x0 : D =>
NNPP (R x0 \/ ~ R x0)
  (fun H : ~ (R x0 \/ ~ R x0) =>
   (fun H0 : R x0 -> False =>
    (fun H1 : ~ R x0 -> False =>
     (fun H2 : False => False_ind False H2) (H1 H0))
      (fun H1 : ~ R x0 => H (or_intror H1)))
     (fun H0 : R x0 => H (or_introl H0)))
     : forall x : D, R x \/ ~ R x

Upvotes: 1

Views: 200

Answers (1)

user1861759
user1861759

Reputation:

One way to prove it would be

Print classic.
Print R.
Print x.
Check R x.
Check classic (R x).
Check fun y => classic (R y).

Definition tes2 : forall x, (R x \/ ~ R x) := fun y => classic (R y).

Or using tactics

Lemma tes3 : forall x, (R x \/ ~ R x). Proof. intro. apply classic. Qed.

Print tes3.

The proof tauto found was

Lemma tes : forall x, (R x \/ ~R x).
Proof.
intro.
eapply NNPP.
intro.
assert (R x0 -> False).
intro.
eapply H.
eapply or_introl.
exact H0.
assert (~ R x0 -> False).
intro.
eapply H.
eapply or_intror.
exact H1.
assert False.
eapply H1.
exact H0.
eapply False_ind.
exact H2.
Qed.

The intro tactic builds lambda abstractions, and performs implication introduction and universal quantification introduction, the apply tactic combines previously proven theorems, and performs modus ponens where the first antecedent has already been proven, the exact tactic gives the exact proof term, and the assert tactic also performs modus ponens where none of the antecedents of the rule are given. To see how tactics manipulate the proof term use the Show Proof command before and after applying a tactic.

Upvotes: 0

Related Questions