如何在 coq 中使用大小写匹配和变量等价

Question

我正在尝试使用以下定理

Theorem nat_rect_1_2: forall (P:nat->Type), (P O -> P 1 
  -> (forall n:nat, P n -> P (S n) -> P (S (S n))) -> forall n:nat, P n ).
Print nat_rect.
exact (fun (P : nat -> Type) (f0 : P 0) (f1 : P 1)
  (ff : forall n : nat, P n -> P(S n) -> P (S(S n))) =>
  fix F (n : nat) : P n :=
    match n as n0 return (P n0) with
    | 0 => f0
    | S n' =>  match n' with
       | 0 => f1
       | S n'' => ff n'' (F n'') (F n')
       end
    end).
Qed.

问题是 F n' 的类型是 (P n') 并且在那个位置，但它应该是 P(S n'')。但显然，S n'' 与 n' 相同，因为我们处于那种情况，但 Coq 无法检测到这一点。我该如何解决这个问题？

Answer 1

我建议使用策略来证明引理，你是故意手写证明项吗？

无论如何，我认为您需要在 "convoy pattern" 方面帮助 Coq，以便它可以统一这两个术语。阅读有关此技术的更多信息 here。

使用策略编辑证明：如果我没记错的话，这个证明有一个"trick"。你不能直接用 induction 来证明它，因为归纳一次 "one" 步，你需要两个。诀窍是先证明：

Theorem nat_rect_1_2_gen: forall (P:nat->Type), (P O -> P 1 -> 
  (forall n:nat, P n -> P (S n) -> P (S (S n))) -> forall n:nat, (P n) *(P (S n))).

通过对n的归纳，然后用这个结果来证明你原来的目标。证明将从以下内容开始：

intros P hP0 hP1 hPS. (* introducing basic assumptions *)
induction n as [ | h [hn hSn]]. (* induction on n *)

并且您应该能够想出如何证明每个子目标。如果您需要更多帮助，我会提供更多详细信息。

如何在 coq 中使用大小写匹配和变量等价

How to use matched case and variable equivalence in coq

coq