Library example_mybaby

Back to Coq Main Page

MyBaby: Jazz Song Analyzed

Human-oriented proof

Let us consider a song written in 1924 that later became one of the standard songs, sung by multiple jazz artists at different times. Everybody Loves My Baby (But My Baby Don't Love Nobody But Me); music by Spencer Williams, lyric by Jack Palmer
The example was taken from this logic textbook: Logic as a Tool by Valentin Goranko, 2016.
The lyrics of this song mentions humans MyBaby and Me satisfying hypotheses:
ItemA
Every human loves MyBaby
ItemB
On the other hand MyBaby does not love anyone except Me
If L(x,y) is the predicate to denote that x loves y, then for every human x: L(x,MyBaby). In the meantime: for every human x, as long as x≠Me, then ~L(MyBaby,x) (namely, MyBaby does not love x).
Let us prove that in this case MyBaby and Me is the same person. Let's start with a human-readable proof:
  • Define the set of all humans: HUM.
  • Denote elements MyBaby and Me in this set.
  • Assume that MyBaby≠Me.
  • Substitute in the property (ItemB): x = MyBaby
  • Because of the assumption MyBaby≠Me, MyBaby does not love MyBaby, since MyBaby only loves Me
  • On the other hand, by assumption (ItemA): everybody must love MyBaby.
  • By (ItemA) MyBaby also loves MyBaby.
  • This is a contradiction, since L(MyBaby,MyBaby) should be either true or false.
Contradiction was obtained, since we assumed MyBaby≠Me. Therefore, we should always have MyBaby=Me.

Machine-verified proof

We will need the contrapositive tautology

Axiom ContraPos : forall p q: Prop, (p -> q) <-> (~q -> ~p).

We assume two hypotheses (ItemA, ItemB) and prove Lemma that MyBaby and Me are equal.

Section mybaby.

Here the same proof is formalized with Coq. HUM is the set of all humans.
Parameter HUM : Type.
Me and MyBaby are humans.
Parameter Me : HUM.
Parameter MyBaby : HUM.

The predicate L(x,y) is true if and only if x loves y.
Parameter L : HUM*HUM -> Prop.

Hypothesis ItemA: forall x: HUM, L(x,MyBaby).
Hypothesis ItemB: forall x: HUM, ~(x=Me) -> ~(L(MyBaby,x)).

Lemma who_is_mybaby: MyBaby=Me.
Proof.
  assert (MyBaby <> Me -> ~L(MyBaby,MyBaby)).
  apply ItemB with (x := MyBaby).
  assert (L(MyBaby,MyBaby)).
  apply ItemA with (x := MyBaby).
  clear ItemA ItemB.
  elim (ContraPos (L(MyBaby,MyBaby)) (MyBaby = Me)).
  intros.
  clear H1.
  pose (H2 H) as H3.
  pose (H3 H0) as H4.
  exact H4.
Qed.

End mybaby.