coq - Coq:在 if-then-else 下重写
问题描述
我有时需要在 if-then-else 的一个分支中应用简化而不破坏被歧视者。
From Coq Require Import Setoid.
Lemma true_and :
forall P, True /\ P <-> P.
Proof.
firstorder.
Qed.
Goal (forall (b:bool) P Q, if b then True /\ P else Q).
intros.
Fail rewrite (true_and P).
Abort.
在这个例子中rewrite
失败(setoid_rewrite
too),建议注册如下
"subrelation eq (Basics.flip Basics.impl)"
: 对我来说似乎很公平"subrelation iff eq"
: 没门!
为什么重写引擎要求如此之高?
解决方案
我认为重写策略失败了,因为你想要的不是重写,而是减少(True /\ P
技术上不等于P
)。如果您想保持if then else
声明,我会建议以下解决方案(但有点不满意):
在Tactics.v
文件中,添加以下引理和 ltacs :
Lemma if_then_else_rewrite:
forall (b: bool) (T1 T2 E1 E2 : Prop),
(T1 -> T2) ->
(E1 -> E2) ->
(if b then T1 else E1) ->
(if b then T2 else E2).
Proof.
destruct b; auto.
Qed.
Ltac ite_app1 Th :=
match goal with
| H:_ |- if ?b then ?T2 else ?E =>
eapply if_then_else_rewrite with (E1 := E) (E2 := E);
[eapply Th | eauto |]
end.
Ltac ite_app2 Th :=
match goal with
| H:_ |- if ?b then ?T else ?E2 =>
eapply if_then_else_rewrite with (T1 := T) (T2 := T);
[eauto | eapply Th |]
end.
然后,当您有一个顶级的目标时if then else
,您可以使用 或 将定理Th
应用于左侧或ite_app1 Th
右侧ite_app2 Th
。例如,您的目标是:
Goal (forall (b:bool) P Q, if b then (True /\ P) else Q).
intros.
ite_app1 true_and. (* -> if b then P else Q *)
您可能需要根据您的需要微调 ltacs(应用于上下文与目标等),但这是第一个解决方案。也许有人可以带来更多的 ltac 黑暗魔法,以更通用的方式解决这个问题。
推荐阅读
- c# - 在 .net Core 3.1 中将 ActionFilterAttribute 解析为 TypeFilter 时出错
- python - 如果对象列表包含值,则返回该对象
- google-chrome - selenium:在 Selenium Webdriver 中运行测试自动化时 PC 帐户锁定
- javascript - 使用 date-fns 过滤 Sequelize
- java - Android:如何将 Spinner 值发送到我的 UserHelper 对象?
- huawei-mobile-services - 我有华为开发者账号吗?
- java - 每 3 秒生成一次号码并更新当前号码
- docker - 尝试运行“提交的”Docker 映像,得到“无法在现有文件上挂载卷,文件存在”
- heroku - 将密钥放在heroku配置中是否安全
- php - Laravel:将值 0 从前端传回控制器