Software Foundations: Inductively Defined Propositions

IndProp.v

Require Import Arith.
Require Import Bool.
Require Import Nat.
Require Import List.
Import ListNotations.
Require Import Omega.

Inductive regex : Type :=
| empty
| char' (a : nat)
| app' (r1 r2 : regex)
| union (r1 r2 : regex)
| star (r : regex).

Reserved Notation "s =~ r" (at level 80).

Inductive regex_match : list nat -> regex -> Prop :=
| char a : [a] =~ char' a
| app s1 s2 r1 r2 (H1 : s1 =~ r1) (H2 : s2 =~ r2) : s1 ++ s2 =~ app' r1 r2
| union_l s r1 r2 (H : s =~ r1) : s =~ union r1 r2
| union_r s r1 r2 (H : s =~ r2) : s =~ union r1 r2
| star_O r : [] =~ star r
| star_S s1 s2 r (H1 : s1 =~ r) (H2 : s2 =~ star r) : s1 ++ s2 =~ star r
where "s =~ r" := (regex_match s r).

Lemma empty_star : forall s,
  s =~ star empty -> s = [].
Proof.
  intros.
  inversion H; subst.
  - reflexivity.
  - inversion H2.
Qed.

Fixpoint regex_of_list l :=
match l with
| [] => star empty
| x :: l => app' (char' x) (regex_of_list l)
end.

Lemma star_regex : forall s r,
  s =~ r -> s =~ star r.
Proof.
  intros.
  rewrite <- (app_nil_r s).
  apply star_S; auto; constructor.
Qed.

Lemma empty_regex : forall s,
  ~(s =~ empty).
Proof. intros s H. inversion H. Qed.

Lemma star_fold_regex : forall ss r,
  (forall s, In s ss -> s =~ r) -> fold_right (@List.app nat) [] ss =~ star r.
Proof.
  intros.
  induction ss; simpl; constructor.
  - apply H. left. reflexivity.
  - apply IHss. intros. apply H. right. assumption.
Qed.

Lemma regex_of_list_refl : forall s1 s2,
  s1 =~ regex_of_list s2 <-> s1 = s2.
Proof.
  split; generalize dependent s1; induction s2; intros.
  - inversion H; subst.
    + reflexivity.
    + inversion H2.
  - inversion H. subst.
    inversion H3. subst.
    apply f_equal. apply IHs2. assumption.
  - rewrite H. apply (star_O empty).
  - rewrite H.
    assert (a :: s2 = [a] ++ s2) as eq by auto. rewrite eq.
    apply app.
    * apply char.
    * apply IHs2. reflexivity.
Qed.

Fixpoint regex_characters r :=
match r with
| empty => []
| char' a => [a]
| app' r1 r2 => regex_characters r1 ++ regex_characters r2
| union r1 r2 => regex_characters r1 ++ regex_characters r2
| star r => regex_characters r
end.

Theorem in_regex_characters : forall s r x,
  s =~ r -> In x s -> In x (regex_characters r).
Proof.
  intros s r x Hr Hin.
  induction Hr.
  - apply Hin.
  - apply in_or_app.
    apply in_app_or in Hin as [].
    + left. apply IHHr1. assumption.
    + right. apply IHHr2. assumption.
  - apply in_or_app.
    left. apply IHHr. assumption.
  - apply in_or_app.
    right. apply IHHr. assumption.
  - contradiction.
  - apply in_app_or in Hin as [].
    + apply IHHr1. assumption.
    + apply IHHr2. assumption.
Qed.

Fixpoint regex_matches r :=
match r with
| empty => false
| char' _ => true
| app' r1 r2 => regex_matches r1 && regex_matches r2
| union r1 r2 => regex_matches r1 || regex_matches r2
| star r => true
end.

Lemma regex_matches_correct : forall r,
  regex_matches r = true <-> exists s, s =~ r.
