证明内容列表的属性

Question

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'为1，那么项目（S n'）也为1？有没有比对n进行归纳更好的方法？

Answer 1

[如果查看定理，您会注意到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有一个轻松的方案来解决nat双重归纳法。

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.