Proving first order logic in coq

Question

I want to prove something like:

Theorem new_theorem : $\forall (A B: \text{Prop}), ((A \wedge B) \iff (B \wedge A))$.

in coq. I know, i could just type firstorder., but could i prove this in coq without this tactic and if so how?

Answer 1

I'll post a sequence of proof scripts, starting from an "uphill both ways, in the snow" version that elaborately proofs every single step.

Version 1:

Require Import Utf8.

Lemma and_commutative: ∀ P Q, P ∧ Q ↔ Q ∧ P.
Proof.
  intros P Q.
  split.
  - intros HPandQ.
    destruct HPandQ as [HP HQ].
    split.
    + exact HQ.
    + exact HP.
  - intros HQandP.
    destruct HQandP as [HQ HP].
    split.
    + exact HP.
    + exact HQ.
Qed.

This splits the proof into two goals, $P \wedge Q \to Q \wedge P$ and $Q \wedge P \to P \wedge Q$. It proves each by splitting the assumtion in its constituent parts, splitting the goal into two subgoals and solving the subgoals with the corresponding assumptions.

Looking at this proof, there's a lot of duplication: we can simplify it with a lemma, like this:

Require Import Utf8.

Lemma and_commutative: ∀ P Q, P ∧ Q ↔ Q ∧ P.
Proof.
  assert (∀ P Q, P ∧ Q → Q ∧ P) as Himplication. {
    intros P Q HPandQ.
    destruct HPandQ as [HP HQ].
    split.
    + exact HQ.
    + exact HP.
  }
  intros P Q.
  split.
  - apply Himplication.
  - apply Himplication.
Qed.

This is basically the same proof as before, only made more succinct by using an assert.

There's yet another improvement to be made: we are laboriously using exact to prove the goals, but they follow trivially from assumptions. Let's simplify again:

Require Import Utf8.

Lemma and_commutative: ∀ P Q, P ∧ Q ↔ Q ∧ P.
Proof.
  assert (∀ P Q, P ∧ Q → Q ∧ P) as Himplication. {
    intros P Q HPandQ.
    destruct HPandQ as [HP HQ].
    split; assumption.
  }
  intros P Q.
  split; apply Himplication.
Qed.

This uses a ; tactical to shorten the proof a bit more, by merging identical tactic sequences into one. A final simplification would be to use introduction patterns and the fact that split will auto-introduce assumptions if neccessary:

Require Import Utf8.

Lemma and_commutative: ∀ P Q, P ∧ Q ↔ Q ∧ P.
Proof.
  assert (∀ P Q, P ∧ Q → Q ∧ P) as Himplication. {
    intros P Q  [HP HQ].
    split; assumption.
  }
  split; apply Himplication.
Qed.

Further improvement would be possible here by using auto instead of the split; ... sequences, but at this point, we're almost at the level of using firstorder anyway...

JFTR: I only Require Import Utf8 so that I can use unicode symbols such as \forall and \leftrightarrow; it has no influence on the proofs themselves.