Proof.
  split.
  - induction r; simpl; intros.
    + discriminate.
    + exists [a]. apply char.
    + unfold andb in H.
      destruct (regex_matches r1); try discriminate.
      destruct (regex_matches r2); try discriminate.
      destruct IHr1 as [s1 Hr1]; auto.
      destruct IHr2 as [s2 Hr2]; auto.
      exists (s1 ++ s2).
      apply app; assumption.
    + unfold orb in H.
      destruct (regex_matches r1).
      * destruct IHr1 as [s Hr]; auto.
        exists s. apply union_l. assumption.
      * destruct (regex_matches r2); try discriminate.
        destruct IHr2 as [s Hr]; auto.
        exists s. apply union_r. assumption.
    + exists []. apply star_O.
  - intros [s H].
    induction H; simpl; intuition.
Qed.

Lemma star_app : forall s1 s2 r,
  s1 =~ star r -> s2 =~ star r -> s1 ++ s2 =~ star r.
Proof.
  intros s1 s2 r H1.
  generalize dependent s2.
  remember (star r) as sr.
  induction H1; try discriminate; auto.
  injection Heqsr. intros.
  rewrite <- app_assoc.
  apply star_S; auto.
Qed.

Lemma star_regex_matches : forall s r,
  s =~ star r -> exists ss, s = fold_right (@List.app nat) [] ss /\ forall s, In s ss -> s =~ r.
Proof.
  intros.
  remember (star r) as sr.
  induction H; auto; try discriminate.
  - exists [].
    split; auto.
    intros. inversion H.
  - injection Heqsr as eq. subst.
    destruct IHregex_match2 as [ss [Hss Hin]]; auto.
    exists (s1 :: ss).
    split.
    + rewrite Hss. reflexivity.
    + intros s []; subst; auto.
Qed.

Fixpoint napp {A} n l : list A :=
  match n with O => [] | S n => l ++ napp n l end.

Lemma napp_plus : forall {A} n m (l : list A),
  napp (n + m) l = napp n l ++ napp m l.
Proof.
  intros. induction n; auto.
  simpl. rewrite IHn, app_assoc. reflexivity.
Qed.

Fixpoint pumping_constant r :=
match r with
| empty => 0
| char' _ => 2
| app' r1 r2 => pumping_constant r1 + pumping_constant r2
| union r1 r2 => pumping_constant r1 + pumping_constant r2
| star _ => 1
end.

Lemma pumping_match : forall r s,
  s =~ r -> 0 < pumping_constant r.
Proof. intros. induction H; simpl; try constructor; omega. Qed.

Lemma pumping : forall r s,
  s =~ r -> pumping_constant r <= length s ->
  exists s1 s2 s3,
    s = s1 ++ s2 ++ s3 /\
    s2 <> [] /\
    forall n, s1 ++ napp n s2 ++ s3 =~ r.
