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 `length`

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