Software Foundations: Logic in Coq

Logic.v

Require Import Bool.
Require Import List.
Require Import Nat.
Require Import Setoid.

Example and_exercise : forall (n m : nat),
  n + m = 0 -> n = 0 /\ m = 0.
Proof.
  intros [] [] eq.
  - split. reflexivity. reflexivity.
  - discriminate.
  - discriminate.
  - discriminate.
Qed.

Theorem and_assoc : forall A B C : Prop,
  (A /\ B) /\ C <-> A /\ (B /\ C).
Proof.
  split.
  - intros [[HA HB] HC].
    exact (conj HA (conj HB HC)).
  - intros [HA [HB HC]].
    exact (conj (conj HA HB) HC).
Qed.

Theorem ex_falso_quodlibet : forall (P : Prop),
  False -> P.
Proof.
  intros.
  destruct H.
Qed.

Theorem not_implies_ex_falso_quodlibet : forall (P : Prop),
  ~P -> (forall (Q: Prop), P -> Q).
Proof.
  intros.
  destruct (H H0).
Qed.

Theorem not_false : ~False.
Proof.
  unfold not.
  trivial.
Qed.

Theorem contradiction_implies_anything : forall (P Q : Prop),
  (P /\ ~P) -> Q.
Proof.
  intros.
  destruct H.
  destruct (H0 H).
Qed.

Theorem double_neg : forall (P : Prop),
  P -> ~~P.
Proof.
  unfold not.
  intros.
  destruct (H0 H).
Qed.

Theorem contrapositive : forall (P Q : Prop),
  (P -> Q) -> (~Q -> ~P).
Proof.
  unfold not.
  intros.
  destruct (H0 (H H1)).
Qed.

Theorem not_both_true_and_false : forall (P : Prop),
  ~(P /\ ~P).
Proof.
  unfold not.
  intros P [H negH].
  destruct (negH H).
Qed.

Theorem not_true_is_false : forall (b : bool),
  b <> true -> b = false.
Proof.
  intros [] H.
  - destruct H. reflexivity.
  - reflexivity.
Qed.

Theorem not_true_is_false' : forall (b: bool),
  b <> true -> b = false.
Proof.
  intros [] H.
  - unfold not in H.
    exfalso.
    apply H.
    reflexivity.
  - reflexivity.
Qed.

Lemma not_true_iff_false : forall (b : bool),
  b <> true <-> b = false.
Proof.
  split.
  - apply not_true_is_false.
  - intros H. rewrite H. intros H'. discriminate H'.
Qed.

Theorem or_distributes_over_and : forall (P Q R : Prop),
  P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R).
