Доказать свойства списков

Question

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

Require Import List.

Fixpoint list_gen lng acc :=
match lng with
0 => acc
| S lng_1 => list_gen (lng_1) (1::acc)
end.

Lemma lm0 : length(list_gen 0 nil) = 0.
intuition.
Qed.

Lemma lm1 : forall lng:nat, length(list_gen lng nil) = lng.
induction lng.
apply lm0.

Теперь после применения lm0 шаг индукции остался:

1 subgoal
lng : nat
IHlng : length (list_gen lng nil) = lng
______________________________________(1/1)
length (list_gen (S lng) nil) = S lng

Я надеялся, что доказательство этого шага будет выведено изкод list_gen, но это, скорее всего, ошибочная концепция.Как можно доказать эту подцель?

Answer 1

Я бы пошел с подходом Даниэля, однако немного более общим было бы написать спецификацию list_gen, например, используя нерекурсивную repeat функцию:

Require Import List Arith.
Import ListNotations.

Lemma list_gen_spec : forall lng acc, list_gen lng acc = repeat 1 lng ++ acc.
Proof.
  induction lng as [| lng IH]; intros xs; simpl; trivial.
  rewrite IH.
  now rewrite app_cons_middle, repeat_singleton, repeat_app, Nat.add_comm.
Qed.

, где мне пришлось добавить несколько лемм о взаимодействии repeat с некоторыми стандартными функциями списка.

Lemma repeat_singleton {A} (x : A) :
  [x] = repeat x 1.
Admitted.

Lemma repeat_app {A} (x : A) n m :
  repeat x n ++ repeat x m = repeat x (n + m).
Admitted.

Lemma app_cons {A} (x : A) xs :
  x :: xs = [x] ++ xs.
Admitted.  (* this is a convenience lemma for the next one *)

Lemma app_cons_middle {A} (y : A) xs ys :
  xs ++ y :: ys = (xs ++ [y]) ++ ys.
Admitted.

Я оставлю доказательства этих лемм в качестве упражнения.

После доказательства спецификации ваша лемма может быть доказана с помощью нескольких переписываний.

Lemma lm1 lng : length(list_gen lng nil) = lng.
Proof.
  now rewrite list_gen_spec, app_nil_r, repeat_length.
Qed.