Coq：在 if-then-else 下重写

如何解决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也是如此），建议注册如下

• "subrelation eq (Basics.flip Basics.impl)"：对我来说似乎很公平
• "subrelation iff eq"：不可能！

为什么重写引擎要求这么高？

解决方法

我认为重写策略失败了，因为您想要的不是重写，而是减少（True /\ P 在技术上不等于 P）。如果你想维护 if then else 语句，我会建议以下解决方案（但有点不满意）：

在 Tactics.v 文件中，添加以下引理和 ltac：

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 *)

您可能需要根据自己的需要微调 ltac（应用于上下文与目标等），但这是第一个解决方案。也许有人可以带来更多的ltac黑暗魔法，以更通用的方式解决这个问题。