gpt4 book ai didi

automation - 有没有办法通过重写步骤自动化 Coq 证明?

转载 作者:行者123 更新时间:2023-12-04 18:02:52 26 4
gpt4 key购买 nike

我正在做一个证明,我的一个子目标看起来有点像这样:

Goal forall
(a b : bool)
(p: Prop)
(H1: p -> a = b)
(H2: p),
negb a = negb b.
Proof.
intros.
apply H1 in H2. rewrite H2. reflexivity.
Qed.

证明不依赖于任何外部引理,仅包括将上下文中的一个假设应用于另一个假设,并使用已知假设进行重写步骤。

有没有办法自动化这个?我试着做 intros. auto.但它没有效果。我怀疑这是因为 auto只能做 apply步骤但没有 rewrite步骤,但我不确定。也许我需要一些更强的战术?

我想自动化这一点的原因是,在我的原始问题中,我实际上有大量与此非常相似的子目标,但假设的名称(H1、H2 等)、假设(有时有一两个额外的归纳假设)和最后的 bool 公式。我认为如果我可以使用自动化来解决这个问题,我的整体证明脚本会更加简洁和健壮。

编辑:如果假设之一中有 forall 怎么办?
Goal forall
(a b c : bool)
(p: bool -> Prop)
(H1: forall x, p x -> a = b)
(H2: p c),
negb a = negb b.
Proof.
intros.
apply H1 in H2. subst. reflexivity.
Qed

最佳答案

当您在证明某些引理的方式中看到重复模式时,您通常可以定义自己的策略来自动化证明。

在您的具体情况下,您可以编写以下内容:

Ltac rewrite_all' :=
match goal with
| H : _ |- _ => rewrite H; rewrite_all'
| _ => idtac
end.

Ltac apply_in_all :=
match goal with
| H : _, H2 : _ |- _ => apply H in H2; apply_in_all
| _ => idtac
end.

Ltac my_tac :=
intros;
apply_in_all;
rewrite_all';
auto.

Goal forall (a b : bool) (p: Prop) (H1: p -> a = b) (H2: p), negb a = negb b.
Proof.
my_tac.
Qed.

Goal forall (a b c : bool) (p: bool -> Prop)
(H1: forall x, p x -> a = b)
(H2: p c),
negb a = negb b.
Proof.
my_tac.
Qed.

如果你想走这条写校样的道路,经常推荐的一个引用(但我没有读过)是 CPDT通过亚当·奇利帕拉。

关于automation - 有没有办法通过重写步骤自动化 Coq 证明?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/40596015/

26 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com