如何使用重写策略指定位置？

Question

我有一个简单的列表引理，它说 n::l = [n]++l 其证明如下。

Lemma cons_to_app : (forall (n: nat) (l: list nat),  n :: l = [n] ++ l).
Proof.
  simpl. reflexivity.
Qed.

现在我想在证明目标中出现的任何地方使用这个证明重写缺点项::。例如，考虑以下内容。

Lemma easy_lemma : forall (n : nat) (xs ys : list nat), (n::xs) ++ (n::ys) = (n::xs) ++ ([n] ++ ys).

我想将 (n::ys) 重写为 [n] ++ ys 并且证明已完成。由于n::ys是::第二次出现在proof goal中，我以为rewrite const_to_app at 2会起作用，但实际上它作用于第3次::并改变了proof goal至 (n :: xs) ++ n :: ys = ([n] ++ xs) ++ [n] ++ ys.

我可以指定什么位置来重写 (n::ys) 术语？

Answer 1

我仍然找不到谈论 rewrite at（the one eponier mentioned 除外）确切行为的原始来源。 link 处的 post 写于 2011 年，但截至 2019 年 Coq 8.9.1 版本似乎仍然有效，并且可能不会是 "fixed" 因为问题已关闭"invalid" 说 "changing the behavior will break backwards compatibility".

问题

rewrite lemma at n 使用第一次出现实例化相等性，然后重写它的第 n 次出现。

给定引理来证明

Lemma easy_lemma :
  forall (n : nat) (xs ys : list nat), (n::xs) ++ (n::ys) = (n::xs) ++ ([n] ++ ys).

和用于重写的引理

Lemma cons_to_app : (forall (n: nat) (l: list nat),  n :: l = [n] ++ l).

rewrite cons_to_app at n. 总是选择子项 n :: xs，然后将第 n 次出现的 n :: xs 重写为 [n] ++ xs。第二个 n :: xs 刚好是第三个 _ :: _.

解决方法

简单的解决方案是提供足够的参数来告诉 Coq 要重写的确切内容。 rewrite (cons_to_app _ ys) 在这种情况下就足够了。

一种替代方法是使用 setoid_rewrite 策略，它会查看所有适用的子项。然而，它有时看起来过于深入定义，这个例子确实如此； setoid_rewrite cons_to_app at 1. 给出

1 subgoal
n : nat
xs, ys : list nat
______________________________________(1/1)
[n] ++
(fix app (l m : list nat) {struct l} : list nat := match l with
                                                   | [] => m
                                                   | a :: l1 => a :: app l1 m
                                                   end) xs (n :: ys) = (n :: xs) ++ [n] ++ ys

折叠 app 得到 [n] ++ (xs ++ n :: ys)，这与我们想要的不同，即 ([n] ++ xs) ++ n :: ys。我们可以观察到 setoid_rewrite 展开了 app 一次，将 LHS 更改为 n :: (xs ++ n :: ys)，然后实例化引理以重写最外层的 _ :: _.

为了避免展开app，我们可以在重写之前声明Opaque app.。然后 setoid_rewrite ... at 1 给出了我们想要的（at 2 也是如此）。要恢复 Opaque 的效果，请使用 Transparent.

如何使用重写策略指定位置？

How to specify a location with the rewrite tactic?

coq

coq-tactic

问题

解决方法