如何将 let 变量移至单独的假设？

Question

在 Coq 中，作为一个简化的示例（使用

False

忽略结论），

Theorem example
    (f : nat -> bool)
    (g : bool -> bool -> bool)
    (cmplx :=
      let a := f 0 in
      let b := f 1 in
      g a b
    )
    : False.

我想将 let 变量

a

和

b

移出

cmplx

的范围，并使它们成为单独的假设，例如

Theorem example
    (f : nat -> bool)
    (g : bool -> bool -> bool)
    (a := f 0)
    (b := f 1)
    (cmplx := g a b)
    : False.

这在特定情况下很容易证明，例如直接使用

change

，或者如果您可以

pattern

表达式来捕获 let 变量的使用方式，

Theorem let_up {B C D} (b : B) (c : B -> C) (d : C -> D)
    : let r := let a := b in c a in d r = let a := b in let r := c a in d r.
Proof.
  apply eq_refl.
Qed.

Theorem example : ...
Proof.
  revert cmplx.
  (* manually patterning *)
  change (let cmplx := let a := f 0 in (fun a => let b := f 1 in g a b) a in (fun _ => False) cmplx).
  rewrite let_up.
  intros.

不过，这会提高

a

，并且可以对

b

进行类似的操作。

一般有这样做的策略吗？或者，我可以写一个更大的

Ltac

来自动处理它？我有一个更复杂的函数，有很多让我想单独操作的函数，所以我想以这种方式将它们分开。我可以

change

它，但它太长了，这会很烦人。我也尝试过类似的事情

lazymatch goal with
| H := let _ := ?b in _ |- _ => idtac H "has" b
end.

但是，它似乎不允许您匹配

in

子句，可能是由于非自由变量。

也就是说，我希望能够说类似的话

let_up cmplx a

从

a

中提高

cmplx

。

Answer 1

set (a:=f 0). 
set (b:=f 1). 
fold a b in cmplx.
simpl in cmplx.

set

在上下文中定义新变量。

fold

用定义相同的定义替换术语。

simpl

可以帮助“摆脱”let 绑定。