Proof.
  split.
  - intros [HP | [HQ HR]].
    + split.
      * left. apply HP.
      * left. apply HP.
    + split.
      * right. apply HQ.
      * right. apply HR.
  - intros [[HP | HQ] [HP' | HR]].
    + left. apply HP.
    + left. apply HP.
    + left. apply HP'.
    + right.
      split.
      * apply HQ.
      * apply HR.
Qed.

Lemma mult_0 : forall (m n : nat),
  n * m = 0 <-> n = 0 \/ m = 0.
Proof.
  split.
  - induction n.
    + left. reflexivity.
    + simpl.
      intros.
      apply and_exercise, proj1 in H.
      right.
      apply H.
  - intros [Hn | Hm].
    + rewrite Hn. reflexivity.
    + rewrite Hm, <- mult_n_O. reflexivity.
Qed.

Lemma mult_0_3 : forall (n m p : nat),
  n * m * p = 0 <-> n = 0 \/ m = 0 \/ p = 0.
Proof.
  intros.
  rewrite mult_0, mult_0.
  apply or_assoc.
Qed.

Theorem exists_example : forall (n : nat),
  (exists (m : nat), n = 4 + m) -> (exists (o : nat), n = 2 + o).
Proof.
  intros n [m Hm].
  exists (2 + m).
  apply Hm.
Qed.

Theorem dist_not_exists : forall (A : Type) (P : A -> Prop),
  (forall (a : A), P a) -> ~(exists (a : A), ~(P a)).
Proof.
  unfold not.
  intros A P H [a negPa].
  destruct (negPa (H a)).
Qed.

Theorem dist_exists_or : forall (A : Type) (P Q : A -> Prop),
  (exists a, P a \/ Q a) <-> (exists a, P a) \/ (exists a, Q a).
Proof.
  split.
  - intros [a [Pa | Qa]].
    + left.
      exists a.
      apply Pa.
    + right.
      exists a.
      apply Qa.
  - intros [[a Pa] | [a Qa]].
    + exists a.
      left.
      apply Pa.
    + exists a.
      right.
      apply Qa.
Qed.

Fixpoint In {A : Type} (a : A) (l : list A) :=
  match l with
  | nil => False
  | a' :: l => a' = a \/ In a l
  end.

Lemma In_map : forall {A B : Type} (a : A) (f : A -> B) (l : list A),
  In a l -> In (f a) (map f l).
Proof.
  induction l.
  - trivial.
  - intros [H | H].
    + left. apply f_equal, H.
    + right. apply IHl, H.
Qed.

Lemma In_map_iff : forall {A B} (f : A -> B) (l : list A) (b : B),
  In b (map f l) <-> exists a,  f a = b /\ In a l.
Proof.
  induction l.
  - split.
    + intros [].
    + intros [a [_ contra]].
      destruct contra.
  - split.
    + intros [H | H].
      * exists a.
        split.
        { apply H. }
        { left. reflexivity. }
      * apply (IHl b) in H.
        destruct H as [a' [H H']].
        exists a'.
        split.
        { apply H. }
        { right. apply H'. }
    + intros [a' [H [H' | H']]].
      * left.
        rewrite H'.
        apply H.
      * right.
        apply IHl.
        exists a'.
        split.
        { apply H. }
        { apply H'. }
Qed.

Lemma In_app_iff : forall {A} l l' (a : A),
  In a (l ++ l') <-> In a l \/ In a l'.
Proof.
  induction l.
  - split.
    + right.
      apply H.
    + intros [contra | H].
      * destruct contra.
      * apply H.
  - split.
    + intros [H | H].
      * left.
        left.
        apply H.
      * apply IHl in H.
        destruct H as [H | H].
        { left. right. apply H. }
        { right. apply H. }
    + intros [[H | H] | H].
      * left.
        apply H.
      * right.
        apply IHl.
        left.
        apply H.
      * right.
        apply IHl.
        right.
        apply H.
Qed.

Fixpoint All {A : Type} (P : A -> Prop) (l :list A) : Prop :=
  match l with
  | nil => True
  | a :: l => P a /\ All P l
  end.

Lemma All_In : forall {A} (P : A -> Prop) (l : list A),
  (forall a, In a l ->  P a) <-> All P l.
Proof.
  induction l.
  - split.
    + simpl. intros. trivial.
    + simpl. intros _ a [].
  - split.
    + split.
      * apply H.
        left.
        reflexivity.
      * apply IHl.
        intros a' H'.
        apply (H a').
        right.
        apply H'.
    + intros [Pa H] a' [H' | H'].
      * rewrite <- H'.
        apply Pa.
      * rewrite <- IHl in H.
        apply H.
        apply H'.
Qed.

Definition combine_odd_even (Podd Peven : nat -> Prop) : nat -> Prop :=
  fun n =>
    if odd n
      then Podd n
      else Peven n.

Theorem combine_odd_even_intro : forall (Podd Peven : nat -> Prop) (n : nat),
  (odd n = true -> Podd n) -> (odd n = false -> Peven n) -> combine_odd_even Podd Peven n.
Proof.
  induction n.
  - intros _ H.
    apply H.
    reflexivity.
  - unfold combine_odd_even.
    destruct (odd (S n)) eqn:HSn.
    + intros H _.
      apply H.
      reflexivity.
    + intros _ H.
      apply H.
      reflexivity.
Qed.

Theorem combine_odd_even_elim_odd : forall (Podd Peven : nat -> Prop) (n : nat),
  combine_odd_even Podd Peven n -> odd n = true -> Podd n.
Proof.
  intros Podd Peven n H HSn.
  unfold combine_odd_even in H.
  rewrite HSn in H.
  apply H.
Qed.

Theorem combine_odd_even_elim_even : forall (Podd Peven : nat -> Prop) (n : nat),
  combine_odd_even Podd Peven n -> odd n = false -> Peven n.
Proof.
  intros Podd Peven n H HSn.
  unfold combine_odd_even in H.
  rewrite HSn in H.
  apply H.
Qed.

Fixpoint shunt {A} (l1 l2 : list A) : list A :=
  match l1 with
  | nil => l2
  | a :: l1 => shunt l1 (a :: l2)
  end.

Definition rev' {A} (l : list A) : list A := shunt l nil.

Lemma shunt_app : forall {A} (l1 l2 : list A),
  rev l1 ++ l2 = shunt l1 l2.
Proof.
  induction l1.
  - reflexivity.
  - intros.
    simpl.
    rewrite <- app_assoc.
    apply IHl1.
Qed.

Theorem rev'_correct : forall {A} (l : list A),
  rev l = rev' l.
Proof.
  induction l.
  - reflexivity.
  - unfold rev'.
    simpl.
    apply shunt_app.
Qed.

Fixpoint double n :=
  match n with
  | O => O
  | S n => S (S (double n))
  end.

Theorem even_double : forall n,
  even (double n) = true.
Proof.
  induction n.
  - reflexivity.
  - simpl. apply IHn.
Qed.

Lemma double_negb : forall b,
  negb (negb b) = b.
Proof.
  destruct b. reflexivity. reflexivity.
Qed.

Lemma even_S : forall n,
  even (S n) = negb (even n).
Proof.
  induction n.
  - reflexivity.
  - rewrite IHn.
    rewrite (double_negb (even n)).
    reflexivity.
Qed.

Theorem even_double_conv : forall n,
  exists k, n = if even n then double k else S (double k).
Proof.
  induction n.
  - exists 0. reflexivity.
  - destruct IHn as [k IHn].
    rewrite even_S.
    destruct (even n).
    + exists k.
      rewrite IHn.
      reflexivity.
    + exists (S k).
      rewrite IHn.
      reflexivity.
Qed.

Theorem even_bool_prop : forall n,
  even n = true <-> exists k, n = double k.
Proof.
  split.
  - intros.
    destruct (even_double_conv n) as [k Hk].
    rewrite Hk.
    rewrite H.
    exists k.
    reflexivity.
  - intros [k Hk].
    rewrite Hk.
    apply even_double.
Qed.

Lemma eqb_true : forall n m,
  n =? m = true -> n = m.
Proof.
  induction n, m.
  - reflexivity.
  - discriminate.
  - discriminate.
  - simpl. intros. rewrite (IHn m H). reflexivity.
Qed.

Lemma eqb_refl : forall n,
  n =? n = true.
Proof.
  induction n.
  - reflexivity.
  - apply IHn.
Qed.

Theorem eqb_eq : forall n1 n2,
  n1 =? n2 = true <-> n1 = n2.
Proof.
  split.
  - apply eqb_true.
  - intros H. rewrite H. apply eqb_refl.
Qed.

Example even_1000 : exists k, 1000 = double k.
Proof. apply even_bool_prop. reflexivity. Qed.

Example not_even_1001 : ~(exists k, 1001 = double k).
Proof.
  rewrite <- even_bool_prop.
  unfold not.
  intros.
  discriminate H.
Qed.

Lemma plus_eqb_example : forall n m p,
  n =? m = true -> n + p =? m + p = true.
Proof.
  intros.
  rewrite eqb_eq in H.
  rewrite H, eqb_eq.
  reflexivity.
Qed.

Lemma andb_true_iff : forall b1 b2,
  b1 && b2 = true <-> b1 = true /\ b2 = true.
Proof.
  split.
  - destruct b1, b2.
    + split. reflexivity. reflexivity.
    + discriminate.
    + discriminate.
    + discriminate.
  - intros [Hb1 Hb2].
    rewrite Hb1, Hb2.
    reflexivity.
Qed.

Lemma orb_true_iff : forall b1 b2,
  b1 || b2 = true <-> b1 = true \/ b2 = true.
Proof.
  split.
  - destruct b1, b2.
    + left. reflexivity.
    + left. reflexivity.
    + right. reflexivity.
    + discriminate.
  - intros [H | H].
    + rewrite H.
      reflexivity.
    + rewrite H, orb_comm.
      reflexivity.
Qed.

Theorem eqb_neg : forall n m,
  n =? m = false <-> n <> m.
Proof.
  split.
  - unfold not.
    intros H eq.
    apply eqb_eq in eq.
    destruct (n =? m).
    + discriminate.
    + discriminate.
  - rewrite <- eqb_eq.
    intros.
    destruct (n =? m).
    + destruct (H (eq_refl true)).
    + reflexivity.
Qed.

Fixpoint eqb_list {A : Type} (eqb : A -> A -> bool) (l1 l2 : list A) : bool :=
  match (l1, l2) with
  | (nil, nil) => true
  | (a1 :: l1, a2 :: l2) => eqb a1 a2 && eqb_list eqb l1 l2
  | _ => false
  end.

Definition double_negation_elimination := forall P, ~~P -> P.

Lemma not_eqb : double_negation_elimination -> forall {A} (eqb : A -> A -> bool),
  (forall a1 a2, eqb a1 a2 = true <-> a1 = a2) <-> (forall a1 a2, eqb a1 a2 = false <-> a1 <> a2).
Proof.
  intro double_negation_elimination.
  split.
  - split.
    + destruct (eqb a1 a2) eqn:?.
      * discriminate.
      * unfold not.
        intros _ eq.
        rewrite <- H in eq.
        rewrite Heqb in eq.
        discriminate.
    + destruct (eqb a1 a2) eqn:?.
      * apply H in Heqb.
        unfold not.
        intros neq.
        destruct (neq Heqb).
      * reflexivity.
  - split.
    + destruct (eqb a1 a2) eqn:?.
      * specialize (H a1 a2).
        rewrite Heqb in H.
        elim H.
        intros _ goal.
        assert (convert : (a1 <> a2 -> true = false) <-> ~~(a1 = a2)).
        { unfold not.
          split.
          - intros.
            discriminate (H0 H1).
          - intros.
            destruct (H0 H1). }
        rewrite convert in goal.
        apply double_negation_elimination in goal.
        trivial.
      * discriminate.
    + destruct (eqb a1 a2) eqn:?.
      * reflexivity.
      * specialize (H a1 a2).
        rewrite H in Heqb.
        intros.
        destruct (Heqb H0).
Qed.

Lemma eqb_list_true_iff : forall {A} (eqb : A -> A -> bool),
  (forall a1 a2, eqb a1 a2 = true <-> a1 = a2) -> (forall l1 l2, eqb_list eqb l1 l2 = true <-> l1 = l2).
Proof.
  induction l1.
  - destruct l2.
    + split; reflexivity.
    + split; discriminate.
  - destruct l2.
    + split; discriminate.
    + simpl. destruct (eqb a a0) eqn:?.
      * simpl.
        split.
        { rewrite H in Heqb.
          rewrite Heqb.
          intros.
          rewrite IHl1 in H0.
          rewrite H0.
          reflexivity. }
        { intros.
          injection H0 as _ Hl.
          rewrite <- IHl1 in Hl.
          apply Hl. }
      * split.
        { discriminate. }
        { intros eq.
          injection eq as eq _.
          apply (H a a0) in eq.
          rewrite Heqb in eq.
          discriminate. }
Qed.

Fixpoint forallb {A : Type} (test : A -> bool) (l : list A) : bool :=
  match l with
  | nil => true
  | a :: l => test a && forallb test l
  end.

Theorem forallb_true_iff : forall {A} test (l : list A),
  forallb test l = true <-> All (fun x => test x = true) l.
Proof.
  induction l.
  - split; reflexivity.
  - simpl. split; destruct (test a) eqn:?.
    + split.
      * reflexivity.
      * apply IHl, H.
    + split; discriminate.
    + intros [_ goal].
      rewrite <- IHl in goal.
      apply goal.
    + intros [contra _].
      discriminate.
Qed.

Theorem restricted_excluded_middle : forall P b,
  (P <-> b = true) -> P \/ ~P.
Proof.
  intros P [] H.
  - left. rewrite H. reflexivity.
  - right. rewrite H. intros contra. discriminate.
Qed.

Theorem restricted_excluded_middle_eq : forall n m : nat,
  n = m \/ n <> m.
Proof.
  intros n m.
  apply (restricted_excluded_middle (n = m) (n =? m)).
  symmetry.
  apply eqb_eq.
Qed.

Definition excluded_middle := forall P, P \/ ~P.

Theorem excluded_middle_irrefutable : forall P,
  ~~(P \/ ~P).
Proof.
  unfold not.
  intros.
  apply H.
  intros.
  right.
  intros p.
  apply H.
  left.
  assumption.
Qed.

Theorem not_exists_dist : excluded_middle -> forall {A} (P : A -> Prop),
  ~(exists a, ~P a) -> forall a, P a.
Proof.
  intro em.
  intros.
  destruct em with (P := P a) as [Pa | nPa].
  - apply Pa.
  - exfalso.
    apply H.
    exists a.
    apply nPa.
Qed.

Definition peirce := forall P Q : Prop, ((P -> Q) -> P) -> P.

Definition impl_disj := forall P Q : Prop, (P -> Q) -> ~P \/ Q.

Definition de_morgan := forall P Q : Prop, ~(~P /\ ~Q) -> P \/ Q.

(* Excluded middle. *)

Theorem excluded_middle_irrefutable' : forall P,
  ~~(P \/ ~P).
Proof.
  unfold not.
  intros.
  apply H.
  right.
  intros p.
  apply H.
  left.
  assumption.
Qed.

Theorem excluded_middle_double_negation_elimination :
  excluded_middle <-> double_negation_elimination.
Proof.
  unfold double_negation_elimination, excluded_middle, not.
  split.
  - intros excluded_middle P H.
    destruct (excluded_middle P) as [p | nP].
    + assumption.
    + destruct (H nP).
  - intros double_negation_elimination P.
    apply double_negation_elimination.
    intros H.
    apply H.
    right.
    intros p.
    apply H.
    left.
    assumption.
Qed.

Theorem excluded_middle_peirce :
  excluded_middle <-> peirce.
Proof.
  unfold excluded_middle, not, peirce.
  split.
  - intros excluded_middle P Q H.
    destruct (excluded_middle P) as [p | nP].
    + assumption.
    + apply H.
      intros p.
      destruct (excluded_middle Q) as [q | nQ].
      * assumption.
      * exfalso.
        apply nP.
        assumption.
  - intros peirce P.
    apply peirce with (Q := False).
    intros H.
    right.
    intros p.
    apply H.
    left.
    assumption.
Qed.

Theorem excluded_middle_impl_disj :
  excluded_middle <-> impl_disj.
Proof.
  unfold excluded_middle, impl_disj, not.
  split.
  - intros excluded_middle P Q H.
    destruct (excluded_middle Q) as [q | nQ].
    + right.
      assumption.
    + left.
      intros q.
      apply nQ.
      apply H.
      assumption.
  - intros impl_disj P.
    destruct (impl_disj P P).
    + trivial.
    + right.
      assumption.
    + left.
      assumption.
Qed.

Theorem excluded_middle_de_morgan :
  excluded_middle <-> de_morgan.
Proof.
  unfold de_morgan, excluded_middle, not.
  split.
  - intros excluded_middle P Q H.
    destruct (excluded_middle P) as [p | nP].
    + left.
      assumption.
    + destruct (excluded_middle Q) as [q | nQ].
      * right.
        assumption.
      * exfalso.
        apply H.
        split; assumption.
  - intros de_morgan P.
    apply de_morgan.
    intros [nP nnP].
    apply nnP.
    assumption.
Qed.

(* Double negation elimination. *)

Theorem double_negation_elimination_irrefutable : forall P,
  ~~(~~P -> P).
Proof.
  unfold not.
  intros P double_negation_elimination.
  apply double_negation_elimination.
  intros.
  exfalso.
  apply H.
  intros p.
  apply double_negation_elimination.
  intros.
  assumption.
Qed.

Theorem double_negation_elimination_peirce :
  double_negation_elimination <-> peirce.
Proof.
  unfold double_negation_elimination, not, peirce.
  split.
  - intros double_negation_elimination P Q H.
    apply double_negation_elimination.
    intros nP.
    apply nP.
    apply H.
    intros p.
    exfalso.
    apply nP.
    assumption.
  - intros peirce P H.
    apply peirce with (Q := False).
    intros nP.
    exfalso.
    apply H.
    intros p.
    apply nP.
    assumption.
Qed.

Theorem double_negation_elimination_impl_disj :
  double_negation_elimination <-> impl_disj.
Proof.
  unfold double_negation_elimination, impl_disj, not.
  split.
  - intros double_negation_elimination P Q H.
    apply double_negation_elimination.
    intros H'.
    apply H'.
    left.
    intros p.
    apply H'.
    right.
    apply H.
    assumption.
  - intros impl_disj P H.
    destruct (impl_disj P P) as [nP | p].
    + trivial.
    + exfalso.
      apply H.
      intros p.
      apply nP.
      assumption.
    + assumption.
Qed.

Theorem double_negation_elimination_de_morgan :
  double_negation_elimination <-> de_morgan.
Proof.
  unfold de_morgan, double_negation_elimination, not.
  split.
  - intros double_negation_elimination P Q H.
    apply double_negation_elimination.
    intros H'.
    apply H.
    split.
    + intros p.
      apply H'.
      left.
      assumption.
    + intros q.
      apply H'.
      right.
      assumption.
  - intros de_morgan P H.
    destruct (de_morgan P P); try assumption.
    + intros [nP _].
      apply H.
      intros p.
      apply nP.
      assumption.
Qed.

(* Peirce's law. *)

Theorem peirce_irrefutable : forall P Q : Prop,
  ~~(((P -> Q) -> P) -> P).
Proof.
  unfold not.
  intros P Q H.
  apply H.
  intros H'.
  apply H'.
  intros p.
  exfalso.
  apply H.
  intros.
  assumption.
Qed.

Theorem peirce_impl_disj :
  peirce <-> impl_disj.
Proof.
  unfold impl_disj, not, peirce.
  split.
  - intros peirce P Q H.
    apply peirce with (Q := False).
    intros H'.
    left.
    intros p.
    apply H'.
    right.
    apply H.
    assumption.
  - intros impl_disj P Q H.
    destruct (impl_disj P P) as [nP | p].
    + trivial.
    + apply H.
      intros p.
      exfalso.
      apply nP.
      assumption.
    + assumption.
Qed.

Theorem peirce_de_morgan :
  peirce <-> de_morgan.
Proof.
  unfold de_morgan, not, peirce.
  split.
  - intros peirce P Q H.
    apply peirce with (Q := False).
    intros H'.
    exfalso.
    apply H.
    split.
    + intros p.
      apply H'.
      left.
      assumption.
    + intros q.
      apply H'.
      right.
      assumption.
  - intros de_morgan P Q H.
    destruct (de_morgan P P); try assumption.
    + intros [nP _].
      apply nP.
      apply H.
      intros p.
      exfalso.
      apply nP.
      assumption.
Qed.

(* Implication as disjunction. *)

Theorem impl_disj_irrefutable : forall P Q : Prop,
  ~~((P -> Q) -> ~P \/ Q).
Proof.
  unfold not.
  intros P Q H.
  apply H.
  intros H'.
  left.
  intros p.
  apply H.
  right.
  apply H'.
  assumption.
Qed.

Theorem impl_disj_de_morgan :
  impl_disj <-> de_morgan.
Proof.
  unfold de_morgan, impl_disj, not.
  split.
  - intros impl_disj P Q H.
    destruct (impl_disj (P \/ Q) (P \/ Q)) as [nPQ | pq].
    + trivial.
    + exfalso.
      apply H.
      split.
      * intros p.
        apply nPQ.
        left.
        assumption.
      * intros q.
        apply nPQ.
        right.
        assumption.
    + assumption.
  - intros de_morgan P Q H.
    apply de_morgan.
    intros [nnP nQ].
    apply nnP.
    intros p.
    apply nQ.
    apply H.
    assumption.
Qed.

(* De Morgan. *)

Theorem de_morgan_irrefutable : forall P Q : Prop,
  ~~(~(~P /\ ~Q) -> P \/ Q).
Proof.
  unfold not.
  intros P Q H.
  apply H.
  intros H'.
  exfalso.
  apply H'.
  split.
  - intros p.
    apply H.
    intros.
    left.
    assumption.
  - intros q.
    apply H.
    intros.
    right.
    assumption.
Qed.