Завершение леммы о списке нац

Две вещи:

1. При доказательстве свойства некоторой функции f с помощью прямой индукции выберите параметр, для которого f является структурно рекурсивным. Итак, в вашем примере с участием sumoneseq индуктируйте lb вместо ln, поскольку sumoneseq структурно рекурсивен на lb.
2. Доказательство свойства некоторой функции f, в которой один или несколько ее аргументов зафиксированы на определенных значениях (например, sumoneseq со вторым аргументом []) с помощью прямой индукции почти гарантированно не удастся, поскольку значение этого аргумента меняется между рекурсивными вызовами f , что означает, что вы не сможете применить гипотезу индукции в своем индуктивном случае. В этом случае вам необходимо вручную обобщить гипотезу индукции, найдя более общее свойство, на котором выполняется f, причем каждый из его аргументов является достаточно общим. Например, вместо того, чтобы доказывать forall lb ln, sumones (sumoneseq lb ln) = sumones ln + sumones (sumoneseq lb []) непосредственно по индукции, попробуйте обобщить его до чего-то вроде forall lb ln ln', sumones (sumoneseq lb (ln ++ ln')) = sumones ln + sumones (sumoneseq lb ln') и докажите это с помощью прямой индукции. Ваш желаемый результат является следствием этого более общего результата.

Вы можете узнать больше об обобщении гипотезы индукции в сообщении в блоге Джеймса Уилкокса, которое щедро включает 8 упражнений с возрастающей сложностью на делаю именно это.

Теперь попытайтесь доказать свою лемму с учетом этих двух моментов. Подсказка: при доказательстве вашего более общего утверждения о sumoneseq с помощью прямой индукции вы также можете найти подходящую лемму об определенном свойстве sumones.

Если вы попытались снова, но безуспешно, полное решение приведено под горизонтальной линейкой (предупреждение о спойлере!).

Вот полное решение. Как вы, вероятно, видите, требуется много анализа случаев помимо основной индукции (вероятно, из-за вашей оптимизации в sumoneseq отбрасывания 0s из ln), и рассуждения для многих из этих случаев на самом деле очень похожи и повторяются. Я, вероятно, мог бы еще больше сократить сценарий проверки, добавив немного Ltac программирования в поисках похожих шаблонов в различных случаях, но я не стал этим заниматься, так как просто сразу взломал его.

From Coq Require Import List Lia.
Import ListNotations.

Fixpoint sumoneseq (lb: list bool) (ln: list nat)
  : list nat :=
  match lb, ln with
  | nil, 0::tl'' => tl''
  | nil, _ => ln
  | true::tl', nil => sumoneseq tl' (1::nil)
  | true::tl', h::tl'' => sumoneseq tl' (S h::tl'')
  | false::tl', 0::tl'' => sumoneseq tl' ln
  | false::tl', _ => sumoneseq tl' (0::ln)
  end.

Fixpoint sumones (ln: list nat) : nat :=
  match ln with
  | nil => 0
  | r::tl => r + (sumones tl)
  end.

Lemma sumones_app_plus_distr : forall l l',
  sumones (l ++ l') = sumones l + sumones l'.
Proof.
  induction l; simpl; intros; auto.
  rewrite IHl; lia.
Qed.

Lemma sumones_l' : forall lb ln ln',
  sumones (sumoneseq lb (ln ++ ln')) =
  sumones ln + sumones (sumoneseq lb ln').
Proof.
  induction lb; simpl; intros.
  - destruct ln, ln'; simpl; auto.
    + destruct n; rewrite app_nil_r; simpl; auto.
    + destruct n, n0; simpl; rewrite sumones_app_plus_distr;
        simpl; lia.
  - destruct a, ln, ln'; simpl; auto.
    + replace (S n :: ln ++ []) with ((S n :: ln) ++ [])
        by reflexivity.
      replace [1] with ([1] ++ []) by now rewrite app_nil_r.
      repeat rewrite IHlb; simpl; lia.
    + replace (S n :: ln ++ n0 :: ln')
        with ((S n :: ln ++ [n0]) ++ ln')
        by (simpl; now rewrite <- app_assoc).
      replace (S n0 :: ln') with ([S n0] ++ ln')
        by reflexivity.
      repeat rewrite IHlb.
      replace (S n :: ln ++ [n0])
        with ((S n :: ln) ++ [n0])
        by reflexivity.
      repeat rewrite sumones_app_plus_distr; simpl; lia.
    + destruct n.
      * replace (0 :: ln ++ []) with ((0 :: ln) ++ [])
          by reflexivity.
        replace [0] with ([0] ++ [])
          by now rewrite app_nil_r.
        repeat rewrite IHlb; simpl; lia.
      * replace (0 :: S n :: ln ++ [])
          with ((0 :: S n :: ln) ++ []) by reflexivity.
        replace [0] with ([0] ++ [])
          by now rewrite app_nil_r.
        repeat rewrite IHlb; simpl; lia.
    + destruct n, n0.
      * replace (0 :: ln ++ 0 :: ln')
          with ((0 :: ln ++ [0]) ++ ln')
          by (simpl; now rewrite <- app_assoc).
        replace (0 :: ln') with ([0] ++ ln') by reflexivity.
        repeat rewrite IHlb.
        repeat (repeat rewrite sumones_app_plus_distr;
          simpl); lia.
      * replace (0 :: ln ++ S n0 :: ln')
          with ((0 :: ln ++ [S n0]) ++ ln')
          by (simpl; now rewrite <- app_assoc).
        replace (0 :: S n0 :: ln') with ([0; S n0] ++ ln')
          by reflexivity.
        repeat rewrite IHlb.
        repeat (repeat rewrite sumones_app_plus_distr;
          simpl); lia.
      * replace (0 :: S n :: ln ++ 0 :: ln')
          with ((0 :: S n :: ln ++ [0]) ++ ln')
          by (simpl; now rewrite <- app_assoc).
        replace (0 :: ln') with ([0] ++ ln')
          by reflexivity.
        repeat rewrite IHlb.
        repeat (repeat rewrite sumones_app_plus_distr;
          simpl); lia.
      * replace (0 :: S n :: ln ++ S n0 :: ln')
          with ((0 :: S n :: ln ++ [S n0]) ++ ln')
          by (simpl; now rewrite <- app_assoc).
        replace (0 :: S n0 :: ln') with ([0; S n0] ++ ln')
          by reflexivity.
        repeat rewrite IHlb.
        repeat (repeat rewrite sumones_app_plus_distr;
          simpl); lia.
Qed.

Lemma sumones_l: forall lb ln,
  sumones (sumoneseq lb ln) =
  sumones ln + sumones (sumoneseq lb []).
Proof.
  intros; replace (sumoneseq lb ln)
    with (sumoneseq lb (ln ++ []))
    by (now rewrite app_nil_r); apply sumones_l'.
Qed.