代码之家 › 专栏 › 技术社区 › Mei Zhang

重写ltac中的单个事件

ltac coq-tactic coq

5

Mei Zhang · 技术社区 · 8 年前

rewrite 在ltac中只重写一个事件?我认为coq的文件提到了一些关于 rewrite at 但我还没有能够在实践中实际使用它,也没有例子。

Definition f (a b: nat): nat.
Admitted.

Theorem theorem1: forall a b: nat, f a b = 4.
Admitted.

Theorem theorem2: forall (a b: nat), (f a b) + (f a b) = 8.
Proof.
intros a b.
(*
my goal here is f a b + f a b = 8
I want to only rewrite the first f a b
The following tactic call doesn't work
*)
rewrite -> theorem1 at 1.

3 回复 | 直到 8 年前

1

6

Yves 8 年前

当我尝试时 rewrite -> theorem1 at 1. 正如你所建议的,我得到了

Error: Tactic failure: Setoid library not loaded.

作为回应,我重新启动了您的脚本,包括以下命令一开始。

Require Import Setoid.

2

4

Rob Blanco 8 年前

您正在使用 rewrite at https://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic121

theorem1 ),然后用新假设进行重点重写。

这项工作无需借助任何图书馆:

intros a b.
assert (H: f a b + f a b = 4 + f a b) by (rewrite theorem1; reflexivity).
rewrite H.

3

2

Anton Trunov 8 年前

有几种选择,其中一种是由@Yves指出的。

pattern 策略:

pattern (f a b) at 1.
rewrite theorem1.

pattern (f a b) at 1.

f a b + f a b = 8

进入

(fun n : nat => n + f a b = 8) (f a b)

基本上,它扩展了你的目标,从第一次出现 f a b .此外,通常 rewrite fun x => x + 0 fun x => x

然后 rewrite theorem1. (f a b) 到 4 并简化了一点(它可以减少beta),因此您可以获得 4 + f a b = 8

旁注:您也可以使用 replace 这样的策略:

replace (f a b + f a b) with (4 + f a b) by now rewrite theorem1.