重写策略无法在模式匹配中找到术语出现

Question

在Coq中,我遇到了rewrite在以下情况下应用策略的问题:

Section Test.

Hypothesis s t        : nat -> nat.
Hypothesis s_ext_eq_t : forall (x : nat), s x = t x.

Definition dummy_s : nat -> nat :=
  fun n => match n with
         | O => 42
         | S np => s np
       end.

Definition dummy_t : nat -> nat :=
  fun n => match n with
         | O => 42
         | S np => t np
       end.

Goal forall (n : nat), dummy_s n = dummy_t n.
Proof.
  intro n. unfold dummy_s. unfold dummy_t.

在那个阶段,当地背景和当前目标如下:

1 subgoals, subgoal 1 (ID 6)

s : nat -> nat
t : nat -> nat
s_ext_eq_t : forall x : nat, s x = t x
n : nat
============================
match n with
| 0 => 42
| S np => s np
end = match n with
      | 0 => 42
      | S np => t np
      end

现在应该可以应用rewrite策略来替换s np目标中的出现t np,从而可以使用来解决目标reflexivity.然而,

rewrite s_ext_eq_t.

给

Toplevel input, characters 0-18:
Error: Found no subterm matching "s ?190" in the current goal.

我究竟做错了什么？人们可以进入rewrite适用的情况

 destruct n. 
   (* n = 0 *)
   reflexivity.
   (* n > 0 *)
   rewrite s_ext_eq_t.
   reflexivity.
 Qed.

但是在我面临的实际情况中,有几个这样的破坏是必要的,我想知道rewrite它的变体是否能够自动完成.

---

附录当证明通过有根据的递归定义的函数具有所需的定点属性时,自然会出现上述情况:

假设A: Type,这R: A -> A -> Prop是一个有充分根据的关系,即我们有Rwf: well_founded R.然后,给定一个类型族,P: A -> Type我们可以构造一个部分

Fix : forall (x : A), P a

通过递归R,使用作为函数给出的递归步骤

 F : forall x:A, (forall y:A, R y x -> P y) -> P x

请参阅https://coq.inria.fr/library/Coq.Init.Wf.html但是,要显示Fix确实具有固定点属性

  forall (x : A), Fix x = F (fun (y:A) _ => Fix y)`

我们需要提供证人

  F_ext : forall (x:A) (f g:forall y:A, R y x -> P y),
             (forall (y:A) (p:R y x), f y p = g y p) -> F f = F g.

即我们必须表明F不使用给定的其他任何东西f: forall y:A, R y x -> P y但是它的值.当然,在任何具体的情况下,这应该是微不足道的验证,但是当一个人试图证明它时,会遇到一个我在上面提到的最小例子:一个面临两个代码副本的巨大相等对于递归步骤,一次f和另一次使用g.你的假设告诉我们f并且g在扩展上是相等的,所以应该能够重写它们.但是,在递归步骤的代码中,可能存在大量的模式匹配和新变量,这些变量在本地上下文中没有意义,因此destruct在被允许之前它会(不必要地)相当繁琐几十次申请rewrite.

Answer 1

正如上面的评论中提到的，不能直接在match语句的分支上执行重写，因为np不在顶级环境的范围内。就 Coq 的理论而言，你的陈述的证明将不得不n在某个时候被破坏。

虽然我不知道自动化此类问题的任何策略，但想出一些自定义 ltac 代码来解决您的问题并不会太痛苦：

Ltac solve_eq :=
  try reflexivity;
  match goal with
  | |- match ?x with _ => _ end
       = match ?x with _ => _ end =>
    destruct x; auto
  end.

Goal forall (n : nat), dummy_s n = dummy_t n.
Proof.
  intro n. unfold dummy_s. unfold dummy_t.
  solve_eq.
Qed.

如果您的外延等式结果是出现在您的上下文中的假设，那么solve_eq应该能够解决这种形状的许多目标；如果没有，您可能需要向提示数据库添加额外的引理。