переименование части гипотезы в Coq

Question

После уничтожения n в моем доказательстве я застрял в следующем:

1 subgoal
n : nat
X : Type
h : X
t : list X
n' : nat
E : n = S n'
H' : length t = n'
IHl : length t = n -> nth_error t n = None
______________________________________(1/1)
nth_error t n' = None

Я хочу переписать, используя IHl, но это невозможно.Как мне составить IHl и H ', чтобы иметь смысл и доказать эту теорему?

Answer 1

Я просто пытаюсь уточнить ответ @Arthur.

Мне удалось воспроизвести вашу цель с помощью следующего сценария:

Require Import List.

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

и я согласен, что эта цель не может быть доказана. Теперь, если вместо этого вы начнете доказательство со следующего текста (необходимо заменить строки Proof и induction), это будет доказуемо (я проверял).

Proof.
revert n.
induction l as [ | h t IHl]; intros n.

Разница в том, что теперь у индукционной гипотезы есть следующее утверждение.

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

Что случилось? В первом (ошибочном) варианте вы пытаетесь доказать утверждение для всех списков, длина которых равна точному n, потому что n фиксируется до того, как вы начнете доказательство по индукции. Во втором (правильном) варианте вы пытаетесь доказать утверждение для всех списков l, и этот оператор принимает любые n до тех пор, пока length l = n.

В первом варианте n является фиксированным, и равенство length l = n ограничивает l тем, что имеет длину точно n. Во втором случае сначала выбирается l, а n не является фиксированным, но равенство length l = n ограничивает n в соответствии с длиной l.

Это называется "загрузкой индукции", потому что оператор forall n, length l = n -> nth_error l n = None сильнее (он загружен), чем оператор, который вы пытаетесь доказать в первом варианте (только для одного конкретного n), но, как это ни удивительно, легче доказать.

Answer 2

Вы не можете, потому что ваша индуктивная гипотеза недостаточно общая. Вот утверждение, которое должно быть легче доказать:

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