代码之家 › 专栏 › 技术社区 › 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.

推荐文章

Mei Zhang · 定义“依赖类型”模函子

6 年前

Jason Hu · 参见Ltac中的Hintbase

6 年前

lllllllllllll · 通过两个实现对阶乘程序进行Coq验证

6 年前

MikkelBybjerg · 如何延迟lambda评估,以便替换lambda

6 年前

user9335697 · 实例化参数以评估函数定义

6 年前

Jian Wang · Coq中的背景目标、搁置目标和放弃目标是什么?

6 年前

Pablo Inostroza · 有没有可能表达一个定理,说明应用了哪些构造函数?

6 年前

jmite · Coq:在校样脚本编写期间查看校样术语

6 年前

ConfusedFormalizer · a是怎样的。vo文件的结构是否便于coqchk使用?

6 年前

Siddharth Bhat · 查看所有已安装的库以及如何在Coq中导入它们

7 年前