如何用coq来证明这第n题和第n题？

Question

Theorem fiset_ref_fact : forall (r r' n : nat) (f f' D g g' h h' : list nat) (b b' : bool),
  length f = n /\ n > 0 /\ r < n /\
  h = firstn r f /\ 
  h' = (app h ((nth r f 0)::nil)) /\ r' = r + 1 -> h' = firstn r' f.

我正在尝试使用感应，但我不知道要继续...

firstorder.
  induction r eqn:E. destruct f eqn:E0.  simpl in H. symmetry in H. rewrite H in H0. inversion H0. 
  simpl in H2. rewrite H2 in H4. simpl in H4. rewrite H5. simpl. apply H4. 
  destruct f eqn:E0. simpl in H. symmetry in H. rewrite H in H0. inversion H0.

Answer 1

这不是传统的“答案”，而是一些（可能是主动提供的）关于如何按照机器人的建议澄清问题的帮助，因为您需要能够提出好问题，然后才能期望得到好的答案，对于新用户来说，如何提出好问题可能并不明显。

我们更喜欢的问题标准是“最小工作示例”（MWE）的概念，这意味着一个尽可能小的示例，读者可以将其直接插入到 Coq 文件中以调查您的问题的内容。在这种情况下，您的定理不是 MWE，因为术语 firstn 未定义（从而违反了 MWE 的“工作”要求）。您需要导入适当的库：

From Coq Require Import List.
Theorem fiset_ref_fact : forall (r r' n : nat) (f f' D g g' h h' : list nat) (b b' : bool),
  length f = n /\ n > 0 /\ r < n /\
  h = firstn r f /\ 
  h' = (app h ((nth r f 0)::nil)) /\ r' = r + 1 -> h' = firstn r' f.

应用此更正后，您的示例现在可以运行（它是一个“工作示例”），但它仍然不是最小的。您的定理包含许多变量 (

f' D g g' b b'

)，这些变量在定理陈述中的任何地方都没有使用。删除这些变量，我们现在得到

From Coq Require Import List.
Theorem fiset_ref_fact : forall (r r' n : nat) (f h h' : list nat),
  length f = n /\ n > 0 /\ r < n /\
  h = firstn r f /\ 
  h' = (app h ((nth r f 0)::nil)) /\ r' = r + 1 -> h' = firstn r' f.

现在有资格成为 MWE。

我建议进行进一步的修改。在 Coq 和其他证明助手中，构造

P ∧ Q → R.

并不是惯用的。相反，我们更喜欢

P → Q → R.

，它在逻辑上等价于

P ∧ Q → R.

，但在 Coq 中应用起来更容易，因为您不需要构造或破坏连词来应用

P → Q → R.

形式。应用这个建议，你的定理陈述现在变成了

From Coq Require Import List.
Theorem fiset_ref_fact : forall (r r' n : nat) (f h h' : list nat),
  length f = n -> n > 0 -> r < n ->
  h = firstn r f ->
    h' = (app h ((nth r f 0)::nil)) -> r' = r + 1 -> h' = firstn r' f.

现在您已经准备好解决实际问题了。