coq - 自动调度单例归纳类型

Question

我正在尝试学习如何做 Coq 证明自动化 à la Chlipala/ crush。为此，我想知道自动分解单例归纳类型的便捷方法是什么，例如在解决以下问题时：

Goal forall {A B: Prop}, (A <-> B) -> (A -> B).
Goal forall {A B: Type}, A * B -> A.

我只想在有意义的时候自动分解这些- 也就是说，只有当我这样做不会丢失任何信息时。那可能吗？

标签： coqltac