Докажите свойства списков относительно содержания - PullRequest
Новая
       81

Докажите свойства списков относительно содержания

0 голосов
/ 04 мая 2020

pattern_1 генерирует список, заполненный 1. Я хотел бы доказать, что есть 1 в определенных или всех позициях в списке. Я думаю, что я должен как-то ссылаться на внутреннюю часть функции генератора, но не знаю, как это сделать. Это то, что у меня есть: 

Require Import List.
Import ListNotations.

Fixpoint pattern_1 (lng:nat) : (list nat) :=
  match lng with
    0 => nil
    | S lng' => 1 :: (pattern_1 lng')
end.

Lemma item_nth0_is_1 : forall lng:nat, lng > 0 -> nth 0 (pattern_1 lng) 1 = 1.
Proof.
  intros.
  induction lng.
  trivial.
  intuition.
Qed.

Theorem item_nth_is_1 : forall lng n:nat, lng > n -> (nth n (pattern_1 lng) 1) = 1.
Proof.
  intros.
  induction n as [| n' IH_n'].
  apply item_nth0_is_1.
  apply H.

На данный момент состояние доказательства: 

1 subgoal
lng, n' : nat
H : lng > S n'
IH_n' : lng > n' -> nth n' (pattern_1 lng) 1 = 1
______________________________________(1/1)
nth (S n') (pattern_1 lng) 1 = 1

Как можно доказать, что если элемент n 'равен единице, то элемент ( S n ') тоже один? Есть ли лучший подход, чем индукция по lng?

1 Ответ

1 голос
/ 04 мая 2020

Если вы посмотрите на свою теорему, вы заметите, что nth зависит от «n» и «lng», однако, когда вы делаете индукцию только в «n», вы застрянете, как только lng будет зафиксирован, поэтому никогда не сможет быть уничтоженным / оцененным. Вы можете исправить это, просто обобщив «lng», поэтому, когда вы делаете индукцию по n, вы можете сказать, что теорема верна для всех «lng»: 

Theorem item_nth_is_1' : forall lng n:nat, lng > n -> (nth n (pattern_1 lng) 1) = 1.
Proof.
  intros.
  generalize dependent lng.
  induction n as [| n' IH_n'].
    - intros.
      destruct lng.
        + trivial.
        + trivial.
     - intros.
      destruct lng.
      trivial.
      exact (IH_n' lng (le_S_n _ _ H)).
Qed.

Конечно, вам, вероятно, понадобится больше деструктурирование / переписывание, чтобы решить цель. К счастью, у coq есть случайная схема для решения нат двойных индукций. 

Theorem item_nth_is_1 : forall lng n:nat, lng > n -> (nth n (pattern_1 lng) 1) = 1.
Proof.
  intros.
  elim/@nat_double_ind : n/lng H.
  intros; by destruct n.
  intros; inversion H.
  intros; apply : (H (le_S_n _ _ H0)).
Qed.
...