Renaming part of hypothesis in Coq

Link:: https://stackoverflow.com/q/52350119

Display all goals and responses

Question

After destructing n in my proof, I am stuck at the following:

1 subgoal

  n : nat
  X : Type
  h : nat
  t : list nat
  IHl : length t = n -> nth_error t n = None
  n' : nat
  E : n = S n'
  H' : length t = n'
  ============================
  nth_error t n' = None

I want to rewrite using IHl, but that is not possible. How do I compose IHl and H' to make sense and prove this theorem?

Answer (Yves)

I am just trying to elaborate on @Arthur answer.

I was able to reproduce your goal with the following script:

Require Import List.

Lemma toto (n : nat) (X : Type) (l : list nat) :
  length l = n -> nth_error l n = None.n: nat
X: Type
l: list nat
length l = n -> nth_error l n = None
Proof.n: nat
X: Type
l: list nat
length l = n -> nth_error l n = None
  induction l as [ | h t IHl].n: nat
X: Type
length nil = n -> nth_error nil n = None
n: nat
X: Type
h: nat
t: list nat
IHl: length t = n -> nth_error t n = None
length (h :: t) = n -> nth_error (h :: t) n = None
  -n: nat
X: Type
length nil = n -> nth_error nil n = None case_eq n.n: nat
X: Type
n = 0 -> length nil = 0 -> nth_error nil 0 = None
n: nat
X: Type
forall n0 : nat,
n = S n0 ->
length nil = S n0 -> nth_error nil (S n0) = None
    +n: nat
X: Type
n = 0 -> length nil = 0 -> nth_error nil 0 = None simpl.n: nat
X: Type
n = 0 -> 0 = 0 -> None = None auto.
    +n: nat
X: Type
forall n0 : nat,
n = S n0 ->
length nil = S n0 -> nth_error nil (S n0) = None simpl.n: nat
X: Type
forall n0 : nat, n = S n0 -> 0 = S n0 -> None = None discriminate.
  -n: nat
X: Type
h: nat
t: list nat
IHl: length t = n -> nth_error t n = None
length (h :: t) = n -> nth_error (h :: t) n = None case_eq n.n: nat
X: Type
h: nat
t: list nat
IHl: length t = n -> nth_error t n = None
n = 0 ->
length (h :: t) = 0 -> nth_error (h :: t) 0 = None
n: nat
X: Type
h: nat
t: list nat
IHl: length t = n -> nth_error t n = None
forall n0 : nat,
n = S n0 ->
length (h :: t) = S n0 ->
nth_error (h :: t) (S n0) = None
    +n: nat
X: Type
h: nat
t: list nat
IHl: length t = n -> nth_error t n = None
n = 0 ->
length (h :: t) = 0 -> nth_error (h :: t) 0 = None simpl.n: nat
X: Type
h: nat
t: list nat
IHl: length t = n -> nth_error t n = None
n = 0 -> S (length t) = 0 -> Some h = None discriminate.
    +n: nat
X: Type
h: nat
t: list nat
IHl: length t = n -> nth_error t n = None
forall n0 : nat,
n = S n0 ->
length (h :: t) = S n0 ->
nth_error (h :: t) (S n0) = None intros n' E.n: nat
X: Type
h: nat
t: list nat
IHl: length t = n -> nth_error t n = None
n': nat
E: n = S n'
length (h :: t) = S n' ->
nth_error (h :: t) (S n') = None simpl.n: nat
X: Type
h: nat
t: list nat
IHl: length t = n -> nth_error t n = None
n': nat
E: n = S n'
S (length t) = S n' -> nth_error t n' = None
      intros E'.n: nat
X: Type
h: nat
t: list nat
IHl: length t = n -> nth_error t n = None
n': nat
E: n = S n'
E': S (length t) = S n'
nth_error t n' = None injection E'.n: nat
X: Type
h: nat
t: list nat
IHl: length t = n -> nth_error t n = None
n': nat
E: n = S n'
E': S (length t) = S n'
length t = n' -> nth_error t n' = None clear E'.n: nat
X: Type
h: nat
t: list nat
IHl: length t = n -> nth_error t n = None
n': nat
E: n = S n'
length t = n' -> nth_error t n' = None intros H'.n: nat
X: Type
h: nat
t: list nat
IHl: length t = n -> nth_error t n = None
n': nat
E: n = S n'
H': length t = n'
nth_error t n' = None

and I agree that this goal cannot be proved. Now, if you instead start your proof with the following text (the Proof and induction lines have to be replaced), it will be provable (I checked).

      Restart.n: nat
X: Type
l: list nat
length l = n -> nth_error l n = None
      revert n.X: Type
l: list nat
forall n : nat, length l = n -> nth_error l n = None
      induction l as [ | h t IHl]; intros n.X: Type
n: nat
length nil = n -> nth_error nil n = None
X: Type
h: nat
t: list nat
IHl: forall n : nat, length t = n -> nth_error t n = None
n: nat
length (h :: t) = n -> nth_error (h :: t) n = None

The difference is that the induction hypothesis now has the following statement.

IHl
     : forall n : nat,
       length t = n -> nth_error t n = None

What happened? In the first (faulty) variant, you attempt to prove a statement for all lists whose length is equal to a precise n, because n is fixed before you start the proof by induction. In the second (correct) variant, you attempt to prove a statement for all lists l, and this statement accepts any n as long as length l = n.

In the first variant, n is fixed and the equality length l = n restricts l to be among those that have length precisely n. In the second case, l is chosen first, and n is not fixed, but the equality length l = n restricts n to follow the length of l.

This is called "loading the induction" because the statement forall n, length l = n -> nth_error l n = None is stronger (it is loaded) than the statement that you attempt to prove in the first variant (just for one specific n), but surprisingly it is easier to prove.

Answer (Arthur Azevedo De Amorim)

You cannot, because your induction hypothesis is not general enough. Here is a statement that should be easier to prove:

forall (X : Type) (t : list X), nth_error t (length t) = None