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

重写ltac中的单个事件

ltac coq-tactic coq

Mei Zhang · 技术社区 · 7 年前

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 回复 | 直到 7 年前

Yves 7 年前

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

Error: Tactic failure: Setoid library not loaded.

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

Require Import Setoid.

Rob Blanco 7 年前

您正在使用 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.

Anton Trunov 7 年前

有几种选择,其中一种是由@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.

推荐文章

Jian Wang · elim在Coq中是如何工作的?

7 年前

Lorenz · Coq强制和目标匹配

7 年前

Carl Patenaude Poulin · 证明共自然数的共归纳原理

7 年前

user285827 · 如何利用Coq中包含forall的假设?

7 年前

Carl Patenaude Poulin · 问:为什么我需要手动展开一个值,即使它上面有一个“提示展开”?

8 年前

scubed · 如何在每次调用函数时选择性地简化参数,而不计算函数本身?

8 年前

thor BabarQB · Coq“局部战术应用”的正确用法是什么?

8 年前

Sara · 如何在Coq中使用带有假设的策略?

9 年前