Proof.
  intros r s H.
  induction H; simpl; intros; try omega.
  - (* app *)
    rewrite app_length in H1.
    apply Nat.add_le_cases in H1 as [].
    + destruct (IHregex_match1 H1) as [s1' [s2' [s3' [eq [H' Hnapp]]]]].
      exists s1', s2', (s3' ++ s2); split; try split; auto.
      * rewrite eq, <- app_assoc, <- app_assoc. reflexivity.
      * intros. repeat rewrite app_assoc.
        apply app; auto.
        repeat rewrite <- app_assoc. apply Hnapp.
    + destruct (IHregex_match2 H1) as [s1' [s2' [s3' [eq [H' Hnapp]]]]].
      exists (s1 ++ s1'), s2', s3'; split; try split; auto.
      * rewrite eq, <- app_assoc. reflexivity.
      * intros. repeat rewrite <- app_assoc.
        apply app; auto.
  - (* union_l *)
    assert (pumping_constant r1 <= length s) by omega.
    destruct IHregex_match as [s1' [s2' [s3' [eq []]]]]; auto.
    exists s1', s2', s3'; split; try split; intros; try apply union_l; auto.
  - (* union_r *)
    assert (pumping_constant r2 <= length s) by omega.
    destruct IHregex_match as [s1' [s2' [s3' [eq []]]]]; auto.
    exists s1', s2', s3'; split; try split; intros; try apply union_r; auto.
  - (* star_S *)
    exists [], (s1 ++ s2), []; split; try split; simpl; intros.
    + rewrite app_nil_r. reflexivity.
    + destruct (s1 ++ s2).
      * simpl in H1. omega.
      * discriminate.
    + rewrite app_nil_r.
      induction n.
      * apply star_O.
      * apply star_app.
        { apply star_S; auto. }
        { apply IHn. }
Qed.

Definition evenb := even.

Inductive even : nat -> Prop :=
| even_O : even 0
| even_S : forall n, even n -> even (S (S n)).

Theorem even_4 : even 4.
Proof. apply even_S, even_S, even_O. Qed.

Theorem even_plus_4 : forall n,
  even n -> even (4 + n).
Proof. intros. apply even_S, even_S, H. Qed.

Theorem even_double : forall n,
  even (double n).
Proof.
  induction n.
  - apply even_O.
  - unfold double.
    rewrite <- plus_n_Sm.
    apply even_S, IHn.
Qed.

Theorem even_inversion : forall n,
  even n -> n = 0 \/ exists m, n = S (S m) /\ even m.
Proof.
  intros n E.
  destruct E eqn:?.
  - left. reflexivity.
  - right. exists n. split. reflexivity. apply e.
Qed.

Theorem even_pred_pred : forall n,
  even n -> even (pred (pred n)).
Proof.
  intros n E.
  destruct E eqn:?.
  - apply even_O.
  - apply e.
Qed.

Theorem even_S_S : forall n,
  even (S (S n)) -> even n.
Proof.
  intros.
  apply even_inversion in H.
  destruct H.
  - discriminate.
  - destruct H as [m [eq H]].
    injection eq as eq.
    rewrite eq.
    apply H.
Qed.


Theorem even_S_S' : forall n,
  even (S (S n)) -> even (pred (pred (S (S n)))).
Proof.
  intros.
  destruct H.
  - apply even_O.
  - apply H.
Qed.

Theorem even_S_S'' : forall n,
  even (S (S n)) -> even n.
Proof. intros. inversion H. apply H1. Qed.

Theorem one_not_even : ~even 1.
Proof.
  intros H.
  apply even_inversion in H.
  destruct H as [| [m [H _]]]; discriminate.
Qed.

Theorem one_not_even' : ~even 1.
Proof. intros H. inversion H. Qed.

Theorem even_4_plus : forall n,
  even (4 + n) -> even n.
Proof.
  intros.
  apply even_inversion in H.
  destruct H as [| [m [H Hm]]].
  - discriminate.
  - injection H as eq.
    rewrite <- eq in Hm.
    apply even_inversion in Hm.
    destruct Hm as [| [p [H Hp]]].
    + discriminate.
    + injection H as H.
      rewrite H.
      apply Hp.
Qed.

Theorem even_4_plus' : forall n,
  even (4 + n) -> even n.
Proof. intros. inversion H. inversion H1. trivial. Qed.

Theorem five_not_even : ~even 5.
Proof. intros H. inversion H. inversion H1. inversion H3. Qed.

Theorem inversion_example : forall n m o : nat,
  [n; m] = [o; o] -> [n] = [m].
Proof. intros. inversion H. reflexivity. Qed.

Lemma even_even : forall n,
  even n -> exists k, n = double k.
Proof.
  intros.
  induction H.
  - exists 0. reflexivity.
  - destruct IHeven as [k Hk].
    rewrite Hk.
    exists (S k).
    unfold double.
    rewrite <- plus_n_Sm.
    reflexivity.
Qed.

Theorem even_iff_even : forall n,
  even n <-> exists k, n = double k.
Proof.
  split.
  - apply even_even.
  - intros [k Hk]. rewrite Hk. apply even_double.
Qed.

Theorem even_plus : forall n m,
  even n -> even m -> even (n + m).
Proof.
  intros n m En Em.
  induction En.
  - apply Em.
  - inversion IHEn as [eq | p Hp eq]; simpl.
    + rewrite <- eq. apply even_S, even_O.
    + rewrite <- eq. apply even_S, even_S in Hp. apply Hp.
Qed.

Theorem even_plus' : forall n m,
  even n -> even m -> even (n + m).
Proof.
  intros n m En Em.
  induction En.
  - apply Em.
  - apply even_S in IHEn.
    destruct Em; apply IHEn.
Qed.

Inductive even' : nat -> Prop :=
| even'_0 : even' 0
| even'_2 : even' 2
| even'_plus {n m} (Hn : even' n) (Hm : even' m) : even' (n + m).

Theorem even'_even : forall n,
  even n <-> even' n.
Proof.
  split.
  - intros.
    induction H.
    + apply even'_0.
    + apply (even'_plus even'_2) in IHeven.
      apply IHeven.
  - intros.
    induction H.
    + apply even_O.
    + apply even_S, even_O.
    + apply even_plus.
      * apply IHeven'1.
      * apply IHeven'2.
Qed.

Theorem even_even_even : forall n m,
  even (n + m) -> even n -> even m.
Proof.
  intros n m Enm En.
  induction En.
  - apply Enm.
  - inversion Enm as [| n' goal].
    apply IHEn in goal.
    apply goal.
Qed.

Theorem even_plus_plus : forall n m p,
  even (n + m) -> even (n + p) -> even (m + p).
Proof.
  intros n m p Enm Enp.
  assert (H : even ((n + m) + (n + p))).
  { apply even_plus. apply Enm. apply Enp. }
  rewrite plus_assoc in H.
  rewrite (plus_comm n m) in H.
  rewrite <- (plus_assoc m n n) in H.
  rewrite (plus_comm m (n + n)) in H.
  rewrite <- plus_assoc in H.
  assert (Hnn : even (n + n)).
  { apply even_double. }
  apply (even_even_even (n + n)).
  - apply H.
  - apply Hnn.
Qed.

Inductive le : nat -> nat -> Prop :=
| le_n : forall n, le n n
| le_S : forall n m, le n m -> le n (S m).

Notation "n <= m" := (le n m).

Definition lt n m := le (S n) m.

Notation "n < m" := (lt n m).

Lemma le_O : forall n,
  O <= n.
Proof.
  induction n.
  - apply le_n.
  - apply le_S in IHn.
    apply IHn.
Qed.

Lemma le_trans : forall {n m o},
  n <= m -> m <= o -> n <= o.
Proof.
  intros n m o Hnm Hmo.
  induction Hmo.
  - trivial.
  - apply le_S.
    apply IHHmo.
    apply Hnm.
Qed.

Theorem le_injective : forall n m,
  n <= m <-> S n <= S m.
Proof.
  split; intros.
  - induction H.
    + apply le_n.
    + apply le_S in IHle.
      apply IHle.
  - inversion H as [| n' m' H'].
    + apply le_n.
    + assert (Hn : n <= S n).
      { apply le_S, le_n. }
      apply (le_trans Hn H').
Qed.

Theorem le_plus : forall n m,
  n <= n + m.
Proof.
  induction n.
  - apply le_O.
  - intros.
    simpl.
    rewrite <- le_injective.
    trivial.
Qed.

Theorem le_plus' : forall n m,
  n <= n + m.
Proof.
  induction m.
  - rewrite <- plus_n_O.
    apply le_n.
  - rewrite <- plus_n_Sm.
    apply le_S.
    assumption.
Qed.

Theorem plus_lt : forall n1 n2 m,
  n1 + n2 < m -> n1 < m /\ n2 < m.
Proof.
  unfold lt.
  split.
  - inversion H as [| n' m' Hm].
    + rewrite <- le_injective.
      apply le_plus.
    + assert (Hn : S n1 <= S n1 + n2).
      { apply le_plus. }
      apply le_S.
      apply (le_trans Hn Hm).
  - inversion H as [| n' m' Hm].
    + rewrite <- le_injective.
      rewrite <- plus_comm.
      apply le_plus.
    + assert (Hn : S n2 <= S n1 + n2).
      { rewrite plus_Snm_nSm, plus_comm. apply le_plus. }
      apply le_S.
      apply (le_trans Hn Hm).
Qed.

Theorem lt_S : forall n m,
  n < m -> n < S m.
Proof.
  unfold lt.
  intros.
  apply le_S.
  assumption.
Qed.

Theorem leb_complete : forall n m,
  n <=? m = true -> n <= m.
Proof.
  induction n; intros.
  - apply le_O.
  - destruct m.
    + discriminate.
    + rewrite <- le_injective.
      inversion H as [goal].
      apply IHn in goal.
      assumption.
Qed.

Lemma leb_refl : forall n,
  (n <=? n) = true.
Proof.
  induction n.
  - reflexivity.
  - apply IHn.
Qed.

Lemma leb_S : forall n m,
  n <=? m = true -> n <=? S m = true.
Proof.
  induction n.
  - trivial.
  - destruct m.
    + discriminate.
    + apply IHn.
Qed.

Theorem leb_correct : forall n m,
  n <= m -> n <=? m = true.
Proof.
  intros. induction m.
  - inversion H. reflexivity.
  - inversion H as [| n' m' goal].
    + apply leb_refl.
    + apply IHm in goal.
      apply leb_S.
      trivial.
Qed.

Theorem leb_trans : forall n m o,
  n <=? m = true -> m <=? o = true -> n <=? o = true.
Proof.
  intros n m o Hnm Hmo.
  apply leb_correct.
  apply leb_complete in Hnm.
  apply leb_complete in Hmo.
  apply (le_trans Hnm Hmo).
Qed.

Theorem leb_iff : forall n m,
  n <=? m = true <-> n <= m.
Proof.
  split. apply leb_complete. apply leb_correct.
Qed.

Module R.

Inductive R : nat -> nat -> nat -> Prop :=
| c1 : R 0 0 0
| c2 m n o (H : R m n o) : R (S m) n (S o)
| c3 m n o (H : R m n o) : R m (S n) (S o)
| c4 m n o (H : R (S m) (S n) (S (S o))) : R m n o
| c5 m n o (H : R m n o) : R n m o.

Inductive R' : nat -> nat -> nat -> Prop :=
| c1' : R' 0 0 0
| c2' m n o (H : R' m n o) : R' (S m) n (S o)
| c4' m n o (H : R' (S m) (S n) (S (S o))) : R' m n o
| c5' m n o (H : R' m n o) : R' n m o.

Theorem relation_plus : forall m n o,
  R m n o <-> m + n = o.
Proof.
  split.
  - intros. induction H.
    + reflexivity.
    + rewrite <- IHR. reflexivity.
    + rewrite <- plus_n_Sm. rewrite IHR. reflexivity.
    + rewrite <- plus_n_Sm in IHR.
      injection IHR.
      trivial.
    + rewrite plus_comm.
      assumption.
  - generalize dependent o.
    generalize dependent n.
    induction m; induction n; intros.
      + simpl in H. rewrite <- H. apply c1.
      + simpl in H. rewrite <- H.
        apply c3.
        apply IHn.
        apply plus_O_n.
      + rewrite <- plus_n_O in H. rewrite <- H.
        apply c2.
        apply IHm.
        rewrite plus_n_O.
        reflexivity.
      + destruct o.
         * discriminate.
         * destruct o; rewrite <- plus_n_Sm in H.
           { discriminate. }
           { injection H as H.
              apply c2, c3.
              apply IHm.
              assumption. }
Qed.

Theorem relation'_plus : forall m n o,
  R' m n o <-> m + n = o.
Proof.
  split.
  - intros. induction H.
    + reflexivity.
    + rewrite <- IHR'. reflexivity.
    + rewrite <- plus_n_Sm in IHR'.
      injection IHR'.
      trivial.
    + rewrite plus_comm.
      assumption.
  - generalize dependent o.
    generalize dependent n.
    induction m; induction n; intros.
    + simpl in H.
      rewrite <- H.
      apply c1'.
    + simpl in H. rewrite <- H.
      apply c5', c2', c5'.
      apply IHn.
      reflexivity.
    + rewrite <- plus_n_O in H. rewrite <- H.
      apply c2'.
      apply IHm.
      rewrite plus_n_O.
      reflexivity.
    + destruct o.
         * discriminate.
         * destruct o; rewrite <- plus_n_Sm in H.
           { discriminate. }
           { injection H as H.
             apply c2', c5', c2', c5'.
             apply IHm.
             assumption. }
Qed.

Theorem relation_relation' : forall m n o,
  R m n o <-> R' m n o.
Proof.
  split; intros.
  - apply relation_plus in H.
    apply relation'_plus.
    assumption.
  - apply relation'_plus in H.
    apply relation_plus.
    assumption.
Qed.

Inductive R'' : nat -> nat -> nat -> Prop :=
| c1'' : R'' 0 0 0
| c2'' m n o (H : R'' m n o) : R'' (S m) n (S o)
| c3'' m n o (H : R'' m n o) : R'' m (S n) (S o)
| c5'' m n o (H : R'' m n o) : R'' n m o.

Theorem relation''_plus : forall m n o,
  R'' m n o <-> m + n = o.
Proof.
  split.
  - intros. induction H.
    + reflexivity.
    + rewrite <- IHR''. reflexivity.
    + rewrite <- plus_n_Sm. rewrite IHR''. reflexivity.
    + rewrite plus_comm.
      assumption.
  - generalize dependent o.
    generalize dependent n.
    induction m; induction n; intros.
    + simpl in H. rewrite <- H. apply c1''.
    + simpl in H. rewrite <- H.
      apply c3''.
      apply IHn.
      apply plus_O_n.
    + rewrite <- plus_n_O in H. rewrite <- H.
      apply c2''.
      apply IHm.
      rewrite plus_n_O.
      reflexivity.
    + destruct o.
      * discriminate.
      * destruct o; rewrite <- plus_n_Sm in H.
        { discriminate. }
        { injection H as H.
          apply c2'', c3''.
          apply IHm.
          assumption. }
Qed.

Theorem relation_relation'' : forall m n o,
  R m n o <-> R'' m n o.
Proof.
  split; intros.
  - apply relation_plus in H.
    apply relation''_plus.
    assumption.
  - apply relation''_plus in H.
    apply relation_plus.
    assumption.
Qed.

End R.

Inductive subseq {A : Type} : list A -> list A -> Prop :=
| subseq_nil l1 : subseq nil l1
| subseq_append l1 l2 (H : subseq l1 l2) a : subseq (a :: l1) (a :: l2)
| subseq_skip l1 l2 (H : subseq l1 l2) a : subseq l1 (a :: l2).

Example example_1 : subseq [1; 2; 3] [1; 2; 3].
Proof.
  apply subseq_append, subseq_append, subseq_append, subseq_nil.
Qed.

Example example_2 : subseq [1; 2; 3] [1; 1; 1; 2; 2; 3].
Proof.
  apply subseq_append, subseq_skip, subseq_skip, subseq_append, subseq_skip, subseq_append, subseq_nil.
Qed.

Example example_3 : subseq [1; 2; 3] [1; 2; 7; 3].
Proof.
  apply subseq_append, subseq_append, subseq_skip, subseq_append, subseq_nil.
Qed.

Example example_4 : subseq [1; 2; 3] [5; 6; 1; 9; 9; 2; 7; 3; 8].
Proof.
  apply subseq_skip, subseq_skip, subseq_append, subseq_skip, subseq_skip, subseq_append, subseq_skip, subseq_append, subseq_nil.
Qed.

Theorem subseq_refl : forall {A} (l : list A),
  subseq l l.
Proof.
  induction l.
  - apply subseq_nil.
  - apply subseq_append.
    assumption.
Qed.

Theorem subseq_app : forall {A} (l1 l2 l3 : list A),
  subseq l1 l2 -> subseq l1 (l2 ++ l3).
Proof.
  intros. induction H.
  - apply subseq_nil.
  - apply subseq_append. assumption.
  - apply subseq_skip. assumption.
Qed.

Lemma subseq_cons : forall {A} (l1 l2 : list A) a,
  subseq l1 l2 -> subseq l1 (a :: l2).
Proof.
  intros. destruct H.
  - apply subseq_nil.
  - apply subseq_skip.
    apply subseq_append.
    assumption.
  - apply subseq_skip, subseq_skip.
    assumption.
Qed.

Theorem subseq_trans : forall {A} (l1 l2 l3 : list A),
  subseq l1 l2 -> subseq l2 l3 -> subseq l1 l3.
Proof.
  intros A l1 l2 l3 H12 H23.
  generalize dependent l1.
  induction H23.
  - intros. inversion H12. apply subseq_nil.
  - intros. inversion H12.
    + apply subseq_nil.
    + apply subseq_append.
      apply IHsubseq.
      assumption.
    + apply subseq_cons.
      apply IHsubseq.
      assumption.
  - intros. inversion H12.
    + apply subseq_nil.
    + apply subseq_cons.
      apply IHsubseq.
      rewrite H0.
      assumption.
    + apply subseq_cons.
      apply IHsubseq.
      assumption.
Qed.

Inductive R : nat -> list nat -> Prop :=
| c1 : R 0 []
| c2 : forall {n l}, R n l -> R (S n) (n :: l)
| c3 : forall {n l}, R (S n) l -> R n l.

Example example_5 : R 2 [1; 0].
Proof. apply c2, c2, c1. Qed.

Example example_6 : R 1 [1; 2; 1; 0].
Proof. apply c3, c2, c3, c3, c2, c2, c2, c1. Qed.

Inductive reflect (P : Prop) : bool -> Prop :=
| ReflectT (H : P) : reflect P true
| ReflectF (H : ~P) : reflect P false.

Theorem iff_reflect : forall P b,
  (P <-> b = true) -> reflect P b.
Proof. destruct b; constructor; rewrite H; auto. Qed.

Theorem reflect_iff : forall P b,
  reflect P b -> (P <-> b = true).
Proof.
  destruct b; intros.
  - inversion H; split; auto.
  - inversion H; split; auto; discriminate.
Qed.

Lemma eqbP : forall n m, reflect (n = m) (n =? m).
Proof. intros. apply iff_reflect. rewrite Nat.eqb_eq. reflexivity. Qed.

Theorem filter_not_empty_In : forall n l,
  filter (fun x => n =? x) l <> [] <-> In n l.
Proof.
  induction l as [| m]; simpl; split; auto.
  - destruct (eqbP n m); auto.
    right. apply IHl. assumption.
  - intros []; subst.
    + rewrite Nat.eqb_refl. discriminate.
    + destruct (n =? m); try discriminate.
      rewrite IHl. assumption.
Qed.

Fixpoint count n l :=
match l with
| [] => 0
| m :: l => (if n =? m then 1 else 0) + count n l
end.

Example example_7 : forall n l, count n l = 0 <-> ~In n l.
Proof.
  induction l as [| m]; simpl; split; auto.
  - destruct (eqbP n m); try discriminate.
    rewrite IHl. intros H' []; auto.
  - destruct (eqbP n m) as [H | _]; intros H'.
    + exfalso. auto.
    + rewrite IHl. intros H. auto.
Qed.