处理当前目标中的 let-in 表达式

Dealing with let-in expressions in current goal

我在围绕 state monad 做一些 coq 证明时被卡住了。具体来说,我已将情况简化为以下证明:

Definition my_call {A B C} (f : A -> B * C) (a : A) : B * C :=
  let (b, c) := f a in (b, c).

Lemma mycall_is_call : forall {A B C} (f : A -> B * C) (a : A), my_call f a = f a.
Proof.
  intros A B C f a.
  unfold my_call.
  (* stuck! *)
Abort.

调用 unfold 后的最终目标是 (let (b, c) := f a in (b, c)) = f a。如果我没记错的话,等式的两边应该完全一样,但我不知道如何从这里显示出来。有帮助吗?

--

附带说明一下,我发现当函数结果中不涉及任何产品类型时,coq 会自动应用简化:

Definition my_call' {A B : Type} (f : A -> B) (a : A) : B :=
  let b := f a in b.

Lemma my_call_is_call' : forall A B (f : A -> B) (a : A), my_call' f a = f a.
Proof.
  intros A B f a.
  unfold my_call'.
  reflexivity.
Qed.

一旦您回忆起来,就很容易看出您下一步需要做什么

let (b, c) := f a in (b, c)

的语法糖
match f a with (b, c) => (b, c) end

这意味着您需要在 f a 上进行析构以完成证明:

Lemma mycall_is_call {A B C} (f : A -> B * C) a :
  my_call f a = f a.
Proof.
  unfold my_call.
  now destruct (f a).
Qed.