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

Две вещи:

1. При доказательстве свойства некоторой функции f с помощью прямой индукции выберите параметр, для которого f структурно рекурсивна. Так что в вашем примере с sumoneseq по lb вместо ln поскольку sumoneseq структурно рекурсивен по sumoneseq
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 отбрасывания 0 с из 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.