Stuck on Software Foundations Pigeonhole Principle

Using Coq
1

Hi everyone. I’m new to formal methods and have started with Software Foundations and I’m finally properly stuck at the pigeonhole principle proof in the Inductive Propositions chapter. IndProp: Inductively Defined Propositions

I’ve tried to find other proofs applying Excluded Middle as the book suggests, but I’ve only been able to find a couple proofs that do not use EM and everything else I can find is marked as todo or admitted. I have tried to follow this Stack Overflow answer, but I seem to be hitting a wall at the point that the answers suggests using in_split. coq - How should the excluded middle be used in the proof of the pigeonhole principle? - Stack Overflow

I will share some of my work here. I have proven every theorem up to this point, including in_split.

Inductive repeats {X:Type} : list X -> Prop :=
  | repeats_x x xs : In x xs -> repeats (x::xs)
  | repeats_xs x xs : repeats xs -> repeats (x::xs).

Theorem pigeonhole_principle: excluded_middle ->
  forall (X:Type) (l1  l2:list X),
  (forall x, In x l1 -> In x l2) ->
  length l2 < length l1 ->
  repeats l1.
Proof.
  intros EM X l1. induction l1 as [|x l1' IHl1'].
  - simpl. intros. inversion H0.
  - simpl. destruct l2.
    + intros. simpl in H. exfalso. apply (H x). left. reflexivity.
    + destruct (EM (In x l1')).
      * left. apply H.
      * (* keep getting stuck here, I have included my current attempt but this is not my best attempt *)
        intros. right. apply (IHl1' (x0::l2)). intros.
           destruct (in_split _ x1 (x0::l2)) as [la [lb H3]].
           ++ apply (H0 x1). right. apply H2.
           ++ apply (H0 x1). right. apply H2.
           ++

And the proof state up to the comment where I’ve tried different ideas:

EM: excluded_middle
X: Type
x: X
l1': list X
IHl1': forall l2 : list X,
        (forall x : X, In x l1' -> In x l2) ->
        length l2 < length l1' -> repeats l1'
x0: X
l2: list X
H: ~ In x l1'

And the proof state at the end:

EM: excluded_middle
X: Type
x: X
l1': list X
IHl1': forall l2 : list X, (forall x : X, In x l1' -> In x l2) -> length l2 < length l1' -> repeats l1'
x0: X
l2: list X
H: ~ In x l1'
H0: forall x1 : X, x = x1 \/ In x1 l1' -> In x1 (x0 :: l2)
H1: length (x0 :: l2) < S (length l1')

I have tried multiple orders and variations of destructing in_split and EM (In x l1'), but have been unable to get somewhere that I can get to the end, usually with something that seems like an illogical statement about the lengths of l2 and l1'. I am trying to follow the tactics that are taught in the book up to this point, but I would still appreciate any solutions using more advanced tactics. Is my approach up to the comment generally correct? I would appreciate any guidance, I’ve been totally stuck for a couple hours. Thank you!

2

In a brief moment of pure luck I figured it out.

Proof.
  intros EM X l1. induction l1 as [|x l1' IHl1'].
  - (* l1 = [] *)
    simpl. intros. inversion H0.
  - (* l1 = x :: l1' *)
    simpl. intros l2 HIn Hlen. destruct l2 as [|y l2'].
    + (* l2 = [] *)
      intros. simpl in Hlen. exfalso. apply (HIn x). left. reflexivity.
    + (* l2 = y :: l2' *)
      destruct (EM (In x l1')) as [EmInT | EmInF].
      * (* In x l1' *)
        apply repeats_x. apply EmInT.
      * (* ~ In x l1' *) 
        destruct (in_split _ x (y::l2')) as [la [lb Eyl2]].
        -- (* must prove [In x (y :: l2')] to get equation below *) 
           apply (HIn x). left. reflexivity.
        -- (* Eyl2: y :: l2' = la ++ x :: lb *)
           apply repeats_xs. apply (IHl1' (la++lb)).
           ++ (* must prove [In x l1' -> In x l2] where [l2 = la ++ lb] *)
              intros z HInz. rewrite Eyl2 in HIn.
              (* assertion is important below *)
              assert (Neqx : x <> z).
              { unfold not in HInz. unfold not. intros Exz. rewrite Exz in EmInF.
                apply EmInF. apply HInz. }
              (* need to show this implication when [x <> z] so we can apply later *)
              assert (In_split_Neqx: In z (la ++ x :: lb) -> In z (la ++ lb)).
              { intros In_unsplit. apply In_app_iff. apply In_app_iff in In_unsplit.
                destruct In_unsplit as [Iu | Iu].
                left. apply Iu. right. simpl in Iu. destruct Iu as [Eqx | In_lb].
                exfalso. apply Neqx, Eqx.
                apply In_lb. }
              apply In_split_Neqx. apply HIn. right. apply HInz.
           ++ (* must prove [length l2 < length l1'] where [l2 = la ++ lb] *)
              rewrite Eyl2 in Hlen.
              rewrite app_length in Hlen. simpl in Hlen. rewrite <- plus_n_Sm in Hlen.
              apply -> leSBoth in Hlen. unfold lt. rewrite app_length. apply Hlen.
Qed.

leSBoth is a theorem I wrote that has been helpful throughout the chapter.

Theorem leSBoth : forall n m, S n <= S m <-> n <= m.
Proof.
  split.
  - intros. inversion H. apply le_n.
    rewrite <- plus_1_l in H1. apply plus_le, proj2 in H1. apply H1.
  - intros. induction H. apply le_n. apply le_S. apply IHle.
Qed.