Proving increasing iota in Coq

Question

I am stuck on a goal.

Assume we have the following definition:

Fixpoint iota (n : nat) : list nat :=
  match n with
  | 0   => []
  | S k => iota k ++ [k]
  end.

I use these two lemmas, proofs omitted:

Axiom app_split : forall A x (l l2 : list A),
    In x (l ++ l2) -> not (In x l2) -> In x l.
Axiom s_inj : forall n, ~(n = S n).

And we want to prove:

Theorem t1 : forall n, In n (iota n) -> False.
forall n : nat, In n (iota n) -> False

So far, I have managed to the following:

Theorem t1 : forall n, In n (iota n) -> False.
forall n : nat, In n (iota n) -> False
Proof.
forall n : nat, In n (iota n) -> False
  intros.
n: nat
H: In n (iota n)
False induction n.
H: In 0 (iota 0)
False
n: nat
H: In (S n) (iota (S n))
IHn: In n (iota n) -> False
False
  -
H: In 0 (iota 0)
False cbn in H.
H: False
False contradiction.
  -
n: nat
H: In (S n) (iota (S n))
IHn: In n (iota n) -> False
False cbn in H.
n: nat
H: In (S n) (iota n ++ [n])
IHn: In n (iota n) -> False
False apply app_split in H.
n: nat
H: In (S n) (iota n)
IHn: In n (iota n) -> False
False
n: nat
H: In (S n) (iota n ++ [n])
IHn: In n (iota n) -> False
~ In (S n) [n]
    2:{
n: nat
H: In (S n) (iota n ++ [n])
IHn: In n (iota n) -> False
~ In (S n) [n] unfold not.
n: nat
H: In (S n) (iota n ++ [n])
IHn: In n (iota n) -> False
In (S n) [n] -> False intros.
n: nat
H: In (S n) (iota n ++ [n])
IHn: In n (iota n) -> False
H0: In (S n) [n]
False
        unfold In in H0.
n: nat
H: In (S n) (iota n ++ [n])
IHn: In n (iota n) -> False
H0: n = S n \/ False
False destruct H0.
n: nat
H: In (S n) (iota n ++ [n])
IHn: In n (iota n) -> False
H0: n = S n
False
n: nat
H: In (S n) (iota n ++ [n])
IHn: In n (iota n) -> False
H0: False
False
        +
n: nat
H: In (S n) (iota n ++ [n])
IHn: In n (iota n) -> False
H0: n = S n
False assert (~(n = S n)) by now apply s_inj.
n: nat
H: In (S n) (iota n ++ [n])
IHn: In n (iota n) -> False
H0: n = S n
H1: n <> S n
False contradiction.
        +
n: nat
H: In (S n) (iota n ++ [n])
IHn: In n (iota n) -> False
H0: False
False apply H0. }
n: nat
H: In (S n) (iota n)
IHn: In n (iota n) -> False
False
    1:{
n: nat
H: In (S n) (iota n)
IHn: In n (iota n) -> False
False apply IHn.
n: nat
H: In (S n) (iota n)
IHn: In n (iota n) -> False
In n (iota n)
Abort.

However, I am completely stuck, I need to somehow show that: In n (iota n) assuming In (S n) (iota n).

Answer

As you've observed the fact that the n in In n and the one in iota n are in lockstep in your statement makes the induction hypothesis hard to invoke (if not completely useless).

The trick here is to prove a more general statement than the one you are actually interested in which breaks this dependency between the two ns. I would suggest:

Theorem t : forall n k, n <= k -> In k (iota n) -> False.
forall n k : nat, n <= k -> In k (iota n) -> False
Proof.
forall n k : nat, n <= k -> In k (iota n) -> False
  intro n; induction n; intros k nlek kin.
k: nat
nlek: 0 <= k
kin: In k (iota 0)
False
n: nat
IHn: forall k : nat, n <= k -> In k (iota n) -> False
k: nat
nlek: S n <= k
kin: In k (iota (S n))
False
  -
k: nat
nlek: 0 <= k
kin: In k (iota 0)
False cbn in kin; contradiction.
  -
n: nat
IHn: forall k : nat, n <= k -> In k (iota n) -> False
k: nat
nlek: S n <= k
kin: In k (iota (S n))
False cbn in kin; apply app_split in kin.
n: nat
IHn: forall k : nat, n <= k -> In k (iota n) -> False
k: nat
nlek: S n <= k
kin: In k (iota n)
False
n: nat
IHn: forall k : nat, n <= k -> In k (iota n) -> False
k: nat
nlek: S n <= k
kin: In k (iota n ++ [n])
~ In k [n]
    +
n: nat
IHn: forall k : nat, n <= k -> In k (iota n) -> False
k: nat
nlek: S n <= k
kin: In k (iota n)
False eapply IHn with (k := k).
n: nat
IHn: forall k : nat, n <= k -> In k (iota n) -> False
k: nat
nlek: S n <= k
kin: In k (iota n)
n <= k
n: nat
IHn: forall k : nat, n <= k -> In k (iota n) -> False
k: nat
nlek: S n <= k
kin: In k (iota n)
In k (iota n)
      *
n: nat
IHn: forall k : nat, n <= k -> In k (iota n) -> False
k: nat
nlek: S n <= k
kin: In k (iota n)
n <= k transitivity (S n); eauto.
      *
n: nat
IHn: forall k : nat, n <= k -> In k (iota n) -> False
k: nat
nlek: S n <= k
kin: In k (iota n)
In k (iota n) assumption.
    +
n: nat
IHn: forall k : nat, n <= k -> In k (iota n) -> False
k: nat
nlek: S n <= k
kin: In k (iota n ++ [n])
~ In k [n] inversion 1; subst.
k: nat
H: In k [k]
kin: In k (iota k ++ [k])
nlek: S k <= k
IHn: forall k0 : nat,
k <= k0 -> In k0 (iota k) -> False
False
n: nat
IHn: forall k : nat, n <= k -> In k (iota n) -> False
k: nat
nlek: S n <= k
kin: In k (iota n ++ [n])
H: In k [n]
H0: In k []
False
      *
k: nat
H: In k [k]
kin: In k (iota k ++ [k])
nlek: S k <= k
IHn: forall k0 : nat,
k <= k0 -> In k0 (iota k) -> False
False apply (Nat.nle_succ_diag_l _ nlek).
      *
n: nat
IHn: forall k : nat, n <= k -> In k (iota n) -> False
k: nat
nlek: S n <= k
kin: In k (iota n ++ [n])
H: In k [n]
H0: In k []
False contradiction.
Qed.

from which you can derive t1 as a corollary:

Corollary t1 : forall n, In n (iota n) -> False.
forall n : nat, In n (iota n) -> False
  intro n; apply (t n n); reflexivity.
Qed.

If you want to peek at the proof of t, you can have a look at this self-contained gist

Q: Interesting - how does one get the intuition for when something's impossible to prove with its current formulation - is it that either some of the assumptions or the inductive hypothesis would be directly (or indirectly) in contradiction with the conclusion? Or is there a notion of "not sufficient / strong" enough inductive hypothesis? How can one tell? (This is obvious once you show me, but figuring this out myself...)

A: Experience mostly. But whenever two things are in lockstep or one value is fixed to be a constant and that prevents you from using the induction hypothesis, that's a strong smell that you may want to look for a more general statement. This blog post sets up a number of exercises where you have to generalize the induction hypothesis to make it work. You may want to look into it.