Stuck on Software Foundations Pigeonhole Principle

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.
  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!

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

  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.

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

Theorem leSBoth : forall n m, S n <= S m <-> n <= m.
  - 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.