Я хочу доказать некоторые свойства списка, но я застрял в индукции - PullRequest
Новая
       10

Я хочу доказать некоторые свойства списка, но я застрял в индукции

0 голосов
/ 01 июля 2019

Я попробовал следующие доказательства, 

Require Import List Omega.
Import ListNotations.
Variable X : Type.

Lemma length_n_nth_app_error_same : forall (n:nat) (x:X) (l:list X),
n <= length l -> 0 < n -> nth_error l n = nth_error (l ++ [x]) n .
Proof.
  intros.
  induction l eqn:eqHl.
  - unfold length in H. omega.
  -

, но я застрял, потому что у меня есть только 

1 subgoal
n : nat
x : X
l : list X
a : X
l0 : list X
eqHl : l = a :: l0
H : n <= length (a :: l0)
H0 : 0 < n
IHl0 : l = l0 ->
       n <= length l0 ->
       nth_error l0 n = nth_error (l0 ++ [x]) n
______________________________________(1/1)
nth_error (a :: l0) n = nth_error ((a :: l0) ++ [x]) n

Я встречал некоторые подобные случаи и для других доказательств насписки.Я не знаю, была бы полезна обычная индукция.

Как мне доказать это?Должен ли я использовать обобщение?

1 Ответ

1 голос
/ 01 июля 2019

Ваша теорема неверна. Возможно, ваше понимание nth_error неверно.

В частности, когда n = length l, nth_error l n возвращает None, а nth_error (l ++ [x]) n возвращает Some x. 

Require Import List Omega.
Import ListNotations.

Lemma length_n_nth_app_error_not_always_same :
  (forall (n:nat) (X:Type) (x:X) (l:list X),
  n <= length l -> 0 < n -> nth_error l n = nth_error (l ++ [x]) n)
  -> False.
Proof.
  intros.
  assert (1 <= 1) by omega. assert (0 < 1) by omega.
  specialize (H 1 nat 2 [1] H0 H1). simpl in H. inversion H. Qed.

С другой стороны, доказать аналогичную теорему с фиксированным неравенством легко: 

Lemma length_n_nth_app_error_same : forall (n:nat) (X:Type) (x:X) (l:list X),
n < length l -> nth_error l n = nth_error (l ++ [x]) n .
Proof.
  induction n; intros.
  - simpl. destruct l; simpl in *.
    + omega.
    + reflexivity.
  - simpl. destruct l; simpl in *.
    + omega.
    + apply IHn. omega. Qed.

Обратите внимание, что я использовал induction n вместо induction l. Это в основном потому, что nth_error делает рекурсивные вызовы при уменьшении n.

Кроме того, если вы почувствовали, что гипотеза об индукции недостаточно общая, возможно, это из-за того, что ваш порядок intros и induction был неверным. Основное правило - начать доказательство с induction, а затем intros переменных. Если этого по-прежнему недостаточно, вы можете revert dependent все переменные, кроме той, которая выполняет индукцию, а затем induction x; intros.

...