两件事：

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')之类，然后通过直接归纳证明那。然后，您希望得到的结果就是该结果的推论。

您可以在James Wilcox's blog post中了解有关归纳归纳假设的更多信息，该归纳假设包括8个练习，在这样做时难度越来越大。

现在，请考虑这两点，以证明您的引理。 提示：在通过直接归纳证明关于sumoneseq的更一般的陈述时，您可能还会发现为sumones的某些属性提取合适的引理很有帮助。 >

如果您再次尝试无济于事，则会在水平线下方提供完整的解决方案（剧透警报！）。

这里是完整的解决方案。如您所见，在主要归纳法的基础上，还需要进行大量案例分析（可能是由于您在sumoneseq中进行了优化，从0中丢弃了ln s）以及这些案例中有许多实际上非常相似且重复。我可能可以通过一些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.