如何用Coq证明关于firstn与nth的定理fiset_ref_fact？

待证明的定理 #

需证明的Coq定理如下：

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.

后续证明思路与优化建议 #

这个定理不需要复杂的归纳操作，直接利用firstn和nth的基础性质即可完成证明：

• 首先，由假设r' = r + 1，目标可转化为证明app (firstn r f) [nth r f 0] = firstn (r+1) f
• 可以直接调用Coq标准库中关于firstn的引理（比如firstn_S），或者对r做简单归纳：
  1. 基例（r=0）：firstn 0 f = []，nth 0 f 0是f的首元素，firstn 1 f恰好是[f的首元素]，等式显然成立
  2. 归纳步（r=S k）：假设对k结论成立，结合firstn (S m) f = hd f :: firstn m (tl f)的定义，以及nth (S k) f 0 = nth k (tl f) 0的性质，就能推导得出结论

另外，你当前的证明步骤可以优化：在firstorder之后，先把合取式假设拆分为单独的前提，比如执行以下命令：

destruct H as [H_len [H_n_pos [H_r_lt [H_h_firstn [H_h'_app H_r'_eq]]]]].

这样后续引用假设时，能通过有意义的名称（比如H_len表示length f = n）避免混淆自动生成的H0、H2等编号，让证明过程更清晰。

内容的提问来源于stack exchange，提问作者io ieong